Final theorem (correctness of the Sieve of Eratosthenes)

example/arith/Makefile

@@ -5,7 +5,9 @@ FCL_FILES=$(wildcard *.fcl)
 V_FILES=$(wildcard *.v)
 ART_FILES=natural.art natural-order-thm.art natural-funpow-thm.art natural-divides.art natural-prime-def.art natural-prime-thm.art
 
-all: $(FCL_FILES:.fcl=.dko) $(V_FILES:.v=.dko)
+all: $(FCL_FILES:.fcl=.dko) $(V_FILES:.v=.dko) final.dko
+
+final.dko: final_coll.dko
 
 HolNaturals.art: $(ART_FILES)
 	cat $^ > $@

example/arith/final_coll.fcl

+open "basics";;
+open "naturals";;
+open "natmorph";;
+open "natural_hol";;
+open "natural_coq";;
+
+species Final (B is HolNatPrime) =
+  inherit CoqMorph(B);
+
+  theorem le_refl1 : all m n : Self, m = n -> le(m, n)
+  proof =
+  <1>1 assume m n : Self,
+       hypothesis H : m = n,
+       prove le(m, n)
+       <2>1 prove B!le(morph(m), morph(m))
+            by property B!le_refl
+       <2>2 prove B!le(morph(m), morph(n))
+            by step <2>1 hypothesis H
+       <2>3 qed by step <2>2 property morph_le_rev
+  <1>f conclude;
+
+  theorem le_refl2 : all n m : Self, n = m -> le(m, n)
+  proof =
+  <1>1 assume n m : Self,
+       hypothesis H : n = m,
+       prove le(m, n)
+       <2>1 prove B!le(morph(m), morph(m))
+            by property B!le_refl
+       <2>2 prove B!le(morph(m), morph(n))
+            by step <2>1 hypothesis H
+       <2>3 qed by step <2>2 property morph_le_rev
+  <1>f conclude;
+end;;
+
+collection FinalColl = implement Final(HolNatPrimeDivColl); end;;

example/arith/natural_coq.fcl

@@ -262,4 +262,25 @@ species CoqMorph (B is NatPrimeDiv) =
     definition of morph, succ
     {* (n : (hol.term coq_nat__t) =>
         hol.REFL _p_B_T (abst_morph (abst_succ n))). *};
+
+  let one = succ(zero);
+  proof of one_spec = by definition of one;
+
+  logical let lt (m : Self, n : Self) = le(succ(m), n);
+  proof of lt_spec = by definition of lt;
+
+  logical let divides (m : Self, n : Self) = ex p : Self, times(m, p) = n;
+  proof of divides_times = by definition of divides;
+
+  logical let sd (m : Self, n : Self) = divides(m, n) /\ lt(one, m) /\ lt(m, n);
+  proof of sd_intro = by definition of sd;
+  proof of sd_1 = by definition of sd;
+  proof of sd_lt = by definition of sd;
+  proof of sd_divides = by definition of sd;
+
+  logical let prime (p : Self) = lt(one, p) /\ (all d : Self, ~(sd(d, p)));
+  proof of prime_1 = by definition of prime;
+  proof of prime_sd = by definition of prime;
+  proof of prime_intro = by definition of prime;
+
 end;;

example/arith/natural_full.fcl

@@ -179,7 +179,6 @@ species NatDividesMorph(B is NatDividesInd) =
   <1>2 conclude;
 end;;
 
-
 species NatSDInd = inherit NatStrictlyDivides, NatInd; end;;
 
 species NatSDMorph (B is NatSDInd) =
@@ -309,6 +308,20 @@ end;;
 species NatPrimeDivTransfer (B is NatPrimeDiv) =
   inherit NatPrimeDiv, NatPrimeMorph(B);
 
+  proof of divides_le =
+  <1>1 assume a1 a2 : Self,
+       hypothesis Hd : divides(a1, a2),
+       hypothesis Hlt : lt(one, a2),
+       prove le(a1, a2)
+       <2>1 prove B!divides(morph(a1), morph(a2))
+            by property morph_divides hypothesis Hd
+       <2>2 prove B!lt(B!one, morph(a2))
+            by property morph_lt, morph_one hypothesis Hlt
+       <2>3 prove B!le(morph(a1), morph(a2))
+            by step <2>1, <2>2 property B!divides_le
+       <2>4 qed by step <2>3 property morph_le_rev
+  <1>f conclude;
+
   proof of prime_divisor =
   <1>1 assume n : Self,
        hypothesis H : ~(n = one),

example/logic/Makefile

@@ -6,7 +6,7 @@ V_FILES=$(wildcard *.v)
 DK_FILES=$(wildcard *.dk)
 all: $(FCL_FILES:.fcl=.dko) $(V_FILES:.v=.dko) $(DK_FILES:.dk=.dko) Coq__Init__Datatypes.dko Coq__Init__Peano.dko
 
-INCLUDE_DIRS= -I ../../lib/logic
+INCLUDE_DIRS= -I ../../lib/logic -I ../logic
 
 # We have to generate all dks coming from coq at the same time
 # so that universe consistency can be checked globally

example/logic/hol_to_coq.dk

@@ -25,6 +25,14 @@ def Is_true : b : hol.term hol.bool -> Coq.U Coq.prop.
                  (holtypes.carrier A)
                  (x : hol.term A => Is_true (p x)).
 
+(; logical identification of falsehood in HOL and Coq, this axiom is
+   required but the reverse direction is provable ;)
+
+axiom_not_false :
+   Coq.T Coq.prop (hol_to_coq.Is_true hol.false) ->
+   Coq.T Coq.prop Coq__Init__Logic.False.
+
+
 (; Dummy symbol used to require the load of this file and
    to add the previous rules ;)
 Load : Type.

lib/arith/morphisms/natmorph.fcl

@@ -293,6 +293,7 @@ species NatLeMorph(B is NatLeInd) =
             <3>2 qed by step <3>1, <2>3
        <2>f qed by step <2>4 property le_plus
   <1>2 conclude;
+
 end;;
 
 species NatLtInd = inherit NatLt, NatInd; end;;