Skip to content

GitLab

Commit 8f281d7b authored by Raphael Cauderlier's avatar Raphael Cauderlier
Browse files

Holide import

parent 63857b89
Hide whitespace changes
Inline Side-by-side
Showing with 122 additions and 77 deletions
Makefile.rules
View file @ 8f281d7b
......@@ -3,7 +3,7 @@
INCLUDE_DIRS=
DKTACTICS_DIR=$(shell $(DKTACTICS))
DKCHECK_OPT = $(INCLUDE_DIRS)
FOCALIZEC_OPT = $(INCLUDE_DIRS) -no-ocaml-code -no-coq-code -stop-before-dk -dedukti-code
FOCALIZEC_OPT = $(INCLUDE_DIRS) -no-stdlib-path -no-ocaml-code -no-coq-code -stop-before-dk -dedukti-code
%.dko: %.dk
$(DKCHECK) $(DKCHECK_OPT) -e -nl $<
......@@ -14,5 +14,14 @@ FOCALIZEC_OPT = $(INCLUDE_DIRS) -no-ocaml-code -no-coq-code -stop-before-dk -ded
%.sk: %.fcl
$(FOCALIZEC) $(FOCALIZEC_OPT) $<
%.dk: %.art
$(HOLIDE) $< -o $@
%_fcl.fcl: %.art
$(HOLIDE) $< --output-language FoCaLiZe -o $@
%.txt: %.art
$(HOLIDE) $< --output-language Txt -o $@
%.vo: %.v
$(COQC) $<
configure
View file @ 8f281d7b
......@@ -10,6 +10,8 @@ print_to_stderr ()
echo "$1" > /dev/stderr
}
declare -A VARS
find_binary () {
# $1 is the name of the binary
# $2 is an optional extension to be used when we fallback to using
......@@ -43,6 +45,7 @@ find_binary_no_check () {
# $1 and $2 are arguments to find_binary
# $3 is the variable name
A=$(find_binary $1 $2)
VARS[$3]="$A"
print_to_file "$3=\"$A\""
return 0
}
......@@ -53,6 +56,7 @@ find_and_check_binary () {
# $4 is the option to pass to the program to ask for its version
# $5 is the expected answer
A=$(find_binary $1 $2)
VARS[$3]="$A"
VERSION_COMMAND="$A $4"
print_to_stderr "asking '$1' for its version number ($VERSION_COMMAND)"
B=$(eval $VERSION_COMMAND |& cat)
......@@ -80,4 +84,16 @@ find_and_check_binary "focalizec" "" "FOCALIZEC" "-v" "The FoCaLize compiler, ve
find_binary_no_check "focalizedep" "" "FOCALIZEDEP" &&
find_binary_no_check "dktactics" "" "DKTACTICS" &&
find_and_check_binary "coqc" "" "COQC" "-v | grep version | cut -d ' ' -f 6" "8.4pl6" &&
find_and_check_binary "coqtop" "" "COQTOP" "-v | grep version | cut -d ' ' -f 6" "8.4pl6"
find_and_check_binary "coqtop" "" "COQTOP" "-v | grep version | cut -d ' ' -f 6" "8.4pl6" &&
# Check that Coqine is installed, do not know how to check the version
if ( echo 'Require Coqine.' | ${VARS["COQTOP"]})
then
print_to_stderr "Coqine found."
else
print_to_stderr "Coqine not found."
exit 1
fi &&
find_and_check_binary "opentheory" "" "OPENTHEORY" "-v" "opentheory 1.3 (release 20160204)" &&
find_and_check_binary "holide" "" "HOLIDE" "--version" "Holide HOL to Dedukti translator, version 0.2.1 (Holala)"
core/logic/dk_logic.dk
View file @ 8f281d7b
......@@ -3,7 +3,14 @@
def Prop := hol.term hol.bool.
def prop := hol.bool.
def eeP (b : hol.term prop) : Prop := b.
def eP := hol.proof.
(; FIXME: Not confluent ;)
(; forall_type is accepted by Zenon but has no counterpart in HOL. ;)
(; Preprocessing of eP (forall_type) should be done by Focalide. ;)
forall_type : (hol.type -> Prop) -> Prop.
def eP : Prop -> Type.
[F] eP (forall_type F) --> a : hol.type -> eP (F a).
[p] eP p --> hol.proof p.
def true := hol.true.
def false := hol.false.
......
interop/arith/Makefile
View file @ 8f281d7b
......@@ -3,8 +3,14 @@ include ../../Makefile.rules
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)
HolNaturals.art: $(ART_FILES)
cat $^ > $@
HolNaturals.dk: HolNaturals.art
INCLUDE_DIRS= -I ../../core/logic -I ../../core/arith -I ../logic
%.dk: %.vo
......@@ -12,13 +18,18 @@ INCLUDE_DIRS= -I ../../core/logic -I ../../core/arith -I ../logic
echo "Require $*.";\
echo "Dedukti Export All.") | $(COQTOP)
$(ART_FILES): %.art:
$(OPENTHEORY) install $* || echo "Opentheory package $* already installed"
$(OPENTHEORY) info --article -o $@ $*
depend: .depend
.depend:
.depend: $(ART_FILES:.art=.dk)
$(FOCALIZEDEP) $(FCL_FILES) > $@
natural_coq.sk: CoqNaturals.dko
natural_hol.sk: HolNaturals.dko
-include .depend
clean :
rm -f *.dko *.sk* *.fo *.pfc *.zv *.mangled *_fcl.* .depend *.vo *.glob *.dk
rm -f *.dko *.sk* *.fo *.pfc *.zv *.mangled *_fcl.* .depend *.vo *.glob *.sk *.dk _fcl.* *.art *.txt
interop/arith/natural_hol.fcl
View file @ 8f281d7b
......@@ -10,21 +10,24 @@ open "natural_instantiation";;
type hnat = internal
external
| dedukti -> {* natural__div__full.Number_2ENatural_2Enatural *};;
| dedukti -> {* HolNaturals.Number_2ENatural_2Enatural *};;
let hzero = internal hnat
external
| dedukti -> {* natural__div__full.Number_2ENatural_2Ezero *};;
| dedukti -> {* HolNaturals.Number_2ENatural_2Ezero *};;
let hsucc (n : hnat) = internal hnat
external
| dedukti -> {* natural__div__full.Number_2ENatural_2Esuc n *};;
| dedukti -> {* HolNaturals.Number_2ENatural_2Esuc n *};;
theorem hol_induction :
all p : hnat -> bool,
(p(hzero) /\ (all n : hnat, p(n) -> p(hsucc(n)))) ->
(all n : hnat, p(n))
proof = dedukti proof {* natural__div__full.thm_3723. *};;
proof = dedukti proof {* HolNaturals.thm_1238. *};;
(* The statement in HolNaturals.txt:
((p zero) /\ (∀n, (p n) ==> (p (suc n)))) ==> (∀n, p n)
*)
species HolNatDecl =
inherit NatDecl;
......@@ -51,14 +54,16 @@ species HolNatDecl =
<1>1 assume m : Self,
prove ~ (succ(m) = zero)
dedukti proof definition of zero, succ
{* natural__div__full.thm_73 m *}
{* HolNaturals.thm_106 m *}
(* ∀n, ~ ((suc n) = zero) *)
<1>f conclude;
proof of succ_inj =
<1>1 assume m n : Self,
prove (succ(m) = succ(n)) <-> (m = n)
dedukti proof definition of succ
{* natural__div__full.thm_3523 m n *}
{* HolNaturals.thm_107 m n *}
(* ∀m n, ((suc m) = (suc n)) <=> (m = n) *)
<1>f conclude;
end;;
......@@ -67,44 +72,32 @@ collection HolNatDeclColl = implement HolNatDecl; end;;
(* NatIter *)
let id (x : 'a) = x;;
let compose (f : 'b -> 'c, g : 'a -> 'b, x : 'a) = f(g(x));;
(* let id(x : 'a) = x;; *)
let id =
internal 'a -> 'a
external
| dedukti -> {* HolNaturals.Function_2Eid (hol.arr __var_a __var_a).
axiom_id : a : hol.type -> x : hol.term a -> hol.proof (hol.eq a (id a x) x)
*};;
theorem id_x : all x : 'a, id @ x = x
proof = dedukti proof {* axiom_id. *};;
let ( ^ ) =
internal ('a -> 'a) -> hnat -> ('a -> 'a)
external
| dedukti -> {* natural__div__full.Function_2E_5E __var_a *};;
| dedukti -> {* HolNaturals.Function_2E_5E __var_a *};;
theorem power_zero : all f : 'a -> 'a,
f ^ hzero = id
proof =
dedukti proof
{* natural__div__full.thm_27333. *};;
theorem power_succ : all f : 'a -> 'a, all n : hnat,
f ^ hsucc(n) = compose(f, f ^ n)
proof =
dedukti proof
{* natural__div__full.thm_27337. *};;
{* HolNaturals.thm_109. *};;
(* ∀f, (f ^ zero) = id *)
species HolNatIter =
inherit NatIter, HolNatDecl;
(*
let to_hnat (n : Self) : hnat = n;
let from_hnat (n : hnat) : Self = n;
theorem to_hnat_zero : to_hnat(zero) = hzero
proof = by definition of to_hnat, zero;
theorem from_hnat_zero : from_hnat(hzero) = zero
proof = by definition of from_hnat, zero;
theorem to_hnat_succ : all n : Self,
to_hnat(succ(n)) = hsucc(to_hnat(n))
proof = dedukti proof definition of to_hnat, succ {* (n : cc.eT abst_T => hol.REFL abst_T (abst_succ n)). *};
theorem from_hnat_succ : all n : hnat,
from_hnat(hsucc(n)) = succ(from_hnat(n))
proof = dedukti proof definition of from_hnat, succ {* (n : cc.eT abst_T => hol.REFL abst_T (abst_succ n)). *};
*)
let iter(f, z, n) = (f ^ n) @ z;
proof of iter_zero =
<1>1 assume f : Self -> Self,
......@@ -117,7 +110,7 @@ species HolNatIter =
definition of zero
{* power_zero abst_T f *}
<2>3 prove id @ z = z
dedukti proof {* hol.REFL abst_T z *}
dedukti proof {* id_x abst_T z *}
<2>f conclude
<1>f conclude;
......@@ -126,15 +119,8 @@ species HolNatIter =
assume z : Self,
assume n : Self,
prove iter(f, z, succ(n)) = f @ iter(f, z, n)
<2>1 prove iter(f, z, succ(n)) = (f ^ succ(n)) @ z
by definition of iter
<2>2 prove f ^ succ(n) = compose(f, f ^ n)
dedukti proof definition of succ {* power_succ abst_T f n *}
<2>3 prove compose(f, f ^ n) @ z = f @ (iter(f, z, n))
dedukti proof
definition of iter
{* hol.REFL abst_T (f (abst_iter f z n)) *}
<2>f conclude
dedukti proof definition of iter, succ {* HolNaturals.thm_6414 abst_T f n z *}
(* ∀f n x, (f ^ (suc n) x) = (f (f ^ n x)) *)
<1>f conclude;
end;;
......@@ -145,7 +131,7 @@ collection HolNatIterColl = implement HolNatIter; end;;
let hol_plus =
internal hnat -> hnat -> hnat
external
| dedukti -> {* natural__div__full.Number_2ENatural_2E_2B *};;
| dedukti -> {* HolNaturals.Number_2ENatural_2E_2B *};;
species HolPlus =
inherit HolNatIter, NatPlus;
......@@ -155,17 +141,14 @@ species HolPlus =
proof of zero_plus =
dedukti proof
definition of plus, zero
{* natural__div__full.thm_10446. *};
{* HolNaturals.thm_144. *};
(* ∀n, (zero + n) = n *)
proof of succ_plus =
dedukti proof
definition of plus, succ
{* natural__div__full.thm_10450. *};
(* proof of plus_zero = *)
(* dedukti proof *)
(* definition of plus, zero *)
(* {* natural__div__full.thm_10569. *}; *)
{* HolNaturals.thm_147. *};
(* ∀m n, ((suc m) + n) = (suc (m + n)) *)
end;;
collection HolPlusColl = implement HolPlus; end;;
......@@ -175,21 +158,25 @@ collection HolPlusColl = implement HolPlus; end;;
let hol_times (p : hnat, q : hnat) : hnat =
internal hnat
external
| dedukti -> {* natural__div__full.Number_2ENatural_2E_2A p q *};;
| dedukti -> {* HolNaturals.Number_2ENatural_2E_2A p q *};;
theorem hol_times_zero : all n : hnat, hol_times(hzero, n) = hzero
proof = dedukti proof {* natural__div__full.thm_108. *};;
proof = dedukti proof {* HolNaturals.thm_117. *};;
(* ∀n, (zero * n) = zero *)
theorem hol_times_succ : all m n : hnat, hol_times(hsucc(m), n) = hol_plus(hol_times(m, n), n)
proof = dedukti proof {* natural__div__full.thm_109. *};;
proof = dedukti proof {* HolNaturals.thm_157. *};;
(* ∀m n, ((suc m) * n) = ((m * n) + n) *)
theorem hol_times_commute : all m n : hnat,
hol_times (m, n) = hol_times (n, m)
proof = dedukti proof {* natural__div__full.thm_146. *};;
proof = dedukti proof {* HolNaturals.thm_143. *};;
(* ∀m n, (m * n) = (n * m) *)
theorem hol_plus_commute : all m n : hnat,
hol_plus (m, n) = hol_plus (n, m)
proof = dedukti proof {* natural__div__full.thm_113. *};;
proof = dedukti proof {* HolNaturals.thm_129. *};;
(* ∀m n, (m + n) = (n + m) *)
species HolTimes =
inherit NatTimes, HolPlus;
......@@ -213,10 +200,11 @@ collection HolTimesColl = implement HolTimes; end;;
let hol_le (m : hnat, n : hnat) =
internal bool
external | dedukti -> {* natural__div__full.Number_2ENatural_2E_3C_3D m n *};;
external | dedukti -> {* HolNaturals.Number_2ENatural_2E_3C_3D m n *};;
theorem hol_le_plus : all m n : hnat, hol_le(m, n) <-> ex d : hnat, n = hol_plus(m, d)
proof = dedukti proof {* natural__div__full.thm_11363. *};;
proof = dedukti proof {* HolNaturals.thm_132. *};;
(* ∀m n, (m <= n) <=> (∃d, n = (m + d)) *)
species HolLe =
inherit NatLe, HolPlus;
......@@ -231,11 +219,12 @@ collection HolLeColl = implement HolLe; end;;
let hol_divides (p : hnat, q : hnat) : bool =
internal bool
external
| dedukti -> {* natural__div__full.Number_2ENatural_2Edivides p q *};;
| dedukti -> {* HolNaturals.Number_2ENatural_2Edivides p q *};;
theorem hol_divides_times1 : all m n : hnat,
hol_divides (m, n) <-> (ex p : hnat, hol_times(p, m) = n)
proof = dedukti proof {* natural__div__full.thm_185. *};;
proof = dedukti proof {* HolNaturals.thm_241. *};;
(* ∀a b, (divides a b) <=> (∃c, (c * a) = b) *)
theorem hol_divides_times2 : all m n : hnat,
hol_divides (m, n) <-> (ex p : hnat, hol_times(m, p) = n)
......@@ -246,25 +235,30 @@ proof = by property hol_divides_times1, hol_times_commute;;
let hol_lt(m : hnat, n : hnat) =
internal bool
external
| dedukti -> {* natural__div__full.Number_2ENatural_2E_3C m n *};;
| dedukti -> {* HolNaturals.Number_2ENatural_2E_3C m n *};;
theorem hol_lt_le : all m n : hnat, hol_le(hsucc(m), n) <-> hol_lt(m, n)
proof = dedukti proof {* natural__div__full.thm_5766. *};;
proof = dedukti proof {* HolNaturals.thm_189. *};;
(* ∀m n, ((suc m) <= n) <=> (m < n) *)
theorem hol_lt_zero : all m : hnat, ~(hol_lt(m, hzero))
proof = dedukti proof {* natural__div__full.thm_87. *};;
proof = dedukti proof {* HolNaturals.thm_104. *};;
(* ∀m, ~ (m < zero) *)
theorem hol_le_zero : all n : hnat, hol_le(hzero, n)
proof = dedukti proof {* natural__div__full.thm_5905. *};;
proof = dedukti proof {* HolNaturals.thm_1348. *};;
(* ∀n, zero <= n *)
theorem hol_le_lt : all m n : hnat, hol_le(m, n) <-> (hol_lt(m, n) \/ m = n)
proof = dedukti proof {* natural__div__full.thm_7954. *};;
proof = dedukti proof {* HolNaturals.thm_2162. *};;
(* ∀m n, (m <= n) <=> ((m < n) \/ (m = n)) *)
theorem hol_lt_one : all m : hnat, (m = hzero \/ (m = hsucc(hzero) \/ hol_lt(hsucc(hzero), m)))
proof = by property hol_le_zero, hol_le_lt, hol_lt_le;;
theorem hol_lt_irrefl : all n : hnat, ~(hol_lt(n, n))
proof = dedukti proof {* natural__div__full.thm_123. *};;
proof = dedukti proof {* HolNaturals.thm_201. *};;
(* ∀n, ~ (n < n) *)
species HolLt =
inherit NatLt, HolLe;
......@@ -276,7 +270,8 @@ end;;
collection HolLtColl = implement HolLt; end;;
theorem hol_divides_le : all m n : hnat, (~(n = hzero) /\ hol_divides(m, n)) -> hol_le(m, n)
proof = dedukti proof {* natural__div__full.thm_27798. *};;
proof = dedukti proof {* HolNaturals.thm_232. *};;
(* ∀a b, ((~ (b = zero)) /\ (divides a b)) ==> (a <= b) *)
species HolDiv =
inherit NatDivides, HolTimes, HolLt;
......@@ -312,7 +307,7 @@ collection HolDivColl = implement HolDiv; end;;
let hol_prime (p : hnat) : bool =
internal bool
external
| dedukti -> {* natural__div__full.Number_2ENatural_2Eprime p *};;
| dedukti -> {* HolNaturals.Number_2ENatural_2Eprime p *};;
(* The definition of prime in OpenTheory refers to the constant 1
written in binary so we first need to import it and prove it is
......@@ -321,10 +316,11 @@ let hol_prime (p : hnat) : bool =
(* Adding a zero in binary (mulitplication by 2) *)
let b0 (n : hnat) =
internal hnat
external | dedukti -> {* natural__div__full.Number_2ENatural_2Ebit0 n *};;
external | dedukti -> {* HolNaturals.Number_2ENatural_2Ebit0 n *};;
theorem b0_zero : b0(hzero) = hzero
proof = dedukti proof {* natural__div__full.thm_96. *};;
proof = dedukti proof {* HolNaturals.thm_112. *};;
(* (bit0 zero) = zero *)
(* Adding a one in binary (n => 2*n + 1) *)
let b1 (n : hnat) = hsucc (b0(n));;
......@@ -340,13 +336,16 @@ theorem hol_prime_def : all p : hnat,
hol_prime(p) <->
((~(p = hol_one)) /\
all n : hnat, hol_divides(n, p) -> (n = hol_one \/ n = p))
proof = dedukti proof {* natural__div__full.thm_202. *};;
proof = dedukti proof {* HolNaturals.thm_227. *};;
(* ∀p, (prime p) <=> ((~ (p = (bit1 zero))) /\ (∀n, (divides n p) ==> ((n = (bit1 zero)) \/ (n = p)))) *)
theorem hol_prime_zero : ~(hol_prime(hzero))
proof = dedukti proof {* natural__div__full.thm_32289. *};;
proof = dedukti proof {* HolNaturals.thm_14422. *};;
(* ~ (prime zero) *)
theorem hol_prime_one : ~(hol_prime(hol_one))
proof = dedukti proof {* natural__div__full.thm_32306. *};;
proof = dedukti proof {* HolNaturals.thm_14428. *};;
(* ~ (prime (bit1 zero)) *)
species HolPrime =
inherit NatPrime, HolDiv, HolLt;
......@@ -484,7 +483,8 @@ end;;
theorem hol_prime_divisor :
all n : hnat,
(~(n = hol_one)) -> ex p : hnat, hol_prime(p) /\ hol_divides(p, n)
proof = dedukti proof {* natural__div__full.thm_33959. *};;
proof = dedukti proof {* HolNaturals.thm_14683. *};;
(* ∀n, (~ (n = (bit1 zero))) ==> (∃p, (prime p) /\ (divides p n)) *)
(* species HolPrimeDiv = *)
(* inherit NatPrimeDiv, HolPrime; *)
......
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