Proof for Axiom 6.2

[Thomas Refis]

Hi!
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) :
  \start{axiom}{name-inverse-sign}
  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
    end.
  
  Definition signedNameSign (sn : SignedName) : Sign :=
    match sn with
      | MkSignedName s _ => s
    end.
  
  Lemma nameInverseSing : forall (sn : SignedName),
    signedNameSign sn = inverseSign (signedNameSign (signedNameInverse sn)).
  destruct sn; 
  destruct s;
  simpl;
  reflexivity;
  simpl;
  reflexivity...
  Qed.
  (** %
  
  \begin{Iexplanation}
  The inverse of a normal patch is a rollback, and vice-versa.
  \end{Iexplanation}
  \end{Iaxiom}
  %*)

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 !

  drk-sd.