Category Archives: Coq

Coq Blocked

Some time ago Cibele and I were working on a fun logic project that involved encoding classical logic in Coq. Perhaps it seems odd that we would write a logic language in language that has a logic already encoded in it, but this is a classic application of PL goodness (i.e., nonsense): we used Gallina as our meta language to encode the primitives of our target language (propositional logic, for starters). You can see the fruits of our efforts here.

Our initial goal was to be able to prove the first homework assignment using just Coq. We needed to define concepts such as suitability, satisfiability, validity, etc. We ran into problems during our first pass because we tried to define everything as a function, which doesn't lend itself to proofs.

In order to proof even the most simple theorems, we needed to define the concept of suitability. We started by defining atomic formulae and assignments:


Inductive atomic :=
| A : nat -> atomic.

Definition assignment : Set := list (atomic * bool).

Many of things we wanted to prove relied on an assignment being suitable for a formula. However, we did not want to have to traverse the assignment or prove suitability or a number of trivial cases each time we needed suitability. Our initial pass used option types extensively, but this made many of the proofs cumbersome and unruly. It also lead us astray on more complicated proofs. So, we defined some concepts with dependent types to clean things up a bit:


Fixpoint in_assignment n (a : alist) : Prop :=
match a with
| nil => False
| (h,_)::t => if beq_nat n h
then True
else in_assignment n t
end.

Lemma in_empty : forall a, in_assignment a nil -> False.
intros; compute in H; apply H.
Qed.

Fixpoint find_assignment n (a : alist) : in_assignment n a -> bool :=
match a with
| nil => fun pf => match (in_empty n) pf with end
| (h, tv)::t => if beq_nat h n
then fun _ => tv
else find_assignment n t
end.

The above defines a function, find_assignment that gets around using option types. If we could get the above to work, then we could use in_assignment to define suitability and replace in_assignment n a with suitable n a. You can see a discussion of the problem at this gist, where we simplified assignments to be an associative list, so we wouldn't have to worry about atomic types.

The main problem, as discussed on the gist, is that we needed to apply a proof in the inductive case of find_assignment. We couldn't figure out how to do this because we were focused on finding errors in find_assignment. The problem with our code was actually in in_assignment: we were using beq_nat to evaluate down to a boolean, rather than using a proposition that employed sumbool (which would give us a bunch of decidibility theorems for free).

When the needs of the few outweigh the needs of the many

I'm not posting much these days, since I'm currently in California on an internship. I have some posts I'd like to make on notes from the summer, but posts will likely being sparse for the next few months.

However, I'm up thinking about something and thought I'd blog about it.

The facts

A few days ago I received an email from a TA at Prestigious Institution X, asking me to take down my Software Foundations github repository because students were allegedly taking too much "inspiration" from it. My repository contains solutions to a chunk of the textbook, painstakingly solved mostly by me, with some input from Cibele Freire, logician. Posting solutions to a textbook released under the MIT license is, I believe, quite legal. Using those solutions to cheat in a class, however, is typically against an academic institution's honor code. Since there is no course even remotely similar to this at UMass (and in fact, few other resources exist to bootstrap a self-study plan for learning Coq and formal verification), I do not believe I am in violation of UMass' code of student conduct. The email implied none of these things, but I wanted to make sure I wasn't doing anything illegal or malicious in ignorance.

The academic world is a small one, so I consulted with my advisor. He suggested that I email the folks teaching the class, explain my reasons for having a public repo, and offer to make the repository private. The response to my email was indeed a request to make the repository private. I'm putting the previous link to the repository in this blog post, just in case someone comes searching for it and Google happens to index this post:

http://github.com/etosch/software_foundations

If you would like access, please email me directly. I am happy to discuss problems and give people access when it is appropriate to do so. There are plenty of exercises I have not completed, but would like to. I expect anyone who is interested enough to email me to abide by their school's honor code, if applicable.

The principle of the thing

Me taking down my repository does not dissuade cheating. It just buries cheating a little deeper. Dishonesty and plagiarism are pandemic in computer science. This shocked me when I started working in CS. In the humanities, the standards for attribution are quite explicit and stringently applied. Students must routinely attend lectures on academic honesty. I have never seen seen anything even remotely similar in computer science.

Removing the repository from public view shifts the blame from the student plagiarist to the provider of information. At one point in my life, when I thought I would go to grad school for English Literature, I made writing samples publicly available. Would I be culpable for someone plagiarizing my work simply because I wished to promote my work? No one would ask Harold Bloom to stop publishing if a student plagiarized him in a Shakespeare class. Obviously I'm no Harold Bloom.

The perpetrator (plagiarist) here is the one in the wrong.

It's a bit difficult for me to not be personally a little upset/frustrated by this. Not only does it devalue work in our field, but there's something maddening about students at Prestigious University X ruining it for the rest of us. I doubt they think that way, and I doubt anyone would ever put it to them that way. One of the earliest courses I took in computer science was SICP. It was not taught well. Coming from the humanities, where you actually do the reading you're assigned, I read the text. I also did nearly all of the exercises up to the chapter on metacircular evaluation. This self-study was extremely important to my education. When I got stuck on a problem I couldn't solve, I searched for the answer on the internet. Seeing solutions from people who were better programmers than I was made me a better programmer.

Eventually someone else will post solutions and it won't matter much that I took mine down. My solutions are still cached out there and I know some rando forked my repository. A quick search of github for "software foundations" and Coq returns about 80 results and at least one looks fairly complete.

sad spock