Library TLC.LibEqual

Set Implicit Arguments.
From TLC Require Import LibTactics LibAxioms.
Generalizable Variables A.

Definition of equality

Definition of Leibnitz' equality

Arguments eq {A}.

Partial application of Leibnitz' equality

= x is a unary predicate which holds of values equal to x. It simply denotes the partial application of equality. = x :> A allows to specify the type.

Notation "'=' x :> A" := (fun y => y = x :> A)
(at level 71, x at next level).
Notation "'=' x" := (fun y => y = x)
(at level 71).

<> x is a unary predicate which holds of values disequal to x. It simply denotes the partial application of disequality. <> x :> A allows to specify the type.

Notation "'<>' x :> A" := (fun y => y <> x :> A)
(at level 71, x at next level).
Notation "'<>' x" := (fun y => y <> x)
(at level 71).

Typeclass to exploit extensionality

The property Extensionality A captures the fact that the type A features an extensional equality, in the sense that to prove the equality between two values of type A it suffices to prove that those two values are related by some binary relation.

Class Extensionality (A:Type) := Extensionality_make {
extensionality_hyp : A -> A -> Prop;
extensionality : forall (x y : A), extensionality_hyp x y -> x = y }.

Arguments extensionality [A].
Arguments Extensionality_make [A] [extensionality_hyp].

Instance for propositional extensionality

Global Instance extensionatity_prop : Extensionality Prop.
Proof using. intros. apply (Extensionality_make prop_ext). Defined.

Tactic to exploit extensionality

Ltac extens_reveal_eq tt :=
  match goal with
  | |- _ = _ => idtac
  | _ => first [ intro; extens_reveal_eq tt
               | fail 2 "extens needs hnf to reveal an equality" ]
  end.

Ltac extens_core tt :=
  extens_reveal_eq tt;
  applys extensionality;
  simpl extensionality_hyp.

Tactic Notation "extens" :=
  extens_core tt.
Tactic Notation "extens" "~" :=
  extens; auto_tilde.
Tactic Notation "extens" "*" :=
  extens; auto_star.

Properties of equality

This section contains a reformulation of the lemmas provided by the standard library concerning equality.

Equality as an equivalence relation

See also sectin Eq from LibRelation for reformulation of theses results using high-level definitions.

Section EqualityProp.
Variables (A : Type).
Implicit Types x y z : A.

Reflexivity is captured by the constructor eq_refl.

Symmetry

Lemma eq_sym : forall x y,
x = y ->
y = x.
Proof using. introv H. destruct~ H. Qed.

Transitivity

Lemma eq_trans_ll : forall y x z,
  x = y ->
  y = z ->
  x = z.
Proof using. introv H1 H2. destruct~ H2. Qed.

Definition eq_trans := eq_trans_ll.

Lemma eq_trans_lr : forall y x z,
  x = y ->
  z = y ->
  x = z.
Proof using. introv H1 H2. destruct~ H2. Qed.

Lemma eq_trans_rl : forall y x z,
  y = x ->
  y = z ->
  x = z.
Proof using. introv H1 H2. destruct~ H2. Qed.

Lemma eq_trans_rr : forall y x z,
  y = x ->
  z = y ->
  x = z.
Proof using. introv H1 H2. destruct~ H2. Qed.

End EqualityProp.

Arguments eq_trans_ll [A].
Arguments eq_trans_lr [A].
Arguments eq_trans_rl [A].
Arguments eq_trans_rr [A].
Arguments eq_trans [A].

Properties of disequality

Section DisequalityProp.
Variables (A : Type).
Implicit Types x y : A.

Symmetry

Lemma neq_sym : forall x y,
x <> y ->
y <> x.
Proof using. introv H K. destruct~ K. Qed.

End DisequalityProp.

Symmetrized induction principles

Section EqInductionSym.
Variables (A : Type) (x : A).

Definition eq_ind_r : forall (P:A -> Prop),
  P x -> forall y, y = x -> P y.
Proof using. intros. subst*. Qed.

Definition eq_rec_r : forall (P:A -> Set),
  P x -> forall y, y = x -> P y.
