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

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

(** %

\start{definition}{names}
We have a (possibly infinite) set of names $\allnames$.
% *)
Parameter Name : Set.
Parameter Name_compare : Name -> Name -> comparison.
Parameter Name_compare_sym : forall {x y : Name},
                             Name_compare y x = CompOpp (Name_compare x y).
Parameter Name_compare_trans : forall {c : comparison}
                                      {x y z : Name},
                               Name_compare x y = c
                            -> Name_compare y z = c
                            -> Name_compare x z = c.
Parameter Name_eq_is_leibniz : forall {s s' : Name},
                               Name_compare s s' = Eq
                            -> s = s'.

(** %
\end{Idefinition}
%*)


Definition Name_lt (x y : Name) : Prop
    := match Name_compare x y with
       | Lt => True
       | Eq => False
       | Gt => False
       end.

Lemma Name_eq_equiv : Equivalence (@eq Name).
Proof.
intuition.
Qed.

Lemma Name_lt_strorder : StrictOrder Name_lt.
Proof with auto.
intuition.
    intro.
    intro.
    unfold Name_lt in H.
    case_eq (Name_compare x x); intro.
            rewrite H0 in H...
        set (H1 := H0).
        clearbody H1.
        rewrite Name_compare_sym in H1.
        unfold CompOpp in H1.
        rewrite H0 in H1.
        congruence.
    rewrite H0 in H...
intro.
intros.
unfold Name_lt in *.
case_eq (Name_compare x y); intro Heq1; rewrite Heq1 in *; try contradiction.
case_eq (Name_compare y z); intro Heq2; rewrite Heq2 in *; try contradiction.
set (Heq3 := Name_compare_trans Heq1 Heq2).
clearbody Heq3.
rewrite Heq3...
Qed.

Lemma Name_lt_compat : Proper ((@eq Name) ==> (@eq Name) ==> iff) Name_lt.
Proof.
auto with *.
Qed.

Lemma Name_compare_spec : forall x y, CompSpec (@eq Name) Name_lt x y (Name_compare x y).
Proof with auto.
intros.
unfold CompSpec.
case_eq (Name_compare x y); intro.
        apply CompEq.
        apply Name_eq_is_leibniz in H...
    apply CompLt.
    unfold Name_lt.
    rewrite H...
apply CompGt.
unfold Name_lt.
rewrite Name_compare_sym in H.
apply (f_equal CompOpp) in H.
rewrite CompOpp_involutive in H.
rewrite H.
unfold CompOpp...
Qed.

Lemma Name_eq_dec : forall x y, { @eq Name x y } + { ~ @eq Name x y }.
Proof with auto.
intros.
case_eq (Name_compare x y); intro.
        left.
        apply Name_eq_is_leibniz...
    right.
    intro.
    subst.
    set (HX := H).
    clearbody HX.
    rewrite Name_compare_sym in HX.
    unfold CompOpp in HX.
    rewrite H in HX.
    congruence.
right.
intro.
subst.
set (HX := H).
clearbody HX.
rewrite Name_compare_sym in HX.
unfold CompOpp in HX.
rewrite H in HX.
congruence.
Qed.

Lemma Name_eq_leibniz : forall x y, @eq Name x y -> x = y.
Proof.
auto.
Qed.

Module NameOrderedTypeWithLeibniz.

Definition t := Name.
Definition lt := Name_lt.
Definition eq := @Logic.eq Name.
Definition compare := Name_compare.
Definition eq_equiv := Name_eq_equiv.
Definition lt_strorder := Name_lt_strorder.
Definition lt_compat := Name_lt_compat.
Definition compare_spec := Name_compare_spec.
Definition eq_dec := Name_eq_dec.
Definition eq_leibniz := Name_eq_leibniz.

End NameOrderedTypeWithLeibniz.

Module NameSetMod := MSetList.MakeWithLeibniz(NameOrderedTypeWithLeibniz).

Notation NameSet := (NameSetMod.t).
Notation NameSetIn := (NameSetMod.In).
Notation NameSetAdd := (NameSetMod.add).
Notation NameSetRemove := (NameSetMod.remove).
Notation NameSetEqual := (NameSetMod.Equal).

Module NameSetDec := WDecide (NameSetMod).
Ltac nameSetDec := NameSetDec.fsetdec.

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

Definition NameSetEquality {s s' : NameSet}
                           (H : NameSetEqual s s')
                         : s = s'
    := NameSetMod.eq_leibniz H.

Lemma NameSet_eq_dec : forall (x y : NameSet),
                       {x = y} + {x <> y}.
Proof with auto.
intros.
destruct (NameSetMod.eq_dec x y).
    left.
    apply NameSetEquality...
right.
intro.
subst.
elim n.
reflexivity.
Qed.