(** %
\section{\label{sec:names}Names}

% *)
Require Import Coq.MSets.MSets.
Require Import Coq.Structures.Orders.
Require Import Coq.Structures.OrdersAlt.

Require Import names.plain_names.

(** %
\start{definition}{names-signed}
We say that a name is either positive or negative.
% *)
Inductive Sign : Set
    := Positive | Negative.

Inductive SignedName : Set
    := MkSignedName : forall (s : Sign)
                             (n : Name),
                      SignedName.

Definition SignedName_compare (x y : SignedName) : comparison
    := match x, y with
       | MkSignedName Negative _,  MkSignedName Positive _ => Lt
       | MkSignedName Positive _,  MkSignedName Negative _ => Gt
       | MkSignedName Negative x', MkSignedName Negative y' => Name_compare y' x'
       | MkSignedName Positive x', MkSignedName Positive y' => Name_compare x' y'
       end.

Lemma SignedName_compare_sym : forall {x y : SignedName},
                               SignedName_compare y x = CompOpp (SignedName_compare x y).
Proof with auto.
intros.
destruct x as [sx nx].
destruct y as [sy ny].
destruct sx; destruct sy;
unfold SignedName_compare; auto; apply Name_compare_sym.
Qed.

Lemma SignedName_compare_trans :
    forall {c x y z},
    (SignedName_compare x y) = c
 -> (SignedName_compare y z) = c
 -> (SignedName_compare x z) = c.
Proof with auto.
intros.
destruct x as [sx nx].
destruct y as [sy ny].
destruct z as [sz nz].
destruct sx; destruct sy; destruct sz;
unfold SignedName_compare in *...
            apply (Name_compare_trans H H0).
        congruence.
    congruence.
apply (Name_compare_trans H0 H).
Qed.

Lemma SignedName_eq_is_leibniz :
    forall {x y : SignedName},
    SignedName_compare x y = Eq -> x = y.
Proof with auto.
intros.
destruct x as [sx nx].
destruct y as [sy ny].
destruct sx; destruct sy;
unfold SignedName_compare in *.
            apply Name_eq_is_leibniz in H.
            subst...
        congruence.
    congruence.
apply Name_eq_is_leibniz in H.
subst...
Qed.

Definition SignedName_lt (x y : SignedName) : Prop
    := match SignedName_compare x y with
       | Lt => True
       | Eq => False
       | Gt => False
       end.

Lemma SignedName_eq_equiv : Equivalence (@eq SignedName).
Proof.
intuition.
Qed.

Lemma SignedName_lt_strorder : StrictOrder SignedName_lt.
Proof with auto.
intuition.
    intro.
    intro.
    unfold SignedName_lt in H.
    case_eq (SignedName_compare x x); intro.
            rewrite H0 in H...
        set (H1 := H0).
        clearbody H1.
        rewrite SignedName_compare_sym in H1.
        unfold CompOpp in H1.
        rewrite H0 in H1.
        congruence.
    rewrite H0 in H...
intro.
intros.
unfold SignedName_lt in *.
case_eq (SignedName_compare x y); intro Heq1; rewrite Heq1 in *; try contradiction.
case_eq (SignedName_compare y z); intro Heq2; rewrite Heq2 in *; try contradiction.
set (Heq3 := SignedName_compare_trans Heq1 Heq2).
clearbody Heq3.
rewrite Heq3...
Qed.

Lemma SignedName_lt_compat : Proper ((@eq SignedName) ==> (@eq SignedName) ==> iff) SignedName_lt.
Proof.
auto with *.
Qed.

Lemma SignedName_compare_spec : forall x y, CompSpec (@eq SignedName) SignedName_lt x y (SignedName_compare x y).
Proof with auto.
intros.
unfold CompSpec.
case_eq (SignedName_compare x y); intro.
        apply CompEq.
        apply SignedName_eq_is_leibniz in H...
    apply CompLt.
    unfold SignedName_lt.
    rewrite H...
apply CompGt.
unfold SignedName_lt.
rewrite SignedName_compare_sym in H.
apply (f_equal CompOpp) in H.
rewrite CompOpp_involutive in H.
rewrite H.
unfold CompOpp...
Qed.

