Subject: Proof milestone, take 2 To: camp@projects.haskell.org From: Ian Lynagh <igloo@earth.li> Date: Tue, 30 Mar 2010 19:08:03 +0100 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@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