comparisons: types equiped with a comparison function

Require Import List.
Require Import Eqdep Eqdep_dec.
Import ListNotations.
Set Implicit Arguments.

Specifying Boolean

Inductive reflect (P: Prop): bool Set :=
| reflect_t : P reflect P true
| reflect_f : ¬ P reflect P false.

Specifying ternary comparisons

note that Lt and Gt have the same meaning, i.e., not Eq
turning a comparison function into a Boolean test
Definition eqb_of_compare A (f: A A comparison): A A bool :=
fun x ymatch f x y with Eqtrue | _false end.

Lemma eqb_of_compare_spec A f:
( a b: A, compare_spec (a=b) (f a b))
a b, reflect (a=b) (eqb_of_compare f a b).
Proof. unfold eqb_of_compare. intros H a b. now case H; constructor. Qed.

lexicographic ternary comparison
Notation lex a b := match a with Eqb | LtLt | GtGt end.

Lemma lex_spec P Q R a b (H: RPQ):
compare_spec P a compare_spec Q b compare_spec R (lex a b).
Proof.
destruct 1; try (constructor; tauto).
destruct 1; constructor; tauto.
Qed.

Lemma compare_lex_eq a b: lex a b = Eq a = Eq b = Eq.
Proof. destruct a; intuition discriminate. Qed.

Structure for types equiped with a Boolean equality and a comparison function.

Note that the specification of cmp is weak: we only have cmp a b = Eq a=b. As a consequence, the difference betwen Lt and Gt can only be used as a heuristic.
Structure cmpType := mk_cmp {
carr:> Set;
eqb: carr carr bool;
_: x y, reflect (x=y) (eqb x y);
cmp: carr carr comparison;
_: x y, compare_spec (x=y) (cmp x y)
}.
Arguments cmp {c} x y.
Arguments eqb {c} x y.

Lemma eqb_spec (A: cmpType): x y: A, reflect (x=y) (eqb x y).
Proof. now case A. Qed.
Lemma cmp_spec (A: cmpType): x y: A, compare_spec (x=y) (cmp x y).
Proof. now case A. Qed.

building comparison types without providing an equality function
phantom identity to generate cmpTypes by unification (see ssreflect)
Definition cmp_id (A: cmpType) (X: Set) (_:X carr A): cmpType := A.
Notation "[ X :cmp]" := (@cmp_id _ X%type (fun xx)) (at level 0).

basic properties
Lemma cmp_eq (A: cmpType) (x y: A): cmp x y = Eq x=y.
Proof. case cmp_spec; congruence. Qed.

Lemma cmp_refl (A: cmpType) (x: A): cmp x x = Eq.
Proof. case cmp_spec; congruence. Qed.

Lemma eqb_eq (A: cmpType) (x y: A): eqb x y = true x = y.
Proof. case eqb_spec; congruence. Qed.

Lemma eqb_refl (A: cmpType) (x: A): eqb x x = true.
Proof. case eqb_spec; congruence. Qed.

Lemma eqb_sym (A: cmpType) (x y: A): eqb x y = eqb y x.
Proof. case eqb_spec; case eqb_spec; congruence. Qed.

Lemma cmp_dec (A: cmpType) (x y: A): {x=y}+{xy}.
Proof. case (eqb_spec A x y); tauto. Qed.

equality on cmpTypes being decidable, we get uniqueness of identity proofs and elimination of dependent equality
Lemma cmp_eq_dep_eq (A: cmpType) (P: A Type):
p (x y: P p), eq_dep A P p x p y x = y.
Proof. apply eq_dep_eq_dec, cmp_dec. Qed.

Lemma cmp_eq_rect_eq (A: cmpType):
(p: A) Q (x: Q p) (h: p = p), eq_rect p Q x p h = x.
Proof. symmetry. apply eq_rect_eq_dec, cmp_dec. Qed.

Lemma UIP_cmp (A: cmpType) (p q: A) (x y: p=q): x = y.
Proof. apply UIP_dec, cmp_dec. Qed.

Natural numbers as a cmpType

