3.1 The basic library
This section lists the basic notions and results which are directly available in the standard Coq system (These constructions are defined in the Prelude module in directory theories/INIT at the Coq root directory; this includes the modules Logic, Datatypes, Specif, Peano, and Wf plus the module Logic_Type).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 (This syntax is defined in module LogicSyntax) 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] : PropCoq < := 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] : PropCoq < := 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 ommited when A can be synthetised by the system.
Equality
Then, we find equality, defined as an inductive relation. That is, given aSet 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->PropCoq < := 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 definition(They are in Datatypes.v) of the basic data-types of programming, again defined as inductive constructions over the sortSet. 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] : SetCoq < := 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 notions(They are defined in module Specif.v) allows to build new datatypes and specifications. They are available with the syntax shown on figure 3.1.3(This syntax can be found in the module SpecifSyntax.v).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] : SetCoq < := exist : (x:A)(P x) -> (sig A P).Coq < Inductive sig2 [A:Set;P,Q:A->Prop] : SetCoq < := 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] : SetCoq < := 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] : SetCoq < := 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] : SetCoq < := 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] : SetCoq < := 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:Syntax of datatypes and specifications
We may define variants of the axiom of choice, like in Martin-Lof'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 multiplication(This is in module Peano.v).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->PropCoq < := [n:nat](<Prop>Cases n of O => FalseCoq < | (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 -> PropCoq < := 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 induction(This is defined in module Wf.v).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 definitions(This is in module Logic_Type.v) of logical quantifiers axiomatized at theType 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] : PropCoq < := exT_intro : (x:A)(P x)->(exT A P).Coq < Coq < Inductive exT2 [A:Type;P,Q:A->Prop] : PropCoq < := 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 -> PropCoq < := 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 (This syntax is defined in module Logic_TypeSyntax)
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).