Commit c362b55b authored by Raphael Cauderlier's avatar Raphael Cauderlier

Interactivity examples

parent c330aebb
......@@ -117,9 +117,9 @@ done
# Ensures that the file ".config_vars" exists and is empty
echo > .config_vars &&
find_and_check_binary "skcheck" ".native" "DKCHECK" "-version" "Sukerujo devel" &&
find_and_check_binary "skdep" ".native" "DKDEP" "" "" &&
find_and_check_binary "skmeta" ".native" "DKMETA" "-version" "" &&
find_and_check_binary "dkcheck" ".native" "DKCHECK" "-version" "Meta Sukerujo v2.6" &&
find_and_check_binary "dkdep" ".native" "DKDEP" "" "" &&
find_and_check_binary "dkmeta" ".native" "DKMETA" "-version" "Meta Sukerujo v2.6" &&
if $CONFLUENCE_CHECKING
then
......
......@@ -19,6 +19,10 @@ all: $(DKOS)
%.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.
......
#NAME andcomm.
A : fol.prop.
B : fol.prop.
load_pretty : pretty.pretty_load.
def t : nat -> tactic.tactic.
A : fol.prop.
B : fol.prop.
[] pp.pp_prop _ A --> "A".
[] pp.pp_prop _ B --> "B".
[] 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).
......
#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).
......@@ -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 ;)
......
......@@ -21,44 +21,57 @@ def pp_pred : predicate -> string.
var : A : sort -> string -> term A.
def pp_term : A : sort -> term A -> string.
def pp_terms : As : sorts -> terms As -> string.
def pp_terms_cons : A : sort -> term A -> As : sorts -> terms As -> string.
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
[f,ts] pp_term _ (fol.apply_fun f ts) --> printf "%s(%s)" (pp_fun f) (pp_terms (fun_domain f) ts).
[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 --> ""
[A,t,As,ts] pp_terms (fol.cons_sort _ _) (fol.cons_term A t As ts) -->
pp_terms_cons A t As ts.
[] 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.
[B,u] pp_terms_cons B u fol.nil_sort fol.nil_term --> pp_term B u
[B,u,A,t,As,ts] pp_terms_cons B u (fol.cons_sort _ _) (fol.cons_term A t As ts) -->
printf "%s, %s" (pp_term B u) (pp_terms_cons 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).
def pp_prop : nat -> prop -> string.
[A,x,y] pp_prop _ (fol.apply_pred (eq.Eq A) (fol.cons_term _ x _ (fol.cons_term _ y _ fol.nil_term))) --> printf "%s = %s" (pp_term A x) (pp_term A y)
[p,ts] pp_prop _ (fol.apply_pred p ts) --> printf "%s(%s)" (pp_pred p) (pp_terms (pred_domain p) ts)
[] pp_prop _ fol.false --> "⊥"
[] pp_prop _ (fol.imp fol.false fol.false) --> "⊤"
[n,A] pp_prop n (fol.imp A fol.false) --> printf "(¬%s)" (pp_prop n A)
[n,A,B] pp_prop n (fol.and (fol.imp A B) (fol.imp B A)) --> printf "(%s ⇔ %s)" (pp_prop n A) (pp_prop n B)
[n,A,B] pp_prop n (fol.and A B) --> printf "(%s ∧ %s)" (pp_prop n A) (pp_prop n B)
[n,A,B] pp_prop n (fol.or A B) --> printf "(%s ∨ %s)" (pp_prop n A) (pp_prop n B)
[n,A,B] pp_prop n (fol.imp A B) --> printf "(%s ⇒ %s)" (pp_prop n A) (pp_prop n B)
[n,A,P] pp_prop n (fol.all A P) --> (v : string => printf "(∀ %s : %s. %s)" v (pp_sort A) (pp_prop (S n) (P (var A v)))) (printf "x_%d" n)
[n,A,P] pp_prop n (fol.ex A P) --> (v : string => printf "(∃ %s : %s. %s)" v (pp_sort A) (pp_prop (S n) (P (var A v)))) (printf "x_%d" n).
[] 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_sort A) (pp_ctx c)
[A,c] pp_ctx (tactic.cons_ctx_proof A _ c) --> printf " %s
%s" (pp_prop 0 A) (pp_ctx c).
[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 0 goal).
" (pp_ctx c) (pp_prop c 0 goal).
......@@ -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.
......@@ -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 =>
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment