Proof for Axiom 6.2

Thomas Refis refis.thomas at
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)).
  destruct sn; 
  destruct s;
  (** %
  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
the project.
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.

Bye !


More information about the Camp mailing list