Commit 123da7fa authored by Raphael Cauderlier's avatar Raphael Cauderlier

Swap the arguments of eval_tactic

parent 701fcb23
......@@ -322,7 +322,7 @@ When a tactic successfully proves a formula, we can extract a proof of the formu
- =mtac.mrun : A : fol.prop -> mtac.mtactic A -> fol.proof A=
It is defined by the following rewrite rule:
- =[a] run _ (ret _ a) --> a=
- =[a] mtac.mrun _ (mtac.mret _ a) --> a=
** Exceptions and backtracking
......@@ -396,7 +396,7 @@ produces a typed tactic attempting to prove the goal formula.
- =tactic.cons_ctx_var : A : fol.sort -> fol.term A -> tactic.context -> tactic.context=
- =tactic.cons_ctx_proof : A : fol.prop -> fol.proof A -> tactic.context -> tactic.context=
- =tactic.tactic : Type=
- =tactic.run : A : fol.prop -> tactic.context -> tactic.tactic -> mtac.mtactic A=
- =tactic.eval_tactic : tactic.context -> A : fol.prop -> tactic.tactic -> mtac.mtactic A=
- =tactic.prove : A : fol.prop -> tactic.tactic -> fol.proof A=
** Tactic primitives
......
......@@ -22,35 +22,35 @@ cons_ctx_proof : A : prop -> proof A -> context -> context.
tactic : Type.
def eval_tactic : A : prop -> context -> tactic -> mtac.mtactic A.
def eval_tactic : context -> A : prop -> tactic -> mtac.mtactic A.
def prove (A : prop) (c : tactic) : fol.proof A :=
mtac.mrun A (eval_tactic A nil_ctx c).
mtac.mrun A (eval_tactic nil_ctx A c).
(; exact A a proves G |- A for any G ;)
exact_mismatch : prop -> prop -> mtac.exc.
exact : A : prop -> proof A -> tactic.
[A,a] eval_tactic A _ (exact A a) --> mtac.mret A a
[A,B] eval_tactic A _ (exact B _) --> mtac.mraise A (exact_mismatch A B).
[A,a] eval_tactic _ A (exact A a) --> mtac.mret A a
[A,B] eval_tactic _ A (exact B _) --> mtac.mraise A (exact_mismatch A B).
(; raise e proves nothing ;)
raise : mtac.exc -> tactic.
[A,e] eval_tactic A _ (raise e) --> mtac.mraise A e.
[A,e] eval_tactic _ 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 : tactic -> (mtac.exc -> tactic) -> tactic.
[A,G,c1,c2]
eval_tactic A G (try c1 c2)
eval_tactic G A (try c1 c2)
-->
mtac.mtry A (eval_tactic A G c1) (e : mtac.exc => eval_tactic A G (c2 e)).
mtac.mtry A (eval_tactic G A c1) (e : mtac.exc => eval_tactic G A (c2 e)).
(; with_goal (A => c) proves G |- A if c proves G |- A ;)
with_goal : (prop -> tactic) -> tactic.
[A,G,c] eval_tactic A G (with_goal c) --> eval_tactic A G (c A).
[A,G,c] eval_tactic G A (with_goal c) --> eval_tactic G A (c A).
(; with_context is similar to with_goal but abstracts over the context
instead of the goal. ;)
with_context : (context -> tactic) -> tactic.
[A,G,c] eval_tactic A G (with_context c) --> eval_tactic A G (c G).
[A,G,c] eval_tactic G A (with_context c) --> eval_tactic G A (c G).
no_successful_assumption : fol.prop -> context -> mtac.exc.
def try_all_assumptions : (A : prop -> proof A -> tactic) ->
......@@ -82,7 +82,7 @@ def ctx_remove : prop -> context -> context.
(; clear A c proves G |- B if c proves G - A |- B ;)
clear : prop -> tactic -> tactic.
[A,G,B,c] eval_tactic A G (clear B c) --> eval_tactic A (ctx_remove B G) c.
[A,G,B,c] eval_tactic G A (clear B c) --> eval_tactic (ctx_remove B G) A c.
no_successful_variable : fol.prop -> context -> mtac.exc.
def try_all_variables : (A : sort -> term A -> tactic) -> context -> tactic.
......@@ -111,7 +111,7 @@ def assumption : tactic := 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 -> tactic -> (proof A -> tactic) -> tactic.
[B,G,A,c,f] eval_tactic B G (bind A c f) --> mtac.mbind A B (eval_tactic A G c) (a : proof A => eval_tactic B G (f a)).
[B,G,A,c,f] eval_tactic G B (bind A c f) --> mtac.mbind A B (eval_tactic G A c) (a : proof A => eval_tactic G B (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 : tactic) :=
......@@ -178,24 +178,24 @@ def fix_proof : ((A : prop -> proof A -> tactic) ->
[F,A,a] fix_proof F A a --> F (fix_proof F) A a.
repeat : (tactic -> tactic) -> tactic.
[A,G,f] eval_tactic A G (repeat f) --> eval_tactic A G (f (repeat f)).
[A,G,f] eval_tactic G A (repeat f) --> eval_tactic G A (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 : mtac.exc.
intro : tactic -> tactic.
[A,B,G,c]
eval_tactic (fol.imp A B) G (intro c)
eval_tactic G (fol.imp A B) (intro c)
-->
mtac.mintro_proof A B (a : proof A => eval_tactic B (cons_ctx_proof A a G) c)
mtac.mintro_proof A B (a : proof A => eval_tactic (cons_ctx_proof A a G) B c)
[A,B,G,c]
eval_tactic (fol.all A B) G (intro c)
eval_tactic G (fol.all A B) (intro c)
-->
mtac.mintro_term A B (a : term A => eval_tactic (B a) (cons_ctx_var A a G) c)
[] eval_tactic fol.false _ (intro _) --> mtac.mraise fol.false not_a_product
[A,B] eval_tactic (fol.and A B) _ (intro _) --> mtac.mraise (fol.and A B) not_a_product
[A,B] eval_tactic (fol.or A B) _ (intro _) --> mtac.mraise (fol.or A B) not_a_product
[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.
mtac.mintro_term A B (a : term A => eval_tactic (cons_ctx_var A a G) (B a) c)
[] eval_tactic _ fol.false (intro _) --> mtac.mraise fol.false not_a_product
[A,B] eval_tactic _ (fol.and A B) (intro _) --> mtac.mraise (fol.and A B) not_a_product
[A,B] eval_tactic _ (fol.or A B) (intro _) --> mtac.mraise (fol.or A B) not_a_product
[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.
(; exfalso c proves G |- A if c proves G |- false ;)
def exfalso (c : tactic) : tactic :=
......@@ -388,14 +388,14 @@ def destruct_all (A : sort) (B : term A -> prop)
with_goal (G => refine2 (all A B) (imp (B a) G) G (ab => f => fol.imp_elim (B a) G f (fol.all_elim A B ab a)) c1 c2).
(; To delay the comparison of sorts, we define ifeq_sort only when it is eval_tactic ;)
(; To delay the comparison of sorts, we define ifeq_sort only when it is run ;)
ifeq_sort : A : sort -> B : sort -> ((term A -> term B) -> tactic) -> tactic -> tactic.
[G,B,A,f] eval_tactic G B (ifeq_sort A A f _) --> eval_tactic G B (f (x => x))
[G,B,c] eval_tactic G B (ifeq_sort _ _ _ c) --> eval_tactic G B c.
[G,B,A,f] eval_tactic B G (ifeq_sort A A f _) --> eval_tactic B G (f (x => x))
[G,B,c] eval_tactic B G (ifeq_sort _ _ _ c) --> eval_tactic B G c.
ifeq_prop : A : prop -> B : prop -> ((proof A -> proof B) -> tactic) -> tactic -> tactic.
[G,B,A,f] eval_tactic G B (ifeq_prop A A f _) --> eval_tactic G B (f (x => x))
[G,B,c] eval_tactic G B (ifeq_prop _ _ _ c) --> eval_tactic G B c.
[G,B,A,f] eval_tactic B G (ifeq_prop A A f _) --> eval_tactic B G (f (x => x))
[G,B,c] eval_tactic B G (ifeq_prop _ _ _ c) --> eval_tactic B G c.
(; exists A a c proves ex A B if c proves (B a) ;)
witness_of_bad_sort : mtac.exc.
......
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