Proof using. intros. subst*. Qed.

Definition eq_rect_r : forall (P:A -> Type),
  P x -> forall y, y = x -> P y.
Proof using. intros. subst*. Qed.

End EqInductionSym.

Functional extensionality

Dependent functional extensionality

Section FuncExtDep.
Variables (A1 : Type).
Variables (A2 : forall (x1 : A1), Type).
Variables (A3 : forall (x1 : A1) (x2 : A2 x1), Type).
Variables (A4 : forall (x1 : A1) (x2 : A2 x1) (x3 : A3 x2), Type).
Variables (A5 : forall (x1 : A1) (x2 : A2 x1) (x3 : A3 x2) (x4 : A4 x3), Type).
Variables (A6 : forall (x1 : A1) (x2 : A2 x1) (x3 : A3 x2) (x4 : A4 x3) (x5 : A5 x4), Type).

Lemma fun_ext_1 : forall (f g : forall (x1:A1), A2 x1),
  (forall x1, f x1 = g x1 ) ->
  f = g.
Proof using. repeat (intros; apply fun_ext_dep). auto. Qed.

Lemma fun_ext_2 : forall (f g : forall (x1:A1) (x2:A2 x1), A3 x2),
  (forall x1 x2, f x1 x2 = g x1 x2 ) ->
  f = g.
Proof using. repeat (intros; apply fun_ext_dep). auto. Qed.

Lemma fun_ext_3 : forall (f g : forall (x1:A1) (x2:A2 x1) (x3:A3 x2), A4 x3),
  (forall x1 x2 x3, f x1 x2 x3 = g x1 x2 x3 ) ->
  f = g.
Proof using. repeat (intros; apply fun_ext_dep). auto. Qed.

Lemma fun_ext_4 : forall (f g: forall (x1:A1) (x2:A2 x1) (x3:A3 x2)
  (x4:A4 x3), A5 x4),
  (forall x1 x2 x3 x4, f x1 x2 x3 x4 = g x1 x2 x3 x4 ) ->
  f = g.
Proof using. repeat (intros; apply fun_ext_dep). auto. Qed.

Lemma fun_ext_5 : forall (f g: forall (x1:A1) (x2:A2 x1) (x3:A3 x2)
  (x4:A4 x3) (x5:A5 x4), A6 x5),
  (forall x1 x2 x3 x4 x5, f x1 x2 x3 x4 x5 = g x1 x2 x3 x4 x5 ) ->
  f = g.
Proof using. repeat (intros; apply fun_ext_dep). auto. Qed.

Global Instance Extensionality_fun_1 :
  Extensionality (forall (x1:A1), A2 x1).
Proof using. intros. apply (Extensionality_make fun_ext_1). Defined.

Global Instance Extensionality_fun_2 :
  Extensionality (forall (x1:A1) (x2:A2 x1), A3 x2).
Proof using. intros. apply (Extensionality_make fun_ext_2). Defined.

Global Instance Extensionality_fun_3 :
  Extensionality (forall (x1:A1) (x2:A2 x1) (x3:A3 x2), A4 x3).
Proof using. intros. apply (Extensionality_make fun_ext_3). Defined.

Global Instance Extensionality_fun_4 :
  Extensionality (forall (x1:A1) (x2:A2 x1) (x3:A3 x2) (x4:A4 x3), A5 x4).
Proof using. intros. apply (Extensionality_make fun_ext_4). Defined.

Global Instance Extensionality_fun_5 :
  Extensionality (forall (x1:A1) (x2:A2 x1) (x3:A3 x2)
  (x4:A4 x3) (x5:A5 x4), A6 x5).
Proof using. intros. apply (Extensionality_make fun_ext_5). Defined.

End FuncExtDep.

Non-dependent functional extensionality

Lemma fun_ext_nondep_1 : forall A1 B (f g : A1 -> B),
  (forall x1, f x1 = g x1 ) ->
  f = g.
Proof using. intros. apply~ fun_ext_1. Qed.

Lemma fun_ext_nondep_2 : forall A1 A2 B (f g : A1 -> A2 -> B),
  (forall x1 x2, f x1 x2 = g x1 x2 ) ->
  f = g.
