Proof milestone, take 2

[Ian Lynagh]

Hi all,

It's been some time since I last sent anything to this list, but the
proofs are finally all going through again, up to:

Lemma hunkCommuteInSequenceConsistent : forall [...],
    (<<qs :+> r :> s :> []>> <~~>* <<us :+> r' :> s' :> vs>>)
 -> (np_name r = np_name r')
 -> (np_name s = np_name s')
 -> (r <~?~> s)
 -> (r' <~?~> s').

or in English:

    If the sequence (qs r s) can be commuted to (us r' s' vs), and (r s)
    commutes, then (r' s') commutes.

This isn't quite the full lemma we want - the [] should be any sequence
ts, so we start with (qs r s 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".

Those with long memories will note that this is the same result I had
almost a year ago. However, the underlying definitions are much changed;
in particular, sequences can now contain inverse patches.


The next step for the proof will probably be to implement catches, and
prove that they can be used to create patch universes. However, I'm also
tempted (after struggling with some coq issues, and also with some
worrying proof-rot) to look into converting the proof into Isabelle and
see how it compares.


If you want to try it yourself, this is
    Tue Mar 30 18:16:37 BST 2010  Ian Lynagh <igloo at earth.li>
      tagged Working proof, with coq trunk r12851

You'll need coq trunk to compile the proof (or to build the PDF); I have
r12851:

$ time make
coqc coqdoc.v
coqc unnamed_patches.v
coqc names.v
coqc patch_universes.v
coqc named_patches.v
coqc hunks.v
coqc notation.v
coqc unnamed_patch_sequences.v
make  396.58s user 3.38s system 99% cpu 6:43.45 total

It uses a few axioms. The first 3 are from coq libraries, and I think no
big deal. The 4th and 7th are really parameters (the proof is
parameterised over the sort of names you want to use). The 5th and 6th
are the ones it would be nice to fix - perhaps by making a set
implementation based on sorted lists in which set equality really is =
equality?

Coq < Print Assumptions hunkCommuteInSequenceConsistent.
Axioms:
JMeq.JMeq_eq : forall (A : Type) (x y : A), JMeq.JMeq x y -> x = y
ProofIrrelevance.proof_irrelevance : forall (P : Prop) (p1 p2 : P), p1 = p2
Eqdep.Eq_rect_eq.eq_rect_eq : forall (U : Type) (p : U)
                                (Q : U -> Type) (x : Q p)
                                (h : p = p), x = eq_rect p Q x p h
names.names.Name : Set
names.names.NameSetEquality : forall s s' : names.names.NameSetMod.t,
                              names.names.NameSetMod.Equal s s' -> s = s'
names.names.SignedNameSetEquality : forall
                                      s s' : names.names.SignedNameSetMod.t,
                                    names.names.SignedNameSetMod.Equal s s' ->
                                    s = s'
names.names.eq_Name_dec : forall n o : names.names.Name, {n = o} + {n <> o}


Thanks
Ian