Commit b14840f1 authored by François Thiré's avatar François Thiré

Merge branch 'sttforall' of git.lsv.fr:cauderlier/dktactics into sttforall

parents 7531987e 1e2fbe16
.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 =>