Proof using. intros. apply~ fun_ext_2. Qed.

Lemma fun_ext_nondep_3 : forall A1 A2 A3 B (f g : A1 -> A2 -> A3 -> B),
  (forall x1 x2 x3, f x1 x2 x3 = g x1 x2 x3 ) ->
  f = g.
Proof using. intros. apply~ fun_ext_3. Qed.

Lemma fun_ext_nondep_4 : forall A1 A2 A3 A4 B (f g : A1 -> A2 -> A3 -> A4 -> B),
  (forall x1 x2 x3 x4, f x1 x2 x3 x4 = g x1 x2 x3 x4 ) ->
  f = g.
Proof using. intros. apply~ fun_ext_4. Qed.

Lemma fun_ext_nondep_5 : forall A1 A2 A3 A4 A5 B (f g : A1 -> A2 -> A3 -> A4 -> A5 -> B),
  (forall x1 x2 x3 x4 x5, f x1 x2 x3 x4 x5 = g x1 x2 x3 x4 x5 ) ->
  f = g.
Proof using. intros. apply~ fun_ext_5. Qed.

Eta-conversion

Lemma fun_eta_dep_1 : forall (A:Type) (B:A ->Type) (f : forall x, B x),
  (fun x1 => f x1 ) = f.
Proof using. intros. apply~ fun_ext_1. Qed.

Lemma fun_eta_1 : forall A1 B (f : A1 -> B),
  (fun x1 => f x1 ) = f.
Proof using. intros. apply~ fun_ext_1. Qed.

Lemma fun_eta_2 : forall A1 A2 B (f : A1 -> A2 -> B),
  (fun x1 x2 => f x1 x2 ) = f.
Proof using. intros. apply~ fun_ext_2. Qed.

Lemma fun_eta_3 : forall A1 A2 A3 B (f : A1 -> A2 -> A3 -> B),
  (fun x1 x2 x3 => f x1 x2 x3 ) = f.
Proof using. intros. apply~ fun_ext_3. Qed.

Lemma fun_eta_4 : forall A1 A2 A3 A4 B (f : A1 -> A2 -> A3 -> A4 -> B),
  (fun x1 x2 x3 x4 => f x1 x2 x3 x4 ) = f.
Proof using. intros. apply~ fun_ext_4. Qed.

Lemma fun_eta_5 : forall A1 A2 A3 A4 A5 B (f : A1 -> A2 -> A3 -> A4 -> A5 -> B),
  (fun x1 x2 x3 x4 x5 => f x1 x2 x3 x4 x5 ) = f.
Proof using. intros. apply~ fun_ext_4. Qed.

Hint Rewrite fun_eta_1 fun_eta_2 fun_eta_3 fun_eta_4 fun_eta_5 : rew_eta.

Predicate extensionality

Dependend predicates

Section PropExt.
Variables (A1 : Type).
Variables (A2 : forall (x1 : A1), Type).
Variables (A3 : forall (x1 : A1) (x2 : A2 x1), Type).
Variables (A4 : forall (x1 : A1) (x2 : A2 x1) (x3 : A3 x2), Type).
Variables (A5 : forall (x1 : A1) (x2 : A2 x1) (x3 : A3 x2) (x4 : A4 x3), Type).
Variables (A6 : forall (x1 : A1) (x2 : A2 x1) (x3 : A3 x2) (x4 : A4 x3) (x5 : A5 x4), Type).

Lemma pred_ext_1 : forall (P Q : forall (x1:A1), Prop),
  (forall x1, P x1 <-> Q x1 ) ->
  P = Q.
Proof using. repeat (intros; apply fun_ext_dep). intros. apply~ prop_ext. Qed.

Lemma pred_ext_2 : forall (P Q : forall (x1:A1) (x2:A2 x1), Prop),
  (forall x1 x2, P x1 x2 <-> Q x1 x2 ) ->
  P = Q.
Proof using. repeat (intros; apply fun_ext_dep). intros. apply~ prop_ext. Qed.

