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