Module mathcomp.classical.internal_Eqdep_dec

Attributes deprecated(since="mathcomp-analysis 1.10.0",
  note="This file is for internal purpose only and should not \
  be imported nor used. It may be removed in the future.").

Import EqNotations.

Section Dependent_Equality.

Variables ( : Type) ( : U -> Type).

Inductive ( : U) ( : P p) : forall : U, P q -> Prop :=
   : eq_dep p x p x.

Lemma ( : U) ( : P p) ( : P q) :
  eq_dep p x q y -> eq_dep q y p x.

Proof.

destruct 1; auto; apply eq_dep_intro. Qed.

Inductive ( : U) ( : P p) ( : U) ( : P q) : Prop :=
: forall : q = p, x = rew h in y -> eq_dep1 p x q y.

Lemma ( : U) ( : P p) ( : P q) :
eq_dep p x q y -> eq_dep1 p x q y.

Proof.

revert p q x y; intros p; destruct 1.
apply eq_dep1_intro with (eq_refl p); simpl; trivial.
Qed.

End Dependent_Equality.

Section Equivalences.

Variable : Type.

Definition ( : U) ( : U -> Type) ( : Q p) :=
  forall ( : p = p), x = eq_rect p Q x p h.
Definition := forall , Eq_rect_eq_on p Q x.

Definition ( : U -> Type) ( : U) ( : P p) :=
  forall ( : P p), eq_dep _ _ p x p y -> x = y.
Definition := forall , Eq_dep_eq_on P p x.

Definition ( : U) ( : x = x -> Prop) :=
  P (eq_refl x) -> forall : x = x, P p.
Definition := forall , Streicher_K_on_ x P.

Lemma ( : U) ( : U -> Type) ( : P p) :
  Eq_rect_eq_on p P y -> forall ( : P p), eq_dep1 _ _ p x p y -> x = y.

Proof.

intro ere; simple destruct 1; intro; rewrite <-ere; auto. Qed.

Lemma :
  Eq_rect_eq -> forall (:U->Type) (:U) ( :P p), eq_dep1 _ _ p x p y -> x = y.
Proof (fun =>
  @eq_rect_eq_on__eq_dep1_eq_on p P x (eq_rect_eq p P x) y).

Lemma ( : U) ( : U -> Type) ( : P p) :
  Eq_rect_eq_on p P x -> Eq_dep_eq_on P p x.

Proof.

intros eq_rect_eq; red; intros y H.
symmetry; apply (eq_rect_eq_on__eq_dep1_eq_on _ _ _ eq_rect_eq).
apply eq_dep_sym in H; apply eq_dep_dep1; trivial.
Qed.

Lemma : Eq_rect_eq -> Eq_dep_eq.
Proof (fun =>
@eq_rect_eq_on__eq_dep_eq_on p P x (eq_rect_eq p P x) y).

Lemma ( : U) ( : U -> Type) ( : P p) :
Streicher_K_on_ p (fun => x = rew -> [P] h in x) -> Eq_rect_eq_on p P x.

Proof.

intro Streicher_K; red; intros; apply Streicher_K; reflexivity. Qed.

Lemma : Streicher_K_ -> Eq_rect_eq.

Proof.

exact (fun =>
@Streicher_K_on__eq_rect_eq_on p P x (Streicher_K p _)).
Qed.

End Equivalences.

Set SsrOldRewriteGoalsOrder.
Set Implicit Arguments.

Section EqdepDec.

Variable : Type.

Let ( : A) ( : x = y) ( : x = y') : y = y' :=
eq_ind _ (fun => a = y') eq2 _ eq1.

Remark ( : A) ( : x = y) : comp u u = eq_refl y.

Proof.

now case u. Qed.

Variables ( : A) ( : forall : A, x = y \/ x <> y).

Let (:A) (:x = y) : x = y :=
  match eq_dec y with
  | or_introl eqxy => eqxy
  | or_intror neqxy => False_ind _ (neqxy u)
  end.

#[local] Lemma ( : A) ( : x = y) : nu u = nu v.

Proof.

now unfold nu; destruct (eq_dec y) as [Heq|Hneq]; [reflexivity|case Hneq].
Qed.

Let ( : A) ( : x = y) : x = y := comp (nu (eq_refl x)) v.

Remark (:A) (:x = y) : nu_inv (nu u) = u.

Proof.

case u; unfold nu_inv; apply trans_sym_eq. Qed.

Theorem ( : A) ( : x = y) : p1 = p2.

Proof.

elim (nu_left_inv_on p1).
elim (nu_left_inv_on p2).
elim nu_constant with y p1 p2.
reflexivity.
Qed.

Theorem ( : x = x -> Prop) ( : P (eq_refl x)) ( : x = x) : P p.

Proof.

now elim eq_proofs_unicity_on with x (eq_refl x) p. Qed.

End EqdepDec.

Theorem ( : forall : A, x = y \/ x <> y) ( : A) :
forall : x = x -> Prop, P (eq_refl x) -> forall : x = x, P p.

Proof.

exact (@K_dec_on A x (eq_dec x)). Qed.

Section Eq_dec.

Variables ( : Type) ( : forall : A, {x = y} + {x <> y}).

Theorem ( : A) ( : x = x -> Prop) ( : P (eq_refl x)) ( : x = x) :
P p.

Proof.

elim p using K_dec; [|now trivial].
now intros x0 y; case (eq_dec x0 y); [left|right].
Qed.

Theorem : forall ( : A) ( : A -> Type) ( : Q p) ( : p = p),
x = eq_rect p Q x p h.

Proof.

exact (Streicher_K__eq_rect_eq A K_dec_type). Qed.

Unset Implicit Arguments.

Lemma ( : Type) ( : U -> Type) ( : U) ( : P p) ( : P q) :
existT P p x = existT P q y -> eq_dep _ _ p x q y.

Proof.

intros * H; dependent rewrite H; apply eq_dep_intro. Qed.

Section Corollaries.

Variable : Type.

Definition ( : U -> Type) ( : U) ( : P p) :=
forall ( : P p), existT P p x = existT P p y -> x = y.
Definition := forall , Inj_dep_pair_on P p x.

Lemma ( : U -> Type) ( : U) ( : P p) :
Eq_dep_eq_on U P p x -> Inj_dep_pair_on P p x.

Proof.

intro ede; red; intros; apply ede; apply eq_sigT_eq_dep; assumption. Qed.

Lemma : Eq_dep_eq U -> Inj_dep_pair.
Proof (fun =>
@eq_dep_eq_on__inj_pair2_on P p x (eq_dep_eq P p x)).

End Corollaries.

Lemma :
forall ( : A -> Type) ( : A) ( : P p), existT P p x = existT P p y -> x = y.

Proof.

  apply eq_dep_eq__inj_pair2.
  apply eq_rect_eq__eq_dep_eq.
  unfold Eq_rect_eq, Eq_rect_eq_on.
  intros; apply eq_rect_eq_dec.
Qed.

End Eq_dec.

Files

Module mathcomp.classical.internal_Eqdep_dec