Fixpoint eqb_nat i j :=
match i,j with
| O,Otrue
| S i,S jeqb_nat i j
| _,_false
end.
Lemma eqb_nat_spec: i j, reflect (i=j) (eqb_nat i j).
Proof.
induction i; intros [|j]; try (constructor; congruence).
simpl. case IHi; constructor; congruence.
Qed.
Fixpoint nat_compare i j :=
match i,j with
| O,OEq
| S i,S jnat_compare i j
| O,_Lt
| _,OGt
end.
Lemma nat_compare_spec: i j, compare_spec (i=j) (nat_compare i j).
Proof.
induction i; intros [|j]; try (constructor; congruence).
simpl. case IHi; constructor; congruence.
Qed.
Canonical Structure cmp_nat := mk_cmp _ eqb_nat_spec _ nat_compare_spec.

Booleans as a cmpType

Definition eqb_bool i j :=
match i,j with
| false,false | true,truetrue
| _,_false
end.
Arguments eqb_bool !i !j/.
Lemma eqb_bool_spec: i j, reflect (i=j) (eqb_bool i j).
Proof. destruct i; destruct j; constructor; congruence. Qed.
Definition bool_compare i j :=
match i,j with
| false,false | true,trueEq
| false,trueLt
| true,falseGt
end.
Arguments bool_compare !i !j/.
Lemma bool_compare_spec: i j, compare_spec (i=j) (bool_compare i j).
Proof. destruct i; destruct j; constructor; congruence. Qed.
Canonical Structure cmp_bool := mk_cmp _ eqb_bool_spec _ bool_compare_spec.

Pairs of cmpTypes

Section p.
Variables A B: cmpType.
Definition eqb_pair (x y: A×B) :=
let '(x1,x2) := x in
let '(y1,y2) := y in
if (eqb x1 y1) then (eqb x2 y2) else false.
Lemma eqb_pair_spec: x y, reflect (x=y) (eqb_pair x y).
Proof.
unfold eqb_pair. intros [? ?] [? ?]; simpl;
repeat case eqb_spec; constructor; congruence.
Qed.
Definition pair_compare (x y: A×B) :=
let '(x1,x2) := x in
let '(y1,y2) := y in
lex (cmp x1 y1) (cmp x2 y2).
Lemma pair_compare_spec: x y, compare_spec (x=y) (pair_compare x y).
Proof.
unfold pair_compare. intros [? ?] [? ?]; simpl;
repeat case cmp_spec; constructor; congruence.
Qed.
Canonical Structure cmp_pair := mk_cmp _ eqb_pair_spec _ pair_compare_spec.
End p.

Sums of cmpTypes

Section s.
Variables A B: cmpType.
Definition eqb_sum (x y: A+B) :=
match x,y with
| inl x,inl y | inr x,inr yeqb x y
| _,_false
end.
Lemma eqb_sum_spec: x y, reflect (x=y) (eqb_sum x y).
Proof.
unfold eqb_sum. intros [?|?] [?|?]; simpl;
try case eqb_spec; constructor; congruence.
Qed.
Definition sum_compare (x y: A+B) :=
match x,y with
| inl x,inl y | inr x,inr ycmp x y
| inl _,inr _Lt
| inr _,inl _Gt
end.
Lemma sum_compare_spec: x y, compare_spec (x=y) (sum_compare x y).
Proof.
unfold sum_compare. intros [?|?] [?|?]; simpl;
try case cmp_spec; constructor; congruence.
Qed.
Canonical Structure cmp_sum := mk_cmp _ eqb_sum_spec _ sum_compare_spec.
End s.

Lists of a cmpType

Section l.
Variables A: cmpType.
Fixpoint eqb_list (h k: list A) :=
match h,k with
| nil, niltrue
| u::h, v::kif eqb u v then eqb_list h k else false
| _, _false
end.
Fixpoint list_compare (h k: list A) :=
match h,k with
| nil, nilEq
| nil, _Lt
| _, nilGt
| u::h, v::klex (cmp u v) (list_compare h k)
end.
Lemma eqb_list_spec: h k, reflect (h=k) (eqb_list h k).
Proof.
induction h as [|x h IH]; destruct k; simpl;
try case eqb_spec; try case IH; constructor; congruence.
Qed.
Lemma list_compare_spec: h k, compare_spec (h=k) (list_compare h k).
Proof.
induction h as [|x h IH]; destruct k; simpl;
try case cmp_spec; try case IH; constructor; congruence.
Qed.
Canonical Structure cmp_list := mk_cmp _ eqb_list_spec _ list_compare_spec.
End l.