Lemma SignedName_eq_dec (x y : SignedName)
                      : {x = y} + {~(x = y)}.
Proof with auto.
intros.
case_eq (SignedName_compare x y); intro.
        left.
        apply SignedName_eq_is_leibniz...
    right.
    intro.
    subst.
    set (HX := H).
    clearbody HX.
    rewrite SignedName_compare_sym in HX.
    unfold CompOpp in HX.
    rewrite H in HX.
    congruence.
right.
intro.
subst.
set (HX := H).
clearbody HX.
rewrite SignedName_compare_sym in HX.
unfold CompOpp in HX.
rewrite H in HX.
congruence.
Qed.

Lemma SignedName_eq_leibniz : forall x y, @eq SignedName x y -> x = y.
Proof.
auto.
Qed.

(** %
\begin{Iexplanation}
Here's some intuition for what this means: When you record a patch in
camp, the patch name is positive (think: it adds something to the
repo). If you roll back that patch, then camp makes the corresponding
negative patch (which removes something from the repo).
\end{Iexplanation}
\end{Idefinition}

\start{axiom}{names-invertible}
$\forall j \in \allnames . j^ \in \allnames$.
% *)
Definition signedNameInverse (n : SignedName) : SignedName
    := match n with
       | MkSignedName Positive b => MkSignedName Negative b
       | MkSignedName Negative b => MkSignedName Positive b
       end.

Lemma nameInverseInverse : forall (sn : SignedName), signedNameInverse (signedNameInverse sn) = sn.
Proof with auto.
intros.
destruct sn.
destruct s...
Qed.

Lemma namesInverseInjective: forall (sn1: SignedName) (sn2: SignedName),
                             signedNameInverse sn1 = signedNameInverse sn2 -> sn1 = sn2.
Proof with auto.
intros.
destruct sn1;
destruct s;
destruct sn2;
destruct s;
unfold signedNameInverse in *;
inversion H...
Qed.

(** %
\begin{Iexplanation}
Names have an inverse.
\end{Iexplanation}
\end{Iaxiom}

\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.
% *)
(* XXX TODO *)
(** %

\begin{Iexplanation}
The inverse of a normal patch is a rollback, and vice-versa.
\end{Iexplanation}
\end{Iaxiom}
%*)

Module SignedNameOrderedTypeWithLeibniz.
Definition t := SignedName.
Definition lt := SignedName_lt.
Definition eq := @Logic.eq SignedName.
Definition compare := SignedName_compare.
Definition eq_equiv := SignedName_eq_equiv.
Definition lt_strorder := SignedName_lt_strorder.
Definition lt_compat := SignedName_lt_compat.
Definition compare_spec := SignedName_compare_spec.
Definition eq_dec := SignedName_eq_dec.
Definition eq_leibniz := SignedName_eq_leibniz.
End SignedNameOrderedTypeWithLeibniz.

Module SignedNameSetMod := MSetList.MakeWithLeibniz(SignedNameOrderedTypeWithLeibniz).

Notation SignedNameSet := (SignedNameSetMod.t).
Notation SignedNameSetIn := (SignedNameSetMod.In).
Notation SignedNameSetAdd := (SignedNameSetMod.add).
Notation SignedNameSetRemove := (SignedNameSetMod.remove).
Notation SignedNameSetEqual := (SignedNameSetMod.Equal).

Module SignedNameSetDec := WDecide (SignedNameSetMod).
Ltac signedNameSetDec := SignedNameSetDec.fsetdec.

Definition SignedNameSetEquality {s s' : SignedNameSet}
                                 (H : SignedNameSetEqual s s')
                               : s = s'
    := SignedNameSetMod.eq_leibniz H.

Lemma SignedNameSet_eq_dec : forall (x y : SignedNameSet),
                             {x = y} + {x <> y}.
Proof with auto.
intros.
destruct (SignedNameSetMod.eq_dec x y).
    left.
    apply SignedNameSetEquality...
right.
intro.
subst.
elim n.
reflexivity.
Qed.