User's manual of the library
Version 0.85

• 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 ...