Files

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 (USource code : Type) (PSource code : U -> Type).

Inductive eq_depSource code (pSource code : U) (xSource code : P p) : forall qSource code : U, P q -> Prop :=
  eq_dep_introSource code : eq_dep p x p x.

Lemma eq_dep_symSource code (pSource code qSource code : U) (xSource code : P p) (ySource code : P q) :
  eq_dep p x q y -> eq_dep q y p x.
Proof.
destruct 1; auto; apply eq_dep_intro. Qed.

Inductive eq_dep1Source code (pSource code : U) (xSource code : P p) (qSource code : U) (ySource code : P q) : Prop :=
  eq_dep1_introSource code : forall hSource code : q = p, x = rew h in y -> eq_dep1 p x q y.

Lemma eq_dep_dep1Source code (pSource code qSource code : U) (xSource code : P p) (ySource code : 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 USource code : Type.

Definition Eq_rect_eq_on

Eq_rect_eq_on : forall (U : Type) (p : U) (Q : U -> Type), Q p -> Prop Eq_rect_eq_on is not universe polymorphic Arguments Eq_rect_eq_on U%_type_scope p Q%_function_scope x Eq_rect_eq_on is transparent Expands to: Constant mathcomp.classical.internal_Eqdep_dec.Eq_rect_eq_on Declared in library mathcomp.classical.internal_Eqdep_dec, line 36, characters 11-24

Source code (pSource code : U) (QSource code : U -> Type) (xSource code : Q p) :=
  forall (hSource code : p = p), x = eq_rect p Q x p h.
Definition Eq_rect_eq

Eq_rect_eq : Type -> Prop Eq_rect_eq is not universe polymorphic Arguments Eq_rect_eq U%_type_scope Eq_rect_eq is transparent Expands to: Constant mathcomp.classical.internal_Eqdep_dec.Eq_rect_eq Declared in library mathcomp.classical.internal_Eqdep_dec, line 38, characters 11-21

Source code := forall pSource code QSource code xSource code, Eq_rect_eq_on p Q x.

Definition Eq_dep_eq_on

Eq_dep_eq_on : forall (U : Type) (P : U -> Type) (p : U), P p -> Prop Eq_dep_eq_on is not universe polymorphic Arguments Eq_dep_eq_on U%_type_scope P%_function_scope p x Eq_dep_eq_on is transparent Expands to: Constant mathcomp.classical.internal_Eqdep_dec.Eq_dep_eq_on Declared in library mathcomp.classical.internal_Eqdep_dec, line 40, characters 11-23

Source code (PSource code : U -> Type) (pSource code : U) (xSource code : P p) :=
  forall (ySource code : P p), eq_dep _ _ p x p y -> x = y.
Definition Eq_dep_eq

Eq_dep_eq : Type -> Prop Eq_dep_eq is not universe polymorphic Arguments Eq_dep_eq U%_type_scope Eq_dep_eq is transparent Expands to: Constant mathcomp.classical.internal_Eqdep_dec.Eq_dep_eq Declared in library mathcomp.classical.internal_Eqdep_dec, line 42, characters 11-20

Source code := forall PSource code pSource code xSource code, Eq_dep_eq_on P p x.

Definition Streicher_K_on_

Streicher_K_on_ : forall (U : Type) (x : U), (x = x -> Prop) -> Prop Streicher_K_on_ is not universe polymorphic Arguments Streicher_K_on_ U%_type_scope x P%_function_scope Streicher_K_on_ is transparent Expands to: Constant mathcomp.classical.internal_Eqdep_dec.Streicher_K_on_ Declared in library mathcomp.classical.internal_Eqdep_dec, line 44, characters 11-26

Source code (xSource code : U) (PSource code : x = x -> Prop) :=
  P (eq_refl x) -> forall pSource code : x = x, P p.
Definition Streicher_K_

Streicher_K_ : Type -> Prop Streicher_K_ is not universe polymorphic Arguments Streicher_K_ U%_type_scope Streicher_K_ is transparent Expands to: Constant mathcomp.classical.internal_Eqdep_dec.Streicher_K_ Declared in library mathcomp.classical.internal_Eqdep_dec, line 46, characters 11-23

Source code := forall xSource code PSource code, Streicher_K_on_ x P.

Lemma eq_rect_eq_on__eq_dep1_eq_onSource code (pSource code : U) (PSource code : U -> Type) (ySource code : P p) :
  Eq_rect_eq_on p P y -> forall (xSource code : 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__eq_dep1_eqSource code :
  Eq_rect_eq -> forall (PSource code:U->Type) (pSource code:U) (xSource code ySource code:P p), eq_dep1 _ _ p x p y -> x = y.
Proof (fun eq_rect_eqSource code PSource code pSource code ySource code xSource code =>
  @eq_rect_eq_on__eq_dep1_eq_on p P x (eq_rect_eq p P x) y).

Lemma eq_rect_eq_on__eq_dep_eq_onSource code (pSource code : U) (PSource code : U -> Type) (xSource code : 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_eqSource code : Eq_rect_eq -> Eq_dep_eq.
Proof (fun eq_rect_eqSource code PSource code pSource code xSource code ySource code =>
  @eq_rect_eq_on__eq_dep_eq_on p P x (eq_rect_eq p P x) y).

Lemma Streicher_K_on__eq_rect_eq_onSource code (pSource code : U) (PSource code : U -> Type) (xSource code : P p) :
  Streicher_K_on_ p (fun hSource code => 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_eqSource code : Streicher_K_ -> Eq_rect_eq.
Proof.
exact (fun Streicher_KSource code pSource code PSource code xSource code =>
  @Streicher_K_on__eq_rect_eq_on p P x (Streicher_K p _)).
Qed.
End Equivalences.

Unset SsrOldRewriteGoalsOrder.  
Set Implicit Arguments.

Section EqdepDec.

Variable ASource code : Type.

Let compSource code (xSource code ySource code y'Source code : A) (eq1Source code : x = y) (eq2Source code : x = y') : y = y' :=
  eq_ind _ (fun aSource code => a = y') eq2 _ eq1.

Remark trans_sym_eqSource code (xSource code ySource code : A) (uSource code : x = y) : comp u u = eq_refl y.
Proof.
now case u. Qed.

Variables (xSource code : A) (eq_decSource code : forall ySource code : A, x = y \/ x <> y).

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

#[local] Lemma nu_constantSource code (ySource code : A) (uSource code vSource code : x = y) : nu u = nu v.
Proof.
now unfold nu; destruct (eq_dec y) as [Heq|Hneq]; [reflexivity|case Hneq].
Qed.

Let nu_invSource code (ySource code : A) (vSource code : x = y) : x = y := comp (nu (eq_refl x)) v.

Remark nu_left_inv_onSource code (ySource code:A) (uSource code:x = y) : nu_inv (nu u) = u.
Proof.
case u; unfold nu_inv; apply trans_sym_eq. Qed.

Theorem eq_proofs_unicity_onSource code (ySource code : A) (p1Source code p2Source code : 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 K_dec_onSource code (PSource code : x = x -> Prop) (HSource code : P (eq_refl x)) (pSource code : x = x) : P p.
Proof.
now elim eq_proofs_unicity_on with x (eq_refl x) p. Qed.

End EqdepDec.

Theorem K_decSource code ASource code (eq_decSource code : forall xSource code ySource code : A, x = y \/ x <> y) (xSource code : A) :
  forall PSource code : x = x -> Prop, P (eq_refl x) -> forall pSource code : x = x, P p.
Proof.
exact (@K_dec_on A x (eq_dec x)). Qed.

Section Eq_dec.

Variables (ASource code : Type) (eq_decSource code : forall xSource code ySource code : A, {x = y} + {x <> y}).

Theorem K_dec_typeSource code (xSource code : A) (PSource code : x = x -> Prop) (HSource code : P (eq_refl x)) (pSource code : 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 eq_rect_eq_decSource code : forall (pSource code : A) (QSource code : A -> Type) (xSource code : Q p) (hSource code : 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 eq_sigT_eq_depSource code (USource code : Type) (PSource code : U -> Type) (pSource code qSource code : U) (xSource code : P p) (ySource code : 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 USource code : Type.

Definition Inj_dep_pair_on

Inj_dep_pair_on : forall (U : Type) (P : U -> Type) (p : U), P p -> Prop Inj_dep_pair_on is not universe polymorphic Arguments Inj_dep_pair_on U%_type_scope P%_function_scope p x Inj_dep_pair_on is transparent Expands to: Constant mathcomp.classical.internal_Eqdep_dec.Inj_dep_pair_on Declared in library mathcomp.classical.internal_Eqdep_dec, line 151, characters 11-26

Source code (PSource code : U -> Type) (pSource code : U) (xSource code : P p) :=
  forall (ySource code : P p), existT P p x = existT P p y -> x = y.
Definition Inj_dep_pair

Inj_dep_pair : Type -> Prop Inj_dep_pair is not universe polymorphic Arguments Inj_dep_pair U%_type_scope Inj_dep_pair is transparent Expands to: Constant mathcomp.classical.internal_Eqdep_dec.Inj_dep_pair Declared in library mathcomp.classical.internal_Eqdep_dec, line 153, characters 11-23

Source code := forall PSource code pSource code xSource code, Inj_dep_pair_on P p x.

Lemma eq_dep_eq_on__inj_pair2_onSource code (PSource code : U -> Type) (pSource code : U) (xSource code : 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__inj_pair2Source code : Eq_dep_eq U -> Inj_dep_pair.
Proof (fun eq_dep_eqSource code PSource code pSource code xSource code =>
  @eq_dep_eq_on__inj_pair2_on P p x (eq_dep_eq P p x)).

End Corollaries.

Lemma inj_pair2_eq_decUsed by
  • mathcomp.classical.boolp
Source code :
  forall (PSource code : A -> Type) (pSource code : A) (xSource code ySource code : 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.
Generated by rocqnavi
Source
Uses
Used By