Lemma pred_ext_3 : forall (P Q : forall (x1:A1) (x2:A2 x1) (x3:A3 x2), Prop),
  (forall x1 x2 x3, P x1 x2 x3 <-> Q x1 x2 x3 ) ->
  P = Q.
Proof using. repeat (intros; apply fun_ext_dep). intros. apply~ prop_ext. Qed.

Lemma pred_ext_4 : forall (P Q : forall (x1:A1) (x2:A2 x1) (x3:A3 x2)
  (x4:A4 x3), Prop),
  (forall x1 x2 x3 x4, P x1 x2 x3 x4 <-> Q x1 x2 x3 x4 ) ->
  P = Q.
Proof using. repeat (intros; apply fun_ext_dep). intros. apply~ prop_ext. Qed.

Lemma pred_ext_5 : forall (P Q : forall (x1:A1) (x2:A2 x1) (x3:A3 x2)
  (x4:A4 x3) (x5:A5 x4), Prop),
  (forall x1 x2 x3 x4 x5, P x1 x2 x3 x4 x5 <-> Q x1 x2 x3 x4 x5 ) ->
  P = Q.
Proof using. repeat (intros; apply fun_ext_dep). intros. apply~ prop_ext. Qed.

Lemma pred_ext_6 : forall (P Q : forall (x1:A1) (x2:A2 x1) (x3:A3 x2)
  (x4:A4 x3) (x5:A5 x4) (x6:A6 x5), Prop),
  (forall x1 x2 x3 x4 x5 x6, P x1 x2 x3 x4 x5 x6 <-> Q x1 x2 x3 x4 x5 x6 ) ->
  P = Q.
Proof using. repeat (intros; apply fun_ext_dep). intros. apply~ prop_ext. Qed.

Global Instance Extensionality_pred_1 :
  Extensionality (forall (x1:A1), Prop).
Proof using. intros. apply (Extensionality_make pred_ext_1). Defined.

Global Instance Extensionality_pred_2 :
  Extensionality (forall (x1:A1) (x2:A2 x1), Prop).
Proof using. intros. apply (Extensionality_make pred_ext_2). Defined.

Global Instance Extensionality_pred_3 :
  Extensionality (forall (x1:A1) (x2:A2 x1) (x3:A3 x2), Prop).
Proof using. intros. apply (Extensionality_make pred_ext_3). Defined.

Global Instance Extensionality_pred_4 :
  Extensionality (forall (x1:A1) (x2:A2 x1) (x3:A3 x2) (x4:A4 x3), Prop).
Proof using. intros. apply (Extensionality_make pred_ext_4). Defined.

Global Instance Extensionality_pred_5 :
  Extensionality (forall (x1:A1) (x2:A2 x1) (x3:A3 x2)
  (x4:A4 x3) (x5:A5 x4), Prop).
Proof using. intros. apply (Extensionality_make pred_ext_5). Defined.

Global Instance Extensionality_pred_6 :
  Extensionality (forall (x1:A1) (x2:A2 x1) (x3:A3 x2)
  (x4:A4 x3) (x5:A5 x4) (x6:A6 x5), Prop).
Proof using. intros. apply (Extensionality_make pred_ext_6). Defined.

End PropExt.

Non-dependend predicate extensionality

Lemma pred_ext_nondep_1 :
  forall A1 (P Q : A1 -> Prop),
  (forall x1, P x1 <-> Q x1 ) ->
  P = Q.
Proof using. intros. apply~ pred_ext_1. Qed.

Lemma pred_ext_nondep_2 :
  forall A1 A2 (P Q : A1 -> A2 -> Prop),
  (forall x1 x2, P x1 x2 <-> Q x1 x2 ) ->
  P = Q.
Proof using. intros. apply~ pred_ext_2. Qed.

Lemma pred_ext_nondep_3 :
  forall A1 A2 A3 (P Q : A1 -> A2 -> A3 -> Prop),
  (forall x1 x2 x3, P x1 x2 x3 <-> Q x1 x2 x3 ) ->
  P = Q.
Proof using. intros. apply~ pred_ext_3. Qed.

