# Proof for Axiom 6.2

Thomas Refis refis.thomas at gmail.com
Thu Jun 3 21:53:04 EDT 2010

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.