Library RelationAlgebra.comparisons


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
Definition mk_simple_cmp A cmp cmp_spec :=
  @mk_cmp A _ (eqb_of_compare_spec _ cmp_spec) cmp cmp_spec.

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

Fixpoint eqb_bool i j :=
  match i,j with
    | false,false | true,truetrue
    | _,_false
  end.
Lemma eqb_bool_spec: i j, reflect (i=j) (eqb_bool i j).
Proof. destruct i; destruct j; constructor; congruence. Qed.
Fixpoint bool_compare i j :=
  match i,j with
    | false,false | true,trueEq
    | false,trueLt
    | true,falseGt
  end.
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.