Lemma pred_ext_nondep_4 :
  forall A1 A2 A3 A4 (P Q : A1 -> A2 -> A3 -> A4 -> Prop),
  (forall x1 x2 x3 x4, P x1 x2 x3 x4 <-> Q x1 x2 x3 x4 ) ->
  P = Q.
Proof using. intros. apply~ pred_ext_4. Qed.

Lemma pred_ext_nondep_5 :
  forall A1 A2 A3 A4 A5 (P Q : A1 -> A2 -> A3 -> A4 -> A5 -> Prop),
  (forall x1 x2 x3 x4 x5, P x1 x2 x3 x4 x5 <-> Q x1 x2 x3 x4 x5 ) ->
  P = Q.
Proof using. intros. apply~ pred_ext_5. Qed.

Lemma pred_ext_nondep_6 :
  forall A1 A2 A3 A4 A5 A6 (P Q : A1 -> A2 -> A3 -> A4 -> A5 -> A6 -> Prop),
  (forall x1 x2 x3 x4 x5 x6, P x1 x2 x3 x4 x5 x6 <-> Q x1 x2 x3 x4 x5 x6 ) ->
  P = Q.
Proof using. intros. apply~ pred_ext_6. Qed.

Equality of function and predicate applications

A same function applied to equal arguments yield equal result

Section ArgsEq.
Variables (A1 A2 A3 A4 A5 B : Type).

Lemma args_eq_1 : forall (f:A1 ->B) x1 y1,
  x1 = y1 ->
  f x1 = f y1.
Proof using. intros. subst~. Qed.

Lemma args_eq_2 : forall (f:A1 ->A2 ->B) x1 y1 x2 y2,
  x1 = y1 ->
  x2 = y2 ->
  f x1 x2 = f y1 y2.
Proof using. intros. subst~. Qed.

Lemma args_eq_3 : forall (f:A1 ->A2 ->A3 ->B) x1 y1 x2 y2 x3 y3,
  x1 = y1 ->
  x2 = y2 ->
  x3 = y3 ->
  f x1 x2 x3 = f y1 y2 y3.
Proof using. intros. subst~. Qed.

Lemma args_eq_4 : forall (f:A1 ->A2 ->A3 ->A4 ->B) x1 y1 x2 y2 x3 y3 x4 y4,
  x1 = y1 ->
  x2 = y2 ->
  x3 = y3 ->
  x4 = y4 ->
  f x1 x2 x3 x4 = f y1 y2 y3 y4.
Proof using. intros. subst~. Qed.

Lemma args_eq_5 : forall (f:A1 ->A2 ->A3 ->A4 ->A5 ->B) x1 y1 x2 y2 x3 y3 x4 y4 x5 y5,
  x1 = y1 ->
  x2 = y2 ->
  x3 = y3 ->
  x4 = y4 ->
  x5 = y5 ->
  f x1 x2 x3 x4 x5 = f y1 y2 y3 y4 y5.
Proof using. intros. subst~. Qed.

End ArgsEq.

Equal functions applied to same arguments return equal results

These results are exploited by tactic fequals (see LibTactics); however the lemmas remain useful for forward-reasoning.

Section FuncEq.
Variables (A1 A2 A3 A4 A5 B:Type).
Variables (x1:A1) (x2:A2) (x3:A3) (x4:A4) (x5:A5).

Lemma fun_eq_1 : forall f g,
  f = g ->
  f x1 = g x1 :> B.
Proof using. intros. subst~. Qed.

Lemma fun_eq_2 : forall f g,
  f = g ->
  f x1 x2 = g x1 x2 :> B.
Proof using. intros. subst~. Qed.

Lemma fun_eq_3 : forall f g,
  f = g ->
  f x1 x2 x3 = g x1 x2 x3 :> B.
Proof using. intros. subst~. Qed.

Lemma fun_eq_4 : forall f g,
  f = g ->
  f x1 x2 x3 x4 = g x1 x2 x3 x4 :> B.
Proof using. intros. subst~. Qed.

Lemma fun_eq_5 : forall f g,
  f = g ->
  f x1 x2 x3 x4 x5 = g x1 x2 x3 x4 x5 :> B.
