Library Coq.Init.Logic
Set Implicit Arguments.
Require Export Notations.
Notation "A -> B" := (forall (_ : A), B) : type_scope.
False is the always false proposition
not A, written ~A, is the negation of A
Create the "core" hint database, and set its transparent state for
variables and constants explicitely.
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.
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.
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.
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.
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).
(IF_then_else P Q R), written IF P then Q else R denotes
either P and Q, or ~P and R
Definition IF_then_else (P Q R:Prop) := P /\ Q \/ ~ P /\ R.
Notation "'IF' c1 'then' c2 'else' c3" := (IF_then_else c1 c2 c3)
(at level 200, right associativity) : type_scope.
First-order quantifiers
Inductive ex (A:Type) (P:A -> Prop) : Prop :=
ex_intro : forall x:A, P x -> ex (A:=A) P.
Inductive ex2 (A:Type) (P Q:A -> Prop) : Prop :=
ex_intro2 : forall x:A, P x -> Q x -> ex2 (A:=A) P Q.
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 ident, 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 ident, 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.
Notation "x = y" := (x = y :>_) : type_scope.
Notation "x <> y :> T" := (~ x = y :>T) : type_scope.
Notation "x <> y" := (x <> y :>_) : type_scope.
Hint Resolve I conj or_introl or_intror : core.
Hint Resolve eq_refl: core.
Hint Resolve ex_intro ex_intro2: core.
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.
Theorem eq_trans : x = y -> y = z -> x = z.
Theorem eq_trans_r : x = y -> z = y -> x = z.
Theorem f_equal : x = y -> f x = f y.
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.
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).
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 : forall (H: x = y), rew H in f x = f y.
End equality_dep.
Section equality_dep2.
Variable A A' : Type.
Variable B : A -> Type.
Variable B' : A' -> Type.
Variable f : A -> A'.
Variable g : forall a:A, B a -> B' (f a).
Variables x y : A.
Lemma f_equal_dep2 : forall {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.
End equality_dep2.
Lemma rew_opp_r : forall 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 : forall 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.
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 : forall 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 : forall A (x y:A) (e:x=y), eq_trans eq_refl e = e.
Theorem eq_trans_refl_r : forall A (x y:A) (e:x=y), eq_trans e eq_refl = e.
Theorem eq_sym_involutive : forall A (x y:A) (e:x=y), eq_sym (eq_sym e) = e.
Theorem eq_trans_sym_inv_l : forall A (x y:A) (e:x=y), eq_trans (eq_sym e) e = eq_refl.
Theorem eq_trans_sym_inv_r : forall A (x y:A) (e:x=y), eq_trans e (eq_sym e) = eq_refl.
Theorem eq_trans_assoc : forall 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 : forall 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 : forall {A B} {x1 x2 x3:A} {y1:B x1} {y2:B x2} {y3:B x3},
forall (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 : forall {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 : forall {A B} {P:A->Type} {Q:B->Type} (f:A->B) (g : forall x, P x -> Q (f x)),
forall {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 : forall 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 : forall 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 : forall A (f:A->A) (Hf:forall a, a = f a), forall a, f_equal f (Hf a) = Hf (f a).
Theorem eq_id_comm_r : forall A (f:A->A) (Hf:forall a, f a = a), forall a, f_equal f (Hf a) = Hf (f a).
Lemma eq_refl_map_distr : forall A B x (f:A->B), f_equal f (eq_refl x) = eq_refl (f x).
Lemma eq_trans_map_distr : forall 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 : forall 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 : forall 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 : forall 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 : forall 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).
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.
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.
Equality for ex
Section ex.
Local Unset Implicit Arguments.
Definition eq_ex_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 P u1 u2 = ex_intro P v1 v2.
Definition eq_ex {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 P u1 u2 = ex_intro P v1 v2
:= eq_ex_uncurried P (ex_intro _ p q).
Definition eq_ex_hprop {A} {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 u1 v1 u2 v2 p (P_hprop _ _ _).
Lemma rew_ex {A x} {P : A -> Type} (Q : forall a, P a -> Prop) (u : exists p, Q x p) {y} (H : x = y)
: rew [fun a => exists p, Q a p] H in u
= match u with
| ex_intro _ u1 u2
=> ex_intro
(Q y)
(rew H in u1)
(rew dependent H in u2)
end.
End ex.
Local Unset Implicit Arguments.
Definition eq_ex_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 P u1 u2 = ex_intro P v1 v2.
Definition eq_ex {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 P u1 u2 = ex_intro P v1 v2
:= eq_ex_uncurried P (ex_intro _ p q).
Definition eq_ex_hprop {A} {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 u1 v1 u2 v2 p (P_hprop _ _ _).
Lemma rew_ex {A x} {P : A -> Type} (Q : forall a, P a -> Prop) (u : exists p, Q x p) {y} (H : x = y)
: rew [fun a => exists p, Q a p] H in u
= match u with
| ex_intro _ u1 u2
=> ex_intro
(Q y)
(rew H in u1)
(rew dependent H in u2)
end.
End ex.
Equality for ex2
Section ex2.
Local Unset Implicit Arguments.
Definition eq_ex2_uncurried {A : Type} (P Q : A -> Prop) {u1 v1 : A}
{u2 : P u1} {v2 : P v1}
{u3 : Q u1} {v3 : Q v1}
(pq : exists2 p : u1 = v1, rew p in u2 = v2 & rew p in u3 = v3)
: ex_intro2 P Q u1 u2 u3 = ex_intro2 P Q v1 v2 v3.
Definition eq_ex2 {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_ex2_uncurried P Q (ex_intro2 _ _ p q r).
Definition eq_ex2_hprop {A} {P Q : A -> Prop}
(P_hprop : forall (x : A) (p q : P x), p = q)
(Q_hprop : forall (x : A) (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_ex2 u1 v1 u2 v2 u3 v3 p (P_hprop _ _ _) (Q_hprop _ _ _).
Lemma rew_ex2 {A x} {P : A -> Type}
(Q : forall a, P a -> Prop)
(R : forall a, P a -> Prop)
(u : exists2 p, Q x p & R x p) {y} (H : x = y)
: rew [fun a => exists2 p, Q a p & R a p] H in u
= match u with
| ex_intro2 _ _ u1 u2 u3
=> ex_intro2
(Q y)
(R y)
(rew H in u1)
(rew dependent H in u2)
(rew dependent H in u3)
end.
End ex2.
Local Unset Implicit Arguments.
Definition eq_ex2_uncurried {A : Type} (P Q : A -> Prop) {u1 v1 : A}
{u2 : P u1} {v2 : P v1}
{u3 : Q u1} {v3 : Q v1}
(pq : exists2 p : u1 = v1, rew p in u2 = v2 & rew p in u3 = v3)
: ex_intro2 P Q u1 u2 u3 = ex_intro2 P Q v1 v2 v3.
Definition eq_ex2 {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_ex2_uncurried P Q (ex_intro2 _ _ p q r).
Definition eq_ex2_hprop {A} {P Q : A -> Prop}
(P_hprop : forall (x : A) (p q : P x), p = q)
(Q_hprop : forall (x : A) (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_ex2 u1 v1 u2 v2 u3 v3 p (P_hprop _ _ _) (Q_hprop _ _ _).
Lemma rew_ex2 {A x} {P : A -> Type}
(Q : forall a, P a -> Prop)
(R : forall a, P a -> Prop)
(u : exists2 p, Q x p & R x p) {y} (H : x = y)
: rew [fun a => exists2 p, Q a p & R a p] H in u
= match u with
| ex_intro2 _ _ u1 u2 u3
=> ex_intro2
(Q y)
(R y)
(rew H in u1)
(rew dependent H in u2)
(rew dependent H in u3)
end.
End ex2.