Library Coq.Init.Logic
Set Implicit Arguments.
Require Export Notations.
Require Import Ltac.
Notation "A -> B" := (forall (_ : A), B) : type_scope.
False is the always false proposition
not A, written ~A, is the negation of A
Definition not (A:Prop) := A -> False.
Notation "~ x" := (not x) : type_scope.
Register not as core.not.type.
Notation "~ x" := (not x) : type_scope.
Register not as core.not.type.
Negation of a type in Type
Create the "core" hint database, and set its transparent state for
variables and constants explicitly.
Create HintDb core.
#[global]
Hint Variables Opaque : core.
#[global]
Hint Constants Opaque : core.
#[global]
Hint Unfold not: core.
and A B, written A /\ B, is the conjunction of A and B
conj p q is a proof of A /\ B as soon as
p is a proof of A and q a proof of B
proj1 and proj2 are first and second projections of a conjunction
Inductive and (A B:Prop) : Prop :=
conj : A -> B -> A /\ B
where "A /\ B" := (and A B) : type_scope.
Register and as core.and.type.
Register conj as core.and.conj.
Section Conjunction.
Variables A B : Prop.
Theorem proj1 : A /\ B -> A.
Theorem proj2 : A /\ B -> B.
End Conjunction.
or A B, written A \/ B, is the disjunction of A and B
Inductive or (A B:Prop) : Prop :=
| or_introl : A -> A \/ B
| or_intror : B -> A \/ B
where "A \/ B" := (or A B) : type_scope.
Arguments or_introl [A B] _, [A] B _.
Arguments or_intror [A B] _, A [B] _.
Register or as core.or.type.
iff A B, written A <-> B, expresses the equivalence of A and B
Definition iff (A B:Prop) := (A -> B) /\ (B -> A).
Notation "A <-> B" := (iff A B) : type_scope.
Register iff as core.iff.type.
Register proj1 as core.iff.proj1.
Register proj2 as core.iff.proj2.
Section Equivalence.
Theorem iff_refl : forall A:Prop, A <-> A.
Theorem iff_trans : forall A B C:Prop, (A <-> B) -> (B <-> C) -> (A <-> C).
Theorem iff_sym : forall A B:Prop, (A <-> B) -> (B <-> A).
End Equivalence.
#[global]
Hint Unfold iff: extcore.
Backward direction of the equivalences above does not need assumptions
Theorem and_iff_compat_l : forall A B C : Prop,
(B <-> C) -> (A /\ B <-> A /\ C).
Theorem and_iff_compat_r : forall A B C : Prop,
(B <-> C) -> (B /\ A <-> C /\ A).
Theorem or_iff_compat_l : forall A B C : Prop,
(B <-> C) -> (A \/ B <-> A \/ C).
Theorem or_iff_compat_r : forall A B C : Prop,
(B <-> C) -> (B \/ A <-> C \/ A).
Theorem imp_iff_compat_l : forall A B C : Prop,
(B <-> C) -> ((A -> B) <-> (A -> C)).
Theorem imp_iff_compat_r : forall A B C : Prop,
(B <-> C) -> ((B -> A) <-> (C -> A)).
Theorem not_iff_compat : forall A B : Prop,
(A <-> B) -> (~ A <-> ~B).
Some equivalences
Theorem neg_false : forall A : Prop, ~ A <-> (A <-> False).
Theorem and_cancel_l : forall A B C : Prop,
(B -> A) -> (C -> A) -> ((A /\ B <-> A /\ C) <-> (B <-> C)).
Theorem and_cancel_r : forall A B C : Prop,
(B -> A) -> (C -> A) -> ((B /\ A <-> C /\ A) <-> (B <-> C)).
Theorem and_comm : forall A B : Prop, A /\ B <-> B /\ A.
Theorem and_assoc : forall A B C : Prop, (A /\ B) /\ C <-> A /\ B /\ C.
Theorem or_cancel_l : forall A B C : Prop,
(B -> ~ A) -> (C -> ~ A) -> ((A \/ B <-> A \/ C) <-> (B <-> C)).
Theorem or_cancel_r : forall A B C : Prop,
(B -> ~ A) -> (C -> ~ A) -> ((B \/ A <-> C \/ A) <-> (B <-> C)).
Theorem or_comm : forall A B : Prop, (A \/ B) <-> (B \/ A).
Theorem or_assoc : forall A B C : Prop, (A \/ B) \/ C <-> A \/ B \/ C.
Lemma iff_and : forall A B : Prop, (A <-> B) -> (A -> B) /\ (B -> A).
Lemma iff_to_and : forall A B : Prop, (A <-> B) <-> (A -> B) /\ (B -> A).
First-order quantifiers
Inductive ex (A:Type) (P:A -> Prop) : Prop :=
ex_intro : forall x:A, P x -> ex (A:=A) P.
Register ex as core.ex.type.
Register ex_intro as core.ex.intro.
Section Projections.
Variables (A:Prop) (P:A->Prop).
Definition ex_proj1 (x:ex P) : A :=
match x with ex_intro _ a _ => a end.
Definition ex_proj2 (x:ex P) : P (ex_proj1 x) :=
match x with ex_intro _ _ b => b end.
Register ex_proj1 as core.ex.proj1.
Register ex_proj2 as core.ex.proj2.
End Projections.
Inductive ex2 (A:Type) (P Q:A -> Prop) : Prop :=
ex_intro2 : forall x:A, P x -> Q x -> ex2 (A:=A) P Q.
ex2 of a predicate can be projected to an ex.
This allows ex_proj1 and ex_proj2 to be usable with ex2.
We have two choices here: either we can set up the definition so
that ex_proj1 of a coerced X : ex2 P Q will unify with let
(a, _, _) := X in a by restricting the first argument of ex2 to
be a Prop, or we can define a more general ex_of_ex2 which
does not satisfy this conversion rule. We choose the former,
under the assumption that there is no reason to turn an ex2 into
an ex unless it is to project out the components.
Definition ex_of_ex2 (A : Prop) (P Q : A -> Prop) (X : ex2 P Q) : ex P
:= ex_intro P
(let (a, _, _) := X in a)
(let (x, p, _) as s return (P (let (a, _, _) := s in a)) := X in p).
Section ex2_Projections.
Variables (A:Prop) (P Q:A->Prop).
Definition ex_proj3 (x:ex2 P Q) : Q (ex_proj1 (ex_of_ex2 x)) :=
match x with ex_intro2 _ _ _ _ b => b end.
End ex2_Projections.
Definition all (A:Type) (P:A -> Prop) := forall x:A, P x.
Notation "'exists' x .. y , p" := (ex (fun x => .. (ex (fun y => p)) ..))
(at level 200, x binder, right associativity,
format "'[' 'exists' '/ ' x .. y , '/ ' p ']'")
: type_scope.
Notation "'exists2' x , p & q" := (ex2 (fun x => p) (fun x => q))
(at level 200, x name, p at level 200, right associativity) : type_scope.
Notation "'exists2' x : A , p & q" := (ex2 (A:=A) (fun x => p) (fun x => q))
(at level 200, x name, A at level 200, p at level 200, right associativity,
format "'[' 'exists2' '/ ' x : A , '/ ' '[' p & '/' q ']' ']'")
: type_scope.
Notation "'exists2' ' x , p & q" := (ex2 (fun x => p) (fun x => q))
(at level 200, x strict pattern, p at level 200, right associativity) : type_scope.
Notation "'exists2' ' x : A , p & q" := (ex2 (A:=A) (fun x => p) (fun x => q))
(at level 200, x strict pattern, A at level 200, p at level 200, right associativity,
format "'[' 'exists2' '/ ' ' x : A , '/ ' '[' p & '/' q ']' ']'")
: type_scope.
Derived rules for universal quantification
Section universal_quantification.
Variable A : Type.
Variable P : A -> Prop.
Theorem inst : forall x:A, all (fun x => P x) -> P x.
Theorem gen : forall (B:Prop) (f:forall y:A, B -> P y), B -> all P.
End universal_quantification.
Equality
Inductive eq (A:Type) (x:A) : A -> Prop :=
eq_refl : x = x :>A
where "x = y :> A" := (@eq A x y) : type_scope.
Arguments eq {A} x _.
Arguments eq_refl {A x} , [A] x.
Arguments eq_ind [A] x P _ y _ : rename.
Arguments eq_rec [A] x P _ y _ : rename.
Arguments eq_rect [A] x P _ y _ : rename.
Notation "x = y" := (eq x y) : type_scope.
Notation "x <> y :> T" := (~ x = y :>T) : type_scope.
Notation "x <> y" := (~ (x = y)) : type_scope.
#[global]
Hint Resolve I conj or_introl or_intror : core.
#[global]
Hint Resolve eq_refl: core.
#[global]
Hint Resolve ex_intro ex_intro2: core.
Register eq as core.eq.type.
Register eq_refl as core.eq.refl.
Register eq_ind as core.eq.ind.
Register eq_rect as core.eq.rect.
Section Logic_lemmas.
Theorem absurd : forall A C:Prop, A -> ~ A -> C.
Section equality.
Variables A B : Type.
Variable f : A -> B.
Variables x y z : A.
Theorem eq_sym : x = y -> y = x.
Register eq_sym as core.eq.sym.
Theorem eq_trans : x = y -> y = z -> x = z.
Register eq_trans as core.eq.trans.
Theorem eq_trans_r : x = y -> z = y -> x = z.
Theorem f_equal : x = y -> f x = f y.
Register f_equal as core.eq.congr.
Theorem not_eq_sym : x <> y -> y <> x.
End equality.
Definition eq_sind_r :
forall (A:Type) (x:A) (P:A -> SProp), P x -> forall y:A, y = x -> P y.
Definition eq_ind_r :
forall (A:Type) (x:A) (P:A -> Prop), P x -> forall y:A, y = x -> P y.
Defined.
Register eq_ind_r as core.eq.ind_r.
Definition eq_rec_r :
forall (A:Type) (x:A) (P:A -> Set), P x -> forall y:A, y = x -> P y.
Defined.
Definition eq_rect_r :
forall (A:Type) (x:A) (P:A -> Type), P x -> forall y:A, y = x -> P y.
Defined.
End Logic_lemmas.
Module EqNotations.
Notation "'rew' H 'in' H'" := (eq_rect _ _ H' _ H)
(at level 10, H' at level 10,
format "'[' 'rew' H in '/' H' ']'").
Notation "'rew' [ P ] H 'in' H'" := (eq_rect _ P H' _ H)
(at level 10, H' at level 10,
format "'[' 'rew' [ P ] '/ ' H in '/' H' ']'").
Notation "'rew' <- H 'in' H'" := (eq_rect_r _ H' H)
(at level 10, H' at level 10,
format "'[' 'rew' <- H in '/' H' ']'").
Notation "'rew' <- [ P ] H 'in' H'" := (eq_rect_r P H' H)
(at level 10, H' at level 10,
format "'[' 'rew' <- [ P ] '/ ' H in '/' H' ']'").
Notation "'rew' -> H 'in' H'" := (eq_rect _ _ H' _ H)
(at level 10, H' at level 10, only parsing).
Notation "'rew' -> [ P ] H 'in' H'" := (eq_rect _ P H' _ H)
(at level 10, H' at level 10, only parsing).
Notation "'rew' 'dependent' H 'in' H'"
:= (match H with
| eq_refl => H'
end)
(at level 10, H' at level 10,
format "'[' 'rew' 'dependent' '/ ' H in '/' H' ']'").
Notation "'rew' 'dependent' -> H 'in' H'"
:= (match H with
| eq_refl => H'
end)
(at level 10, H' at level 10, only parsing).
Notation "'rew' 'dependent' <- H 'in' H'"
:= (match eq_sym H with
| eq_refl => H'
end)
(at level 10, H' at level 10,
format "'[' 'rew' 'dependent' <- '/ ' H in '/' H' ']'").
Notation "'rew' 'dependent' [ 'fun' y p => P ] H 'in' H'"
:= (match H as p in (_ = y) return P with
| eq_refl => H'
end)
(at level 10, H' at level 10, y name, p name,
format "'[' 'rew' 'dependent' [ 'fun' y p => P ] '/ ' H in '/' H' ']'").
Notation "'rew' 'dependent' -> [ 'fun' y p => P ] H 'in' H'"
:= (match H as p in (_ = y) return P with
| eq_refl => H'
end)
(at level 10, H' at level 10, y name, p name, only parsing).
Notation "'rew' 'dependent' <- [ 'fun' y p => P ] H 'in' H'"
:= (match eq_sym H as p in (_ = y) return P with
| eq_refl => H'
end)
(at level 10, H' at level 10, y name, p name,
format "'[' 'rew' 'dependent' <- [ 'fun' y p => P ] '/ ' H in '/' H' ']'").
Notation "'rew' 'dependent' [ P ] H 'in' H'"
:= (match H as p in (_ = y) return P y p with
| eq_refl => H'
end)
(at level 10, H' at level 10,
format "'[' 'rew' 'dependent' [ P ] '/ ' H in '/' H' ']'").
Notation "'rew' 'dependent' -> [ P ] H 'in' H'"
:= (match H as p in (_ = y) return P y p with
| eq_refl => H'
end)
(at level 10, H' at level 10,
only parsing).
Notation "'rew' 'dependent' <- [ P ] H 'in' H'"
:= (match eq_sym H as p in (_ = y) return P y p with
| eq_refl => H'
end)
(at level 10, H' at level 10,
format "'[' 'rew' 'dependent' <- [ P ] '/ ' H in '/' H' ']'").
End EqNotations.
Import EqNotations.
Section equality_dep.
Variable A : Type.
Variable B : A -> Type.
Variable f : forall x, B x.
Variables x y : A.
Theorem f_equal_dep (H: x = y) : rew H in f x = f y.
End equality_dep.
Lemma f_equal_dep2 {A A' B B'} (f : A -> A') (g : forall a:A, B a -> B' (f a))
{x1 x2 : A} {y1 : B x1} {y2 : B x2} (H : x1 = x2) :
rew H in y1 = y2 -> rew f_equal f H in g x1 y1 = g x2 y2.
Lemma rew_opp_r A (P:A->Type) (x y:A) (H:x=y) (a:P y) : rew H in rew <- H in a = a.
Lemma rew_opp_l A (P:A->Type) (x y:A) (H:x=y) (a:P x) : rew <- H in rew H in a = a.
Theorem f_equal2 :
forall (A1 A2 B:Type) (f:A1 -> A2 -> B) (x1 y1:A1)
(x2 y2:A2), x1 = y1 -> x2 = y2 -> f x1 x2 = f y1 y2.
Register f_equal2 as core.eq.congr2.
Theorem f_equal3 :
forall (A1 A2 A3 B:Type) (f:A1 -> A2 -> A3 -> B) (x1 y1:A1)
(x2 y2:A2) (x3 y3:A3),
x1 = y1 -> x2 = y2 -> x3 = y3 -> f x1 x2 x3 = f y1 y2 y3.
Theorem f_equal4 :
forall (A1 A2 A3 A4 B:Type) (f:A1 -> A2 -> A3 -> A4 -> B)
(x1 y1:A1) (x2 y2:A2) (x3 y3:A3) (x4 y4:A4),
x1 = y1 -> x2 = y2 -> x3 = y3 -> x4 = y4 -> f x1 x2 x3 x4 = f y1 y2 y3 y4.
Theorem f_equal5 :
forall (A1 A2 A3 A4 A5 B:Type) (f:A1 -> A2 -> A3 -> A4 -> A5 -> B)
(x1 y1:A1) (x2 y2:A2) (x3 y3:A3) (x4 y4:A4) (x5 y5:A5),
x1 = y1 ->
x2 = y2 ->
x3 = y3 -> x4 = y4 -> x5 = y5 -> f x1 x2 x3 x4 x5 = f y1 y2 y3 y4 y5.
Theorem f_equal_compose A B C (a b:A) (f:A->B) (g:B->C) (e:a=b) :
f_equal g (f_equal f e) = f_equal (fun a => g (f a)) e.
The groupoid structure of equality
Theorem eq_trans_refl_l A (x y:A) (e:x=y) : eq_trans eq_refl e = e.
Theorem eq_trans_refl_r A (x y:A) (e:x=y) : eq_trans e eq_refl = e.
Theorem eq_sym_involutive A (x y:A) (e:x=y) : eq_sym (eq_sym e) = e.
Theorem eq_trans_sym_inv_l A (x y:A) (e:x=y) : eq_trans (eq_sym e) e = eq_refl.
Theorem eq_trans_sym_inv_r A (x y:A) (e:x=y) : eq_trans e (eq_sym e) = eq_refl.
Theorem eq_trans_assoc A (x y z t:A) (e:x=y) (e':y=z) (e'':z=t) :
eq_trans e (eq_trans e' e'') = eq_trans (eq_trans e e') e''.
Theorem rew_map A B (P:B->Type) (f:A->B) x1 x2 (H:x1=x2) (y:P (f x1)) :
rew [fun x => P (f x)] H in y = rew f_equal f H in y.
Theorem eq_trans_map {A B} {x1 x2 x3:A} {y1:B x1} {y2:B x2} {y3:B x3}
(H1:x1=x2) (H2:x2=x3) (H1': rew H1 in y1 = y2) (H2': rew H2 in y2 = y3) :
rew eq_trans H1 H2 in y1 = y3.
Lemma map_subst {A} {P Q:A->Type} (f : forall x, P x -> Q x) {x y} (H:x=y) (z:P x) :
rew H in f x z = f y (rew H in z).
Lemma map_subst_map {A B} {P:A->Type} {Q:B->Type} (f:A->B) (g : forall x, P x -> Q (f x))
{x y} (H:x=y) (z:P x) :
rew f_equal f H in g x z = g y (rew H in z).
Lemma rew_swap A (P:A->Type) x1 x2 (H:x1=x2) (y1:P x1) (y2:P x2) : rew H in y1 = y2 -> y1 = rew <- H in y2.
Lemma rew_compose A (P:A->Type) x1 x2 x3 (H1:x1=x2) (H2:x2=x3) (y:P x1) :
rew H2 in rew H1 in y = rew (eq_trans H1 H2) in y.
Extra properties of equality
Theorem eq_id_comm_l A (f:A->A) (Hf:forall a, a = f a) a : f_equal f (Hf a) = Hf (f a).
Theorem eq_id_comm_r A (f:A->A) (Hf:forall a, f a = a) a : f_equal f (Hf a) = Hf (f a).
Lemma eq_refl_map_distr A B x (f:A->B) : f_equal f (eq_refl x) = eq_refl (f x).
Lemma eq_trans_map_distr A B x y z (f:A->B) (e:x=y) (e':y=z) : f_equal f (eq_trans e e') = eq_trans (f_equal f e) (f_equal f e').
Lemma eq_sym_map_distr A B (x y:A) (f:A->B) (e:x=y) : eq_sym (f_equal f e) = f_equal f (eq_sym e).
Lemma eq_trans_sym_distr A (x y z:A) (e:x=y) (e':y=z) : eq_sym (eq_trans e e') = eq_trans (eq_sym e') (eq_sym e).
Lemma eq_trans_rew_distr A (P:A -> Type) (x y z:A) (e:x=y) (e':y=z) (k:P x) :
rew (eq_trans e e') in k = rew e' in rew e in k.
Lemma rew_const A P (x y:A) (e:x=y) (k:P) :
rew [fun _ => P] e in k = k.
Notation sym_eq := eq_sym (only parsing).
Notation trans_eq := eq_trans (only parsing).
Notation sym_not_eq := not_eq_sym (only parsing).
Notation refl_equal := eq_refl (only parsing).
Notation sym_equal := eq_sym (only parsing).
Notation trans_equal := eq_trans (only parsing).
Notation sym_not_equal := not_eq_sym (only parsing).
#[global]
Hint Immediate eq_sym not_eq_sym: core.
Basic definitions about relations and properties
Definition subrelation (A B : Type) (R R' : A->B->Prop) :=
forall x y, R x y -> R' x y.
Definition unique (A : Type) (P : A->Prop) (x:A) :=
P x /\ forall (x':A), P x' -> x=x'.
Definition uniqueness (A:Type) (P:A->Prop) := forall x y, P x -> P y -> x = y.
Unique existence
Notation "'exists' ! x .. y , p" :=
(ex (unique (fun x => .. (ex (unique (fun y => p))) ..)))
(at level 200, x binder, right associativity,
format "'[' 'exists' ! '/ ' x .. y , '/ ' p ']'")
: type_scope.
Lemma unique_existence : forall (A:Type) (P:A->Prop),
((exists x, P x) /\ uniqueness P) <-> (exists! x, P x).
Lemma forall_exists_unique_domain_coincide :
forall A (P:A->Prop), (exists! x, P x) ->
forall Q:A->Prop, (forall x, P x -> Q x) <-> (exists x, P x /\ Q x).
Lemma forall_exists_coincide_unique_domain :
forall A (P:A->Prop),
(forall Q:A->Prop, (forall x, P x -> Q x) <-> (exists x, P x /\ Q x))
-> (exists! x, P x).
Being inhabited
Inductive inhabited (A:Type) : Prop := inhabits : A -> inhabited A.
#[global]
Hint Resolve inhabits: core.
Lemma exists_inhabited : forall (A:Type) (P:A->Prop),
(exists x, P x) -> inhabited A.
Lemma inhabited_covariant (A B : Type) : (A -> B) -> inhabited A -> inhabited B.
Declaration of stepl and stepr for eq and iff
Lemma eq_stepl : forall (A : Type) (x y z : A), x = y -> x = z -> z = y.
Declare Left Step eq_stepl.
Declare Right Step eq_trans.
Lemma iff_stepl : forall A B C : Prop, (A <-> B) -> (A <-> C) -> (C <-> B).
Declare Left Step iff_stepl.
Declare Right Step iff_trans.
More properties of ex and ex2 that rely on equality being present
We define restricted versions of ex_rect and ex_rec which
allow elimination into non-Prop sorts when the inductive is not
informative
η Principles
Definition ex_eta {A : Prop} {P} (p : exists a : A, P a)
: p = ex_intro _ (ex_proj1 p) (ex_proj2 p).
Definition ex2_eta {A : Prop} {P Q} (p : exists2 a : A, P a & Q a)
: p = ex_intro2 _ _ (ex_proj1 (ex_of_ex2 p)) (ex_proj2 (ex_of_ex2 p)) (ex_proj3 p).
Section ex_Prop.
Variables (A:Prop) (P:A->Prop).
Definition ex_rect (P0 : ex P -> Type) (f : forall x p, P0 (ex_intro P x p))
: forall e, P0 e
:= fun e => rew <- ex_eta e in f _ _.
Definition ex_rec : forall (P0 : ex P -> Set) (f : forall x p, P0 (ex_intro P x p)),
forall e, P0 e
:= ex_rect.
End ex_Prop.
: p = ex_intro _ (ex_proj1 p) (ex_proj2 p).
Definition ex2_eta {A : Prop} {P Q} (p : exists2 a : A, P a & Q a)
: p = ex_intro2 _ _ (ex_proj1 (ex_of_ex2 p)) (ex_proj2 (ex_of_ex2 p)) (ex_proj3 p).
Section ex_Prop.
Variables (A:Prop) (P:A->Prop).
Definition ex_rect (P0 : ex P -> Type) (f : forall x p, P0 (ex_intro P x p))
: forall e, P0 e
:= fun e => rew <- ex_eta e in f _ _.
Definition ex_rec : forall (P0 : ex P -> Set) (f : forall x p, P0 (ex_intro P x p)),
forall e, P0 e
:= ex_rect.
End ex_Prop.
Equality for ex
Projecting an equality of a pair to equality of the first components
Definition ex_proj1_eq {A : Prop} {P : A -> Prop} {u v : exists a : A, P a} (p : u = v)
: ex_proj1 u = ex_proj1 v
:= f_equal (@ex_proj1 _ _) p.
: ex_proj1 u = ex_proj1 v
:= f_equal (@ex_proj1 _ _) p.
Projecting an equality of a pair to equality of the second components
Definition ex_proj2_eq {A : Prop} {P : A -> Prop} {u v : exists a : A, P a} (p : u = v)
: rew ex_proj1_eq p in ex_proj2 u = ex_proj2 v
:= rew dependent p in eq_refl.
: rew ex_proj1_eq p in ex_proj2 u = ex_proj2 v
:= rew dependent p in eq_refl.
Equality of ex is itself a ex (forwards-reasoning version)
Definition eq_ex_intro_uncurried {A : Type} {P : A -> Prop} {u1 v1 : A} {u2 : P u1} {v2 : P v1}
(pq : exists p : u1 = v1, rew p in u2 = v2)
: ex_intro _ u1 u2 = ex_intro _ v1 v2.
(pq : exists p : u1 = v1, rew p in u2 = v2)
: ex_intro _ u1 u2 = ex_intro _ v1 v2.
Equality of ex is itself a ex (backwards-reasoning version)
Definition eq_ex_uncurried {A : Prop} {P : A -> Prop} (u v : exists a : A, P a)
(pq : exists p : ex_proj1 u = ex_proj1 v, rew p in ex_proj2 u = ex_proj2 v)
: u = v.
(pq : exists p : ex_proj1 u = ex_proj1 v, rew p in ex_proj2 u = ex_proj2 v)
: u = v.
Curried version of proving equality of ex types
Definition eq_ex_intro {A : Type} {P : A -> Prop} {u1 v1 : A} {u2 : P u1} {v2 : P v1}
(p : u1 = v1) (q : rew p in u2 = v2)
: ex_intro _ u1 u2 = ex_intro _ v1 v2
:= eq_ex_intro_uncurried (ex_intro _ p q).
(p : u1 = v1) (q : rew p in u2 = v2)
: ex_intro _ u1 u2 = ex_intro _ v1 v2
:= eq_ex_intro_uncurried (ex_intro _ p q).
Curried version of proving equality of ex types
Definition eq_ex {A : Prop} {P : A -> Prop} (u v : exists a : A, P a)
(p : ex_proj1 u = ex_proj1 v) (q : rew p in ex_proj2 u = ex_proj2 v)
: u = v
:= eq_ex_uncurried u v (ex_intro _ p q).
(p : ex_proj1 u = ex_proj1 v) (q : rew p in ex_proj2 u = ex_proj2 v)
: u = v
:= eq_ex_uncurried u v (ex_intro _ p q).
In order to have a performant inversion_sigma, we define
specialized versions for when we have constructors on one or
both sides of the equality
Definition eq_ex_intro_l {A : Prop} {P : A -> Prop} u1 u2 (v : exists a : A, P a)
(p : u1 = ex_proj1 v) (q : rew p in u2 = ex_proj2 v)
: ex_intro P u1 u2 = v
:= eq_ex (ex_intro P u1 u2) v p q.
Definition eq_ex_intro_r {A : Prop} {P : A -> Prop} (u : exists a : A, P a) v1 v2
(p : ex_proj1 u = v1) (q : rew p in ex_proj2 u = v2)
: u = ex_intro P v1 v2
:= eq_ex u (ex_intro P v1 v2) p q.
(p : u1 = ex_proj1 v) (q : rew p in u2 = ex_proj2 v)
: ex_intro P u1 u2 = v
:= eq_ex (ex_intro P u1 u2) v p q.
Definition eq_ex_intro_r {A : Prop} {P : A -> Prop} (u : exists a : A, P a) v1 v2
(p : ex_proj1 u = v1) (q : rew p in ex_proj2 u = v2)
: u = ex_intro P v1 v2
:= eq_ex u (ex_intro P v1 v2) p q.
Induction principle for @eq (ex _)
Definition eq_ex_eta {A : Prop} {P : A -> Prop} {u v : exists a : A, P a} (p : u = v) : p = eq_ex u v (ex_proj1_eq p) (ex_proj2_eq p).
Definition eq_ex_rect {A : Prop} {P : A -> Prop} {u v : exists a : A, P a} (Q : u = v -> Type)
(f : forall p q, Q (eq_ex u v p q))
: forall p, Q p
:= fun p => rew <- eq_ex_eta p in f _ _.
Definition eq_ex_rec {A : Prop} {P : A -> Prop} {u v} (Q : u = v :> (exists a : A, P a) -> Set) := eq_ex_rect Q.
Definition eq_ex_ind {A : Prop} {P : A -> Prop} {u v} (Q : u = v :> (exists a : A, P a) -> Prop) := eq_ex_rec Q.
Definition eq_ex_rect {A : Prop} {P : A -> Prop} {u v : exists a : A, P a} (Q : u = v -> Type)
(f : forall p q, Q (eq_ex u v p q))
: forall p, Q p
:= fun p => rew <- eq_ex_eta p in f _ _.
Definition eq_ex_rec {A : Prop} {P : A -> Prop} {u v} (Q : u = v :> (exists a : A, P a) -> Set) := eq_ex_rect Q.
Definition eq_ex_ind {A : Prop} {P : A -> Prop} {u v} (Q : u = v :> (exists a : A, P a) -> Prop) := eq_ex_rec Q.
In order to have a performant inversion_sigma, we define
specialized versions for when we have constructors on one or
both sides of the equality
Definition eq_ex_rect_ex_intro_l {A : Prop} {P : A -> Prop} {u1 u2 v} (Q : _ -> Type)
(f : forall p q, Q (eq_ex_intro_l (P:=P) u1 u2 v p q))
: forall p, Q p
:= eq_ex_rect Q f.
Definition eq_ex_rect_ex_intro_r {A : Prop} {P : A -> Prop} {u v1 v2} (Q : _ -> Type)
(f : forall p q, Q (eq_ex_intro_r (P:=P) u v1 v2 p q))
: forall p, Q p
:= eq_ex_rect Q f.
Definition eq_ex_rect_ex_intro {A : Prop} {P : A -> Prop} {u1 u2 v1 v2} (Q : _ -> Type)
(f : forall p q, Q (@eq_ex_intro A P u1 v1 u2 v2 p q))
: forall p, Q p
:= eq_ex_rect Q f.
Definition eq_ex_rect_uncurried {A : Prop} {P : A -> Prop} {u v : exists a : A, P a} (Q : u = v -> Type)
(f : forall pq, Q (eq_ex u v (ex_proj1 pq) (ex_proj2 pq)))
: forall p, Q p
:= eq_ex_rect Q (fun p q => f (ex_intro _ p q)).
Definition eq_ex_rec_uncurried {A : Prop} {P : A -> Prop} {u v} (Q : u = v :> (exists a : A, P a) -> Set) := eq_ex_rect_uncurried Q.
Definition eq_ex_ind_uncurried {A : Prop} {P : A -> Prop} {u v} (Q : u = v :> (exists a : A, P a) -> Prop) := eq_ex_rec_uncurried Q.
(f : forall p q, Q (eq_ex_intro_l (P:=P) u1 u2 v p q))
: forall p, Q p
:= eq_ex_rect Q f.
Definition eq_ex_rect_ex_intro_r {A : Prop} {P : A -> Prop} {u v1 v2} (Q : _ -> Type)
(f : forall p q, Q (eq_ex_intro_r (P:=P) u v1 v2 p q))
: forall p, Q p
:= eq_ex_rect Q f.
Definition eq_ex_rect_ex_intro {A : Prop} {P : A -> Prop} {u1 u2 v1 v2} (Q : _ -> Type)
(f : forall p q, Q (@eq_ex_intro A P u1 v1 u2 v2 p q))
: forall p, Q p
:= eq_ex_rect Q f.
Definition eq_ex_rect_uncurried {A : Prop} {P : A -> Prop} {u v : exists a : A, P a} (Q : u = v -> Type)
(f : forall pq, Q (eq_ex u v (ex_proj1 pq) (ex_proj2 pq)))
: forall p, Q p
:= eq_ex_rect Q (fun p q => f (ex_intro _ p q)).
Definition eq_ex_rec_uncurried {A : Prop} {P : A -> Prop} {u v} (Q : u = v :> (exists a : A, P a) -> Set) := eq_ex_rect_uncurried Q.
Definition eq_ex_ind_uncurried {A : Prop} {P : A -> Prop} {u v} (Q : u = v :> (exists a : A, P a) -> Prop) := eq_ex_rec_uncurried Q.
Equality of ex when the property is an hProp
Definition eq_ex_hprop {A : Prop} {P : A -> Prop} (P_hprop : forall (x : A) (p q : P x), p = q)
(u v : exists a : A, P a)
(p : ex_proj1 u = ex_proj1 v)
: u = v
:= eq_ex u v p (P_hprop _ _ _).
Definition eq_ex_intro_hprop {A : Type} {P : A -> Prop} (P_hprop : forall (x : A) (p q : P x), p = q)
{u1 v1 : A} {u2 : P u1} {v2 : P v1}
(p : u1 = v1)
: ex_intro P u1 u2 = ex_intro P v1 v2
:= eq_ex_intro p (P_hprop _ _ _).
(u v : exists a : A, P a)
(p : ex_proj1 u = ex_proj1 v)
: u = v
:= eq_ex u v p (P_hprop _ _ _).
Definition eq_ex_intro_hprop {A : Type} {P : A -> Prop} (P_hprop : forall (x : A) (p q : P x), p = q)
{u1 v1 : A} {u2 : P u1} {v2 : P v1}
(p : u1 = v1)
: ex_intro P u1 u2 = ex_intro P v1 v2
:= eq_ex_intro p (P_hprop _ _ _).
Equivalence of equality of ex with a ex of equality We could actually prove an isomorphism here, and not just <->,
but for simplicity, we don't.
Definition eq_ex_uncurried_iff {A : Prop} {P : A -> Prop} (u v : exists a : A, P a)
: u = v <-> exists p : ex_proj1 u = ex_proj1 v, rew p in ex_proj2 u = ex_proj2 v.
: u = v <-> exists p : ex_proj1 u = ex_proj1 v, rew p in ex_proj2 u = ex_proj2 v.
Equivalence of equality of ex involving hProps with equality of the first components
Definition eq_ex_hprop_iff {A : Prop} {P : A -> Prop} (P_hprop : forall (x : A) (p q : P x), p = q)
(u v : exists a : A, P a)
: u = v <-> (ex_proj1 u = ex_proj1 v)
:= conj (fun p => f_equal (@ex_proj1 _ _) p) (eq_ex_hprop P_hprop u v).
Lemma rew_ex {A' : Type} {x} {P : A' -> Prop} (Q : forall a, P a -> Prop) (u : exists p : P x, Q x p) {y} (H : x = y)
: rew [fun a => exists p : P a, Q a p] H in u
= ex_intro
(Q y)
(rew H in ex_proj1 u)
(rew dependent H in ex_proj2 u).
End ex.
Global Arguments eq_ex_intro A P _ _ _ _ !p !q / .
Section ex2_Prop.
Variables (A:Prop) (P Q:A->Prop).
Definition ex2_rect (P0 : ex2 P Q -> Type) (f : forall x p q, P0 (ex_intro2 P Q x p q))
: forall e, P0 e
:= fun e => rew <- ex2_eta e in f _ _ _.
Definition ex2_rec : forall (P0 : ex2 P Q -> Set) (f : forall x p q, P0 (ex_intro2 P Q x p q)),
forall e, P0 e
:= ex2_rect.
End ex2_Prop.
(u v : exists a : A, P a)
: u = v <-> (ex_proj1 u = ex_proj1 v)
:= conj (fun p => f_equal (@ex_proj1 _ _) p) (eq_ex_hprop P_hprop u v).
Lemma rew_ex {A' : Type} {x} {P : A' -> Prop} (Q : forall a, P a -> Prop) (u : exists p : P x, Q x p) {y} (H : x = y)
: rew [fun a => exists p : P a, Q a p] H in u
= ex_intro
(Q y)
(rew H in ex_proj1 u)
(rew dependent H in ex_proj2 u).
End ex.
Global Arguments eq_ex_intro A P _ _ _ _ !p !q / .
Section ex2_Prop.
Variables (A:Prop) (P Q:A->Prop).
Definition ex2_rect (P0 : ex2 P Q -> Type) (f : forall x p q, P0 (ex_intro2 P Q x p q))
: forall e, P0 e
:= fun e => rew <- ex2_eta e in f _ _ _.
Definition ex2_rec : forall (P0 : ex2 P Q -> Set) (f : forall x p q, P0 (ex_intro2 P Q x p q)),
forall e, P0 e
:= ex2_rect.
End ex2_Prop.
Equality for ex2
Projecting an equality of a pair to equality of the first components
Definition ex_of_ex2_eq {A : Prop} {P Q : A -> Prop} {u v : exists2 a : A, P a & Q a} (p : u = v)
: u = v :> exists a : A, P a
:= f_equal _ p.
Definition ex_proj1_of_ex2_eq {A : Prop} {P Q : A -> Prop} {u v : exists2 a : A, P a & Q a} (p : u = v)
: ex_proj1 u = ex_proj1 v
:= ex_proj1_eq (ex_of_ex2_eq p).
: u = v :> exists a : A, P a
:= f_equal _ p.
Definition ex_proj1_of_ex2_eq {A : Prop} {P Q : A -> Prop} {u v : exists2 a : A, P a & Q a} (p : u = v)
: ex_proj1 u = ex_proj1 v
:= ex_proj1_eq (ex_of_ex2_eq p).
Projecting an equality of a pair to equality of the second components
Definition ex_proj2_of_ex2_eq {A : Prop} {P Q : A -> Prop} {u v : exists2 a : A, P a & Q a} (p : u = v)
: rew ex_proj1_of_ex2_eq p in ex_proj2 u = ex_proj2 v
:= rew dependent p in eq_refl.
: rew ex_proj1_of_ex2_eq p in ex_proj2 u = ex_proj2 v
:= rew dependent p in eq_refl.
Projecting an equality of a pair to equality of the third components
Definition ex_proj3_eq {A : Prop} {P Q : A -> Prop} {u v : exists2 a : A, P a & Q a} (p : u = v)
: rew ex_proj1_of_ex2_eq p in ex_proj3 u = ex_proj3 v
:= rew dependent p in eq_refl.
: rew ex_proj1_of_ex2_eq p in ex_proj3 u = ex_proj3 v
:= rew dependent p in eq_refl.
Equality of ex2 is itself a ex2 (fowards-reasoning version)
Definition eq_ex_intro2_uncurried {A : Type} {P Q : A -> Prop} {u1 v1 : A} {u2 : P u1} {v2 : P v1} {u3 : Q u1} {v3 : Q v1}
(pqr : exists2 p : u1 = v1, rew p in u2 = v2 & rew p in u3 = v3)
: ex_intro2 _ _ u1 u2 u3 = ex_intro2 _ _ v1 v2 v3.
(pqr : exists2 p : u1 = v1, rew p in u2 = v2 & rew p in u3 = v3)
: ex_intro2 _ _ u1 u2 u3 = ex_intro2 _ _ v1 v2 v3.
Equality of ex2 is itself a ex2 (backwards-reasoning version)
Definition eq_ex2_uncurried {A : Prop} {P Q : A -> Prop} (u v : exists2 a : A, P a & Q a)
(pqr : exists2 p : ex_proj1 u = ex_proj1 v,
rew p in ex_proj2 u = ex_proj2 v & rew p in ex_proj3 u = ex_proj3 v)
: u = v.
(pqr : exists2 p : ex_proj1 u = ex_proj1 v,
rew p in ex_proj2 u = ex_proj2 v & rew p in ex_proj3 u = ex_proj3 v)
: u = v.
Curried version of proving equality of ex types
Definition eq_ex2 {A : Prop} {P Q : A -> Prop} (u v : exists2 a : A, P a & Q a)
(p : ex_proj1 u = ex_proj1 v)
(q : rew p in ex_proj2 u = ex_proj2 v)
(r : rew p in ex_proj3 u = ex_proj3 v)
: u = v
:= eq_ex2_uncurried u v (ex_intro2 _ _ p q r).
Definition eq_ex_intro2 {A : Type} {P Q : A -> Prop} {u1 v1 : A} {u2 : P u1} {v2 : P v1} {u3 : Q u1} {v3 : Q v1}
(p : u1 = v1)
(q : rew p in u2 = v2)
(r : rew p in u3 = v3)
: ex_intro2 P Q u1 u2 u3 = ex_intro2 P Q v1 v2 v3
:= eq_ex_intro2_uncurried (ex_intro2 _ _ p q r).
(p : ex_proj1 u = ex_proj1 v)
(q : rew p in ex_proj2 u = ex_proj2 v)
(r : rew p in ex_proj3 u = ex_proj3 v)
: u = v
:= eq_ex2_uncurried u v (ex_intro2 _ _ p q r).
Definition eq_ex_intro2 {A : Type} {P Q : A -> Prop} {u1 v1 : A} {u2 : P u1} {v2 : P v1} {u3 : Q u1} {v3 : Q v1}
(p : u1 = v1)
(q : rew p in u2 = v2)
(r : rew p in u3 = v3)
: ex_intro2 P Q u1 u2 u3 = ex_intro2 P Q v1 v2 v3
:= eq_ex_intro2_uncurried (ex_intro2 _ _ p q r).
In order to have a performant inversion_sigma, we define
specialized versions for when we have constructors on one or
both sides of the equality
Definition eq_ex_intro2_l {A : Prop} {P Q : A -> Prop} u1 u2 u3 (v : exists2 a : A, P a & Q a)
(p : u1 = ex_proj1 v) (q : rew p in u2 = ex_proj2 v) (r : rew p in u3 = ex_proj3 v)
: ex_intro2 P Q u1 u2 u3 = v
:= eq_ex2 (ex_intro2 P Q u1 u2 u3) v p q r.
Definition eq_ex_intro2_r {A : Prop} {P Q : A -> Prop} (u : exists2 a : A, P a & Q a) v1 v2 v3
(p : ex_proj1 u = v1) (q : rew p in ex_proj2 u = v2) (r : rew p in ex_proj3 u = v3)
: u = ex_intro2 P Q v1 v2 v3
:= eq_ex2 u (ex_intro2 P Q v1 v2 v3) p q r.
(p : u1 = ex_proj1 v) (q : rew p in u2 = ex_proj2 v) (r : rew p in u3 = ex_proj3 v)
: ex_intro2 P Q u1 u2 u3 = v
:= eq_ex2 (ex_intro2 P Q u1 u2 u3) v p q r.
Definition eq_ex_intro2_r {A : Prop} {P Q : A -> Prop} (u : exists2 a : A, P a & Q a) v1 v2 v3
(p : ex_proj1 u = v1) (q : rew p in ex_proj2 u = v2) (r : rew p in ex_proj3 u = v3)
: u = ex_intro2 P Q v1 v2 v3
:= eq_ex2 u (ex_intro2 P Q v1 v2 v3) p q r.
Equality of ex2 when the second property is an hProp
Definition eq_ex2_hprop {A : Prop} {P Q : A -> Prop} (Q_hprop : forall (x : A) (p q : Q x), p = q)
(u v : exists2 a : A, P a & Q a)
(p : u = v :> exists a : A, P a)
: u = v
:= eq_ex2 u v (ex_proj1_eq p) (ex_proj2_eq p) (Q_hprop _ _ _).
Definition eq_ex_intro2_hprop_nondep {A : Type} {P : A -> Prop} {Q : Prop} (Q_hprop : forall (p q : Q), p = q)
{u1 v1 : A} {u2 : P u1} {v2 : P v1} {u3 v3 : Q}
(p : ex_intro _ u1 u2 = ex_intro _ v1 v2)
: ex_intro2 _ _ u1 u2 u3 = ex_intro2 _ _ v1 v2 v3
:= rew [fun v3 => _ = ex_intro2 _ _ _ _ v3] (Q_hprop u3 v3) in
f_equal (fun u => match u with ex_intro _ u1 u2 => ex_intro2 _ _ u1 u2 u3 end) p.
Definition eq_ex_intro2_hprop {A : Type} {P Q : A -> Prop}
(P_hprop : forall x (p q : P x), p = q)
(Q_hprop : forall x (p q : Q x), p = q)
{u1 v1 : A} {u2 : P u1} {v2 : P v1} {u3 : Q u1} {v3 : Q v1}
(p : u1 = v1)
: ex_intro2 P Q u1 u2 u3 = ex_intro2 P Q v1 v2 v3
:= eq_ex_intro2 p (P_hprop _ _ _) (Q_hprop _ _ _).
(u v : exists2 a : A, P a & Q a)
(p : u = v :> exists a : A, P a)
: u = v
:= eq_ex2 u v (ex_proj1_eq p) (ex_proj2_eq p) (Q_hprop _ _ _).
Definition eq_ex_intro2_hprop_nondep {A : Type} {P : A -> Prop} {Q : Prop} (Q_hprop : forall (p q : Q), p = q)
{u1 v1 : A} {u2 : P u1} {v2 : P v1} {u3 v3 : Q}
(p : ex_intro _ u1 u2 = ex_intro _ v1 v2)
: ex_intro2 _ _ u1 u2 u3 = ex_intro2 _ _ v1 v2 v3
:= rew [fun v3 => _ = ex_intro2 _ _ _ _ v3] (Q_hprop u3 v3) in
f_equal (fun u => match u with ex_intro _ u1 u2 => ex_intro2 _ _ u1 u2 u3 end) p.
Definition eq_ex_intro2_hprop {A : Type} {P Q : A -> Prop}
(P_hprop : forall x (p q : P x), p = q)
(Q_hprop : forall x (p q : Q x), p = q)
{u1 v1 : A} {u2 : P u1} {v2 : P v1} {u3 : Q u1} {v3 : Q v1}
(p : u1 = v1)
: ex_intro2 P Q u1 u2 u3 = ex_intro2 P Q v1 v2 v3
:= eq_ex_intro2 p (P_hprop _ _ _) (Q_hprop _ _ _).
Equivalence of equality of ex2 with a ex2 of equality We could actually prove an isomorphism here, and not just <->,
but for simplicity, we don't.
Definition eq_ex2_uncurried_iff {A : Prop} {P Q : A -> Prop} (u v : exists2 a : A, P a & Q a)
: u = v
<-> exists2 p : ex_proj1 u = ex_proj1 v,
rew p in ex_proj2 u = ex_proj2 v & rew p in ex_proj3 u = ex_proj3 v.
: u = v
<-> exists2 p : ex_proj1 u = ex_proj1 v,
rew p in ex_proj2 u = ex_proj2 v & rew p in ex_proj3 u = ex_proj3 v.
Induction principle for @eq (ex2 _ _)
Definition eq_ex2_eta {A : Prop} {P Q : A -> Prop} {u v : exists2 a : A, P a & Q a} (p : u = v)
: p = eq_ex2 u v (ex_proj1_of_ex2_eq p) (ex_proj2_of_ex2_eq p) (ex_proj3_eq p).
Definition eq_ex2_rect {A : Prop} {P Q : A -> Prop} {u v : exists2 a : A, P a & Q a} (R : u = v -> Type)
(f : forall p q r, R (eq_ex2 u v p q r))
: forall p, R p
:= fun p => rew <- eq_ex2_eta p in f _ _ _.
Definition eq_ex2_rec {A : Prop} {P Q : A -> Prop} {u v} (R : u = v :> (exists2 a : A, P a & Q a) -> Set) := eq_ex2_rect R.
Definition eq_ex2_ind {A : Prop} {P Q : A -> Prop} {u v} (R : u = v :> (exists2 a : A, P a & Q a) -> Prop) := eq_ex2_rec R.
: p = eq_ex2 u v (ex_proj1_of_ex2_eq p) (ex_proj2_of_ex2_eq p) (ex_proj3_eq p).
Definition eq_ex2_rect {A : Prop} {P Q : A -> Prop} {u v : exists2 a : A, P a & Q a} (R : u = v -> Type)
(f : forall p q r, R (eq_ex2 u v p q r))
: forall p, R p
:= fun p => rew <- eq_ex2_eta p in f _ _ _.
Definition eq_ex2_rec {A : Prop} {P Q : A -> Prop} {u v} (R : u = v :> (exists2 a : A, P a & Q a) -> Set) := eq_ex2_rect R.
Definition eq_ex2_ind {A : Prop} {P Q : A -> Prop} {u v} (R : u = v :> (exists2 a : A, P a & Q a) -> Prop) := eq_ex2_rec R.
In order to have a performant inversion_sigma, we define
specialized versions for when we have constructors on one or
both sides of the equality
Definition eq_ex2_rect_ex_intro2_l {A : Prop} {P Q : A -> Prop} {u1 u2 u3 v} (R : _ -> Type)
(f : forall p q r, R (eq_ex_intro2_l (P:=P) (Q:=Q) u1 u2 u3 v p q r))
: forall p, R p
:= eq_ex2_rect R f.
Definition eq_ex2_rect_ex_intro2_r {A : Prop} {P Q : A -> Prop} {u v1 v2 v3} (R : _ -> Type)
(f : forall p q r, R (eq_ex_intro2_r (P:=P) (Q:=Q) u v1 v2 v3 p q r))
: forall p, R p
:= eq_ex2_rect R f.
Definition eq_ex2_rect_ex_intro2 {A : Prop} {P Q : A -> Prop} {u1 u2 u3 v1 v2 v3} (R : _ -> Type)
(f : forall p q r, R (@eq_ex_intro2 A P Q u1 v1 u2 v2 u3 v3 p q r))
: forall p, R p
:= eq_ex2_rect R f.
Definition eq_ex2_rect_uncurried {A : Prop} {P Q : A -> Prop} {u v : exists2 a : A, P a & Q a} (R : u = v -> Type)
(f : forall pqr : exists2 p : _ = _, _ & _, R (eq_ex2 u v (ex_proj1 pqr) (ex_proj2 pqr) (ex_proj3 pqr)))
: forall p, R p
:= eq_ex2_rect R (fun p q r => f (ex_intro2 _ _ p q r)).
Definition eq_ex2_rec_uncurried {A : Prop} {P Q : A -> Prop} {u v} (R : u = v :> (exists2 a : A, P a & Q a) -> Set) := eq_ex2_rect_uncurried R.
Definition eq_ex2_ind_uncurried {A : Prop} {P Q : A -> Prop} {u v} (R : u = v :> (exists2 a : A, P a & Q a) -> Prop) := eq_ex2_rec_uncurried R.
(f : forall p q r, R (eq_ex_intro2_l (P:=P) (Q:=Q) u1 u2 u3 v p q r))
: forall p, R p
:= eq_ex2_rect R f.
Definition eq_ex2_rect_ex_intro2_r {A : Prop} {P Q : A -> Prop} {u v1 v2 v3} (R : _ -> Type)
(f : forall p q r, R (eq_ex_intro2_r (P:=P) (Q:=Q) u v1 v2 v3 p q r))
: forall p, R p
:= eq_ex2_rect R f.
Definition eq_ex2_rect_ex_intro2 {A : Prop} {P Q : A -> Prop} {u1 u2 u3 v1 v2 v3} (R : _ -> Type)
(f : forall p q r, R (@eq_ex_intro2 A P Q u1 v1 u2 v2 u3 v3 p q r))
: forall p, R p
:= eq_ex2_rect R f.
Definition eq_ex2_rect_uncurried {A : Prop} {P Q : A -> Prop} {u v : exists2 a : A, P a & Q a} (R : u = v -> Type)
(f : forall pqr : exists2 p : _ = _, _ & _, R (eq_ex2 u v (ex_proj1 pqr) (ex_proj2 pqr) (ex_proj3 pqr)))
: forall p, R p
:= eq_ex2_rect R (fun p q r => f (ex_intro2 _ _ p q r)).
Definition eq_ex2_rec_uncurried {A : Prop} {P Q : A -> Prop} {u v} (R : u = v :> (exists2 a : A, P a & Q a) -> Set) := eq_ex2_rect_uncurried R.
Definition eq_ex2_ind_uncurried {A : Prop} {P Q : A -> Prop} {u v} (R : u = v :> (exists2 a : A, P a & Q a) -> Prop) := eq_ex2_rec_uncurried R.
Equivalence of equality of ex2 involving hProps with equality of the first components
Definition eq_ex2_hprop_iff {A : Prop} {P Q : A -> Prop} (Q_hprop : forall (x : A) (p q : Q x), p = q)
(u v : exists2 a : A, P a & Q a)
: u = v <-> (u = v :> exists a : A, P a)
:= conj (fun p => f_equal (@ex_of_ex2 _ _ _) p) (eq_ex2_hprop Q_hprop u v).
(u v : exists2 a : A, P a & Q a)
: u = v <-> (u = v :> exists a : A, P a)
:= conj (fun p => f_equal (@ex_of_ex2 _ _ _) p) (eq_ex2_hprop Q_hprop u v).
Non-dependent classification of equality of ex
Definition eq_ex2_nondep {A : Prop} {B C : Prop} (u v : @ex2 A (fun _ => B) (fun _ => C))
(p : ex_proj1 u = ex_proj1 v) (q : ex_proj2 u = ex_proj2 v) (r : ex_proj3 u = ex_proj3 v)
: u = v
:= @eq_ex2 _ _ _ u v p (eq_trans (rew_const _ _) q) (eq_trans (rew_const _ _) r).
(p : ex_proj1 u = ex_proj1 v) (q : ex_proj2 u = ex_proj2 v) (r : ex_proj3 u = ex_proj3 v)
: u = v
:= @eq_ex2 _ _ _ u v p (eq_trans (rew_const _ _) q) (eq_trans (rew_const _ _) r).
Classification of transporting across an equality of ex2s
Lemma rew_ex2 {A' : Type} {x} {P : A' -> Prop} (Q R : forall a, P a -> Prop)
(u : exists2 p : P x, Q x p & R x p)
{y} (H : x = y)
: rew [fun a => exists2 p : P a, Q a p & R a p] H in u
= ex_intro2
(Q y)
(R y)
(rew H in ex_proj1 u)
(rew dependent H in ex_proj2 u)
(rew dependent H in ex_proj3 u).
End ex2.
Global Arguments eq_ex_intro2 A P Q _ _ _ _ _ _ !p !q !r / .
(u : exists2 p : P x, Q x p & R x p)
{y} (H : x = y)
: rew [fun a => exists2 p : P a, Q a p & R a p] H in u
= ex_intro2
(Q y)
(R y)
(rew H in ex_proj1 u)
(rew dependent H in ex_proj2 u)
(rew dependent H in ex_proj3 u).
End ex2.
Global Arguments eq_ex_intro2 A P Q _ _ _ _ _ _ !p !q !r / .