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.