Require command.| Logic | Classical logic and dependent equality |
| Bool | Booleans (basic functions and results) |
| Arith | Basic Peano arithmetic |
| Zarith | Basic integer arithmetic |
| Reals | Axiomatization of Real Numbers (classical, basic functions and results, integer part and fractional part, requires the Zarith library). |
| Lists | Monomorphic and polymorphic lists (basic functions and results), Streams (infinite sequences defined with co-inductive types) |
| Sets | Sets (classical, constructive, finite, infinite, power set, etc.) |
| Relations | Relations (definitions and basic results). |
| Wellfounded | Well-founded relations (basic results). |
| IntMap | Representation of finite sets by an efficient structure of map (trees indexed by binary integers). |
<tms@dcs.ed.ac.uk> in Lego
adapted to Coq by B. Barras
Credit: Proofs up to K_dec follows an outline by Michael Hedberg
let induction_ltof1 F a = indrec ((f a)+1) a
where rec indrec =
function 0 -> (function a -> error)
|(S m) -> (function a -> (F a (function y -> indrec y m)));;
the ML-like program for induction_ltof2 is :
let induction_ltof2 F a = indrec a where rec indrec a = F a indrec;;
(n:nat)(Q n)==(n:nat)(P (inject_nat n)) ===> (x:Z)`x > 0) -> (P x)
/\
||
||
(Q O) (n:nat)(Q n)->(Q (S n)) <=== (P 0) (x:Z) (P x) -> (P (Zs x))
<=== (inject_nat (S n))=(Zs (inject_nat n))
<=== inject_nat_complete
Then the diagram will be closed and the theorem proved.
This document was translated from LATEX by HEVEA.