Proof using. intros. subst~. Qed.

End FuncEq.

Equal predicates applied to same arguments return equivalent results

These results are exploited by tactic fequals (see LibTactics); however the lemmas remain useful for forward-reasoning.

Section PredEq.
Variables (A1 A2 A3 A4 A5 B:Type).
Variables (x1:A1) (x2:A2) (x3:A3) (x4:A4) (x5:A5).

Lemma pred_eq_1 : forall P Q,
  P = Q ->
  P x1 <-> Q x1.
Proof using. intros. subst*. Qed.

Lemma pred_eq_2 : forall P Q,
  P = Q ->
  P x1 x2 <-> Q x1 x2.
Proof using. intros. subst*. Qed.

Lemma pred_eq_3 : forall P Q,
  P = Q ->
  P x1 x2 x3 <-> Q x1 x2 x3.
Proof using. intros. subst*. Qed.

Lemma pred_eq_4 : forall P Q,
  P = Q ->
  P x1 x2 x3 x4 <-> Q x1 x2 x3 x4.
Proof using. intros. subst*. Qed.

Lemma pred_eq_5 : forall P Q,
  P = Q ->
  P x1 x2 x3 x4 x5 <-> Q x1 x2 x3 x4 x5.
Proof using. intros. subst*. Qed.

End PredEq.

Proof Irrelevance

The proof irrelevance lemma states that two proofs of a same proposition are always equal. forall (P : Prop) (p q : P), p = q This result is a consequence of propositional extensionality.

Proof of the proof-irrelevance result

Module PIfromExt.

Implicit Types P : Prop.

First, we prove that on an inhabited proposition type, there exists a fixpoint combinator.

Lemma prop_eq_self_impl_when_true : forall P,
  P ->
  P = (P -> P ).
Proof using. intros. apply* prop_ext. Qed.

Record has_fixpoint (P:Prop) : Prop := has_fixpoint_make
  { has_fixpoint_F : (P -> P ) -> P;
    has_fixpoint_fix : forall f, has_fixpoint_F f = f (has_fixpoint_F f) }.

Lemma prop_has_fixpoint_when_true : forall P,
  P ->
  has_fixpoint P.
