Proof milestone

[Ian Lynagh]

Hi all,

With a lot of help from numerous people on and off this list, I've
finally just pushed patches that complete the proof of Lemma
commuteInSequenceConsistent:

    (<<qs :+> r :> s :> []>> <~~>* <<us :+> r' :> s' :> vs>>)
 -> (NameOf r = NameOf r')
 -> (NameOf s = NameOf s')
 -> (r <~?~> s)
 -> (r' <~?~> s').

or in English:

    If (qs r s) commutes to (us r' s' vs), and (r s) commutes,
    then (r' s') commutes.

This isn't quite the full lemma - the [] should be any sequence ts - but
proving the remaining bit just inolves repeating some of the existing
proof, but for "commutes to the right" instead of "commutes to the left".

This is quite a big milestone: It's the first proof of something that
sounds useful, and not entirely trivial. There's still a long way to go,
but we are at least making progress!


I plan to take a step back now, and look at where we are.

If any coq folk are interested in looking at the proof and telling me
what I've done stupidly, that would be great. It's all in the camp paper
repo:
    darcs get http://code.haskell.org/camp/devel/paper/
Note that you need the trunk version of coq in order to build the proof;
8.2 isn't sufficient. You'll even need trunk coqdoc to make the PS/PDF,
although the snapshow is up-to-date:
    http://projects.haskell.org/camp/files/theory.pdf
Also, you need to do "make coq" before opening it in coqide etc, as the
module imports need to be compiled.

There are a few things that I know need to be fixed:
* Naming consistency, e.g. rather the first letter is capitalised or not
* Always use "ps" rather than "p" for a sequence of patches
* Prove decidability of <~?~>, and use that rather than Classical_Prop

Florent has been working on proving this lemma in a different way: I
prove it by contradiction, whereas he is working on a constructive
proof. On paper I find the proof by contradiction simpler, and more
satisfying, but I want to see how the two compare in coq.


And I think that's all I have to say for now!


Thanks
Ian