3.1 The basic library
This section lists the basic notions and results which are directly
available in the standard Coq system
1.
3.1.1 Logic
The basic library of Coq comes with the definitions of standard
(intuitionistic) logical connectives (they are defined as inductive
constructions). They are equipped with an appealing syntax enriching the
(subclass form) of the syntactic class term. The syntax
extension
2
is shown on figure 3.1.1.
form |
::= |
True |
(True) |
|
| |
False |
(False) |
|
| |
~ form |
(not) |
|
| |
form /\ form |
(and) |
|
| |
form \/ form |
(or) |
|
| |
form -> form |
(primitive implication) |
|
| |
form <-> form |
(iff) |
|
| |
( ident : type )
form |
(primitive for all) |
|
| |
( ALL ident [: specif] |
form ) |
(all) |
|
| |
( EX ident [: specif] | form ) |
(ex) |
|
| |
( EX ident [: specif] | form & form ) |
(ex2) |
|
| |
term = term |
(eq) |
Remark: The implication is not defined but primitive
(it is a non-dependent product of a proposition over another proposition).
There is also a primitive universal quantification (it is a
dependent product over a proposition). The primitive universal
quantification allows both first-order and higher-order
quantification. There is no need to
use the notation ( ALL ident [: specif] | form ) propositions), except to have a notation dual of
the notation for first-order existential quantification.
Figure 3.1: Syntax of formulas
Propositional Connectives
First, we find propositional calculus connectives:
Coq < Inductive True : Prop := I : True.
Coq < Inductive False : Prop := .
Coq < Definition not := [A:Prop] A->False.
Coq < Inductive and [A,B:Prop] : Prop := conj : A -> B -> A/\B.
Coq < Section Projections.
Coq < Variables A,B : Prop.
Coq < Theorem proj1 : A/\B -> A.
Coq < Theorem proj2 : A/\B -> B.
Coq < End Projections.
Coq < Inductive or [A,B:Prop] : Prop
Coq < := or_introl : A -> A\/B
Coq < | or_intror : B -> A\/B.
Coq < Definition iff := [P,Q:Prop] (P->Q) /\ (Q->P).
Coq < Definition IF := [P,Q,R:Prop] (P/\Q) \/ (~P/\R).
Quantifiers
Then we find first-order quantifiers:
Coq < Definition all := [A:Set][P:A->Prop](x:A)(P x).
Coq < Inductive ex [A:Set;P:A->Prop] : Prop
Coq < := ex_intro : (x:A)(P x)->(ex A P).
Coq < Inductive ex2 [A:Set;P,Q:A->Prop] : Prop
Coq < := ex_intro2 : (x:A)(P x)->(Q x)->(ex2 A P Q).
The following abbreviations are allowed:
(ALL x:A | P) |
(all A [x:A]P) |
(ALL x | P) |
(all A [x:A]P) |
(EX x:A | P) |
(ex A [x:A]P) |
(EX x | P) |
(ex A [x:A]P) |
(EX x:A | P & Q) |
(ex2 A [x:A]P [x:A]Q) |
(EX x | P & Q) |
(ex2 A [x:A]P [x:A]Q) |
The type annotation :A can be omitted when A can be
synthesized by the system.
Equality
Then, we find equality, defined as an inductive relation. That is,
given a Set
A
and an x
of type A
, the
predicate (eq A x)
is the smallest which contains x
.
This definition, due to Christine Paulin-Mohring, is equivalent to
define eq
as the smallest reflexive relation, and it is also
equivalent to Leibniz' equality.
Coq < Inductive eq [A:Set;x:A] : A->Prop
Coq < := refl_equal : (eq A x x).
Lemmas
Finally, a few easy lemmas are provided.
Coq < Theorem absurd : (A:Prop)(C:Prop) A -> ~A -> C.
Coq < Section equality.
Coq < Variable A,B : Set.
Coq < Variable f : A->B.
Coq < Variable x,y,z : A.
Coq < Theorem sym_equal : x=y -> y=x.
Coq < Theorem trans_equal : x=y -> y=z -> x=z.
Coq < Theorem f_equal : x=y -> (f x)=(f y).
Coq < Theorem sym_not_equal : ~(x=y) -> ~(y=x).
Coq < End equality.
Coq < Definition eq_ind_r : (A:Set)(x:A)(P:A->Prop)(P x)->(y:A)y=x->(P y).
Coq < Definition eq_rec_r : (A:Set)(x:A)(P:A->Set)(P x)->(y:A)y=x->(P y).
Coq < Immediate sym_equal sym_not_equal.
3.1.2 Datatypes
In the basic library, we find the definition3
of the basic data-types of programming,
again defined as inductive constructions over the sort
Set
. Some of them come with a special syntax shown on figure
3.1.3.
Programming
Coq < Inductive unit : Set := tt : unit.
Coq < Inductive bool : Set := true : bool
Coq < | false : bool.
Coq < Inductive nat : Set := O : nat
Coq < | S : nat->nat.
Note that zero is the letter O
, and not the numeral
0
.
We then define the disjoint sum of A+B
of two sets A
and
B
, and their product A*B
.
Coq < Inductive sum [A,B:Set] : Set
Coq < := inl : A -> A+B
Coq < | inr : B -> A+B.
Coq < Inductive prod [A,B:Set] : Set := pair : A -> B -> A*B.
Coq < Section projections.
Coq < Variables A,B:Set.
Coq < Definition fst := [H:A*B] Cases H of (x,y) => x end.
Coq < Definition snd := [H:A*B] Cases H of (x,y) => y end.
Coq < End projections.
Coq < Syntactic Definition Fst := (fst ? ?).
Coq < Syntactic Definition Snd := (snd ? ?).
3.1.3 Specification
The following notions4 allows to build new datatypes and specifications.
They are available with the syntax shown on
figure 3.1.35.
For instance, given A:Set
and P:A->Prop
, the construct
{x:A | (P x)}
(in abstract syntax (sig A P)
) is a
Set
. We may build elements of this set as (exist x p)
whenever we have a witness x:A
with its justification
p:(P x)
.
From such a (exist x p)
we may in turn extract its witness
x:A
(using an elimination construct such as Cases
) but
not its justification, which stays hidden, like in an abstract
data type. In technical terms, one says that sig
is a ``weak
(dependent) sum''. A variant sig2
with two predicates is also
provided.
Coq < Inductive sig [A:Set;P:A->Prop] : Set
Coq < := exist : (x:A)(P x) -> (sig A P).
Coq < Inductive sig2 [A:Set;P,Q:A->Prop] : Set
Coq < := exist2 : (x:A)(P x) -> (Q x) -> (sig2 A P Q).
A ``strong (dependent) sum'' {x:A & (P x)}
may be also defined,
when the predicate P
is now defined as a Set
constructor.
Coq < Inductive sigS [A:Set;P:A->Set] : Set
Coq < := existS : (x:A)(P x) -> (sigS A P).
Coq < Section projections.
Coq < Variable A:Set.
Coq < Variable P:A->Set.
Coq < Definition projS1 := [H:(sigS A P)] let (x,h) = H in x.
Coq < Definition projS2 := [H:(sigS A P)]<[H:(sigS A P)](P (projS1 H))>
Coq < let (x,h) = H in h.
Coq < End projections.
Coq < Inductive sigS2 [A:Set;P,Q:A->Set] : Set
Coq < := existS2 : (x:A)(P x) -> (Q x) -> (sigS2 A P Q).
A related non-dependent construct is the constructive sum
{A}+{B}
of two propositions A
and B
.
Coq < Inductive sumbool [A,B:Prop] : Set
Coq < := left : A -> ({A}+{B})
Coq < | right : B -> ({A}+{B}).
This sumbool
construct may be used as a kind of indexed boolean
data type. An intermediate between sumbool
and sum
is
the mixed sumor
which combines A:Set
and B:Prop
in the Set
A+{B}
.
Coq < Inductive sumor [A:Set;B:Prop] : Set
Coq < := inleft : A -> (A+{B})
Coq < | inright : B -> (A+{B}).
specif |
::= |
specif * specif |
(prod) |
|
| |
specif + specif |
(sum) |
|
| |
specif + { specif } |
(sumor) |
|
| |
{ specif } + { specif } |
(sumbool) |
|
| |
{ ident : specif | form } |
(sig) |
|
| |
{ ident : specif | form &
form } |
(sig2) |
|
| |
{ ident : specif & specif } |
(sigS) |
|
| |
{ ident : specif & specif & specif } |
(sigS2) |
|
|
|
|
term |
::= |
( term , term ) |
(pair) |
Figure 3.2:
We may define variants of the axiom of choice, like in Martin-Löf's
Intuitionistic Type Theory.
Coq < Lemma Choice : (S,S':Set)(R:S->S'->Prop)((x:S){y:S'|(R x y)})
Coq < -> {f:S->S'|(z:S)(R z (f z))}.
Coq < Lemma Choice2 : (S,S':Set)(R:S->S'->Set)((x:S){y:S' & (R x y)})
Coq < -> {f:S->S' & (z:S)(R z (f z))}.
Coq < Lemma bool_choice : (S:Set)(R1,R2:S->Prop)((x:S){(R1 x)}+{(R2 x)}) ->
Coq < {f:S->bool | (x:S)( ((f x)=true /\ (R1 x))
Coq < \/ ((f x)=false /\ (R2 x)))}.
The next construct builds a sum between a data type A:Set
and
an exceptional value encoding errors:
Coq < Inductive Exc [A:Set] : Set := value : A->(Exc A)
Coq < | error : (Exc A).
This module ends with one axiom and theorems,
relating the sorts Set
and
Prop
in a way which is consistent with the realizability
interpretation.
Coq < Axiom False_rec : (P:Set)False->P.
Coq < Definition except := False_rec.
Coq < Syntactic Definition Except := (except ?).
Coq < Theorem absurd_set : (A:Prop)(C:Set)A->(~A)->C.
Coq < Theorem and_rec : (A,B:Prop)(C:Set)(A->B->C)->(A/\B)->C.
3.1.4 Basic Arithmetics
The basic library includes a few elementary properties of natural numbers,
together with the definitions of predecessor, addition and
multiplication6.
Coq < Theorem eq_S : (n,m:nat) n=m -> (S n)=(S m).
Coq < Definition pred : nat->nat
Coq < := [n:nat](<nat>Cases n of O => O
Coq < | (S u) => u end).
Coq < Theorem pred_Sn : (m:nat) m=(pred (S m)).
Coq < Theorem eq_add_S : (n,m:nat) (S n)=(S m) -> n=m.
Coq < Immediate eq_add_S.
Coq < Theorem not_eq_S : (n,m:nat) ~(n=m) -> ~((S n)=(S m)).
Coq < Definition IsSucc : nat->Prop
Coq < := [n:nat](<Prop>Cases n of O => False
Coq < | (S p) => True end).
Coq < Theorem O_S : (n:nat) ~(O=(S n)).
Coq < Theorem n_Sn : (n:nat) ~(n=(S n)).
Coq < Fixpoint plus [n:nat] : nat -> nat :=
Coq < [m:nat](<nat>Cases n of
Coq < O => m
Coq < | (S p) => (S (plus p m)) end).
Coq < Lemma plus_n_O : (n:nat) n=(plus n O).
Coq < Lemma plus_n_Sm : (n,m:nat) (S (plus n m))=(plus n (S m)).
Coq < Fixpoint mult [n:nat] : nat -> nat :=
Coq < [m:nat](<nat> Cases n of O => O
Coq < | (S p) => (plus m (mult p m)) end).
Coq < Lemma mult_n_O : (n:nat) O=(mult n O).
Coq < Lemma mult_n_Sm : (n,m:nat) (plus (mult n m) n)=(mult n (S m)).
Finally, it gives the definition of the usual orderings le
,
lt
, ge
, and gt
.
Coq < Inductive le [n:nat] : nat -> Prop
Coq < := le_n : (le n n)
Coq < | le_S : (m:nat)(le n m)->(le n (S m)).
Coq < Definition lt := [n,m:nat](le (S n) m).
Coq < Definition ge := [n,m:nat](le m n).
Coq < Definition gt := [n,m:nat](lt m n).
Properties of these relations are not initially known, but may be
required by the user from modules Le
and Lt
. Finally,
Peano
gives some lemmas allowing pattern-matching, and a double
induction principle.
Coq < Theorem nat_case : (n:nat)(P:nat->Prop)(P O)->((m:nat)(P (S m)))->(P n).
Coq < Theorem nat_double_ind : (R:nat->nat->Prop)
Coq < ((n:nat)(R O n)) -> ((n:nat)(R (S n) O))
Coq < -> ((n,m:nat)(R n m)->(R (S n) (S m)))
Coq < -> (n,m:nat)(R n m).
3.1.5 Well-founded recursion
The basic library contains the basics of well-founded recursion and
well-founded induction7.
Coq < Chapter Well_founded.
Coq < Variable A : Set.
Coq < Variable R : A -> A -> Prop.
Coq < Inductive Acc : A -> Prop
Coq < := Acc_intro : (x:A)((y:A)(R y x)->(Acc y))->(Acc x).
Coq < Lemma Acc_inv : (x:A)(Acc x) -> (y:A)(R y x) -> (Acc y).
Coq < Section AccRec.
Coq < Variable P : A -> Set.
Coq < Variable F : (x:A)((y:A)(R y x)->(Acc y))->((y:A)(R y x)->(P y))->(P x).
Coq < Fixpoint Acc_rec [x:A;a:(Acc x)] : (P x)
Coq < := (F x (Acc_inv x a) [y:A][h:(R y x)](Acc_rec y (Acc_inv x a y h))).
Coq < End AccRec.
Coq < Definition well_founded := (a:A)(Acc a).
Coq < Theorem well_founded_induction :
Coq < well_founded ->
Coq < (P:A->Set)((x:A)((y:A)(R y x)->(P y))->(P x))->(a:A)(P a).
Coq < End Well_founded.
Coq < Section Wf_inductor.
Coq < Variable A:Set.
Coq < Variable R:A->A->Prop.
Coq < Theorem well_founded_ind :
Coq < (well_founded A R) ->
Coq < (P:A->Prop)((x:A)((y:A)(R y x)->(P y))->(P x))->(a:A)(P a).
Coq < End Wf_inductor.
3.1.6 Accessing the Type level
The basic library includes the definitions8 of logical quantifiers axiomatized at the
Type
level.
Coq < Definition allT := [A:Type][P:A->Prop](x:A)(P x).
Coq <
Coq < Section universal_quantification.
Coq < Variable A : Type.
Coq < Variable P : A->Prop.
Coq < Theorem inst : (x:A)(ALLT x | (P x))->(P x).
Coq < Theorem gen : (B:Prop)(f:(y:A)B->(P y))B->(allT ? P).
Coq < End universal_quantification.
Coq < Inductive exT [A:Type;P:A->Prop] : Prop
Coq < := exT_intro : (x:A)(P x)->(exT A P).
Coq <
Coq < Inductive exT2 [A:Type;P,Q:A->Prop] : Prop
Coq < := exT_intro2 : (x:A)(P x)->(Q x)->(exT2 A P Q).
It defines also Leibniz equality x==y
when x
and
y
belong to A:Type
.
Coq < Inductive eqT [A:Type;x:A] : A -> Prop
Coq < := refl_eqT : (eqT A x x).
Coq < Section Equality_is_a_congruence.
Coq < Variables A,B : Type.
Coq < Variable f : A->B.
Coq < Variable x,y,z : A.
Coq < Lemma sym_eqT : (x==y) -> (y==x).
Coq < Lemma trans_eqT : (x==y) -> (y==z) -> (x==z).
Coq < Lemma congr_eqT : (x==y)->((f x)==(f y)).
Coq < End Equality_is_a_congruence.
Coq < Immediate sym_eqT sym_not_eqT.
Coq < Definition eqT_ind_r: (A:Type)(x:A)(P:A->Prop)(P x)->(y:A)y==x -> (P y).
The figure 3.1.6 presents the syntactic notations
corresponding to the main definitions
9
form |
::= |
( ALLT ident [: specif] |
form ) |
(allT) |
|
| |
( EXT ident [: specif] | form ) |
(exT) |
|
| |
( EXT ident [: specif] | form & form ) |
(exT2) |
|
| |
term == term |
(eqT) |
Figure 3.3: Syntax of first-order formulas in the type universe
At the end, it defines datatypes at the Type level.
Coq < Inductive EmptyT: Type :=.
Coq < Inductive UnitT : Type := IT : UnitT.
Coq < Definition notT := [A:Type] A->EmptyT.
Coq <
Coq < Inductive identityT [A:Type; a:A] : A->Type :=
Coq < refl_identityT : (identityT A a a).