User's manual of the library
Propositional constants and negation.
De Morgan Laws.
Usual definitions on binary relations.
Properties of basic operations and predicates on the booleans.
The introduction rules for I B.
Elimination rules for I B.
Left rules for I B.
Definition of functions on booleans.
if ... then ... else ...
Introduction rules for I N.
Elimination rules for I N.
Induction on natural number as an elimination rule.
Elimination by case on I N.
left rules for = on I N
Properties of basic operations and predicates on the product.
The introduction rule for ×
The elimination rules for ×
Very basic facts
Basic definitions and properties
Definitions and axioms
Rules on lists
Left rules (eliminating list constructors)
Decidability of equality
Defining functions by induction on lists
Application : operations on lists
The append function
The map functional
Head and tail of a list as partial functions
Quantifiers bounded on lists.
Existence in a list
Existence in append
Universal quantifer bounded on a list
Membership in a list
Membership in append
About this document ...
Christophe Raffalli 2005-03-02