Proof for Axiom 6.2
refis.thomas at gmail.com
Thu Jun 3 21:53:04 EDT 2010
I just got the paper-experimental5 repo and ran « make », so I started
reading theory.pdf and saw that there was no proof for Axiom 6.2 (you
flaged it as TODO).
As it didn't seem « that hard » I thought I could give it a shot and
here is what I propose (I join the context) :
If $j \in \allnames$ is positive then $j^$ is negative.
If $j \in \allnames$ is negative then $j^$ is positive.
Definition inverseSign (s : Sign) : Sign :=
match s with
| Positive => Negative
| Negative => Positive
Definition signedNameSign (sn : SignedName) : Sign :=
match sn with
| MkSignedName s _ => s
Lemma nameInverseSing : forall (sn : SignedName),
signedNameSign sn = inverseSign (signedNameSign (signedNameInverse sn)).
The inverse of a normal patch is a rollback, and vice-versa.
Even if it seems alright to me, I don't know if it matches your
expectations, that's why I'm posting here rather than sending a patch to
Also, I have the feeling the proof could be factorised, but I don't know
how to do that yet, I'm just learning Coq.
More information about the Camp