- Final Exam
- Imp and IndProp
- Homework Scores
- Homework Grading
- Final Homework Excercises
- Midterm Clarification
- Midterm Exam
- Midterm Exam Info
- Classes Fall 24
- Tactics So Far

Blog

The final is here. LaTeX source is here should you want to use it. Submit your solution via Canvas by 2:30 May 9.

Excercises I will grade from `Imp.v`

and `IndProp.v`

are listed
below. You can do more if you want and I will grade them, but this is
what I will definitely incldue:

Most of these are 1 star with a few more difficult proofs at the end. No 4 or 5 star proofs. I’m not asking you to prove The Pumping Lemma even though Pierce would.

`close_refl_trans`

`perm`

`ev_double`

`inversion_pactice`

`ev5_nonsense`

`ev_sum`

`ev'_ev`

`ev_ev__ev`

`ev_plus_plus`

`total_relation`

`empty_relation`

`subsequence`

`reflect`

The `Imp.v`

chapter doesn’t have too many truly 1 star problems. Set
aside some time to work on these, but none of them are horrible.

`optimize_0plus_b_sound`

`optimize`

(4 star, so be careful)`bevalR`

`ceval_example2`

`loop_never_stops`

`no_whiles_eqv`

`stack_compiler`

(particularly cool)

I just took all grades that I’ve posted offline until I can repost corrected scores. Should be later today. My auto-grader was producing bad values and freaking people out. That is definitely not what I intended and I’m sorry if I caused undo stress. I believe the problem is corrected and I’ve regenerated grades. Still need to check them and post scores.

One issue exists that I need your help with. When I post grades you
may see no grade for an assignment you submitted. This is almost
certainly because your proof file crashed. Likely due to a missing
`Admitted`

statement or due to inclusion of an `Abort`

command. Missing `Admitted`

causes a proof to hang while `Abort`

terminates the proof process. Either of these causes the test file to
fail. What I need you to do is fix the error and resubmit. Your test
file needs to generate output and terminate without throwing errors. I
believe you can do this via Canvas or even better just send me email.

I will ping you again when grades are posted. If you already know your assignment files throw errors, you can go ahead and start fixing that.

Homework grades are gradualing making it to the Canvas site. Unfortunately, my auto-grader has not been formally verified and is not perfect. Please don’t freak out if you see a score that you don’t expect. I plan on looking at every grade that is unusual before I make grades final. If you want to contact me (email or otherwise) about homework scores, please feel free.

As promised in class, here is a list of problems you should choose from for your last 2 homework assignments. I will grade the same way I have been, just limited to these assignments. If you want to do others, I will happily grade them and give you extra homework points.

Unfortunately exercises are not numbered, so I will simply list the theorems to prove by name.

`skip_right`

`if_false`

`swap_if_branches`

`while_true`

`seq_assoc`

`assign_aequiv`

`CIf_congruence`

We did not go over assignment in any detail, but I think the last couple of proofs are quite doable.

`hoare_post_true`

`hoare_pre_false`

`hoare_asgn_examples1`

`hoare_asgn_examples2`

`hoare_asgn_wrong`

`hoare_asgn_forward`

`hoare_asgn_fwd_exists`

`assertion_sub_ex1'`

`assertion_sub_ex2'`

`if_minus_plus`

All homeworks are due on the last day of finals, regardless of what Canvas says. I will try to remember to update the dates.

On Exercise 2 don’t worry about the “guessing decreasing argument” issue the Coq type checker brings up. When I wrote the exam I did not anticipate anyone trying to actually code the tree structure up in the prover because it was intended to be done in class. Assume that Coq can find the decreasing argument. There is a solution to this, but it’s not what I want you spending your time on.

The midterm is here. LaTeX source is here should you want to use it. Submit your solution by email or Canvas by 2:30 Friday.

Small changes and additional information about the midterm that I will go over in class today.

- Midterm will be on Thursday, March 28. I recently learned I will be traveling to Washington, DC that day. Thus the change
- The exam will be available online. I will release it at 2:30pm on the 28th and you will submit it at 5:00pm the same day.
- The exam will be open book, open notes and will cover everything up
to
`IndProp`

. I will provide a topic list next class period.

Sorry for the late change, but I hope having 2.5 hours and open book will make up for it.

Many of you have asked what will be offered in Fall 2024 related to programming languages and specifically what I might be teaching. After checking the KU classes website I discovered that I was not scheduled for any courses. This was not intended. I will be offering EECS 762 in the fall which is our course on operational semantics. Tell your friends as I’m guessing no one knows the course is being taught.

We’ve reached a point where we’ve got enough tactics to do some real work. Here are tactics that we’ve seen in class as of 2024-20-20:

*intros*: move hypotheses/variables from goal to context*reflexivity*: finish the proof (when the goal looks like*e = e*)*apply*: prove goal using a hypothesis, lemma, or constructor*apply… in H*: apply a hypothesis, lemma, or constructor to a hypothesis in the context (forward reasoning)*apply… with…*: explicitly specify values for variables that cannot be determined by pattern matching*simpl*: simplify computations in the goal*simpl in H*: … or a hypothesis*rewrite*: use an equality hypothesis (or lemma) to rewrite the goal*rewrite … in H*: … or a hypothesis*symmetry*: changes a goal of the form*t=u*into*u=t**symmetry in H*: changes a hypothesis of the form*t=u*into*u=t**transitivity y*: prove a goal*x=z*by proving two new subgoals,*x=y*and*y=z**unfold*: replace a defined constant by its right-hand side in the goal*unfold… in H*: … or a hypothesis*destruct… as…*: case analysis on values of inductively defined types*destruct… eqn:…*: specify the name of an equation to be added to the context, recording the result of the case analysis*induction… as…*: induction on values of inductively defined types*injection… as…*: reason by injectivity on equalities between values of inductively defined types*discriminate*: reason by disjointness of constructors on equalities between values of inductively defined types*assert (H: e)*(or*assert (e) as H*): introduce a “local lemma”*e*and call it*H*

There are many more tactics and we’ve not learned much about automation, but this is a good start.

I have updated the grading policy for homework to match what we discussed in class on February 5. If you object to these changes, I will grade your work as defined in the original syllabus. However, the updates are designed to make homework less stressful. Hopefully everyone will approve.

I just pushed new versions of `Basics.v`

and `BasicsTest.v`

to the
website. They should be downloadable now. Feel free to take an extra
day or two to complete the additional exercises.

Welcome to the EECS 755 blog for Spring 2024. You will find late-breaking information about the class and associated projects and exams here. The blog is available via RSS feed if you use an RSS aggregator.

Please keep in mind that this is a math class. We will treat programs as mathematical objects and we will be doing proofs from day one. Our proofs are done in an automated checker built into an IDE, but they are still proofs. We will move quickly and I expect you to install new software, correct syntax problems, and debug code on your own. I will teach you new material you need to know, but we don’t have time for extensive review of prerequisite material.

As you’re getting started it would be a good idea to install Coq on your system of choice. It is strongly suggested that you start with CoqIDE or VSCode. CoqIDE provides a drag-and-drop installation as well as an IDE for Coq. It is the simplest way to get started. VSCode with VSCoq is a far more powerful development environment that requires a bit more heavy lifting to install. Definitely worth the effort. If you are an emacs and linux user then ProofGeneral is a great option. I suspect far more of you use VSCode these days than emacs.

For reference, I am an emacs/ProofGeneral user while most of my students are VSCode users. While this prompts many spirited discussions in the lab, both work quite well.