Library Coq.Init.Logic
Set Implicit Arguments.
Require Export Notations.
Require Import Ltac.
Notation "A -> B" := (
forall (
_ :
A),
B) :
type_scope.
Propositional connectives
True is the always true proposition
Inductive True :
Prop :=
I :
True.
Register True as core.True.type.
Register I as core.True.I.
False is the always false proposition
Inductive False :
Prop :=.
Register False as core.False.type.
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.
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
or A B, written A \/ B, is the disjunction of A and B
iff A B, written A <-> B, expresses the equivalence of A and B
Backward direction of the equivalences above does not need assumptions
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
ex P, or simply
exists x, P x, or also
exists x:A, P x,
expresses the existence of an
x of some type
A in
Set which
satisfies the predicate
P. This is existential quantification.
ex2 P Q, or simply
exists2 x, P x & Q x, or also
exists2 x:A, P x & Q x, expresses the existence of an
x of
type
A which satisfies both predicates
P and
Q.
Universal quantification is primitively written
forall x:A, Q. By
symmetry with existential quantification, the construction
all P
is provided too.
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
Equality
eq x y, or simply
x=y expresses the equality of
x and
y. Both
x and
y must belong to the same type
A.
The definition is inductive and states the reflexivity of the equality.
The others properties (symmetry, transitivity, replacement of
equals by equals) are proved below. The type of
x and
y can be
made explicit using the notation
x = y :> A. This is Leibniz equality
as it expresses that
x and
y are equal iff every property on
A which is true of
x is also true of
y
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 _.
Arguments eq_rec [
A]
x P _ y _.
Arguments eq_rect [
A]
x P _ y _.
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
Extra properties of equality
Basic definitions about relations and properties
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
The predicate
inhabited can be used in different contexts. If
A is
thought as a type,
inhabited A states that
A is inhabited. If
A is
thought as a computationally relevant proposition, then
inhabited A weakens
A so as to hide its computational meaning.
The so-weakened proof remains computationally relevant but only in
a propositional context.
Declaration of stepl and stepr for eq and iff
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
Equality for ex
Section ex.
Local Unset Implicit Arguments.
Projecting an equality of a pair to equality of the first components
Projecting an equality of a pair to equality of the second components
Equality of ex is itself a ex (forwards-reasoning version)
Equality of ex is itself a ex (backwards-reasoning version)
Curried version of proving equality of ex types
Curried version of proving equality of ex types
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
Induction principle for @eq (ex _)
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.
Equality of ex when the property is an 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.
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.
Equality for ex2
Section ex2.
Local Unset Implicit Arguments.
Projecting an equality of a pair to equality of the first components
Projecting an equality of a pair to equality of the second components
Projecting an equality of a pair to equality of the third components
Equality of ex2 is itself a ex2 (fowards-reasoning version)
Equality of ex2 is itself a ex2 (backwards-reasoning version)
Curried version of proving equality of ex types
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
Equality of ex2 when the second property is an 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.
Induction principle for @eq (ex2 _ _)
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.
Equivalence of equality of ex2 involving hProps with equality of the first components
Non-dependent classification of equality of ex
Classification of transporting across an equality of ex2s