Commit 82916e9e authored by Raphael Cauderlier's avatar Raphael Cauderlier
Browse files

Remove dependency on dktactics/fol and add Coq import

Depending on dktactics makes writing the interoperability layer hard
because most types in dktactics are not definable.

Moreover, this removes dependency on Dedukti v2.6 (featuring injective
symbols). When the transfer tactic will be called, it will not know
about the rule [a,b] term (arr a b) --> term a -> term b.
parent 76f22897
......@@ -4,3 +4,6 @@
*.fo
*.pfc
*.zv
*.vo
*.glob
.depend
......@@ -11,25 +11,11 @@
./configure
SUBDIRS = core interop
TARGETS=all clean install uninstall
all:
$(TARGETS):
for d in $(SUBDIRS); do \
$(MAKE) all -C $$d; \
$(MAKE) $@ -C $$d || exit 1; \
done
clean:
for d in $(SUBDIRS); do \
$(MAKE) clean -C $$d; \
done
install:
for d in $(SUBDIRS); do \
$(MAKE) install -C $$d; \
done
uninstall:
for d in $(SUBDIRS); do \
$(MAKE) uninstall -C $$d; \
done
.PHONY: all clean install uninstall
.PHONY: $(TARGETS)
......@@ -2,7 +2,7 @@
INCLUDE_DIRS=
DKTACTICS_DIR=$(shell $(DKTACTICS))
DKCHECK_OPT = -I $(DKTACTICS_DIR)/fol $(INCLUDE_DIRS) -errors-in-snf
DKCHECK_OPT = $(INCLUDE_DIRS)
FOCALIZEC_OPT = $(INCLUDE_DIRS) -no-ocaml-code -no-coq-code -stop-before-dk -dedukti-code
%.dko: %.dk
......
......@@ -53,8 +53,9 @@ 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)
print_to_stderr "asking '$1' for its version number"
B=$($A $4 |& cat)
VERSION_COMMAND="$A $4"
print_to_stderr "asking '$1' for its version number ($VERSION_COMMAND)"
B=$(eval $VERSION_COMMAND |& cat)
print_to_stderr "'$1' has version '$B'"
if [ "$B" = "$5" ]
then
......@@ -71,9 +72,12 @@ echo > .config_vars &&
# Mandatory
find_binary_no_check "dkdep" ".native" "DKDEP" &&
find_and_check_binary "dkcheck" ".native" "DKCHECK" "-version" "Dedukti v2.5.1" &&
find_and_check_binary "dkmeta" ".native" "DKMETA" "-version" "Meta Dedukti v2.5.1" &&
find_and_check_binary "skcheck" ".native" "SKCHECK" "-version" "Sukerujo v2.5.1" &&
find_and_check_binary "skmeta" ".native" "SKMETA" "-version" "Meta Sukerujo v2.5.1" &&
find_and_check_binary "dkcheck" ".native" "DKCHECK" "-version" "Dedukti v2.6" &&
find_and_check_binary "dkmeta" ".native" "DKMETA" "-version" "Meta Dedukti v2.6" &&
find_and_check_binary "skcheck" ".native" "SKCHECK" "-version" "Sukerujo v2.6" &&
# find_and_check_binary "skmeta" ".native" "SKMETA" "-version" "Meta Sukerujo v2.6" &&
find_and_check_binary "focalizec" "" "FOCALIZEC" "-v" "The FoCaLize compiler, version 0.9.2" &&
find_binary_no_check "dktactics" "" "DKTACTICS"
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"
#!/usr/bin/env bash
# Copyright Ali Assaf <ali.assaf@inria.fr>
# and Raphaël Cauderlier <raphael.cauderlier@inria.fr>, 2015
# This software is governed by the CeCILL-B license under French law and
# abiding by the rules of distribution of free software.
# See "http://www.cecill.info".
( echo "Require Coqine."
for arg
do
echo "Require $arg."
done
echo "Dedukti Export All."
)
SUBDIRS = logic arith algebra
SUBDIRS = logic arith # algebra
TARGETS=all clean install uninstall
all:
$(TARGETS):
for d in $(SUBDIRS); do \
$(MAKE) all -C $$d; \
$(MAKE) $@ -C $$d || exit 1; \
done
clean:
for d in $(SUBDIRS); do \
$(MAKE) clean -C $$d; \
done
install:
for d in $(SUBDIRS); do \
$(MAKE) install -C $$d; \
done
uninstall:
for d in $(SUBDIRS); do \
$(MAKE) uninstall -C $$d; \
done
.PHONY: all clean install uninstall
.PHONY: $(TARGETS)
open "basics";;
open "naturals";;
(* Morphisms *)
species NatMorph (B is NatCase) =
species NatMorph (B is NatDecl) =
inherit NatCase;
signature morph : Self -> B;
......@@ -39,10 +36,10 @@ species NatMorph (B is NatCase) =
(all b : Self, morph(succ(a)) = morph(b) -> succ(a) = b)) ->
(all a b : Self, morph(a) = morph(b) -> a = b)
dedukti proof property ind
{* abst_ind (a : fol.term abst_T => fol.all abst_T (
b : fol.term abst_T =>
fol.imp (eq.eq _p_B_T (abst_morph a) (abst_morph b))
(eq.eq abst_T a b))) *}
{* abst_ind (a : cc.eT abst_T => dk_logic.forall abst_T (
b : cc.eT abst_T =>
dk_logic.imp (dk_logic.eq _p_B_T (abst_morph a) (abst_morph b))
(dk_logic.eq abst_T a b))) *}
<1>2 assume b : Self,
hypothesis H : morph(zero) = morph(b),
prove zero = b
......
......@@ -39,11 +39,10 @@ species NatCase =
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));
(* property plus_zero : all m : Self, plus(m, zero) = m; *)
end;;
species NatTimes =
......@@ -66,7 +65,6 @@ end;;
species NatMinus =
inherit NatPlus;
signature minus : Self -> Self -> Self;
property minus_zero_n : all n : Self, minus(zero, n) = zero;
property minus_succ_zero : all n : Self, minus(succ(n), zero) = succ(n);
property minus_succ_succ :
......@@ -75,7 +73,6 @@ end;;
species NatLt =
inherit NatLe;
logical let lt(m, n) = le(succ(m), n);
theorem lt_spec : all m n : Self, lt(m, n) <-> le(succ(m), n)
proof = by definition of lt;
......@@ -87,12 +84,10 @@ species NatDivides =
theorem divides_times : all m n : Self,
divides(m, n) <-> (ex p : Self, times(m, p) = n)
proof = by definition of divides;
end;;
species NatStrictlyDivides =
inherit NatDivides, NatLt;
logical let sd(m, n) = divides(m, n) /\ lt(m, n) /\ lt(succ(zero), m);
theorem sd_divides : all m n : Self, sd(m, n) -> divides(m, n)
proof = by definition of sd;
......@@ -115,7 +110,6 @@ species NatPrime =
proof = by definition of prime;
theorem prime_sd : all p d : Self, prime(p) -> ~(sd(d, p))
proof = by definition of prime;
theorem prime_intro :
all p : Self,
lt(succ(zero), p) ->
......@@ -123,32 +117,3 @@ species NatPrime =
prime(p)
proof = by definition of prime;
end;;
(* species NatPrimeDiv = *)
(* inherit NatPrime; *)
(* property prime_divisor : *)
(* all n : Self, *)
(* (~(n = succ(zero))) -> *)
(* ex p : Self, (prime(p) /\ divides(p, n)); *)
(* signature primediv_pred : Self -> Self -> bool; *)
(* property primediv_pred_spec : all n p : Self, *)
(* primediv_pred(n, p) <-> (prime(p) /\ divides(p, n)); *)
(* let primediv (n : Self) : Self = select (primediv_pred(n)); *)
(* theorem choice_primediv : all n p : Self, *)
(* primediv_pred(n, p) -> primediv_pred(n, primediv(n)) *)
(* proof = *)
(* <1>1 assume n p : Self, *)
(* prove primediv_pred(n, p) -> primediv_pred(n, primediv(n)) *)
(* dedukti proof definition of primediv property choice *)
(* {* abst_choice (abst_primediv_pred n) p *} *)
(* <1>2 conclude; *)
(* theorem primediv_prime : all n : Self, *)
(* (~ n = succ(zero)) -> prime(primediv(n)) *)
(* proof = by property prime_divisor, choice_primediv, primediv_pred_spec; *)
(* theorem primediv_divides : all n : Self, *)
(* (~ n = succ(zero)) -> divides(primediv(n), n) *)
(* proof = by property prime_divisor, choice_primediv, primediv_pred_spec; *)
(* end;; *)
......@@ -4,7 +4,8 @@ include ../../Makefile.rules
all: basics.dko zen.dko focal.dko
basics.dko: dk_builtins.dko
cc.dko:
cc.dko: hol.dko
hol.dko:
dk_bool.dko:
dk_logic.dko: cc.dko dk_bool.dko
focal.dko: dk_logic.dko dk_bool.dko zen.dko
......
#NAME cc.
def eT := fol.term.
def Arrow : Type -> Type -> Type.
[A,B] Arrow A B --> fol.term A -> fol.term B.
def uT : Type := hol.type.
def eT : uT -> Type := hol.term.
def Arrow : uT -> uT -> uT := hol.arr.
#NAME dk_bool.
bool : Type.
def Bool : Type := bool.
def bool : hol.type := hol.bool.
def Bool : Type := hol.term bool.
def bool1 := fol.read_types (nat.S nat.O) bool.
def true : hol.term bool := hol.true.
def false : hol.term bool := hol.false.
IS_TRUE : fol.predicate.
[] fol.pred_arity IS_TRUE --> bool1.
def is_true : Bool -> fol.prop := fol.pred_apply IS_TRUE.
def eq := hol.eq.
def not := hol.not.
def and := hol.and.
def or := hol.or.
def imp := hol.imp.
def ite := hol.cond.
IS_FALSE : fol.predicate.
[] fol.pred_arity IS_FALSE --> bool1.
def is_false : Bool -> fol.prop := fol.pred_apply IS_FALSE.
TRUE : fol.function.
[] fol.fun_arity TRUE --> fol.nil_type.
[] fol.fun_codomain TRUE --> bool.
FALSE : fol.function.
[] fol.fun_arity FALSE --> fol.nil_type.
[] fol.fun_codomain FALSE --> bool.
def true : fol.term bool := fol.fun_apply TRUE.
def false : fol.term bool := fol.fun_apply FALSE.
EQ : A : Type -> fol.function.
[A] fol.fun_arity (EQ A) --> fol.read_types (nat.S (nat.S nat.O)) A A.
[] fol.fun_codomain (EQ _) --> bool.
def eq (A : Type) := fol.fun_apply (EQ A).
NOT : fol.function.
[] fol.fun_arity NOT --> fol.read_types (nat.S nat.O) bool.
[] fol.fun_codomain NOT --> bool.
def not := fol.fun_apply NOT.
def bool2 := fol.read_types (nat.S (nat.S nat.O)) bool bool.
AND : fol.function.
[] fol.fun_arity AND --> bool2.
[] fol.fun_codomain AND --> bool.
def and := fol.fun_apply AND.
OR : fol.function.
[] fol.fun_arity OR --> bool2.
[] fol.fun_codomain OR --> bool.
def or := fol.fun_apply OR.
IMP : fol.function.
[] fol.fun_arity IMP --> bool2.
[] fol.fun_codomain IMP --> bool.
def imp := fol.fun_apply IMP.
ITE : Type -> fol.function.
[A] fol.fun_arity (ITE A) --> fol.read_types (nat.S (nat.S (nat.S nat.O))) bool A A.
[A] fol.fun_codomain (ITE A) --> A.
def ite (A : Type) := fol.fun_apply (ITE A).
match : P : (Bool -> Type) -> P true -> P false -> b : Bool -> P b.
[] fol.apply_pred IS_TRUE
(fol.cons_term bool (fol.apply_fun TRUE fol.nil_term)
fol.nil_type fol.nil_term)
--> fol.true.
[] fol.apply_pred IS_TRUE
(fol.cons_term bool (fol.apply_fun FALSE fol.nil_term)
fol.nil_type fol.nil_term)
--> fol.false.
[A,a,b] fol.apply_pred IS_TRUE
(fol.cons_term bool
(fol.apply_fun (EQ A)
(fol.cons_term _ a
(fol.cons_type _ fol.nil_type)
(fol.cons_term _ b fol.nil_type fol.nil_term)))
fol.nil_type fol.nil_term)
--> eq.eq A a b.
[b] fol.apply_pred IS_FALSE (fol.cons_term bool b fol.nil_type fol.nil_term) --> is_true (not b).
[] fol.apply_fun NOT
(fol.cons_term bool (fol.apply_fun TRUE fol.nil_term) fol.nil_type fol.nil_term)
-->
false.
[] fol.apply_fun NOT
(fol.cons_term bool (fol.apply_fun FALSE fol.nil_term) fol.nil_type fol.nil_term)
-->
true.
[b] fol.apply_fun AND (fol.cons_term bool (fol.apply_fun TRUE fol.nil_term) (fol.cons_type bool fol.nil_type) (fol.cons_term bool b fol.nil_type fol.nil_term))
-->
b.
[] fol.apply_fun AND (fol.cons_term bool (fol.apply_fun FALSE fol.nil_term) (fol.cons_type bool fol.nil_type) (fol.cons_term bool _ fol.nil_type fol.nil_term))
-->
false.
[] fol.apply_fun OR (fol.cons_term bool (fol.apply_fun TRUE fol.nil_term) (fol.cons_type bool fol.nil_type) (fol.cons_term bool _ fol.nil_type fol.nil_term))
-->
true.
[b] fol.apply_fun OR (fol.cons_term bool (fol.apply_fun FALSE fol.nil_term) (fol.cons_type bool fol.nil_type) (fol.cons_term bool b fol.nil_type fol.nil_term))
-->
b.
[A,a] fol.apply_fun (ITE A)
(fol.cons_term bool (fol.apply_fun TRUE fol.nil_term)
(fol.cons_type _ (fol.cons_type _ fol.nil_type))
(fol.cons_term _ a
(fol.cons_type _ fol.nil_type)
(fol.cons_term _ _ fol.nil_type fol.nil_term)))
--> a.
[A,a] fol.apply_fun (ITE A)
(fol.cons_term bool (fol.apply_fun FALSE fol.nil_term)
(fol.cons_type _ (fol.cons_type _ fol.nil_type))
(fol.cons_term _ _
(fol.cons_type _ fol.nil_type)
(fol.cons_term _ a fol.nil_type fol.nil_term)))
--> a.
match : P : (Bool -> cc.uT) -> cc.eT (P true) -> cc.eT (P false) -> b : Bool -> cc.eT (P b).
#NAME dk_builtins.
weak_poly_var_ty : Type.
def prop := fol.prop.
def prop := dk_logic.prop.
#NAME dk_logic.
def Prop := fol.prop.
def eP : Prop -> Type := fol.proof.
def true := fol.true.
def false := fol.false.
def not := fol.not.
def and := fol.and.
def or := fol.or.
def imp := fol.imp.
def forall := fol.all.
def equal := eq.eq.
def exists := fol.ex.
def Prop := hol.term hol.bool.
def prop := hol.bool.
def eeP (b : hol.term prop) : Prop := b.
def eP := hol.proof.
def true := hol.true.
def false := hol.false.
def not := hol.not.
def and := hol.and.
def or := hol.or.
def imp := hol.imp.
def forall := hol.forall.
def equal := hol.eq.
def exists := hol.exists.
def bool := dk_bool.bool.
def ebP := dk_bool.is_true.
def eqv := fol.eqv.
def eqv_refl (A : fol.prop) : fol.proof (eqv A A) :=
fol.and_intro (fol.imp A A) (fol.imp A A) (H => H) (H => H).
def ebP (b : hol.term bool) : Prop := b.
select : A : Type -> P : (A -> dk_bool.Bool) -> A.
choice : A : Type -> P : (A -> dk_bool.Bool) ->
x : fol.term A ->
fol.proof (dk_bool.is_true (P x)) ->
fol.proof (dk_bool.is_true (P (select A P))).
def eq := hol.eq.
def eqv := hol.eq hol.bool.
def eqv_refl (A : Prop) : eP (eqv A A) := hol.REFL hol.bool A.
def select := hol.select.
choice : A : hol.type ->
P : (hol.term A -> Prop) ->
x : hol.term A ->
eP (P x) ->
eP (P (select A P)).
(; forall_type : (cc.uT -> hol.term hol.bool) -> hol.term hol.bool. ;)
(; [F] Coq.T Coq.prop (hol_to_coq.Is_true (forall_type F)) --> A : cc.uT -> hol.proof (F A). ;)
This diff is collapsed.
(; Copyright Ali Assaf <ali.assaf@inria.fr>
and Raphaël Cauderlier <raphael.cauderlier@inria.fr>, 2015
This software is governed by the CeCILL-B license under French law and
abiding by the rules of distribution of free software.
See "http://www.cecill.info". ;)
#NAME hol.
(;-----------;)
(; HOL Types ;)
(;-----------;)
def type : Type.
def bool : type.
ind : type.
def arr : type -> type -> type.
(;-----------;)
(; HOL Terms ;)
(;-----------;)
def term : type -> Type.
[a,b] term (arr a b) --> term a -> term b.
eq : a : type -> term (arr a (arr a bool)).
select : a : type -> term (arr (arr a bool) a).
(;------------;)
(; HOL Proofs ;)
(;------------;)
def proof : term bool -> Type.
REFL : a : type -> t : term a ->
proof (eq a t t).
ABS_THM : a : type -> b : type -> f : (term a -> term b) -> g : (term a -> term b) ->
(x : term a -> proof (eq b (f x) (g x))) ->
proof (eq (arr a b) f g).
APP_THM : a : type -> b : type -> f : term (arr a b) -> g : term (arr a b) -> x : term a -> y : term a ->
proof (eq (arr a b) f g) ->
proof (eq a x y) ->
proof (eq b (f x) (g y)).
PROP_EXT : p : term bool -> q : term bool ->
(proof q -> proof p) ->
(proof p -> proof q) ->
proof (eq bool p q).
EQ_MP : p : term bool -> q : term bool ->
proof (eq bool p q) ->
proof p ->
proof q.
def BETA_CONV : a : type -> b : type -> f : (term a -> term b) -> u : term a ->
proof (eq b (f u) (f u)) :=
a : type => b : type => f : (term a -> term b) => u : term a =>
REFL b (f u).
(;------------;)
(; Version 6 ;)
(;------------;)
TRANS : a : type -> x : term a -> y : term a -> z : term a -> proof (eq a x y) -> proof (eq a y z) -> proof (eq a x z).
PROVE_HYP : x : term bool -> y : term bool -> proof x -> (proof x -> proof y) -> proof y.
SYM : a : type -> x : term a -> y : term a -> proof (eq a x y) -> proof (eq a y x).
(;------------------------;)
(; Additionals for HOLALA ;)
(;------------------------;)
imp : term bool -> term bool -> term bool.
forall : a : type -> (term (arr a bool) -> (term bool)).
[p,q] proof (imp p q) --> proof p -> proof q.
[a,p] proof (forall a p) --> x : term a -> proof (p x).
(;---------------------;)
(; Derived Connectives ;)
(;---------------------;)
def true : term bool := forall bool (p : term bool => imp p p).
def false : term bool :=
forall bool (p : term bool => p).
def and (p : term bool) (q : term bool) : term bool :=
forall bool
(x : term bool => imp (imp p (imp q x)) x).
def or : term (arr bool (arr bool bool)) :=
p : term bool => q : term bool =>
forall bool (r : term bool => imp (imp p r) (imp (imp q r) r)).
def cond : a : type -> term (arr bool (arr a (arr a a))) :=
a : type => t : term bool => t1 : term a => t2 : term a =>
select a (x : term a =>
and
(imp (eq bool t true) (eq a x t1))
(imp (eq bool t false) (eq a x t2))).
def not (p : term bool) :=
imp p false.
def exists (a : type) (p : term a -> term bool) :=
forall bool (r : term bool =>
imp (forall a (x : term a => imp (p x) r))
r).
def witness : a : type -> term a.
(; := a : type => select a (x : term a => true). ;)
def true_intro : proof true := p : term bool => H : proof p => H.
def eq_sym (a : type) (x : term a) (y : term a) (h : proof (eq a x y)) : proof (eq a y x) :=
EQ_MP (eq a x x) (eq a y x)
(APP_THM a bool (eq a x) (eq a y) x x
(APP_THM a (arr a bool) (eq a) (eq a) x y
(REFL (arr a (arr a bool)) (eq a))
(h))
(REFL a x))
(REFL a x).
def eq_true_intro (p : term bool) (h : proof p) : proof (eq bool p true) :=
PROP_EXT p true (h2 : proof true => h) (h : proof p => true_intro).
def eq_true_elim (p : term bool) (h : proof (eq bool p true)) : proof p :=
EQ_MP true p (eq_sym bool p true h) true_intro.
def false_elim (p : term bool) (h : proof false) : proof p := h p.
def and_intro (p : term bool)
(q : term bool)
(Hp : proof p)
(Hq : proof q)
: proof (and p q)
:= x : term bool =>
H : proof (imp p (imp q x)) =>
H Hp Hq.
def and_elim1 (p : term bool)
(q : term bool)
(Hpq : proof (and p q))
: proof p
:=
Hpq p (Hp : proof p => Hq : proof q => Hp).
def and_elim2 (p : term bool)
(q : term bool)
(Hpq : proof (and p q))
: proof q
:=
Hpq q (Hp : proof p => Hq : proof q => Hq).
def or_intro1 (p : term bool)
(q : term bool)
(Hp : proof p)
: proof (or p q)
:=
r : term bool =>
H : proof (imp p r) =>
__ : proof (imp q r) =>
H Hp.
def or_intro2 (p : term bool)
(q : term bool)
(Hq : proof q)
: proof (or p q)
:=
r : term bool =>
__ : proof (imp p r) =>
H : proof (imp q r) =>
H Hq.
def or_elim (p : term bool)
(q : term bool)
(r : term bool)
(Hpq : proof (or p q))
(Hpr : proof p -> proof r)
(Hqr : proof q -> proof r) : proof r
:=
Hpq r Hpr Hqr.
def exists_intro (a : type)
(p : term a -> term bool)
(w : term a)
(Hw : proof (p w)) : proof (exists a p)
:=
r : term bool =>
Hall : (x : term a -> proof (p x) -> proof r) =>