...
 
Commits (8)
.config_vars
*/*.dko
*/*.dk.depend
**/*.dko
**/*.dk.depend
dktactics
\#*
\ No newline at end of file
......@@ -3,7 +3,7 @@
INSTALL_BIN_DIR=/usr/local/bin
INSTALL_LIB_DIR=/usr/local/lib/dedukti/dktactics
SUBDIRS= fol meta example
SUBDIRS= fol meta prettyprint ugly example
# To activate confluence checking, set this to "--with-confluence-checking"
CONFIGURE_FLAGS=
......
......@@ -7,7 +7,7 @@ print_to_file ()
print_to_stderr ()
{
echo "$1" > /dev/stderr
echo "$1" 1>&2
}
find_binary () {
......
......@@ -18,10 +18,6 @@ def fun_apply := fol.fun_apply.
def read_sorts := fol.read_sorts.
def nil_sort := fol.nil_sort.
def 0 := nat.O.
def 1 := nat.S 0.
def 2 := nat.S 1.
(; Signature ;)
A : sort.
LEQ : predicate.
......
......@@ -18,7 +18,7 @@ def Joe : fol.term BAR := fol.fun_apply JOE.
(; The "drink" predicate. ;)
DRINK : fol.predicate.
[] fol.pred_domain DRINK --> fol.read_sorts (nat.S nat.O) BAR.
[] fol.pred_domain DRINK --> fol.read_sorts 1 BAR.
def drink (x : fol.term BAR) : fol.prop := fol.pred_apply DRINK x.
def drinker_statement : fol.prop :=
......
include ../../.config_vars
# Dedukti files
DKMS = $(wildcard *.dkm)
DKS = $(DKMS:.dkm=.dk)
DKOS = $(DKS:.dk=.dko)
DKCHECK_OPTIONS = -I ../../fol
DKMETA_OPTIONS = -I ../../fol -I ../../meta -nl
all: $(DKOS)
%.dk: %.dkm1
$(DKCHECK) $(DKMETA_OPTIONS) -I ../../prettyprint $< > $@
$(DKMETA) $(DKMETA_OPTIONS) -I ../../prettyprint $< > $@
%.dko:
$(DKCHECK) -e $(DKCHECK_OPTIONS) $<
%.dkm1: %.dkm
$(DKMETA) $(DKMETA_OPTIONS) -I ../../ugly $< > $@
%.dkmo: %.dkm
$(DKCHECK) $(DKMETA_OPTIONS) -I ../../ugly $<
# For each dependency foo.dko in the ../fol directory, the previous
# rule will try to create foo.dko here by calling "dkcheck -e" without
# file argument. This actually succeeds but does not produce any file.
# foo.dk.depend lists the modules foo depends on
%.dk.depend: %.dkm
$(DKDEP) $< | sed "s/\.dkm/\.dk/" > $@
DKDEPENDS = $(DKS:.dk=.dk.depend)
-include $(DKDEPENDS)
depend: $(DKDEPENDS)
clean:
rm -f *.dko *.dk *.dkm1 *.depend
install: all
mkdir -p $(INSTALL_LIB_DIR)
install -t $(INSTALL_LIB_DIR) $(DKOS)
uninstall:
for f in $(DKOS); do \
rm -f $(INSTALL_LIB_DIR)/$$f; \
done
rmdir $(INSTALL_LIB_DIR)
.PHONY: clean depend install uninstall all
#NAME andcomm.
A : fol.prop.
B : fol.prop.
load_pretty : pretty.pretty_load.
def t : nat -> tactic.tactic.
[] pp.pp_prop _ _ A --> "A".
[] pp.pp_prop _ _ B --> "B".
[] t 0 --> tactic.intro (t 1).
[] t 1 --> tactic.destruct_and A B (t 2) (t 3).
[] t 2 --> tactic.assumption.
[] t 3 --> tactic.split (t 4) (t 5).
[] t 4 --> tactic.assumption.
[] t 5 --> tactic.assumption.
def and_commutes := tactic.prove (fol.imp (fol.and A B) (fol.and B A)) (t 0).
#NAME plus_comm.
(; Theory ;)
NAT : fol.sort.
O : fol.function.
[] fol.fun_domain O --> fol.nil_sort.
[] fol.fun_codomain O --> NAT.
def o : fol.term NAT := fol.fun_apply O.
SUCC : fol.function.
[] fol.fun_domain SUCC --> fol.read_sorts 1 NAT.
[] fol.fun_codomain SUCC --> NAT.
def succ (n : fol.term NAT) : fol.term NAT := fol.fun_apply SUCC n.
PLUS : fol.function.
[] fol.fun_domain PLUS --> fol.read_sorts 2 NAT NAT.
[] fol.fun_codomain PLUS --> NAT.
def plus (a : fol.term NAT) (b : fol.term NAT) := fol.fun_apply PLUS a b.
(; plus 0 n --> n ;)
[n] fol.apply_fun PLUS
(fol.cons_term _ (fol.apply_fun O fol.nil_term) _
(fol.cons_term _ n _ fol.nil_term)) -->
n
(; plus (succ m) n --> succ (plus m n) ;)
[m,n] fol.apply_fun PLUS
(fol.cons_term _ (fol.apply_fun SUCC
(fol.cons_term _ m _ fol.nil_term)) _
(fol.cons_term _ n _ fol.nil_term)) -->
succ (plus m n).
def induction_statement (P : fol.term NAT -> fol.prop) : fol.prop :=
fol.imp (P o) (
fol.imp (fol.all NAT (n => fol.imp (P n) (P (succ n)))) (
fol.all NAT P)).
induction_axiom :
P : (fol.term NAT -> fol.prop) ->
fol.proof (induction_statement P).
(; Custom Tactics ;)
def match_all_NAT : fol.prop ->
((fol.term NAT -> fol.prop) -> tactic.tactic) ->
tactic.tactic -> tactic.tactic.
[P,t1] match_all_NAT (fol.all NAT P) t1 _ --> t1 P.
induction_failure : mtac.exc.
def induction_tactic (t0 : tactic.tactic) (tS : tactic.tactic) : tactic.tactic :=
tactic.with_goal (G =>
match_all_NAT G (P =>
tactic.refine2 (P o) (fol.all NAT (n => fol.imp (P n) (P (succ n))))
(fol.all NAT P)
(induction_axiom P) t0 tS)
(tactic.raise induction_failure)).
def match_plus : fol.term NAT -> (fol.term NAT -> fol.term NAT -> tactic.tactic) -> tactic.tactic.
[a,b,f] match_plus (fol.apply_fun PLUS
(fol.cons_term _ a _
(fol.cons_term _ b _ fol.nil_term))) f --> f a b.
(; Pretty-printing ;)
load_pretty : pretty.pretty_load.
[] pp.pp_sort NAT --> "nat".
[] pp.pp_fun PLUS --> "+".
[] pp.pp_fun O --> "0".
[] pp.pp_fun SUCC --> "succ".
(; Interactive Proof ;)
def t : nat -> tactic.tactic.
def u : nat -> fol.term NAT -> tactic.tactic.
[] t 0 --> induction_tactic (t 1) (t 2).
[] t 1 --> induction_tactic (t 3) (t 4).
[] t 2 --> tactic.lintro "a" NAT (a => u 0 a).
induction_tactic
(induction_tactic
eqtac.reflexivity
(tactic.lintro "a" NAT (a =>
tactic.intro (eqtac.f_equal SUCC tactic.assumption))))
(tactic.lintro "a" NAT (a =>
tactic.intro
(induction_tactic
(eqtac.f_equal SUCC
(tactic.apply NAT (x => eq.eq NAT (plus a x) (plus x a))
o tactic.assumption))
(tactic.lintro "b" NAT (b =>
tactic.intro
(eqtac.f_equal SUCC
(eqtac.transitivity NAT (succ (plus a b))
(eqtac.transitivity NAT (succ (plus b a))
(tactic.apply NAT (x => eq.eq NAT (plus a x) (plus x a))
(succ b) tactic.assumption)
(eqtac.f_equal SUCC
(tactic.apply NAT (x => eq.eq NAT (plus a x) (plus x a))
b tactic.assumption)))
tactic.assumption))))))).
def plus_comm : fol.proof (fol.all NAT (m => fol.all NAT (n => eq.eq NAT (plus m n) (plus n m)))) := tactic.prove (fol.all NAT (m => fol.all NAT (n => eq.eq NAT (plus m n) (plus n m)))) (t 0).
#NAME plus_zero.
(; This example illustrates Deduction Modulo ;)
(; We start by an encoding of the following theory of Peano addition:
NAT : sort.
o : NAT.
succ : NAT -> NAT.
plus : NAT -> NAT -> NAT.
[n] plus o n --> n
[m,n] plus (succ m) n --> succ (plus m n)
induction_axiom (P : NAT -> prop) :
P o -> (n : NAT -> P n -> P (succ n)) -> n : NAT -> P n.
;)
NAT : fol.sort.
O : fol.function.
[] fol.fun_domain O --> fol.nil_sort.
[] fol.fun_codomain O --> NAT.
def o : fol.term NAT := fol.fun_apply O.
SUCC : fol.function.
[] fol.fun_domain SUCC --> fol.read_sorts 1 NAT.
[] fol.fun_codomain SUCC --> NAT.
def succ (n : fol.term NAT) : fol.term NAT := fol.fun_apply SUCC n.
PLUS : fol.function.
[] fol.fun_domain PLUS --> fol.read_sorts 2 NAT NAT.
[] fol.fun_codomain PLUS --> NAT.
def plus (a : fol.term NAT) (b : fol.term NAT) := fol.fun_apply PLUS a b.
(; plus 0 n --> n ;)
[n] fol.apply_fun PLUS
(fol.cons_term _ (fol.apply_fun O fol.nil_term) _
(fol.cons_term _ n _ fol.nil_term)) -->
n
(; plus (succ m) n --> succ (plus m n) ;)
[m,n] fol.apply_fun PLUS
(fol.cons_term _ (fol.apply_fun SUCC
(fol.cons_term _ m _ fol.nil_term)) _
(fol.cons_term _ n _ fol.nil_term)) -->
succ (plus m n).
def induction_statement (P : fol.term NAT -> fol.prop) : fol.prop :=
fol.imp (P o) (
fol.imp (fol.all NAT (n => fol.imp (P n) (P (succ n)))) (
fol.all NAT P)).
induction_axiom :
P : (fol.term NAT -> fol.prop) ->
fol.proof (induction_statement P).
(; Custom Tactics ;)
(; Tactic matching formulae of the form (fol.all NAT P) ;)
def match_all_NAT (a : fol.prop)
(t0 : (fol.term NAT -> fol.prop) -> tactic.tactic)
(t1 : tactic.tactic) : tactic.tactic :=
tactic.match_all a (A => P => tactic.ifeq_sort NAT A (NAT2A =>
t0 (x => P (NAT2A x))) t1) t1.
induction_failure : mtac.exc.
(; induction_tactic t0 t1 proves G |- ∀n:NAT, P n if t0 proves G |- P 0 and
t1 proves G |- ∀n:NAT, P n → P (succ n) ;)
def induction_tactic (t0 : tactic.tactic) (tS : tactic.tactic) : tactic.tactic :=
tactic.with_goal (G =>
match_all_NAT G (P =>
tactic.refine2 (P o) (fol.all NAT (n => fol.imp (P n) (P (succ n))))
(fol.all NAT P)
(induction_axiom P) t0 tS)
(tactic.raise induction_failure)).
(; Pretty-printing ;)
load_pretty : pretty.pretty_load.
[] pp.pp_sort NAT --> "NAT".
[] pp.pp_fun PLUS --> "PLUS".
[] pp.pp_fun O --> "O".
[] pp.pp_fun SUCC --> "SUCC".
(; Interactive Proof ;)
def t : nat -> tactic.tactic.
[] t 0 --> induction_tactic
eqtac.reflexivity
(tactic.lintro "n" NAT (n =>
tactic.intro (
eqtac.f_equal SUCC
tactic.assumption))).
def plus_zero_statement : fol.prop := fol.all NAT (n => eq.eq NAT (plus n o) n).
def plus_zero : fol.proof plus_zero_statement :=
tactic.prove plus_zero_statement (t 0).
......@@ -18,9 +18,6 @@ def fun_apply := fol.fun_apply.
def read_sorts := fol.read_sorts.
def nil_sort := fol.nil_sort.
def 0 := nat.O.
def 1 := nat.S 0.
(; Signature ;)
A : sort.
P : predicate.
......@@ -28,13 +25,13 @@ P : predicate.
O : function.
[] fol.fun_domain O --> nil_sort.
[] fol.fun_codomain O --> A.
S : function.
[] fol.fun_domain S --> read_sorts 1 A.
[] fol.fun_codomain S --> A.
S_ : function.
[] fol.fun_domain S_ --> read_sorts 1 A.
[] fol.fun_codomain S_ --> A.
def p : term A -> prop := pred_apply P.
def o : term A := fun_apply O.
def s : term A -> term A := fun_apply S.
def s : term A -> term A := fun_apply S_.
(; Axioms ;)
def A0 := p o.
......
......@@ -14,9 +14,15 @@ DKDEP_OPTIONS =
all: $(DKOS)
builtins.dko: builtins.dk
$(DKCHECK) -e $(DKCHECK_CONFLUENCE_OPTION) $(DKCHECK_OPTIONS) -nk $<
%.dko:
$(DKCHECK) -e $(DKCHECK_CONFLUENCE_OPTION) $(DKCHECK_OPTIONS) $<
builtins.dk.depend: builtins.dk
echo > $@
# foo.dk.depend lists the modules foo depends on
%.dk.depend: %.dk
$(DKDEP) $(DKDEP_OPTIONS) $< > $@
......
#NAME builtins.
nat : Type.
0 : nat.
S : nat -> nat.
char : Type.
char_of_nat : nat -> char.
string : Type.
string_nil : string.
string_cons : char -> string -> string.
......@@ -23,12 +23,9 @@ def fun_domain := fol.fun_domain.
def fun_codomain := fol.fun_codomain.
def apply_fun := fol.apply_fun.
def O := nat.O.
def S := nat.S.
(; Equality is a family of binary predicate symbols. ;)
Eq : sort -> predicate.
[A] fol.pred_domain (Eq A) --> read_sorts (S (S O)) A A.
[A] fol.pred_domain (Eq A) --> read_sorts 2 A A.
def eq (A : sort) : term A -> term A -> prop := pred_apply (Eq A).
[A,x,y]
......@@ -109,7 +106,7 @@ def fun_eq : L : sorts -> B : sort -> (terms L -> term B) -> (terms L -> term B)
def eq_fun_eq : L : sorts -> B : sort -> f : (terms L -> term B) -> proof (fun_eq L B f f).
[B,b] eq_fun_eq fol.nil_sort B b --> fol.all_elim B (x => eq B x x) (eq_refl B) (b nil_term)
[A,L,B,f,f'] eq_fun_eq (fol.cons_sort A L) B f -->
[A,L,B,f] eq_fun_eq (fol.cons_sort A L) B f -->
fol.all_intro A (x => all A (y => imp (eq A x y) (fun_eq L B (l : terms L => f (cons_term A x L l)) (l : terms L => f (cons_term A y L l)))))
(x =>
fol.all_intro A (y => imp (eq A x y) (fun_eq L B (l : terms L => f (cons_term A x L l)) (l : terms L => f (cons_term A y L l))))
......
......@@ -17,12 +17,12 @@ cons_sort : sort -> sorts -> sorts.
cons_sort A1 (cons_sort A2 (... cons_sort An nil_sort))
;)
def nat := nat.Nat.
(; The type of the read_sorts function is defined inductively ;)
def read_sorts_T : nat -> Type.
[] read_sorts_T nat.O --> sorts.
[n] read_sorts_T (nat.S n) --> sort -> read_sorts_T n.
[] read_sorts_T 0 --> sorts.
[n] read_sorts_T (S n) --> sort -> read_sorts_T n.
(; Adding an element to the tail of a list of sorts:
snoc_sort [A1 .. An] B = [A1 .. An B] ;)
......@@ -34,9 +34,9 @@ def snoc_sort : sorts -> sort -> sorts.
read_tyes_acc m [A1 .. An] B1 .. Bm = [A1 .. An B1 .. Bm]
;)
def read_sorts_acc : n : nat -> sorts -> read_sorts_T n.
[acc] read_sorts_acc nat.O acc --> acc
[acc] read_sorts_acc 0 acc --> acc
[n,acc]
read_sorts_acc (nat.S n) acc
read_sorts_acc (S n) acc
--> t : sort => read_sorts_acc n (snoc_sort acc t).
(; read_sorts n A1 .. An = [A1 .. An] ;)
......@@ -58,9 +58,9 @@ cons_term : A : sort -> term A ->
tail_types : sorts ->
terms tail_types ->
terms (cons_sort A tail_types).
apply_fun : f : function ->
terms (fun_domain f) ->
term (fun_codomain f).
def apply_fun : f : function ->
terms (fun_domain f) ->
term (fun_codomain f).
(; To limit the number of parentheses when writing function
applications, we derive an nary application fun_apply ;)
......@@ -117,31 +117,31 @@ def eqv (p : prop) (q : prop) := and (imp p q) (imp q p).
def nand_list : props -> prop.
[] nand_list nil_prop --> true
[A] nand_list (cons_prop A nil_prop) --> A
[A1,A2,As] nand_list (cons_prop A1 (cons_prop A2 nil_prop))
--> and A1 (nand_list (cons_prop A2 nil_prop)).
[A1,A2,As] nand_list (cons_prop A1 (cons_prop A2 As))
--> and A1 (nand_list (cons_prop A2 As)).
(; nand_type n == propⁿ -> prop ;)
def nand_type : nat -> Type.
[] nand_type nat.O --> prop
[n] nand_type (nat.S n) --> prop -> nand_type n.
[] nand_type 0 --> prop
[n] nand_type (S n) --> prop -> nand_type n.
(; nand_aux [B₁; …; Bₘ] n A₁ … Aₙ == nand_list [B₁; …; Bₘ; A₁; …; Aₙ]
== B₁ ∧ … ∧ Bₘ ∧ A₁ ∧ … ∧ Aₙ ;)
def nand_aux : props -> n : nat -> nand_type n.
[Bs] nand_aux Bs nat.O --> nand_list Bs
[Bs,n] nand_aux Bs (nat.S n) --> A => nand_aux (snoc_prop Bs A) n.
[Bs] nand_aux Bs 0 --> nand_list Bs
[Bs,n] nand_aux Bs (S n) --> A => nand_aux (snoc_prop Bs A) n.
def nand : n : nat -> nand_type n := nand_aux nil_prop.
def nor_list : props -> prop.
[] nor_list nil_prop --> false
[A] nor_list (cons_prop A nil_prop) --> A
[A1,A2,As] nor_list (cons_prop A1 (cons_prop A2 nil_prop))
--> or A1 (nor_list (cons_prop A2 nil_prop)).
[A1,A2,As] nor_list (cons_prop A1 (cons_prop A2 As))
--> or A1 (nor_list (cons_prop A2 As)).
def nor_aux : props -> n : nat -> nand_type n.
[Bs] nor_aux Bs nat.O --> nor_list Bs
[Bs,n] nor_aux Bs (nat.S n) --> A => nor_aux (snoc_prop Bs A) n.
[Bs] nor_aux Bs 0 --> nor_list Bs
[Bs,n] nor_aux Bs (S n) --> A => nor_aux (snoc_prop Bs A) n.
def nor : n : nat -> nand_type n := nor_aux nil_prop.
......@@ -149,11 +149,11 @@ def nimp_list : props -> prop -> prop.
[B] nimp_list nil_prop B --> B
[A,As,B] nimp_list (cons_prop A As) B --> imp A (nimp_list As B).
def nimp_aux : props -> n : nat -> nand_type (nat.S n).
[Bs] nimp_aux Bs nat.O --> A => nimp_list Bs A
[Bs,n] nimp_aux Bs (nat.S n) --> A => nimp_aux (snoc_prop Bs A) n.
def nimp_aux : props -> n : nat -> nand_type (S n).
[Bs] nimp_aux Bs 0 --> A => nimp_list Bs A
[Bs,n] nimp_aux Bs (S n) --> A => nimp_aux (snoc_prop Bs A) n.
def nimp : n : nat -> nand_type (nat.S n) := nimp_aux nil_prop.
def nimp : n : nat -> nand_type (S n) := nimp_aux nil_prop.
(; nall n A₁ A₂ … Aₙ (a₁ : term A₁ => a₂ : term A₂ => … => aₙ : term Aₙ => P a₁ a₂ … aₙ)
==
......@@ -165,26 +165,26 @@ def nall_aux_type : sorts -> Type.
[A,As] nall_aux_type (cons_sort A As) --> term A -> nall_aux_type As.
def nall_aux : As : sorts -> nall_aux_type As -> prop.
[P] nall_aux nil_sort --> P => P.
[A,As,P] nall_aux (cons_sort A As) --> P => all A (a => nall_aux As (P a)).
[] nall_aux nil_sort --> P => P.
[A,As] nall_aux (cons_sort A As) --> P => all A (a => nall_aux As (P a)).
def nex_aux : As : sorts -> nall_aux_type As -> prop.
[P] nex_aux nil_sort --> P => P.
[A,As,P] nex_aux (cons_sort A As) --> P => ex A (a => nex_aux As (P a)).
[] nex_aux nil_sort --> P => P.
[A,As] nex_aux (cons_sort A As) --> P => ex A (a => nex_aux As (P a)).
(; nall_aux2 [B₁; …; Bₘ] n A₁ … Aₙ = nall_aux [B₁; …; Bₘ; A₁; …; Aₙ] ;)
(; nall_aux2_type Bs n A₁ … Aₙ = nall_aux_type (Bs^As) -> prop ;)
def nall_aux2_type : sorts -> nat -> Type.
[Bs] nall_aux2_type Bs nat.O --> nall_aux_type Bs -> prop
[Bs,n] nall_aux2_type Bs (nat.S n) --> A : sort -> nall_aux2_type (snoc_sort Bs A) n.
[Bs] nall_aux2_type Bs 0 --> nall_aux_type Bs -> prop
[Bs,n] nall_aux2_type Bs (S n) --> A : sort -> nall_aux2_type (snoc_sort Bs A) n.
def nall_aux2 : Bs : sorts -> n : nat -> nall_aux2_type Bs n.
[Bs] nall_aux2 Bs nat.O --> nall_aux Bs
[Bs,n] nall_aux2 Bs (nat.S n) --> A => nall_aux2 (snoc_sort Bs A) n.
[Bs] nall_aux2 Bs 0 --> nall_aux Bs
[Bs,n] nall_aux2 Bs (S n) --> A => nall_aux2 (snoc_sort Bs A) n.
def nex_aux2 : Bs : sorts -> n : nat -> nall_aux2_type Bs n.
[Bs] nex_aux2 Bs nat.O --> nex_aux Bs
[Bs,n] nex_aux2 Bs (nat.S n) --> A => nex_aux2 (snoc_sort Bs A) n.
[Bs] nex_aux2 Bs 0 --> nex_aux Bs
[Bs,n] nex_aux2 Bs (S n) --> A => nex_aux2 (snoc_sort Bs A) n.
def nall (n : nat) : nall_aux2_type nil_sort n := nall_aux2 nil_sort n.
def nex (n : nat) : nall_aux2_type nil_sort n := nex_aux2 nil_sort n.
......
#NAME nat.
Nat : Type.
O : Nat.
S : Nat -> Nat.
......@@ -21,35 +21,35 @@ ONE : fol.function.
ADD : fol.function.
(; Arities ;)
[] fol.pred_domain EQ --> fol.read_sorts (nat.S (nat.S nat.O)) Nat Nat.
[] fol.pred_domain EQ --> fol.read_sorts 2 Nat Nat.
[] fol.fun_domain ZERO --> fol.nil_sort.
[] fol.fun_domain ONE --> fol.nil_sort.
[] fol.fun_domain ADD --> fol.read_sorts (nat.S (nat.S nat.O)) Nat Nat.
[] fol.fun_domain ADD --> fol.read_sorts 2 Nat Nat.
[] fol.fun_codomain ZERO --> Nat.
[] fol.fun_codomain ONE --> Nat.
[] fol.fun_codomain ADD --> Nat.
(; Abbreviations ;)
def eq := fol.pred_apply EQ.
def 0 := fol.fun_apply ZERO.
def 1 := fol.fun_apply ONE.
def 0_ := fol.fun_apply ZERO.
def 1_ := fol.fun_apply ONE.
def add := fol.fun_apply ADD.
def succ (x : fol.term Nat) := add x 1.
def succ (x : fol.term Nat) := add x 1_.
(; Axioms ;)
(; 0 != x + 1 ;)
P1 : fol.proof (fol.all Nat (x => fol.not (eq 0 (succ x)))).
P1 : fol.proof (fol.all Nat (x => fol.not (eq 0_ (succ x)))).
(; x+1 = y+1 -> x = y ;)
P2 : fol.proof (fol.all Nat (x => fol.all Nat (y => fol.imp (eq (succ x) (succ y)) (eq x y)))).
(; x+0 = x ;)
P3 : fol.proof (fol.all Nat (x => eq (add x 0) x)).
P3 : fol.proof (fol.all Nat (x => eq (add x 0_) x)).
(; x + (y + 1) = (x + y) + 1 ;)
P4 : fol.proof (fol.all Nat (x => fol.all Nat (y => eq (add x (succ y)) (succ (add x y))))).
(; Axiom schema of induction ;)
P5 : p : (fol.term Nat -> fol.prop) ->
fol.proof (fol.imp (fol.and (p 0) (fol.all Nat (x => fol.imp (p x) (p (succ x))))) (fol.all Nat p)).
\ No newline at end of file
fol.proof (fol.imp (fol.and (p 0_) (fol.all Nat (x => fol.imp (p x) (p (succ x))))) (fol.all Nat p)).
\ No newline at end of file
......@@ -182,11 +182,11 @@ def f_equal_fun_n : L' : fol.sorts ->
L : fol.sorts ->
certificates L ->
f_equal_T L'.
[L,B,f,as,bs,cs]
[L,cs]
f_equal_fun_n fol.nil_sort L cs
-->
f_equal_fun_on_goal L cs
[A,As,L,B,f,as,bs,cs]
[A,As,L,cs]
f_equal_fun_n (fol.cons_sort A As) L cs
-->
c : tactic =>
......
#NAME pp.
def sort := fol.sort.
def function := fol.function.
def predicate := fol.predicate.
def term := fol.term.
def sorts := fol.sorts.
def terms := fol.terms.
def fun_domain := fol.fun_domain.
def prop := fol.prop.
def pred_domain := fol.pred_domain.
def ctx := tactic.context.
def tactic := tactic.tactic.
def mtac := mtac.mtactic.
def printf := printf.printf.
def pp_sort : sort -> string.
def pp_fun : function -> string.
def pp_pred : predicate -> string.
var : A : sort -> string -> term A.
def pp_term : ctx -> A : sort -> term A -> string.
def pp_terms : ctx -> As : sorts -> terms As -> string.
def pp_terms_cons : ctx -> A : sort -> term A -> As : sorts -> terms As -> string.
def pp_term_in_ctx : ctx -> A : sort -> term A -> string.
[s] pp_term _ _ (var _ s) --> s
[ctx,f,ts] pp_term ctx _ (fol.apply_fun f ts) --> printf "%s(%s)" (pp_fun f) (pp_terms ctx (fun_domain f) ts).
[ctx,A,a] pp_term ctx A a --> pp_term_in_ctx ctx A a.
[] pp_terms _ fol.nil_sort fol.nil_term --> ""
[ctx,A,t,As,ts] pp_terms ctx (fol.cons_sort _ _) (fol.cons_term A t As ts) -->
pp_terms_cons ctx A t As ts.
[ctx,B,u] pp_terms_cons ctx B u fol.nil_sort fol.nil_term --> pp_term ctx B u
[ctx,B,u,A,t,As,ts] pp_terms_cons ctx B u (fol.cons_sort _ _) (fol.cons_term A t As ts) -->
printf "%s, %s" (pp_term ctx B u) (pp_terms_cons ctx A t As ts).
[] pp_term_in_ctx tactic.nil_ctx _ _ --> "???"
[c,A,a] pp_term_in_ctx (tactic.cons_ctx_var _ _ c) A a -->
pp_term_in_ctx c A a
[c,A,a] pp_term_in_ctx (tactic.cons_ctx_proof _ _ c) A a -->
pp_term_in_ctx c A a
[c,l,A,a] pp_term_in_ctx (tactic.cons_ctx_labeled_var l A a c) A a --> l
[c,A,a] pp_term_in_ctx (tactic.cons_ctx_labeled_var _ _ _ c) A a -->
pp_term_in_ctx c A a.
def pp_prop : ctx -> nat -> prop -> string.
[ctx,A,x,y] pp_prop ctx _ (fol.apply_pred (eq.Eq A) (fol.cons_term _ x _ (fol.cons_term _ y _ fol.nil_term))) --> printf "%s = %s" (pp_term ctx A x) (pp_term ctx A y)
[ctx,p,ts] pp_prop ctx _ (fol.apply_pred p ts) --> printf "%s(%s)" (pp_pred p) (pp_terms ctx (pred_domain p) ts)
[] pp_prop _ _ fol.false --> "⊥"
[] pp_prop _ _ (fol.imp fol.false fol.false) --> "⊤"
[ctx,n,A] pp_prop ctx n (fol.imp A fol.false) --> printf "(¬%s)" (pp_prop ctx n A)
[ctx,n,A,B] pp_prop ctx n (fol.and (fol.imp A B) (fol.imp B A)) --> printf "(%s ⇔ %s)" (pp_prop ctx n A) (pp_prop ctx n B)
[ctx,n,A,B] pp_prop ctx n (fol.and A B) --> printf "(%s ∧ %s)" (pp_prop ctx n A) (pp_prop ctx n B)
[ctx,n,A,B] pp_prop ctx n (fol.or A B) --> printf "(%s ∨ %s)" (pp_prop ctx n A) (pp_prop ctx n B)
[ctx,n,A,B] pp_prop ctx n (fol.imp A B) --> printf "(%s ⇒ %s)" (pp_prop ctx n A) (pp_prop ctx n B)
[ctx,n,A,P] pp_prop ctx n (fol.all A P) --> (v : string => printf "(∀ %s : %s. %s)" v (pp_sort A) (pp_prop ctx (S n) (P (var A v)))) (printf "x_%d" n)
[ctx,n,A,P] pp_prop ctx n (fol.ex A P) --> (v : string => printf "(∃ %s : %s. %s)" v (pp_sort A) (pp_prop ctx (S n) (P (var A v)))) (printf "x_%d" n).
def pp_ctx : ctx -> string.
[] pp_ctx tactic.nil_ctx --> ""
[A,c] pp_ctx (tactic.cons_ctx_var A _ c) --> printf "%s
? : %s" (pp_ctx c) (pp_sort A)
[l,A,c] pp_ctx (tactic.cons_ctx_labeled_var l A _ c) --> printf "%s
%s : %s" (pp_ctx c) l (pp_sort A)
[A,c] pp_ctx (tactic.cons_ctx_proof A _ c) --> printf "%s
%s" (pp_ctx c) (pp_prop c 0 A).
def pp_sequent (c : ctx) (goal : prop) : string :=
printf "
%s
------------------
%s
" (pp_ctx c) (pp_prop c 0 goal).
#NAME printf.
digit : Type.
d0 : digit.
d1 : digit.
d2 : digit.
d3 : digit.
d4 : digit.
d5 : digit.
d6 : digit.
d7 : digit.
d8 : digit.
d9 : digit.
(; Number in decimal notation ;)
dlist : Type.
dnil : dlist.
dsnoc : dlist -> digit -> dlist.
def dincr : dlist -> dlist.
[] dincr dnil --> dsnoc dnil d1
[l] dincr (dsnoc l d0) --> dsnoc l d1
[l] dincr (dsnoc l d1) --> dsnoc l d2
[l] dincr (dsnoc l d2) --> dsnoc l d3
[l] dincr (dsnoc l d3) --> dsnoc l d4
[l] dincr (dsnoc l d4) --> dsnoc l d5
[l] dincr (dsnoc l d5) --> dsnoc l d6
[l] dincr (dsnoc l d6) --> dsnoc l d7
[l] dincr (dsnoc l d7) --> dsnoc l d8
[l] dincr (dsnoc l d8) --> dsnoc l d9
[l] dincr (dsnoc l d9) --> dsnoc (dincr l) d0.
def nat_to_dlist : nat -> dlist.
[] nat_to_dlist 0 --> dnil
[n] nat_to_dlist (S n) --> dincr (nat_to_dlist n).
def char_to_string (c : char) : string := string_cons c "".
def string_snoc (s : string) (c : char) := string.append s (char_to_string c).
def digit_to_char : digit -> char.
[] digit_to_char d0 --> '0'
[] digit_to_char d1 --> '1'
[] digit_to_char d2 --> '2'
[] digit_to_char d3 --> '3'
[] digit_to_char d4 --> '4'
[] digit_to_char d5 --> '5'
[] digit_to_char d6 --> '6'
[] digit_to_char d7 --> '7'
[] digit_to_char d8 --> '8'
[] digit_to_char d9 --> '9'.
def dlist_to_string : dlist -> string.
def dlist_to_string_aux : dlist -> string.
[] dlist_to_string_aux dnil --> ""
[l,d] dlist_to_string_aux (dsnoc l d) -->
string_snoc (dlist_to_string_aux l) (digit_to_char d).
[] dlist_to_string dnil --> "0"
[l,d] dlist_to_string (dsnoc l d) -->
string_snoc (dlist_to_string_aux l) (digit_to_char d).
def nat_to_string (n : nat) : string :=
dlist_to_string (nat_to_dlist n).
def printf_type : string -> Type.
[] printf_type "" --> string
[s] printf_type (string_cons '%' (string_cons 'd' s)) --> nat -> printf_type s
[s] printf_type (string_cons '%' (string_cons 's' s)) --> string -> printf_type s
[s] printf_type (string_cons _ s) --> printf_type s.
def printf_acc : fmt : string -> string -> printf_type fmt.
[acc] printf_acc "" acc --> acc
[fmt,acc] printf_acc (string_cons '%' (string_cons 'd' fmt)) acc --> n : nat =>
printf_acc fmt (string.append acc (nat_to_string n))
[fmt,acc] printf_acc (string_cons '%' (string_cons 's' fmt)) acc --> str : string =>
printf_acc fmt (string.append acc str)
[c,fmt,acc] printf_acc (string_cons c fmt) acc -->
printf_acc fmt (string_snoc acc c).
def printf (fmt : string) : printf_type fmt := printf_acc fmt "".
......@@ -36,7 +36,6 @@ def sort := fol.sort.
def term := fol.term.
def tactic := tactic.tactic.
def substitution := unif.substitution.
def nat := nat.Nat.
(; Some properties of disjunction ;)
......@@ -86,27 +85,27 @@ def cproof (C : clauses.clause) := proof (cprop C).
(; /!\ nth_lit n C does not fully reduce if n ≥ lenght(C) ;)
def nth_lit : nat -> clauses.clause -> clauses.literal.
[l] nth_lit nat.O (clauses.cons_clause l _) --> l
[n,C] nth_lit (nat.S n) (clauses.cons_clause _ C) --> nth_lit n C.
[l] nth_lit 0 (clauses.cons_clause l _) --> l
[n,C] nth_lit (S n) (clauses.cons_clause _ C) --> nth_lit n C.
(; /!\ remove_nth n C does not fully reduce if n ≥ length(C) ;)
(; /!\ not tail-rec ;)
def remove_nth : nat -> clauses.clause -> clauses.clause.
[C] remove_nth nat.O (clauses.cons_clause _ C) --> C
[n,l,C] remove_nth (nat.S n) (clauses.cons_clause l C) --> clauses.cons_clause l (remove_nth n C).
[C] remove_nth 0 (clauses.cons_clause _ C) --> C
[n,l,C] remove_nth (S n) (clauses.cons_clause l C) --> clauses.cons_clause l (remove_nth n C).
def cycle_nth (n : nat) (C : clauses.clause) : clauses.clause :=
clauses.cons_clause (nth_lit n C) (remove_nth n C).
def cycle_nth_correct : n : nat -> C : clauses.clause -> cproof C -> cproof (cycle_nth n C).
[l,C,H] cycle_nth_correct nat.O (clauses.cons_clause l C) H --> H
[n,l,C,H] cycle_nth_correct (nat.S n) (clauses.cons_clause l C) H -->
fol.or_elim (lprop l) (cprop C) (cprop (cycle_nth (nat.S n) (clauses.cons_clause l C))) H
[l,C,H] cycle_nth_correct 0 (clauses.cons_clause l C) H --> H
[n,l,C,H] cycle_nth_correct (S n) (clauses.cons_clause l C) H -->
fol.or_elim (lprop l) (cprop C) (cprop (cycle_nth (S n) (clauses.cons_clause l C))) H
(Hl => or_intro_2 (lprop (nth_lit n C)) (or (lprop l) (cprop (remove_nth n C)))
(or_intro_1 (lprop l) (cprop (remove_nth n C)) Hl))
(HC =>
fol.or_elim (lprop (nth_lit n C)) (cprop (remove_nth n C))
(cprop (cycle_nth (nat.S n) (clauses.cons_clause l C)))
(cprop (cycle_nth (S n) (clauses.cons_clause l C)))
(cycle_nth_correct n C HC)
(Hn => or_intro_1 (lprop (nth_lit n C)) (or (lprop l) (cprop (remove_nth n C))) Hn)
(Hr => or_intro_2 (lprop (nth_lit n C)) (or (lprop l) (cprop (remove_nth n C))) (or_intro_2 (lprop l) (cprop (remove_nth n C)) Hr))).
......
#NAME string.
def append : string -> string -> string.
[s] append "" s --> s
[c,s1,s2] append (string_cons c s1) s2 --> string_cons c (append s1 s2).
\ No newline at end of file
......@@ -18,6 +18,7 @@ def imp := fol.imp.
context : Type.
nil_ctx : context.
cons_ctx_var : A : sort -> term A -> context -> context.
cons_ctx_labeled_var : string -> A : sort -> term A -> context -> context.
cons_ctx_proof : A : prop -> proof A -> context -> context.
tactic : Type.
......@@ -63,6 +64,10 @@ def try_all_assumptions : (A : prop -> proof A -> tactic) ->
try_all_assumptions f (cons_ctx_var _ _ G)
-->
try_all_assumptions f G
[f,G]
try_all_assumptions f (cons_ctx_labeled_var _ _ _ G)
-->
try_all_assumptions f G
[f,A,a,G]
try_all_assumptions f (cons_ctx_proof A a G)
-->
......@@ -78,7 +83,8 @@ def ctx_remove : prop -> context -> context.
[] ctx_remove _ nil_ctx --> nil_ctx
[A,G] ctx_remove A (cons_ctx_proof A _ G) --> ctx_remove A G
[A,B,b,G] ctx_remove A (cons_ctx_proof B b G) --> cons_ctx_proof B b (ctx_remove A G)
[A,B,b,G] ctx_remove A (cons_ctx_var B b G) --> cons_ctx_var B b (ctx_remove A G).
[A,B,b,G] ctx_remove A (cons_ctx_var B b G) --> cons_ctx_var B b (ctx_remove A G)
[A,l,B,b,G] ctx_remove A (cons_ctx_labeled_var l B b G) --> cons_ctx_labeled_var l B b (ctx_remove A G).
(; clear A c proves G |- B if c proves G - A |- B ;)
clear : prop -> tactic -> tactic.
......@@ -90,6 +96,10 @@ def try_all_variables : (A : sort -> term A -> tactic) -> context -> tactic.
with_goal (A =>
with_context (G =>
raise (no_successful_variable A G)))
[f,A,a,G]
try_all_variables f (cons_ctx_labeled_var _ A a G)
-->
try (f A a) (__ => try_all_variables f G)
[f,A,a,G]
try_all_variables f (cons_ctx_var A a G)
-->
......@@ -99,12 +109,44 @@ def try_all_variables : (A : sort -> term A -> tactic) -> context -> tactic.
-->
try_all_variables f G.
def try_all_typed_variables : A : sort -> (term A -> tactic) -> context -> tactic.
[] try_all_typed_variables _ _ nil_ctx -->
with_goal (A =>
with_context (G =>
raise (no_successful_variable A G)))
[f,A,a,G]
try_all_typed_variables A f (cons_ctx_labeled_var _ A a G)
-->
try (f a) (__ => try_all_typed_variables A f G)
[f,A,G]
try_all_typed_variables A f (cons_ctx_labeled_var _ _ _ G)
-->
try_all_typed_variables A f G
[f,A,a,G]
try_all_typed_variables A f (cons_ctx_var A a G)
-->
try (f a) (__ => try_all_typed_variables A f G)
[f,A,G]
try_all_typed_variables A f (cons_ctx_var _ _ G)
-->
try_all_typed_variables A f G
[f,A,G]
try_all_typed_variables A f (cons_ctx_proof _ _ G)
-->
try_all_typed_variables A f G.
(; with_variable (A => a => c) proves G |- B if c proves G |- B for
any variable (a : A) in G;)
def with_variable (f : A : sort -> term A -> tactic) : tactic
:=
with_context (G => try_all_variables f G).
(; with_typed_variable A (a => c) proves G |- B if c proves G |- B for
any variable (a : A) in G. Only variables of type A are tried. ;)
def with_typed_variable (A : sort) (f : term A -> tactic) : tactic
:=
with_context (G => try_all_typed_variables A f G).
(; assumption proves G |- A if (a : A) is in G. ;)
def assumption : tactic := with_assumption exact.
......@@ -126,44 +168,44 @@ def refine2 (A : prop) (B : prop) (C : prop) (f : proof A -> proof B -> proof C)
(; refinen n A1 ... An B f c1 ... cn proves G |- B if each ci proves G |- Ai ;)
props : nat.Nat -> Type.
nil_prop : props nat.O.
cons_prop : n : nat.Nat -> prop -> props n -> props (nat.S n).
def snoc_prop : n : nat.Nat -> props n -> prop -> props (nat.S n).
[p] snoc_prop nat.O nil_prop p --> cons_prop nat.O p nil_prop
[n,p,ps,q] snoc_prop (nat.S n) (cons_prop _ p ps) q --> cons_prop (nat.S n) p (snoc_prop n ps q).
props : nat -> Type.
nil_prop : props 0.
cons_prop : n : nat -> prop -> props n -> props (S n).
def snoc_prop : n : nat -> props n -> prop -> props (S n).
[p] snoc_prop 0 nil_prop p --> cons_prop 0 p nil_prop
[n,p,ps,q] snoc_prop (S n) (cons_prop _ p ps) q --> cons_prop (S n) p (snoc_prop n ps q).
tactics : nat.Nat -> Type.
nil_tactic : tactics nat.O.
cons_tactic : n : nat.Nat -> tactic -> tactics n -> tactics (nat.S n).
tactics : nat -> Type.
nil_tactic : tactics 0.
cons_tactic : n : nat -> tactic -> tactics n -> tactics (S n).
def f_T : n : nat.Nat -> prop -> props n -> Type.
[B] f_T nat.O B nil_prop --> proof B
[n,B,A,As] f_T (nat.S n) B (cons_prop _ A As) --> proof A -> f_T n B As.
def f_T : n : nat -> prop -> props n -> Type.
[B] f_T 0 B nil_prop --> proof B
[n,B,A,As] f_T (S n) B (cons_prop _ A As) --> proof A -> f_T n B As.
def refinen_aux : n : nat.Nat -> As : props n -> B : prop -> f_T n B As -> tactics n -> tactic.
[B,b] refinen_aux (nat.O) nil_prop B b nil_tactic --> exact B b
[n,A,As,B,f,c,cs] refinen_aux (nat.S n) (cons_prop _ A As) B f (cons_tactic _ c cs) -->
def refinen_aux : n : nat -> As : props n -> B : prop -> f_T n B As -> tactics n -> tactic.
[B,b] refinen_aux 0 nil_prop B b nil_tactic --> exact B b
[n,A,As,B,f,c,cs] refinen_aux (S n) (cons_prop _ A As) B f (cons_tactic _ c cs) -->
bind A c (a : proof A =>
refinen_aux n As B (f a) cs).
def ntactics_T : nat.Nat -> Type.
[] ntactics_T nat.O --> tactic
[n] ntactics_T (nat.S n) --> tactic -> ntactics_T n.
def ntactics_T : nat -> Type.
[] ntactics_T 0 --> tactic
[n] ntactics_T (S n) --> tactic -> ntactics_T n.
def read_certs : n : nat.Nat -> (tactics n -> tactic) -> ntactics_T n.
[c] read_certs nat.O c --> c nil_tactic
[n,f] read_certs (nat.S n) f --> c => read_certs n (cs => f (cons_tactic n c cs)).
def read_certs : n : nat -> (tactics n -> tactic) -> ntactics_T n.
[c] read_certs 0 c --> c nil_tactic
[n,f] read_certs (S n) f --> c => read_certs n (cs => f (cons_tactic n c cs)).
def refinen_T : m : nat.Nat -> n : nat.Nat -> nat.Nat -> props m -> Type.
[m,k,As] refinen_T m nat.O k As --> B : prop -> f_T m B As -> ntactics_T k.
[m,n,k,As] refinen_T m (nat.S n) k As --> A : prop -> refinen_T (nat.S m) n k (snoc_prop m As A).
def refinen_T : m : nat -> n : nat -> nat -> props m -> Type.
[m,k,As] refinen_T m 0 k As --> B : prop -> f_T m B As -> ntactics_T k.
[m,n,k,As] refinen_T m (S n) k As --> A : prop -> refinen_T (S m) n k (snoc_prop m As A).
def read_props : m : nat.Nat -> n : nat.Nat -> k : nat.Nat -> As : props m -> refinen_T m n k As.
[m,f,As] read_props m nat.O m As --> B => f => read_certs m (refinen_aux m As B f)
[m,n,k,f,As] read_props m (nat.S n) k As --> A => read_props (nat.S m) n k (snoc_prop m As A).
def read_props : m : nat -> n : nat -> k : nat -> As : props m -> refinen_T m n k As.
[m,As] read_props m 0 m As --> B => f => read_certs m (refinen_aux m As B f)
[m,n,k,As] read_props m (S n) k As --> A => read_props (S m) n k (snoc_prop m As A).
def refinen (n : nat.Nat) := read_props nat.O n n nil_prop.
def refinen (n : nat) := read_props 0 n n nil_prop.
(; fix_term A f a proves G |- B if f (fix_term A f) a proves G |- B ;)
def fix_term : A : sort -> ((term A -> tactic) -> term A -> tactic) -> term A -> tactic.
......@@ -197,6 +239,13 @@ intro : tactic -> tactic.
[A,B] eval_tactic _ (fol.ex A B) (intro _) --> mtac.mraise (fol.ex A B) not_a_product
[p,l] eval_tactic _ (fol.apply_pred p l) (intro _) --> mtac.mraise (fol.apply_pred p l) not_a_product.
(; Same as intro but introduces a labeled variable ;)
lintro_exc : mtac.exc.
lintro : string -> A : sort -> (term A -> tactic) -> tactic.
[ctx,A,B,l,t] eval_tactic ctx (fol.all A B) (lintro l A t) -->
mtac.mintro_term A B (a : term A => eval_tactic (cons_ctx_labeled_var l A a ctx) (B a) (t a))
[ctx,G,t] eval_tactic ctx G (lintro _ _ _) --> mtac.mraise G lintro_exc.
(; exfalso c proves G |- A if c proves G |- false ;)
def exfalso (c : tactic) : tactic :=
with_goal (A =>
......@@ -344,7 +393,7 @@ proves G,A |- C, and c3 proves G,B |- C ;)
def destruct_or (A : prop) (B : prop) (c1 : tactic) (c2 : tactic) (c3 : tactic) : tactic
:=
with_goal (G =>
refinen (nat.S (nat.S (nat.S nat.O)))
refinen (S (S (S 0)))
(fol.or A B)
(fol.imp A G)
(fol.imp B G)
......@@ -367,7 +416,7 @@ def assert (A : prop) (c1 : tactic) (c2 : tactic) : tactic
c2 proves G |- A, and c2 proves G,B |- C ;)
def destruct_imp (A : prop) (B : prop) (c1 : tactic) (c2 : tactic) (c3 : tactic) : tactic
:=
with_goal (G => refinen (nat.S (nat.S (nat.S nat.O))) (imp A B) A (imp B G) G (ab => a => bg => fol.imp_elim B G bg (fol.imp_elim A B ab a)) c1 c2 (intro c3)).
with_goal (G => refinen (S (S (S 0))) (imp A B) A (imp B G) G (ab => a => bg => fol.imp_elim B G bg (fol.imp_elim A B ab a)) c1 c2 (intro c3)).
(; absurd proves anything if the current context contains an
assumption and its negation. ;)
......
......@@ -207,30 +207,3 @@ def unify'_aux : unify_problem -> unify_result -> unify_result.
def unify' (pb : unify_problem) :=
unify'_aux pb (unify pb).
A : sort.
f : function.
[] fol.fun_domain f --> read_sorts (nat.S (nat.S nat.O)) A A.
[] fol.fun_codomain f --> A.
a : function.
[] fol.fun_domain a --> read_sorts nat.O.
[] fol.fun_codomain a --> A.
b : function.
[] fol.fun_domain b --> read_sorts nat.O.
[] fol.fun_codomain b --> A.
x : term A.
y : term A.
(;
#SNF unify (unify_cons A x (fun_apply a) unify_nil).
#SNF unify (unify_cons A (fun_apply a) x unify_nil).
#SNF unify' (unify_cons A (fun_apply f x (fun_apply a)) (fun_apply a) unify_nil).
#SNF unify (unify_cons A (fun_apply f x (fun_apply a)) (fun_apply f (fun_apply a) x) unify_nil).
#SNF unify (unify_cons A x x unify_nil).
#SNF unify (unify_cons A x y unify_nil).
#SNF unify (unify_cons A (fun_apply f x (fun_apply a)) (fun_apply f (fun_apply a) y) unify_nil).
#SNF unify' (unify_cons A (fun_apply f (fun_apply b) y) (fun_apply f y (fun_apply a)) unify_nil).
;)
\ No newline at end of file
include ../.config_vars
# Dedukti files
DKS = $(wildcard *.dk)
DKOS = $(DKS:.dk=.dko)
DKCHECK_OPTIONS = -I ../fol -I ../meta -nl
all: $(DKOS)
%.dko:
$(DKCHECK) -e $(DKCHECK_OPTIONS) $<
# For each dependency foo.dko in the ../fol directory, the previous
# rule will try to create foo.dko here by calling "dkcheck -e" without
# file argument. This actually succeeds but does not produce any file.
# foo.dk.depend lists the modules foo depends on
%.dk.depend: %.dk
$(DKDEP) $< > $@
DKDEPENDS = $(DKS:.dk=.dk.depend)
-include $(DKDEPENDS)
depend: $(DKDEPENDS)
clean:
rm -f *.dko *.depend
install: all
mkdir -p $(INSTALL_LIB_DIR)
install -t $(INSTALL_LIB_DIR) $(DKOS)
uninstall:
for f in $(DKOS); do \
rm -f $(INSTALL_LIB_DIR)/$$f; \
done
rmdir $(INSTALL_LIB_DIR)
.PHONY: clean depend install uninstall all
#NAME pretty.
pretty_load : Type.
eval_tactic_pretty : tactic.tactic -> string -> goal : fol.prop ->
mtac.mtactic goal.
[ctx,goal,t] tactic.eval_tactic ctx goal t --> eval_tactic_pretty t (pp.pp_sequent ctx goal) goal.
include ../.config_vars
# Dedukti files
DKS = $(wildcard *.dk)
DKOS = $(DKS:.dk=.dko)
DKCHECK_OPTIONS = -I ../fol -nl
all: $(DKOS)
%.dko:
$(DKCHECK) -e $(DKCHECK_OPTIONS) $<
# For each dependency foo.dko in the ../fol directory, the previous
# rule will try to create foo.dko here by calling "dkcheck -e" without
# file argument. This actually succeeds but does not produce any file.
# foo.dk.depend lists the modules foo depends on
%.dk.depend: %.dk
$(DKDEP) $< > $@
DKDEPENDS = $(DKS:.dk=.dk.depend)
-include $(DKDEPENDS)
depend: $(DKDEPENDS)
clean:
rm -f *.dko *.depend
install: all
mkdir -p $(INSTALL_LIB_DIR)
install -t $(INSTALL_LIB_DIR) $(DKOS)
uninstall:
for f in $(DKOS); do \
rm -f $(INSTALL_LIB_DIR)/$$f; \
done
rmdir $(INSTALL_LIB_DIR)
.PHONY: clean depend install uninstall all
#NAME pretty.
pretty_load : Type.