Commit 617567dc authored by Raphael Cauderlier's avatar Raphael Cauderlier
Browse files

Small fixes: transfer theorems are now checked

parent 97e0a4f9
open "basics";;
open "naturals";;
open "natural_instantiation";;
open "natmorph";;
open "natthms";;
(* This file is very sensible to the numbering of theorems performed
......@@ -29,7 +30,7 @@ type hnat = internal
| coq -> {* *};;
species HolNatFull =
inherit NatFullThm;
inherit NatFullThm, NatInd;
representation = hnat;
......
open "basics";;
open "naturals";;
open "natmorph";; (* For the NatInd species *)
(* An easy way to prove injectivity of successor is to define
the predecessor function *)
species NatPred =
inherit NatCase;
inherit NatInd;
signature pred : Self -> Self;
property pred_succ : all n : Self, pred(succ(n)) = n;
(* pred(zero) is unspecified *)
......@@ -35,7 +35,7 @@ end;;
(* An easy way to prove 0 != succ (n) is to provide a
predicate is_zero evaluating to true on 0 and to false on succ *)
species NatIsZero =
inherit NatDecl;
inherit NatInd;
signature is_zero : Self -> bool;
property is_zero_zero : is_zero(zero);
......@@ -50,7 +50,7 @@ end;;
in particular to define morphisms *)
let ( @ )(f, x) = f(x);;
species NatIter =
inherit NatCase;
inherit NatInd;
signature iter : (Self -> Self) -> Self -> Self -> Self;
property iter_zero : all f : (Self -> Self), all z : Self,
iter(f, z, zero) = z;
......
......@@ -4,6 +4,7 @@
open "basics";;
open "naturals";;
open "natmorph";;
species NatPlusZenon =
inherit NatPlus;
......@@ -21,7 +22,7 @@ species NatLeZenon =
end;;
species NatMinusZenon =
inherit NatMinus, NatCase;
inherit NatMinus, NatInd;
theorem minus_n_zero : all n : Self, minus(n, zero) = n
proof =
......
SUBDIRS = logic arith # algebra
SUBDIRS = logic arith
TARGETS=all clean install uninstall
$(TARGETS):
......
SUBDIRS = definitions morphisms theorems transfer
SUBDIRS = definitions morphisms theorems transfer/meta transfer
TARGETS=all clean install uninstall
$(TARGETS):
......
......@@ -2,43 +2,15 @@
open "basics";;
(* The basic block: Peano axiomatization of natural numbers *)
(* The basic block: 0 and successor *)
species NatDecl =
signature zero : Self;
signature succ : Self -> Self;
property zero_succ : all n : Self, ~(zero = succ(n));
property succ_inj : all m n : Self, succ(m) = succ(n) -> m = n;
(* Highr-order axiom, cannot be given to Zenon *)
(* property ind : all p : Self -> prop, *)
(* p (zero) -> *)
(* (all n : Self, p(n) -> p(succ(n))) -> *)
(* all n : Self, p(n); *)
end;;
species NatCase =
inherit NatDecl;
(* When the induction hypothesis is not needed, we can use
reasoning by case which is better supported by Zenon *)
logical let casep (n : Self) = n = zero \/ ex m : Self, n = succ(m);
property case : all n : Self, n = zero \/ ex m : Self, n = succ(m);
(* proof = *)
(* <1>1 assume n : Self, *)
(* prove casep(n) <-> (n = zero \/ ex m : Self, n = succ(m)) *)
(* by definition of casep *)
(* <1>2 prove casep(zero) -> *)
(* (all n : Self, casep(n) -> casep(succ(n))) -> *)
(* all n : Self, casep(n) *)
(* dedukti proof property ind *)
(* {* abst_ind abst_casep *} *)
(* <1>3 prove casep(zero) by step <1>1 *)
(* <1>4 assume n : Self, prove casep(succ(n)) by step <1>1 *)
(* <1>f conclude; *)
end;;
species NatOne =
inherit NatCase;
inherit NatDecl;
let one = succ(zero);
theorem one_spec : one = succ(zero)
......@@ -46,7 +18,7 @@ species NatOne =
end;;
species NatBinary =
inherit NatCase;
inherit NatDecl;
signature bit0 : Self -> Self;
signature bit1 : Self -> Self;
......@@ -57,7 +29,7 @@ species NatBinary =
end;;
species NatPred =
inherit NatCase;
inherit NatDecl;
signature pred : Self -> Self;
property pred_zero : pred(zero) = zero;
......@@ -65,7 +37,7 @@ species NatPred =
end;;
species NatPlus =
inherit NatCase;
inherit NatDecl;
signature plus : Self -> Self -> Self;
property zero_plus : all n : Self, plus(zero, n) = n;
property succ_plus : all m n : Self, plus(succ(m), n) = succ(plus(m, n));
......
......@@ -2,12 +2,37 @@ open "basics";;
open "naturals";;
species NatInd =
inherit NatCase;
inherit NatDecl;
property zero_succ : all n : Self, ~(zero = succ(n));
property succ_inj : all m n : Self, succ(m) = succ(n) -> m = n;
(* Highr-order axiom, cannot be given to Zenon *)
(* property ind : all p : Self -> prop, *)
(* p (zero) -> *)
(* (all n : Self, p(n) -> p(succ(n))) -> *)
(* all n : Self, p(n); *)
property ind : all p : Self -> prop,
p (zero) ->
(all n : Self, p(n) -> p(succ(n))) ->
all n : Self, p(n);
(* When the induction hypothesis is not needed, we can use
reasoning by case which is better supported by Zenon *)
logical let casep (n : Self) = n = zero \/ ex m : Self, n = succ(m);
theorem case : all n : Self, n = zero \/ ex m : Self, n = succ(m)
proof =
<1>1 assume n : Self,
prove casep(n) <-> (n = zero \/ ex m : Self, n = succ(m))
by definition of casep
<1>2 prove casep(zero) ->
(all n : Self, casep(n) -> casep(succ(n))) ->
all n : Self, casep(n)
dedukti proof property ind
{* abst_ind abst_casep *}
<1>3 prove casep(zero) by step <1>1
<1>4 assume n : Self, prove casep(succ(n)) by step <1>1
<1>f conclude;
end;;
species NatMorph (B is NatInd) =
......
open "basics";;
open "naturals";;
species NatMorph (A is NatCase) =
species NatMorph (A is NatDecl) =
inherit NatDecl;
logical signature morph : A -> Self -> prop;
......
open "basics";;
open "naturals";;
species NatMorph (A is NatCase) =
species NatMorph (A is NatDecl) =
inherit NatDecl;
signature morph : A -> Self;
......
......@@ -9,6 +9,8 @@ INCLUDE_DIRS= -I ../../logic -I ../definitions -I ../morphisms -I ../theorems
## them for the dktransfer tactic
ZENON_MODULO=zenon_transfer
all: $(FCL_FILES:.fcl=.dkm) $(FCL_FILES:.fcl=.dk) $(FCL_FILES:.fcl=.dko)
nattransfer.dkm: nattransfer.sk
cp $< $@
......@@ -19,8 +21,6 @@ nattransfer.dk: nattransfer.dkm
nattransfer.dko: nattransfer.dk
all: $(FCL_FILES:.fcl=.dko)
depend: .depend
.depend:
$(FOCALIZEDEP) $(FCL_FILES) > $@
......
......@@ -91,19 +91,19 @@ def and_increase :
(c:fol.prop ->
((fol.proof A) -> (fol.proof B) -> fol.proof c) -> fol.proof c) ->
c:fol.prop ->
((fol.proof C) -> (fol.proof D) -> fol.proof c) -> fol.proof c.
(; := ;)
(; A:fol.prop => ;)
(; B:fol.prop => ;)
(; C:fol.prop => ;)
(; D:fol.prop => ;)
(; x:((fol.proof A) -> fol.proof C) => ;)
(; x0:((fol.proof B) -> fol.proof D) => ;)
(; x1: ;)
(; (c:fol.prop -> ;)
(; ((fol.proof A) -> (fol.proof B) -> fol.proof c) -> fol.proof c) => ;)
(; fol.and_intro C D (x1 C (x2:(fol.proof A) => x3:(fol.proof B) => x x2)) ;)
(; (x1 D (x2:(fol.proof A) => x3:(fol.proof B) => x0 x3)). ;)
((fol.proof C) -> (fol.proof D) -> fol.proof c) -> fol.proof c
:=
A:fol.prop =>
B:fol.prop =>
C:fol.prop =>
D:fol.prop =>
x:((fol.proof A) -> fol.proof C) =>
x0:((fol.proof B) -> fol.proof D) =>
x1:
(c:fol.prop ->
((fol.proof A) -> (fol.proof B) -> fol.proof c) -> fol.proof c) =>
fol.and_intro C D (x1 C (x2:(fol.proof A) => x3:(fol.proof B) => x x2))
(x1 D (x2:(fol.proof A) => x3:(fol.proof B) => x0 x3)).
def or_increase :
A:fol.prop ->
......@@ -117,20 +117,20 @@ def or_increase :
((fol.proof B) -> fol.proof c) -> fol.proof c) ->
c:fol.prop ->
((fol.proof C) -> fol.proof c) ->
((fol.proof D) -> fol.proof c) -> fol.proof c.
(; := ;)
(; A:fol.prop => ;)
(; B:fol.prop => ;)
(; C:fol.prop => ;)
(; D:fol.prop => ;)
(; x:((fol.proof A) -> fol.proof C) => ;)
(; x0:((fol.proof B) -> fol.proof D) => ;)
(; x1: ;)
(; (c:fol.prop -> ;)
(; ((fol.proof A) -> fol.proof c) -> ;)
(; ((fol.proof B) -> fol.proof c) -> fol.proof c) => ;)
(; x1 (fol.or C D) (x2:(fol.proof A) => fol.or_intro_1 C D (x x2)) ;)
(; (x2:(fol.proof B) => fol.or_intro_2 C D (x0 x2)). ;)
((fol.proof D) -> fol.proof c) -> fol.proof c
:=
A:fol.prop =>
B:fol.prop =>
C:fol.prop =>
D:fol.prop =>
x:((fol.proof A) -> fol.proof C) =>
x0:((fol.proof B) -> fol.proof D) =>
x1:
(c:fol.prop ->
((fol.proof A) -> fol.proof c) ->
((fol.proof B) -> fol.proof c) -> fol.proof c) =>
x1 (fol.or C D) (x2:(fol.proof A) => fol.or_intro_1 C D (x x2))
(x2:(fol.proof B) => fol.or_intro_2 C D (x0 x2)).
def imp_increase :
A:fol.prop ->
......@@ -139,15 +139,15 @@ def imp_increase :
D:fol.prop ->
((fol.proof C) -> fol.proof A) ->
((fol.proof B) -> fol.proof D) ->
((fol.proof A) -> fol.proof B) -> (fol.proof C) -> fol.proof D.
(; := ;)
(; A:fol.prop => ;)
(; B:fol.prop => ;)
(; C:fol.prop => ;)
(; D:fol.prop => ;)
(; x:((fol.proof C) -> fol.proof A) => ;)
(; x0:((fol.proof B) -> fol.proof D) => ;)
(; x1:((fol.proof A) -> fol.proof B) => x2:(fol.proof C) => x0 (x1 (x x2)). ;)
((fol.proof A) -> fol.proof B) -> (fol.proof C) -> fol.proof D
:=
A:fol.prop =>
B:fol.prop =>
C:fol.prop =>
D:fol.prop =>
x:((fol.proof C) -> fol.proof A) =>
x0:((fol.proof B) -> fol.proof D) =>
x1:((fol.proof A) -> fol.proof B) => x2:(fol.proof C) => x0 (x1 (x x2)).
def all_increase :
A:fol.type ->
......@@ -161,23 +161,23 @@ def all_increase :
H2:(c:(fol.term C) ->
c0:fol.prop ->
(a:(fol.term A) -> (fol.proof (R a c)) -> fol.proof c0) -> fol.proof c0) ->
H3:(a:(fol.term A) -> fol.proof (B a)) -> c:(fol.term C) -> fol.proof (D c).
(; := ;)
(; A:fol.type => ;)
(; C:fol.type => ;)
(; B:((fol.term A) -> fol.prop) => ;)
(; D:((fol.term C) -> fol.prop) => ;)
(; R:((fol.term A) -> (fol.term C) -> fol.prop) => ;)
(; H1: ;)
(; (a:(fol.term A) -> ;)
(; c:(fol.term C) -> ;)
(; (fol.proof (R a c)) -> (fol.proof (B a)) -> fol.proof (D c)) => ;)
(; H2: ;)
(; (c:(fol.term C) -> ;)
(; c0:fol.prop -> ;)
(; (a:(fol.term A) -> (fol.proof (R a c)) -> fol.proof c0) -> fol.proof c0) => ;)
(; H3:(a:(fol.term A) -> fol.proof (B a)) => ;)
(; c:(fol.term C) => H2 c (D c) (a => Ha => H1 a c Ha (H3 a)). ;)
H3:(a:(fol.term A) -> fol.proof (B a)) -> c:(fol.term C) -> fol.proof (D c)
:=
A:fol.type =>
C:fol.type =>
B:((fol.term A) -> fol.prop) =>
D:((fol.term C) -> fol.prop) =>
R:((fol.term A) -> (fol.term C) -> fol.prop) =>
H1:
(a:(fol.term A) ->
c:(fol.term C) ->
(fol.proof (R a c)) -> (fol.proof (B a)) -> fol.proof (D c)) =>
H2:
(c:(fol.term C) ->
c0:fol.prop ->
(a:(fol.term A) -> (fol.proof (R a c)) -> fol.proof c0) -> fol.proof c0) =>
H3:(a:(fol.term A) -> fol.proof (B a)) =>
c:(fol.term C) => H2 c (D c) (a => Ha => H1 a c Ha (H3 a)).
def ex_increase :
A:fol.type ->
......@@ -194,27 +194,27 @@ def ex_increase :
H3:(c:fol.prop ->
(a:(fol.term A) -> (fol.proof (B a)) -> fol.proof c) -> fol.proof c) ->
c:fol.prop ->
(a:(fol.term C) -> (fol.proof (D a)) -> fol.proof c) -> fol.proof c.
(; := ;)
(; A:fol.type => ;)
(; C:fol.type => ;)
(; B:((fol.term A) -> fol.prop) => ;)
(; D:((fol.term C) -> fol.prop) => ;)
(; R:((fol.term A) -> (fol.term C) -> fol.prop) => ;)
(; H1: ;)
(; (a:(fol.term A) -> ;)
(; c:(fol.term C) -> ;)
(; (fol.proof (R a c)) -> (fol.proof (B a)) -> fol.proof (D c)) => ;)
(; H2: ;)
(; (a:(fol.term A) -> ;)
(; c:fol.prop -> ;)
(; (a0:(fol.term C) -> (fol.proof (R a a0)) -> fol.proof c) -> fol.proof c) => ;)
(; H3: ;)
(; (c:fol.prop -> ;)
(; (a:(fol.term A) -> (fol.proof (B a)) -> fol.proof c) -> fol.proof c) => ;)
(; H3 (fol.ex C D) ;)
(; (a => ;)
(; HB => H2 a (fol.ex C D) (c => HR => fol.ex_intro C D c (H1 a c HR HB))). ;)
(a:(fol.term C) -> (fol.proof (D a)) -> fol.proof c) -> fol.proof c
:=
A:fol.type =>
C:fol.type =>
B:((fol.term A) -> fol.prop) =>
D:((fol.term C) -> fol.prop) =>
R:((fol.term A) -> (fol.term C) -> fol.prop) =>
H1:
(a:(fol.term A) ->
c:(fol.term C) ->
(fol.proof (R a c)) -> (fol.proof (B a)) -> fol.proof (D c)) =>
H2:
(a:(fol.term A) ->
c:fol.prop ->
(a0:(fol.term C) -> (fol.proof (R a a0)) -> fol.proof c) -> fol.proof c) =>
H3:
(c:fol.prop ->
(a:(fol.term A) -> (fol.proof (B a)) -> fol.proof c) -> fol.proof c) =>
H3 (fol.ex C D)
(a =>
HB => H2 a (fol.ex C D) (c => HR => fol.ex_intro C D c (H1 a c HR HB))).
def pred_increase :
As:fol.types ->
......
......@@ -5,16 +5,6 @@ open "naturals";;
open "natmorph_rel";;
open "natthms";;
(* Warning! All theorems in this file are admitted! *)
(* TODO: move the following false axiom to a separated file which is
not seen by Dedukti *)
let magic_axiom = internal bool
external
| dedukti -> {* dk_bool.true *}
| coq -> {* true *}
;;
species NatPlusTransfer (A is NatPlusThm) =
inherit NatPlusMorph(A), NatPlusThm;
......
#NAME eq.
def Eq (A : fol.type) := fol.make_pred (fol.cons_type A (fol.cons_type A fol.nil_type)) (dk_logic.eq A).
......@@ -80,3 +80,8 @@ def make_pred : As : types -> (pred_arrs As) -> predicate.
(; The type of proofs of a formula is defined using an impredicative encoding ;)
def proof : prop -> Type := dk_logic.eP.
def and_intro := hol.and_intro.
def or_intro_1 := hol.or_intro1.
def or_intro_2 := hol.or_intro2.
def ex_intro := hol.exists_intro.
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment