Skip to content
GitLab
Commit 1783e06a authored by Raphael Cauderlier's avatar Raphael Cauderlier
Browse files

Update to dktactics v0.3

parent c1d4460a
Expand all Hide whitespace changes
Inline Side-by-side
Makefile
View file @ 1783e06a
DKTACTICS=$(shell dktactics)
DKCHECK_OPTIONS=-I $(DKTACTICS)/fol
DKCHECK_OPTIONS=-nl -I $(DKTACTICS)/fol
DKMETA_OPTIONS=$(DKCHECK_OPTIONS) -I $(DKTACTICS)/meta
DKMETA=../dedukti/dkmeta.native
DKCHECK=../dedukti/dkcheck.native
DKMETA=dkmeta
DKCHECK=dkcheck
DKMS=$(wildcard *.dkm)
DKS=$(wildcard *.dk) $(DKMS:%.dkm=%.dk)
auto.dko: auto.dk
all: $(DKS:%.dk=%.dko)
%.dko: %.dk
$(DKCHECK) -e $(DKMETA_OPTIONS) $<
transfer_def.dk: transfer_def.dkm auto.dko
%.dk: %.dkm
$(DKCHECK) $(DKMETA_OPTIONS) $< > $@
$(DKMETA) $(DKMETA_OPTIONS) $< > $@
auto.dko: auto.dk
transfer_def.dk: transfer_def.dkm auto.dko
transfer_def.dko: transfer_def.dk
$(DKCHECK) -e $(DKCHECK_OPTIONS) $<
transfer.dko: transfer.dk transfer_def.dko
$(DKCHECK) -e -nl $(DKMETA_OPTIONS) $<
nat_def.dko: nat_def.dk
$(DKCHECK) -e $(DKCHECK_OPTIONS) $<
nat_transfer_setup.dko: nat_transfer_setup.dk nat_def.dko transfer_def.dko transfer.dko
$(DKCHECK) -e $(DKMETA_OPTIONS) $<
nat_transfer.dk: nat_transfer.dkm auto.dko transfer_def.dko transfer.dko nat_transfer_setup.dko
$(DKMETA) $(DKMETA_OPTIONS) $< > $@
nat_transfer.dko: nat_transfer.dk nat_def.dko nat_transfer_setup.dko
$(DKCHECK) -e $(DKCHECK_OPTIONS) $<
clean:
rm -rf *.dko $(DKMS:.dkm=.dk)
auto.dk
View file @ 1783e06a
......@@ -2,58 +2,59 @@
(; Auto Tactic ;)
auto_exc : tac.exc.
def auto_assumption : cert.certificate -> cert.certificate.
auto_exc : mtac.exc.
def auto_assumption : tactic.tactic -> tactic.tactic.
def destruct_assumption : A : fol.prop -> fol.proof A -> fol.prop ->
cert.certificate -> cert.certificate.
tactic.tactic -> tactic.tactic.
[A,p,B,C,a] destruct_assumption A p (fol.and B C) a -->
cert.clear A (cert.destruct_and B C (cert.exact A p) a)
tactic.clear A (tactic.destruct_and B C (tactic.exact A p) a)
[A,p,B,C,a] destruct_assumption A p (fol.or B C) a -->
cert.clear A (cert.destruct_or B C (cert.exact A p) a a)
tactic.clear A (tactic.destruct_or B C (tactic.exact A p) a a)
[A,p,B,C,a] destruct_assumption A p (fol.imp B C) a -->
cert.clear A (cert.destruct_imp B C (cert.exact A p) a a)
tactic.clear A (tactic.destruct_imp B C (tactic.exact A p) a a)
[A,p,B,C,a] destruct_assumption A p (fol.ex B C) a -->
cert.clear A (cert.destruct_ex B C (cert.exact A p) a)
tactic.clear A (tactic.destruct_ex B C (tactic.exact A p) a)
[] destruct_assumption _ _ _ _ -->
cert.raise auto_exc.
tactic.raise auto_exc.
[g, G, a]
cert.run g G (auto_assumption a)
tactic.eval_tactic G g (auto_assumption a)
-->
cert.run g G (cert.try cert.assumption (__ => cert.with_assumption (A => p => destruct_assumption A p A a))).
tactic.eval_tactic G g (tactic.try tactic.assumption (__ => tactic.with_assumption (A => p => destruct_assumption A p A a))).
def auto_intro : cert.certificate -> cert.certificate.
def auto_intro : tactic.tactic -> tactic.tactic.
[a, G, B, A]
cert.run (fol.and A B) G (auto_intro a)
tactic.eval_tactic G (fol.and A B) (auto_intro a)
-->
cert.run (fol.and A B) G (cert.split a a)
tactic.eval_tactic G (fol.and A B) (tactic.split a a)
[a, G, B, A]
cert.run (fol.or A B) G (auto_intro a)
tactic.eval_tactic G (fol.or A B) (auto_intro a)
-->
cert.run (fol.or A B) G (cert.try (cert.left a) (__ => cert.right a))
tactic.eval_tactic G (fol.or A B) (tactic.try (tactic.left a) (__ => tactic.right a))
[a, G, B, A]
cert.run (fol.imp A B) G (auto_intro a)
tactic.eval_tactic G (fol.imp A B) (auto_intro a)
-->
cert.run (fol.imp A B) G (cert.intro a)
tactic.eval_tactic G (fol.imp A B) (tactic.intro a)
[a, G, B, A]
cert.run (fol.all A B) G (auto_intro a)
tactic.eval_tactic G (fol.all A B) (auto_intro a)
-->
cert.run (fol.all A B) G (cert.intro a)
[G, A] cert.run A G (auto_intro _) --> cert.run A G (cert.raise auto_exc).
tactic.eval_tactic G (fol.all A B) (tactic.intro a)
[G, A] tactic.eval_tactic G A (auto_intro _) --> tactic.eval_tactic G A (tactic.raise auto_exc).
def auto_intros : cert.certificate -> cert.certificate.
def auto_intros : tactic.tactic -> tactic.tactic.
[A, G, c]
cert.run A G (auto_intros c)
tactic.eval_tactic G A (auto_intros c)
-->
cert.run A G
(cert.try (auto_intro (auto_intros c)) (__ => c)).
tactic.eval_tactic G A
(tactic.try (auto_intro (auto_intros c)) (__ => c)).
def auto := cert.repeat (a => auto_intros (auto_assumption a)).
def auto := tactic.repeat (a => auto_intros (auto_assumption a)).
def prove (A : fol.prop) (c : cert.certificate) : fol.proof A
:=
tac.run A (cert.run A cert.nil_ctx c).
def prove := tactic.prove.
def tvar : nat.Nat -> cert.certificate.
def tvar : nat.Nat -> tactic.tactic.
#SNF A : fol.prop => prove (fol.imp A A) auto.
(; #SNF G : tactic.context => A : fol.prop => B : fol.prop => a : tactic.tactic => tactic.eval_tactic G (fol.imp A B) (tactic.intro a). ;)
\ No newline at end of file
nat_def.dk
View file @ 1783e06a
#NAME nat_def.
Nat1 : fol.type.
Nat1 : fol.sort.
ADD1 : fol.function.
[] fol.fun_arity ADD1 --> fol.read_types (nat.S (nat.S nat.O)) Nat1 Nat1.
[] fol.fun_domain ADD1 --> fol.read_sorts (nat.S (nat.S nat.O)) Nat1 Nat1.
[] fol.fun_codomain ADD1 --> Nat1.
def add1 := fol.fun_apply ADD1.
LEQ1 : fol.predicate.
[] fol.pred_arity LEQ1 --> fol.read_types (nat.S (nat.S nat.O)) Nat1 Nat1.
[] fol.pred_domain LEQ1 --> fol.read_sorts (nat.S (nat.S nat.O)) Nat1 Nat1.
def leq1 := fol.pred_apply LEQ1.
Nat2 : fol.type.
Nat2 : fol.sort.
ADD2 : fol.function.
[] fol.fun_arity ADD2 --> fol.read_types (nat.S (nat.S nat.O)) Nat2 Nat2.
[] fol.fun_domain ADD2 --> fol.read_sorts (nat.S (nat.S nat.O)) Nat2 Nat2.
[] fol.fun_codomain ADD2 --> Nat2.
def add2 := fol.fun_apply ADD2.
LEQ2 : fol.predicate.
[] fol.pred_arity LEQ2 --> fol.read_types (nat.S (nat.S nat.O)) Nat2 Nat2.
[] fol.pred_domain LEQ2 --> fol.read_sorts (nat.S (nat.S nat.O)) Nat2 Nat2.
def leq2 := fol.pred_apply LEQ2.
REL : fol.predicate.
[] fol.pred_arity REL --> fol.read_types (nat.S (nat.S nat.O)) Nat1 Nat2.
[] fol.pred_domain REL --> fol.read_sorts (nat.S (nat.S nat.O)) Nat1 Nat2.
def R (n1 : fol.term Nat1) (n2 : fol.term Nat2) := fol.pred_apply REL n1 n2.
axiom_Rsurj1 : fol.proof (fol.all Nat2 (n2 => fol.ex Nat1 (n1 => R n1 n2))).
......@@ -39,8 +39,8 @@ axiom_leq_morph2 : fol.proof (fol.all Nat2 (n2 => fol.all Nat1 (n1 => fol.imp (R
axiom_add_morph1 : fol.proof (fol.all Nat1 (n1 => fol.all Nat2 (n2 => fol.imp (R n1 n2) (fol.all Nat1 (n1' => fol.all Nat2 (n2' => fol.imp (R n1' n2') (R (add1 n1 n1') (add2 n2 n2')))))))).
axiom_add_morph2 : fol.proof (fol.all Nat2 (n2 => fol.all Nat1 (n1 => fol.imp (R n1 n2) (fol.all Nat2 (n2' => fol.all Nat1 (n1' => fol.imp (R n1' n2') (R (add1 n1 n1') (add2 n2 n2')))))))).
def commutes (A : fol.type) (f : fol.term A -> fol.term A -> fol.term A) :=
def commutes (A : fol.sort) (f : fol.term A -> fol.term A -> fol.term A) :=
fol.all A (x => fol.all A (y => eq.eq A (f x y) (f y x))).
def trans (A : fol.type) (p : fol.term A -> fol.term A -> fol.prop) :=
def trans (A : fol.sort) (p : fol.term A -> fol.term A -> fol.prop) :=
fol.all A (x => fol.all A (y => fol.all A (z => fol.imp (p x y) (fol.imp (p y z) (p x z))))).
nat_transfer.dkm
View file @ 1783e06a
......@@ -7,6 +7,6 @@
def load_setup := nat_transfer_setup.load.
def transfer_commute := auto.prove (fol.imp (nat_def.commutes nat_def.Nat1 nat_def.add1) (nat_def.commutes nat_def.Nat2 nat_def.add2)) transfer.transfer_imp_goal.
def transfer_commute := auto.prove (fol.imp (nat_def.commutes nat_def.Nat1 nat_def.add1) (nat_def.commutes nat_def.Nat2 nat_def.add2)) (transfer.transfer_imp_goal transfer.transfer_rel_ctx transfer.transfer_fun_rel_ctx).
def transfer_trans := auto.prove (fol.imp (nat_def.trans nat_def.Nat1 nat_def.leq1) (nat_def.trans nat_def.Nat2 nat_def.leq2)) transfer.transfer_imp_goal.
def transfer_trans := auto.prove (fol.imp (nat_def.trans nat_def.Nat1 nat_def.leq1) (nat_def.trans nat_def.Nat2 nat_def.leq2)) (transfer.transfer_imp_goal transfer.transfer_rel_ctx transfer.transfer_fun_rel_ctx).
nat_transfer_setup.dk
View file @ 1783e06a
......@@ -11,14 +11,14 @@ def R2 :=
transfer_def.cons_Reln
Nat1
Nat2
(fol.read_types (nat.S nat.O) Nat1)
(fol.read_types (nat.S nat.O) Nat2)
(fol.read_sorts (nat.S nat.O) Nat1)
(fol.read_sorts (nat.S nat.O) Nat2)
R
(transfer_def.cons_Reln
Nat1
Nat2
fol.nil_type
fol.nil_type
fol.nil_sort
fol.nil_sort
R
transfer_def.nil_Reln).
......@@ -26,14 +26,14 @@ def Ri2 :=
transfer_def.cons_Reln
Nat2
Nat1
(fol.read_types (nat.S nat.O) Nat2)
(fol.read_types (nat.S nat.O) Nat1)
(fol.read_sorts (nat.S nat.O) Nat2)
(fol.read_sorts (nat.S nat.O) Nat1)
Ri
(transfer_def.cons_Reln
Nat2
Nat1
fol.nil_type
fol.nil_type
fol.nil_sort
fol.nil_sort
Ri
transfer_def.nil_Reln).
......
transfer.dk
View file @ 1783e06a
This diff is collapsed.
transfer_def.dkm
View file @ 1783e06a
......@@ -5,30 +5,30 @@
(setq-local dedukti-check-options `("-nc" "-I" ,(concat dktactics "/fol") "-I" ,(concat dktactics "/meta") "-coc"))
;)
def Rel (A : fol.type) (B : fol.type) : Type
def Rel (A : fol.sort) (B : fol.sort) : Type
:= fol.term A -> fol.term B -> fol.prop.
(; If As and Bs have the same length then Reln As Bs is a list of relations between the As and the Bs ;)
Reln : fol.types -> fol.types -> Type.
nil_Reln : Reln fol.nil_type fol.nil_type.
cons_Reln : A : fol.type -> B : fol.type -> As : fol.types -> Bs : fol.types ->
Reln : fol.sorts -> fol.sorts -> Type.
nil_Reln : Reln fol.nil_sort fol.nil_sort.
cons_Reln : A : fol.sort -> B : fol.sort -> As : fol.sorts -> Bs : fol.sorts ->
Rel A B -> Reln As Bs ->
Reln (fol.cons_type A As) (fol.cons_type B Bs).
Reln (fol.cons_sort A As) (fol.cons_sort B Bs).
def Reln_apply : As : fol.types -> Bs : fol.types -> Rs : Reln As Bs -> fol.terms As -> fol.terms Bs -> fol.prop.
[] Reln_apply fol.nil_type fol.nil_type nil_Reln fol.nil_term fol.nil_term --> fol.true
[A,As,B,Bs,R,Rs,a,as,b,bs] Reln_apply (fol.cons_type A As) (fol.cons_type B Bs) (cons_Reln _ _ _ _ R Rs) (fol.cons_term _ a _ as) (fol.cons_term _ b _ bs) --> fol.and (R a b) (Reln_apply As Bs Rs as bs).
def Reln_apply : As : fol.sorts -> Bs : fol.sorts -> Rs : Reln As Bs -> fol.terms As -> fol.terms Bs -> fol.prop.
[] Reln_apply fol.nil_sort fol.nil_sort nil_Reln fol.nil_term fol.nil_term --> fol.true
[A,As,B,Bs,R,Rs,a,as,b,bs] Reln_apply (fol.cons_sort A As) (fol.cons_sort B Bs) (cons_Reln _ _ _ _ R Rs) (fol.cons_term _ a _ as) (fol.cons_term _ b _ bs) --> fol.and (R a b) (Reln_apply As Bs Rs as bs).
def Rarrs : As : fol.types -> Bs : fol.types -> A : fol.type -> B : fol.type ->
def Rarrs : As : fol.sorts -> Bs : fol.sorts -> A : fol.sort -> B : fol.sort ->
Reln As Bs -> Rel A B -> (fol.terms As -> fol.term A) -> (fol.terms Bs -> fol.term B) -> fol.prop.
[A,B,R,f,g] Rarrs fol.nil_type fol.nil_type A B nil_Reln R f g -->
[A,B,R,f,g] Rarrs fol.nil_sort fol.nil_sort A B nil_Reln R f g -->
R (f fol.nil_term) (g fol.nil_term)
[A,As,B,Bs,A',B',R,Rs,R',f,g] Rarrs (fol.cons_type A As) (fol.cons_type B Bs) A' B' (cons_Reln _ _ _ _ R Rs) R' f g -->
[A,As,B,Bs,A',B',R,Rs,R',f,g] Rarrs (fol.cons_sort A As) (fol.cons_sort B Bs) A' B' (cons_Reln _ _ _ _ R Rs) R' f g -->
fol.all A (a => fol.all B (b => fol.imp (R a b) (Rarrs As Bs A' B' Rs R' (l => f (fol.cons_term A a As l)) (l => g (fol.cons_term B b Bs l))))).
def Rpred : As : fol.types -> Bs : fol.types -> Reln As Bs -> (fol.terms As -> fol.prop) -> (fol.terms Bs -> fol.prop) -> fol.prop.
[f,g] Rpred fol.nil_type fol.nil_type nil_Reln f g --> fol.imp (f fol.nil_term) (g fol.nil_term)
[A,As,B,Bs,R,Rs,f,g] Rpred (fol.cons_type A As) (fol.cons_type B Bs) (cons_Reln _ _ _ _ R Rs) f g
def Rpred : As : fol.sorts -> Bs : fol.sorts -> Reln As Bs -> (fol.terms As -> fol.prop) -> (fol.terms Bs -> fol.prop) -> fol.prop.
[f,g] Rpred fol.nil_sort fol.nil_sort nil_Reln f g --> fol.imp (f fol.nil_term) (g fol.nil_term)
[A,As,B,Bs,R,Rs,f,g] Rpred (fol.cons_sort A As) (fol.cons_sort B Bs) (cons_Reln _ _ _ _ R Rs) f g
-->
fol.all A (a => fol.all B (b => fol.imp (R a b) (Rpred As Bs Rs (l => f (fol.cons_term A a As l)) (l => g (fol.cons_term B b Bs l))))).
......@@ -71,7 +71,7 @@ def imp_increase (A : fol.prop) (B : fol.prop) (C : fol.prop) (D : fol.prop) :
(; For this one, we would need unification to find the assumption to
apply, it is simpler to give the proof term until dktactics can handle
this. ;)
def all_increase (A : fol.type) (C : fol.type)
def all_increase (A : fol.sort) (C : fol.sort)
(B : fol.term A -> fol.prop)
(D : fol.term C -> fol.prop)
(R : Rel A C)
......@@ -82,7 +82,7 @@ def all_increase (A : fol.type) (C : fol.type)
:=
H2 c (D c) (a => Ha => H1 a c Ha (H3 a)).
def ex_increase (A : fol.type) (C : fol.type)
def ex_increase (A : fol.sort) (C : fol.sort)
(B : fol.term A -> fol.prop)
(D : fol.term C -> fol.prop)
(R : Rel A C)
......@@ -93,7 +93,7 @@ def ex_increase (A : fol.type) (C : fol.type)
:=
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 -> Bs : fol.types ->
def pred_increase : As : fol.sorts -> Bs : fol.sorts ->
Rs : Reln As Bs ->
P : (fol.terms As -> fol.prop) ->
Q : (fol.terms Bs -> fol.prop) ->
......@@ -102,8 +102,8 @@ def pred_increase : As : fol.types -> Bs : fol.types ->
fol.proof (Rpred As Bs Rs P Q) ->
fol.proof (Reln_apply As Bs Rs as bs) ->
fol.proof (P as) -> fol.proof (Q bs).
[H1,H2] pred_increase fol.nil_type fol.nil_type nil_Reln _ _ fol.nil_term fol.nil_term H1 _ H2 --> H1 H2.
[A,As,B,Bs,R,Rs,P,Q,H1,a,as,b,bs,H2,H3] pred_increase (fol.cons_type A As) (fol.cons_type B Bs) (cons_Reln _ _ _ _ R Rs) P Q (fol.cons_term _ a _ as) (fol.cons_term _ b _ bs) H1 H2 H3 -->
[H1,H2] pred_increase fol.nil_sort fol.nil_sort nil_Reln _ _ fol.nil_term fol.nil_term H1 _ H2 --> H1 H2.
[A,As,B,Bs,R,Rs,P,Q,H1,a,as,b,bs,H2,H3] pred_increase (fol.cons_sort A As) (fol.cons_sort B Bs) (cons_Reln _ _ _ _ R Rs) P Q (fol.cons_term _ a _ as) (fol.cons_term _ b _ bs) H1 H2 H3 -->
H2 (Q (fol.cons_term B b Bs bs))
(HR : fol.proof (R a b) =>
HRs : fol.proof (Reln_apply As Bs Rs as bs) =>
......@@ -111,8 +111,8 @@ def pred_increase : As : fol.types -> Bs : fol.types ->
def fun_increase : As : fol.types -> A : fol.type ->
Bs : fol.types -> B : fol.type ->
def fun_increase : As : fol.sorts -> A : fol.sort ->
Bs : fol.sorts -> B : fol.sort ->
Rs : Reln As Bs -> R : Rel A B ->
f : (fol.terms As -> fol.term A) ->
g : (fol.terms Bs -> fol.term B) ->
......@@ -121,11 +121,18 @@ def fun_increase : As : fol.types -> A : fol.type ->
fol.proof (Rarrs As Bs A B Rs R f g) ->
fol.proof (Reln_apply As Bs Rs as bs) ->
fol.proof (R (f as) (g bs)).
[H1,H2] fun_increase fol.nil_type _ fol.nil_type _ nil_Reln _ _ _ fol.nil_term fol.nil_term H1 _ --> H1.
[H1,H2] fun_increase fol.nil_sort _ fol.nil_sort _ nil_Reln _ _ _ fol.nil_term fol.nil_term H1 _ --> H1.
[A,As,A',B,Bs,B',R,Rs,R',f,g,a,as,b,bs,H1,H2]
fun_increase (fol.cons_type A As) A' (fol.cons_type B Bs) B' (cons_Reln _ _ _ _ R Rs) R' f g (fol.cons_term _ a _ as) (fol.cons_term _ b _ bs) H1 H2 -->
fun_increase (fol.cons_sort A As) A' (fol.cons_sort B Bs) B' (cons_Reln _ _ _ _ R Rs) R' f g (fol.cons_term _ a _ as) (fol.cons_term _ b _ bs) H1 H2 -->
H2 (R' (f (fol.cons_term A a As as)) (g (fol.cons_term B b Bs bs)))
(HR : fol.proof (R a b) =>
HRs : fol.proof (Reln_apply As Bs Rs as bs) =>
fun_increase As A' Bs B' Rs R' (l => f (fol.cons_term A a As l)) (l => g (fol.cons_term B b Bs l)) as bs (H1 a b HR) HRs).
def Rel1 (A : fol.sort) (B : fol.sort) (R : fol.term A -> fol.term B -> fol.prop) :
Reln (fol.cons_sort A fol.nil_sort) (fol.cons_sort B fol.nil_sort) :=
cons_Reln A B fol.nil_sort fol.nil_sort R nil_Reln.
def Rel2 (A : fol.sort) (B : fol.sort) (R : fol.term A -> fol.term B -> fol.prop) :
Reln (fol.cons_sort A (fol.cons_sort A fol.nil_sort)) (fol.cons_sort B (fol.cons_sort B fol.nil_sort)) :=
cons_Reln A B (fol.cons_sort A fol.nil_sort) (fol.cons_sort B fol.nil_sort) R (Rel1 A B R).
Supports Markdown
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