Proof using.
  intros P a. set (P' := P).
  set (g1 := id : P' -> P). set (g2 := id : P -> P').
  asserts~ Fix: (forall x, g1 (g2 x) = x).
  clearbody g1 g2. gen g1 g2.
  rewrite (prop_eq_self_impl_when_true a).
  subst P'. intros.
  set (Y := fun f => (fun x => f (g1 x x)) (g2 (fun x => f (g1 x x)))).
  applys (has_fixpoint_make Y).   { intros f. unfold Y at 1. rewrite~ Fix. }
Qed.

We exploit the fixpoint combinator on the negation function, applied to the following special proposition type (isomorphic to booleans, but living in Prop).

Inductive boolP : Prop :=
  | trueP : boolP
  | falseP : boolP.

Lemma trueP_eq_falseP : trueP = falseP.
Proof using.
  lets (Y&Yfix): (@prop_has_fixpoint_when_true boolP trueP).
  set (neg := fun b => match b with| trueP => falseP | falseP => trueP end).
  lets F: ((rm Yfix) neg).
  set (b := Y neg).
  asserts~ E: (b = Y neg).
  destruct b.
  { change (trueP = neg trueP) in |- *. rewrite E. rewrite~ <- F. }
  { change (neg falseP = falseP) in |- *. rewrite E. rewrite~ <- F. }
Qed.

We now have two distinct constructors trueP and falseP, which we can distinguish in the logic using match for any goal concluding on a proposition; and, at the same time, these two constructors are provably equal. We can exploit these properties to prove that two proofs of a same theorem are equal.

Lemma proof_irrelevance :
  forall (P : Prop) (p q : P), p = q.
Proof using.
  intros P p q.
  set (f := fun b => match b with | trueP => p | falseP => q end).
  change p with (f trueP).
  change q with (f falseP).
  rewrite~ trueP_eq_falseP.
Qed.

End PIfromExt.

Lemma proof_irrelevance : forall (P : Prop) (p q : P), p = q.
Proof using. exact PIfromExt.proof_irrelevance. Qed.

Consequences of proof irrelevance

Uniqueness of identity proofs

Lemma identity_proofs_unique :
forall (A : Type) (x y : A) (p q : x = y),
p = q.
Proof using. intros. apply proof_irrelevance. Qed.

Uniqueness of reflexive identity proofs (special case)

Lemma reflexive_identity_proofs_unique :
forall (A : Type) (x : A) (p : x = x),
p = refl_equal x.
Proof using. intros. applys identity_proofs_unique. Qed.

Invariance by substitution of reflexive equality proofs

Lemma eq_rect_refl_eq :
forall (A : Type) (p : A) (Q : A -> Type) (x : Q p) (h : p = p),
eq_rect p Q x p h = x.
Proof using. intros. rewrite~ (reflexive_identity_proofs_unique h). Qed.

Streicher's axiom K

Lemma streicher_K :
  forall (A : Type) (x : A) (P : x = x -> Prop),
  P (refl_equal x) ->
  forall (p : x = x), P p.
Proof using. intros. rewrite~ (reflexive_identity_proofs_unique p). Qed.

Injectivity of equality on dependent pairs

This section establishes that existT P p x = existT P p y implies that x is equal to y. It indirectly results from the proof irrelevance property.

Definition of dependent equality, with non-dependent return type

Inductive eq_dep_nd (A : Type) (P : A -> Type)
(p : A) (x : P p) (q : A) (y : P q) : Prop :=
| eq_dep_nd_intro : forall (h : q = p),
x = eq_rect q P y p h -> eq_dep_nd P p x q y.

Arguments eq_dep_nd [A] [P] [p] x [q] y.
Arguments eq_dep_nd_intro [A] [P] [p] [x] [q] [y].

Reflexivity of eq_dep_nd

Lemma eq_dep_nd_refl : forall (A : Type) (P : A -> Type) (p : A) (x : P p),
eq_dep_nd x x.
Proof using. intros. apply (eq_dep_nd_intro (refl_equal p)). auto. Qed.

Injectivity of eq_dep_nd

Lemma eq_dep_nd_same_inv :
  forall (A : Type) (P : A -> Type) (p : A) (x y : P p),
  eq_dep_nd x y ->
  x = y.
Proof using. introv H. inversions H. rewrite~ eq_rect_refl_eq. Qed.

Equality on dependent pairs implies eq_dep_nd

Lemma eq_existT_inv :
  forall (A : Type) (P : A -> Type) (p q : A) (x : P p) (y : P q),
  existT P p x = existT P q y ->
  eq_dep_nd x y.
Proof using. introv E. dependent rewrite E. simpl. apply eq_dep_nd_refl. Qed.

Injectivity of equality on dependent pairs

Lemma eq_existT_same_inv :
  forall (A : Type) (P : A -> Type) (p : A) (x y : P p),
  existT P p x = existT P p y ->
  x = y.
Proof using. intros. apply eq_dep_nd_same_inv. apply~ eq_existT_inv. Qed.

Reformulated as an equality

Lemma eq_existT_same_eq :
  forall (A : Type) (P : A -> Type) (p : A) (x y : P p),
  (existT P p x = existT P p y ) = (x = y ).
Proof using.
  extens. iff M.
  { apply eq_dep_nd_same_inv. apply~ eq_existT_inv. }
  { subst*. }
Qed.

Irrelevance of the membership property for subsets types

This is another consequence of proof irrelevance

Scheme eq_indd := Induction for eq Sort Prop.

Lemma exist_eq_exist : forall (A:Type) (P : A ->Prop) (x y : A) (p : P x) (q : P y),
  x = y ->
  exist P x p = exist P y q.
Proof using.
  intros. rewrite (proof_irrelevance q (eq_rect x P p y H)). subst*.
Qed.

Lemma existT_eq_existT : forall (A:Type) (P:A ->Prop) (x y:A) (p:P x) (q:P y),
  x = y ->
  existT P x p = existT P y q.
Proof using.
  intros. rewrite (proof_irrelevance q (eq_rect x P p y H)). subst*.
Qed.

Dependent equality

In this section, we prove that eq_dep x y implies x = y.

Definition of eq_dep (copied from the Prelude)

Inductive eq_dep (A : Type) (P : A -> Type) (p : A) (x : P p)
: forall q, P q -> Prop :=
| eq_dep_refl : eq_dep P p x p x.

Arguments eq_dep [A] [P] [p] x [q].

Symmetry of eq_dep

Lemma eq_dep_sym : forall (A : Type) (P : A -> Type)
(p q : A) (x : P p) (y : P q),
eq_dep x y ->
eq_dep y x.
Proof using. introv E. destruct E. constructor. Qed.

Transitivity of eq_dep

Lemma eq_dep_trans : forall (A : Type) (P : A -> Type)
(p q r : A) (y : P q) (x : P p) (z : P r),
  eq_dep x y ->
  eq_dep y z ->
  eq_dep x z.
Proof using. introv E F. destruct~ E. Qed.

Proof of equivalence between eq_dep_nd and eq_dep

Scheme eq_induction := Induction for eq Sort Prop.

Lemma eq_dep_of_eq_dep_nd :
  forall (A : Type) (P : A -> Type) (p q : A) (x : P p) (y : P q),
  eq_dep_nd x y ->
  eq_dep x y.
Proof using.
  introv E. destruct E as (h,H).
  destruct h using eq_induction. subst~. constructor.
Qed.

Lemma eq_dep_nd_of_eq_dep :
  forall (A : Type) (P : A -> Type) (p q : A) (x : P p) (y : P q),
  eq_dep x y ->
  eq_dep_nd x y.
Proof using. introv H. destruct H. apply (eq_dep_nd_intro (refl_equal p)); auto. Qed.

Injectivity of dependent equality

Lemma eq_dep_same_inv :
  forall (A : Type) (P : A -> Type) (p : A) (x y : P p),
  eq_dep x y ->
  x = y.
Proof using.
  introv R. inversion R. apply eq_dep_nd_same_inv. apply~ eq_dep_nd_of_eq_dep.
Qed.

Equality on dependent pairs implies dependent equality

Lemma eq_dep_of_eq_existT :
  forall (A : Type) (P : A -> Type) (p q : A) (x : P p) (y : P q),
  existT P p x = existT P q y ->
  eq_dep x y.
Proof using. introv E. dependent rewrite E. simple~. constructor. Qed.

John Major's equality

Require Import Coq.Logic.JMeq.

The module above defines John Major's equality:

Inductive JMeq (A : Type) (x : A) : forall B : Type, B -> Prop := | JMeq_refl : JMeq x x.

In this section, we prove that JMeq x y implies x = y when x and y have the same type.

Symmetry, transitivity of JMeq

Lemma JMeq_sym : forall (A B : Type) (x : A) (y : B),
  JMeq x y ->
  JMeq y x.
Proof using. introv E. destruct~ E. Qed.

Lemma JMeq_trans : forall (A B C : Type) (y : B) (x : A) (z : C),
  JMeq x y ->
  JMeq y z ->
  JMeq x z.
Proof using. introv E F. destruct~ E. Qed.

Local Hint Immediate JMeq_sym.

Relation between JMeq and eq_dep

Lemma eq_dep_of_JMeq : forall (A B : Type) (x : A) (y : B),
  JMeq x y ->
  @eq_dep Type (fun T => T) A x B y.
Proof using. introv E. destruct E. constructor. Qed.

Lemma JMeq_of_eq_dep : forall (A B : Type) (x : A) (y : B),
  @eq_dep Type (fun T => T) A x B y ->
  JMeq x y.
Proof using. introv E. destruct~ E. Qed.

Injectivity of JMeq

Lemma JMeq_same_inv : forall (A : Type) (x y : A),
  JMeq x y ->
  x = y.
Proof using.
  introv E. apply (@eq_dep_same_inv Type (fun T => T)).
  apply~ eq_dep_of_JMeq.
Qed.