Commit f41aedef authored by Raphael Cauderlier's avatar Raphael Cauderlier

tac -> mtac

parent 84e29d99
......@@ -30,7 +30,7 @@ def drinker_statement : fol.prop :=
def ndrink (x : fol.term BAR) := fol.not (drink x).
def drinker_paradox : fol.proof drinker_statement :=
tac.run drinker_statement (
mtac.mrun drinker_statement (
cert.run drinker_statement cert.nil_ctx
(classical_cert.prop_case (fol.all BAR drink)
(; ∀ ⊢ ∃x. drink x → ∀ ;)
......
......@@ -307,34 +307,34 @@ simpler for the following reasons:
** The tactic monad
Like in Lean and Mtac, our tactic language encapsulates computation
inside a monad defined in the file [[./meta/tac.dk][meta/tac.dk]] whose main purpose is
inside a monad defined in the file [[./meta/tac.dk][meta/mtac.dk]] whose main purpose is
to handle failure and backtracking.
- =tac.tactic : fol.prop -> Type=
- =tac.ret : A : fol.prop -> fol.proof A -> tac.tactic A=
- =tac.bind : A : fol.prop -> B : fol.prop -> tac.tactic A -> (fol.proof A -> tac.tactic B) -> tac.tactic B=
- =mtac.mtactic : fol.prop -> Type=
- =mtac.mret : A : fol.prop -> fol.proof A -> mtac.mtactic A=
- =mtac.mbind : A : fol.prop -> B : fol.prop -> mtac.mtactic A -> (fol.proof A -> mtac.mtactic B) -> mtac.mtactic B=
If =A= is a formula, =tac.tactic A= is the Dedukti type of the tactics
If =A= is a formula, =mtac.mtactic A= is the Dedukti type of the tactics
attempting to prove =A=. It forms a monad whose return and bind
operations are =tac.ret= and =tac.bind= respectively.
operations are =mtac.mret= and =mtac.mbind= respectively.
When a tactic successfully proves a formula, we can extract a proof of the formula using the partial function =tac.run=:
- =tac.run : A : fol.prop -> tac.tactic A -> fol.proof A=
When a tactic successfully proves a formula, we can extract a proof of the formula using the partial function =mtac.mrun=:
- =mtac.mrun : A : fol.prop -> mtac.mtactic A -> fol.proof A=
It is defined by the following rewrite rule:
- =[a] run _ (ret _ a) --> a=
** Exceptions and backtracking
Exceptions form an open inductive type =tac.exc=.
Exceptions form an open inductive type =mtac.exc=.
A tactic can fail to prove its goal by raising an exception:
- =tac.raise : A : fol.prop -> tac.exc -> tac.tactic A=
- =mtac.mraise : A : fol.prop -> mtac.exc -> mtac.mtactic A=
Exceptions can be caught by the =tac.try= tactic combinator
Exceptions can be caught by the =mtac.mtry= tactic combinator
implementing backtracking:
- =tac.try : A : fol.prop -> tac.tactic A -> (tac.exc -> tac.tactic A) -> tactic A=
- =mtac.mtry : A : fol.prop -> mtac.mtactic A -> (mtac.exc -> mtac.mtactic A) -> tactic A=
The tactic =tac.try A t f= first tries the tactic =t=, if it succeeds
The tactic =mtac.mtry A t f= first tries the tactic =t=, if it succeeds
then the corresponding proof of =A= is returned otherwise =t= has
failed with an exception =e= and we backtrack to try =f e=.
......@@ -342,29 +342,29 @@ failed with an exception =e= and we backtrack to try =f e=.
The tactic language uses a shallow representation of variables and
contexts. In order to introduce a new variable or assumption in
context, we use non-linear higher-order rewriting to define the symbols =tac.intro_term= and =tac.intro_proof=:
context, we use non-linear higher-order rewriting to define the symbols =mtac.mintro_term= and =mtac.mintro_proof=:
#+BEGIN_SRC dedukti
def intro_term : A : fol.sort ->
B : (fol.term A -> fol.prop) ->
(x : fol.term A -> tac.tactic (B x)) ->
tac.tactic (fol.all A B).
(x : fol.term A -> mtac.mtactic (B x)) ->
mtac.mtactic (fol.all A B).
def intro_proof : A : fol.prop ->
B : fol.prop ->
(fol.proof A -> tac.tactic B) ->
tac.tactic (fol.imp A B).
(fol.proof A -> mtac.mtactic B) ->
mtac.mtactic (fol.imp A B).
[A,B,b] tac.intro_term A B (x => tac.ret (B x) (b x))
[A,B,b] mtac.mintro_term A B (x => mtac.mret (B x) (b x))
-->
tac.ret (fol.all A B) (x : fol.term A => b x)
[A,B,e] tac.intro_term A B (x => tac.raise (B x) e)
mtac.mret (fol.all A B) (x : fol.term A => b x)
[A,B,e] mtac.mintro_term A B (x => mtac.mraise (B x) e)
-->
tac.raise (fol.all A B) e.
[A,B,b] tac.intro_proof A B (x => tac.ret B (b x))
mtac.mraise (fol.all A B) e.
[A,B,b] mtac.mintro_proof A B (x => mtac.mret B (b x))
-->
tac.ret (fol.imp A B) (x : fol.proof A => b x)
[A,B,e] tac.intro_proof A B (x => tac.raise _ e)
mtac.mret (fol.imp A B) (x : fol.proof A => b x)
[A,B,e] mtac.mintro_proof A B (x => mtac.mraise _ e)
-->
tac.raise (fol.imp A B) e.
mtac.mraise (fol.imp A B) e.
#+END_SRC
* The certificate language
......@@ -396,7 +396,7 @@ a tactic attempting to prove the goal formula.
- =cert.cons_ctx_var : A : fol.sort -> fol.term A -> cert.context -> cert.context=
- =cert.cons_ctx_proof : A : fol.prop -> fol.proof A -> cert.context -> cert.context=
- =cert.certificate : Type=
- =cert.run : A : fol.prop -> cert.context -> cert.certificate -> tac.tactic A=
- =cert.run : A : fol.prop -> cert.context -> cert.certificate -> mtac.mtactic A=
- =cert.cert_run : A : fol.prop -> cert.certificate -> fol.proof A=
** Certificate primitives
......@@ -407,21 +407,21 @@ certificates combinators. The few that are not have their semantics
directly defined in term of evaluation by the =cert.run= function. We
call them certificate primitives.
The simplest primitives reflect the two constructors =tac.ret= and
=tac.raise= of the tactic monad:
The simplest primitives reflect the two constructors =mtac.mret= and
=mtac.mraise= of the tactic monad:
- =cert.exact : A : fol.prop -> fol.proof A -> cert.certificate=
- =cert.raise : tac.exc -> cert.certificate=
- =cert.raise : mtac.exc -> cert.certificate=
The =cert.exact A a= certificate succeeds if and only if its goal is
=A= in which case =tac.ret A a= is returned. Otherwise the exception
=A= in which case =mtac.mret A a= is returned. Otherwise the exception
=cert.exact_mismatch= is raised.
The =cert.raise e= certificate always raises the exception =e=.
The other operations of the monad, =tac.try=, =tac.bind=,
=tac.intro_term= and =tac.intro_proof= are also reflected:
- =cert.try : cert.certificate -> (tac.exc -> cert.certificate) -> cert.certificate=
The other operations of the monad, =mtac.mtry=, =mtac.mbind=,
=mtac.mintro_term= and =mtac.mintro_proof= are also reflected:
- =cert.try : cert.certificate -> (mtac.exc -> cert.certificate) -> cert.certificate=
- =cert.bind : A : fol.prop -> cert.certificate -> (fol.proof A -> cert.certificate) -> cert.certificate=
- =cert.intro : cert.certificate -> cert.certificate=
......
......@@ -22,26 +22,26 @@ cons_ctx_proof : A : prop -> proof A -> context -> context.
certificate : Type.
def run : A : prop -> context -> certificate -> tac.tactic A.
def run : A : prop -> context -> certificate -> mtac.mtactic A.
def cert_run (A : prop) (c : certificate) : fol.proof A :=
tac.run A (cert.run A nil_ctx c).
mtac.mrun A (cert.run A nil_ctx c).
(; exact A a proves G |- A for any G ;)
exact_mismatch : prop -> prop -> tac.exc.
exact_mismatch : prop -> prop -> mtac.exc.
exact : A : prop -> proof A -> certificate.
[A,a] run A _ (exact A a) --> tac.ret A a
[A,B] run A _ (exact B _) --> tac.raise A (exact_mismatch A B).
[A,a] run A _ (exact A a) --> mtac.mret A a
[A,B] run A _ (exact B _) --> mtac.mraise A (exact_mismatch A B).
(; raise e proves nothing ;)
raise : tac.exc -> certificate.
[A,e] run A _ (raise e) --> tac.raise A e.
raise : mtac.exc -> certificate.
[A,e] run A _ (raise e) --> mtac.mraise A e.
(; try c1 (e => c2) proves G |- A if c1 proves G |- A or c2 proves G |- A ;)
try : certificate -> (tac.exc -> certificate) -> certificate.
try : certificate -> (mtac.exc -> certificate) -> certificate.
[A,G,c1,c2]
run A G (try c1 c2)
-->
tac.try A (run A G c1) (e : tac.exc => run A G (c2 e)).
mtac.mtry A (run A G c1) (e : mtac.exc => run A G (c2 e)).
(; with_goal (A => c) proves G |- A if c proves G |- A ;)
with_goal : (prop -> certificate) -> certificate.
......@@ -52,7 +52,7 @@ instead of the goal. ;)
with_context : (context -> certificate) -> certificate.
[A,G,c] run A G (with_context c) --> run A G (c G).
no_successful_assumption : fol.prop -> context -> tac.exc.
no_successful_assumption : fol.prop -> context -> mtac.exc.
def try_all_assumptions : (A : prop -> proof A -> certificate) ->
context -> certificate.
[] try_all_assumptions _ nil_ctx -->
......@@ -84,7 +84,7 @@ def ctx_remove : prop -> context -> context.
clear : prop -> certificate -> certificate.
[A,G,B,c] run A G (clear B c) --> run A (ctx_remove B G) c.
no_successful_variable : fol.prop -> context -> tac.exc.
no_successful_variable : fol.prop -> context -> mtac.exc.
def try_all_variables : (A : sort -> term A -> certificate) -> context -> certificate.
[] try_all_variables _ nil_ctx -->
with_goal (A =>
......@@ -111,7 +111,7 @@ def assumption : certificate := with_assumption exact.
(; bind A c f proves G |- B if (f a) proves G |- B where a is the
proof of A produced by c in context G ;)
bind : A : prop -> certificate -> (proof A -> certificate) -> certificate.
[B,G,A,c,f] run B G (bind A c f) --> tac.bind A B (run A G c) (a : proof A => run B G (f a)).
[B,G,A,c,f] run B G (bind A c f) --> mtac.mbind A B (run A G c) (a : proof A => run B G (f a)).
(; refine A B f c1 proves G |- B if c1 proves G |- A ;)
def refine (A : prop) (B : prop) (f : proof A -> proof B) (c : certificate) :=
......@@ -181,21 +181,21 @@ repeat : (certificate -> certificate) -> certificate.
[A,G,f] run A G (repeat f) --> run A G (f (repeat f)).
(; intro c proves either G |- A -> B if c proves G,A |- B or G |- all A B if c proves G, a : A |- B a ;)
not_a_product : tac.exc.
not_a_product : mtac.exc.
intro : certificate -> certificate.
[A,B,G,c]
run (fol.imp A B) G (intro c)
-->
tac.intro_proof A B (a : proof A => run B (cons_ctx_proof A a G) c)
mtac.mintro_proof A B (a : proof A => run B (cons_ctx_proof A a G) c)
[A,B,G,c]
run (fol.all A B) G (intro c)
-->
tac.intro_term A B (a : term A => run (B a) (cons_ctx_var A a G) c)
[] run fol.false _ (intro _) --> tac.raise fol.false not_a_product
[A,B] run (fol.and A B) _ (intro _) --> tac.raise (fol.and A B) not_a_product
[A,B] run (fol.or A B) _ (intro _) --> tac.raise (fol.or A B) not_a_product
[A,B] run (fol.ex A B) _ (intro _) --> tac.raise (fol.ex A B) not_a_product
[p,l] run (fol.apply_pred p l) _ (intro _) --> tac.raise (fol.apply_pred p l) not_a_product.
mtac.mintro_term A B (a : term A => run (B a) (cons_ctx_var A a G) c)
[] run fol.false _ (intro _) --> mtac.mraise fol.false not_a_product
[A,B] run (fol.and A B) _ (intro _) --> mtac.mraise (fol.and A B) not_a_product
[A,B] run (fol.or A B) _ (intro _) --> mtac.mraise (fol.or A B) not_a_product
[A,B] run (fol.ex A B) _ (intro _) --> mtac.mraise (fol.ex A B) not_a_product
[p,l] run (fol.apply_pred p l) _ (intro _) --> mtac.mraise (fol.apply_pred p l) not_a_product.
(; exfalso c proves G |- A if c proves G |- false ;)
def exfalso (c : certificate) : certificate :=
......@@ -300,7 +300,7 @@ def match_pred (A : prop)
c1.
(; split c1 c2 proves and A B if c1 proves A and c2 proves B ;)
not_a_conjunction : tac.exc.
not_a_conjunction : mtac.exc.
def split (c1 : certificate) (c2 : certificate) : certificate :=
with_goal (G =>
match_and G
......@@ -326,7 +326,7 @@ def destruct_and (A : prop) (B : prop) (c1 : certificate) (c2 : certificate)
(intro (intro c2))).
(; left c proves G |- A \/ B if c proves G |- A ;)
not_a_disjunction : tac.exc.
not_a_disjunction : mtac.exc.
def left (c : certificate) : certificate :=
with_goal (G =>
match_or G
......@@ -398,8 +398,8 @@ ifeq_prop : A : prop -> B : prop -> ((proof A -> proof B) -> certificate) -> cer
[G,B,c] run G B (ifeq_prop _ _ _ c) --> run G B c.
(; exists A a c proves ex A B if c proves (B a) ;)
witness_of_bad_sort : tac.exc.
not_an_existential : tac.exc.
witness_of_bad_sort : mtac.exc.
not_an_existential : mtac.exc.
def exists (A : sort) (a : term A) (c : certificate) : certificate
:=
with_goal (G =>
......
......@@ -87,7 +87,7 @@ def not_all_is_ex_not (A : fol.sort) (P : fol.term A -> fol.prop) :
fol.proof (fol.imp (fol.not (fol.all A (x => P x)))
(fol.ex A (x : fol.term A => fol.not (P x))))
:=
tac.run (fol.imp (fol.not (fol.all A (x => P x)))
mtac.mrun (fol.imp (fol.not (fol.all A (x => P x)))
(fol.ex A (x : fol.term A => fol.not (P x))))
(cert.run (fol.imp (fol.not (fol.all A (x => P x)))
(fol.ex A (x : fol.term A => fol.not (P x))))
......
......@@ -18,7 +18,7 @@ def eq := eq.eq.
def imp := fol.imp.
def all := fol.all.
not_an_equality : tac.exc.
not_an_equality : mtac.exc.
def match_equality : prop -> (A : sort -> term A -> term A -> certificate) -> certificate -> certificate.
[c] match_equality fol.false _ c --> c
......@@ -37,7 +37,7 @@ def match_equality : prop -> (A : sort -> term A -> term A -> certificate) -> ce
--> c A a b
[c] match_equality (fol.apply_pred _ _) _ c --> c.
not_convertible : A : sort -> term A -> term A -> tac.exc.
not_convertible : A : sort -> term A -> term A -> mtac.exc.
(; reflexivity proves goals of the form a = a ;)
def reflexivity : certificate :=
......@@ -61,7 +61,7 @@ def symmetry (c : certificate) : certificate :=
)
(cert.raise not_an_equality)).
trans_bad_type : tac.exc.
trans_bad_type : mtac.exc.
(; transitivity A b c1 c2 proves a = c if c1 proves a = b and c2 proves b = c ;)
def transitivity (A : sort) (b : term A) (c1 : certificate) (c2 : certificate) : certificate :=
cert.with_goal (G =>
......
#NAME tac.
#NAME mtac.
(; Customization of Emacs mode for Dedukti: this file is not linear
and requires a path extended with "../fol".
......@@ -23,53 +23,41 @@ def all := fol.all.
def imp := fol.imp.
exc : Type.
tactic : prop -> Type.
mtactic : prop -> Type.
ret : A : prop -> proof A -> tactic A.
raise : A : prop -> exc -> tactic A.
mret : A : prop -> proof A -> mtactic A.
mraise : A : prop -> exc -> mtactic A.
def run : A : prop -> tactic A -> proof A.
[a] run _ (ret _ a) --> a.
def mrun : A : prop -> mtactic A -> proof A.
[a] mrun _ (mret _ a) --> a.
def bind : A : prop -> B : prop -> tactic A -> (proof A -> tactic B) -> tactic B.
[a,f,t] bind _ _ (ret _ t) f --> f t
[B,t] bind _ B (raise _ t) _ --> raise B t.
def mbind : A : prop -> B : prop -> mtactic A -> (proof A -> mtactic B) -> mtactic B.
[a,f,t] mbind _ _ (mret _ t) f --> f t
[B,t] mbind _ B (mraise _ t) _ --> mraise B t.
def try : A : prop -> tactic A -> (exc -> tactic A) -> tactic A.
[A,t] try A (ret _ t) _ --> ret A t
[t,f] try _ (raise _ t) f --> f t.
def mtry : A : prop -> mtactic A -> (exc -> mtactic A) -> mtactic A.
[A,t] mtry A (mret _ t) _ --> mret A t
[t,f] mtry _ (mraise _ t) f --> f t.
def fix_term : A : sort ->
B : (term A -> prop) ->
((x : term A -> tactic (B x)) -> x : term A -> tactic (B x)) ->
x : term A -> tactic (B x).
[A,B,f,t] fix_term A B f t --> f (fix_term A B f) t.
def fix_proof : A : prop ->
B : prop ->
((proof A -> tactic B) -> proof A -> tactic B) ->
proof A -> tactic B.
[A,B,f,t] fix_proof A B f t --> f (fix_proof A B f) t.
def intro_term : A : sort ->
def mintro_term : A : sort ->
B : (term A -> prop) ->
(x : term A -> tactic (B x)) ->
tactic (all A B).
def intro_proof : A : prop ->
(x : term A -> mtactic (B x)) ->
mtactic (all A B).
def mintro_proof : A : prop ->
B : prop ->
(proof A -> tactic B) ->
tactic (imp A B).
(proof A -> mtactic B) ->
mtactic (imp A B).
[A,B,b] intro_term A B (x => ret (B x) (b x))
[A,B,b] mintro_term A B (x => mret (B x) (b x))
-->
ret (all A B) (fol.all_intro A B (x => b x))
[A,B,e] intro_term A B (x => raise (B x) e)
mret (all A B) (fol.all_intro A B (x => b x))
[A,B,e] mintro_term A B (x => mraise (B x) e)
-->
raise (all A B) e.
[A,B,b] intro_proof A B (x => ret B (b x))
mraise (all A B) e.
[A,B,b] mintro_proof A B (x => mret B (b x))
-->
ret (imp A B) (fol.imp_intro A B (x => b x))
[A,B,e] intro_proof A B (x => raise _ e)
mret (imp A B) (fol.imp_intro A B (x => b x))
[A,B,e] mintro_proof A B (x => mraise _ e)
-->
raise (imp A B) e.
mraise (imp A B) e.
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