Next:
Contents
Contents
User's manual of the library
Version 0.85
Christophe Raffalli
Contents
Propositionnal connective.
Conjunction.
Disjunction.
Propositional constants and negation.
Existential quantifiers.
Equality.
Some tautologies.
Classical logic.
Definite description.
Contraposition.
De Morgan Laws.
Usual definitions on binary relations.
Properties of basic operations and predicates on the booleans.
Basic definitions.
The introduction rules for I B.
Elimination rules for I B.
Left rules for I B.
Boolean equality.
Definition of functions on booleans.
if ... then ... else ...
Boolean functions.
Basic definitions.
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.
Basic definitions
The introduction rule for ×
The elimination rules for ×
Projections
Definitions
Very basic facts
Lexicographic ordering
Basic definitions
Matching
Basic definitions and properties
Definitions and axioms
Rules on lists
Introduction rules
Elimination rules
Left rules (eliminating list constructors)
Decidability of equality
Defining functions by induction on lists
Definition
Application : operations on lists
The append function
The map functional
Head and tail of a list as partial functions
Definitions
Basic facts
Quantifiers bounded on lists.
Existence in a list
Definition
Introduction rules
Elimination rules
Existence in append
Universal quantifer bounded on a list
Membership in a list
Introduction rules
Elimination rules
Membership in append
Basic definitions
Compatible fonctions
About this document ...
Christophe Raffalli 2005-03-02