EECS 755 Blog

Midterm Clarification

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.

Midterm Exam

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.

Midterm Exam Info

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

1. Midterm will be on Thursday, March 28. I recently learned I will be traveling to Washington, DC that day. Thus the change
2. 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.
3. 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.

Classes Fall 24

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.

Tactics So Far

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.

Homework Grading

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.

Basics Updated

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

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.