# Library CoLoR.Util.Logic.EqUtil

CoLoR, a Coq library on rewriting and termination. See the COPYRIGHTS and LICENSE files.
• Frederic Blanqui, 2005-02-17
general lemmas and tactics

Set Implicit Arguments.

Functor providing properties the basic properties of Leibniz equality on some type.

Module LeibnizFacts (Import T : Typ).

Definition eq : relation t := @Logic.eq t.

Instance eq_refl : Reflexive eq.

Instance eq_sym : Symmetric eq.

Instance eq_trans : Transitive eq.

End LeibnizFacts.

Type equipped with a boolean equility.

Record Bool_eq_type : Type := mkBool_eq_type {
bet_type :> Type;
bet_eq : bet_type -> bet_type -> bool;
bet_ok : forall x y, bet_eq x y = true <-> x = y }.

Properties of Leibniz equality on decidable types.

Section eq_dep.

Variables (A : Type) (eq_dec : forall x y : A, {x=y}+{~x=y}).

Lemma eq_rect_eq : forall (p : A) Q x h, x = eq_rect p Q x p h.

Lemma eq_dep_eq : forall P (p : A) x y, eq_dep A P p x p y -> x = y.

Lemma UIP : forall (x y : A) (p1 p2 : x = y), p1 = p2.

Lemma UIP_refl : forall (x : A) (p : x = x), p = eq_refl x.

Lemma Streicher_K :
forall (x : A) (P : x = x -> Prop), P (eq_refl x) -> forall p, P p.

Lemma inj_existT :
forall P (x : A) (p q : P x), existT p = existT q -> p = q.

Lemma inj_ex_intro :
forall P (x : A) p q, ex_intro P x p = ex_intro P x q -> p = q.

End eq_dep.

Properties of a boolean function testing Leibniz equality.

Section beq.

Variable A : Type.
Variable beq : A -> A -> bool.
Variable beq_ok : forall x y, beq x y = true <-> x = y.

Lemma beq_refl : forall x, beq x x = true.

Lemma beq_ko : forall x y, beq x y = false <-> x <> y.

Lemma dec_beq : forall x y : A, {x=y}+{~x=y}.

Lemma beq_com : forall x y, beq x y = beq y x.

Lemma beq_sym : forall x y, beq x y = true -> beq y x = true.

Lemma beq_trans : forall x y z,
beq x y = true -> beq y z = true -> beq x z = true.

End beq.

Ltac case_beq beq beq_ok x y := case_eq (beq x y);
[let h := fresh in intro h; rewrite beq_ok in h;
match type of h with ?x = ?y => subst y end
| intro].

Boolean function testing Leibniz equality when it is decidable.

Section eq_dec.

Variable A : Type.
Variable eq_dec : forall x y : A, {x=y}+{~x=y}.

Definition beq_dec x y :=
match eq_dec x y with
| left _ => true
| right _ => false
end.

Lemma beq_dec_ok : forall x y, beq_dec x y = true <-> x = y.

Lemma beq_dec_refl : forall x, beq_dec x x = true.

Lemma beq_dec_sym : forall x y, beq_dec x y = beq_dec y x.

Lemma beq_dec_trans : forall x y z,
implb (beq_dec x y && beq_dec y z) (beq_dec x z) = true.

Lemma beq_dec_ko : forall x y, beq_dec x y = false <-> x <> y.

End eq_dec.