Commit 1e2fbe16 authored by Raphael Cauderlier's avatar Raphael Cauderlier

Add a minimal support for the sttforall logic

parent e4467110
#NAME mtac.
(; Customization of Emacs mode for Dedukti: this file is not linear
and requires a path extended with "../fol".
(setq-local dedukti-check-options '("-nc" "-nl" "-I" "../fol"))
(setq-local dedukti-compile-options '("-nc" "-e" "-nl" "-I" "../fol"))
;)
(; This is a Meta Dedukti port of Mtac with the following simpifications:
- works on first-order logic instead of CIC
This implies a bit of duplication between terms and proofs.
- nu and abs are replaced by the less powerful but simpler to implement intro
- no pattern matching, use rewriting instead
- no deep manipulation of variables and meta variables
;)
def sort := sttforall.type.
def term := sttforall.eta.
def prop := sttforall.eta sttforall.bool.
def proof := sttforall.eps.
def all := sttforall.forall.
def imp := sttforall.impl.
exc : Type.
mtactic : prop -> Type.
mret : A : prop -> proof A -> mtactic A.
mraise : A : prop -> exc -> mtactic A.
def mrun : A : prop -> mtactic A -> proof A.
[a] mrun _ (mret _ a) --> a.
def mbind : A : prop -> B : prop -> mtactic A -> (proof A -> mtactic B) -> mtactic B.
[f,t] mbind _ _ (mret _ t) f --> f t
[B,t] mbind _ B (mraise _ t) _ --> mraise B 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 mintro_term : A : sort ->
B : (term A -> prop) ->
(x : term A -> mtactic (B x)) ->
mtactic (all A B).
def mintro_proof : A : prop ->
B : prop ->
(proof A -> mtactic B) ->
mtactic (imp A B).
[A,B,b] mintro_term A (x => B x) (x => mret (B x) (b x))
-->
mret (all A (x => B x)) (x : term A => b x)
[A,B,e] mintro_term A (x => B x) (x => mraise (B x) e)
-->
mraise (all A (x => B x)) e.
[A,B,b] mintro_proof A B (x => mret B (b x))
-->
mret (imp A B) (x : proof A => b x)
[A,B,e] mintro_proof A B (x => mraise _ e)
-->
mraise (imp A B) e.
#NAME nat.
Nat : Type.
O : Nat.
S : Nat -> Nat.
#NAME tactic.
(; Customization of Emacs mode for Dedukti: this file is not linear
and requires a path extended with "../fol".
(setq-local dedukti-check-options '("-nc" "-nl" "-I" "../fol"))
(setq-local dedukti-compile-options '("-nc" "-e" "-nl" "-I" "../fol"))
;)
def sort := sttforall.type.
def term := sttforall.eta.
def prop := sttforall.eta sttforall.bool.
def proof := sttforall.eps.
def all := sttforall.forall.
def imp := sttforall.impl.
context : Type.
nil_ctx : context.
cons_ctx_var : A : sort -> term A -> context -> context.
cons_ctx_proof : A : prop -> proof A -> context -> context.
tactic : Type.
def eval_tactic : context -> A : prop -> tactic -> mtac.mtactic A.
def prove (A : prop) (c : tactic) : proof A :=
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).
(; raise e proves nothing ;)
raise : mtac.exc -> tactic.
[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 G A (try c1 c2)
-->
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 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 G A (with_context c) --> eval_tactic G A (c G).
no_successful_assumption : prop -> context -> mtac.exc.
def try_all_assumptions : (A : prop -> proof A -> tactic) ->
context -> tactic.
[] try_all_assumptions _ nil_ctx -->
with_goal (A =>
with_context (G =>
raise (no_successful_assumption A G)))
[f,G]
try_all_assumptions f (cons_ctx_var _ _ G)
-->
try_all_assumptions f G
[f,A,a,G]
try_all_assumptions f (cons_ctx_proof A a G)
-->
try (f A a) (__ => try_all_assumptions f G).
(; with_assumption (A => a => c) proves G |- B if c proves G |- B for
any (a : A) in G ;)
def with_assumption (f : A : prop -> proof A -> tactic) : tactic
:=
with_context (G => try_all_assumptions f G).
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).
(; clear A c proves G |- B if c proves G - A |- B ;)
clear : prop -> tactic -> tactic.
[A,G,B,c] eval_tactic G A (clear B c) --> eval_tactic (ctx_remove B G) A c.
no_successful_variable : prop -> context -> mtac.exc.
def try_all_variables : (A : sort -> term A -> tactic) -> context -> tactic.
[] try_all_variables _ nil_ctx -->
with_goal (A =>
with_context (G =>
raise (no_successful_variable A G)))
[f,A,a,G]
try_all_variables f (cons_ctx_var A a G)
-->
try (f A a) (__ => try_all_variables f G)
[f,G]
try_all_variables f (cons_ctx_proof _ _ G)
-->
try_all_variables 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).
(; assumption proves G |- A if (a : A) is in G. ;)
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 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) :=
bind A c (a : proof A =>
exact B (f a)).
(; refine2 A B C f c1 c2 proves G |- C if c1 proves G |- A and c2 proves G |- B ;)
def refine2 (A : prop) (B : prop) (C : prop) (f : proof A -> proof B -> proof C) (c1 : tactic) (c2 : tactic) :=
bind A c1 (a : proof A =>
bind B c2 (b : proof B =>
exact C (f a b))).
(; 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).
tactics : nat.Nat -> Type.
nil_tactic : tactics nat.O.
cons_tactic : n : nat.Nat -> tactic -> tactics n -> tactics (nat.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 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) -->
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 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 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 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 refinen (n : nat.Nat) := read_props nat.O 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.
[A,F,a] fix_term A F a --> F (fix_term A F) a.
def fix_prop : ((prop -> tactic) -> prop -> tactic) -> prop -> tactic.
[F,a] fix_prop F a --> F (fix_prop F) a.
def fix_proof : ((A : prop -> proof A -> tactic) ->
A : prop -> proof A -> tactic) ->
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 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 G (imp A B) (intro 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 G (all A B) (intro c)
-->
mtac.mintro_term A B (a : term A => eval_tactic (cons_ctx_var A a G) (B a) c).
(; assert A c1 c2 proves G |- B if c1 proves G |- A and c2 proves G,A |- B ;)
def assert (A : prop) (c1 : tactic) (c2 : tactic) : tactic
:=
with_goal (B => refine2 (imp A B) A B (x => x) (intro c2) c1).
(; destruct_imp A B c1 c2 c3 proves G |- C if c1 proves G |- A -> B,
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 => bg (ab a)) c1 c2 (intro c3)).
(; apply A B a c proves (B a) if c proves all A B ;)
def apply (A : sort) (B : term A -> prop) (a : term A) : tactic -> tactic :=
refine (all A B) (B a) (ab => ab a).
(; destruct_all A B a c1 c2 proves G if c1 prove (all A B) and c2
proves imp (B a) G ;)
def destruct_all (A : sort) (B : term A -> prop)
(a : term A) (c1 : tactic)
(c2 : tactic) : tactic
:=
with_goal (G => refine2 (all A B) (imp (B a) G) G (ab => f => f (ab a)) c1 c2).
(; 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 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 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.
#NAME sttforall.
type : Type.
arr : type -> type -> type.
bool : type.
def eta : type -> Type.
ptype : Type.
p : type -> ptype.
def etap : ptype -> Type.
forallK : (type -> ptype) -> ptype.
def eps : eta bool -> Type.
impl : eta bool -> eta bool -> eta bool.
forall : t:type -> (eta t -> eta bool) -> eta bool.
forallP : (type -> eta bool) -> eta bool.
[] eta --> t : type => etap (p t).
[l,r] etap (p (arr l r)) --> eta l -> eta r.
[f] etap (forallK f) --> x : type -> etap (f x).
[t,f] eps (forall t f) --> x:eta t -> eps (f x).
[l,r] eps (impl l r) --> eps l -> eps r.
[f] eps (forallP f) --> x:type -> eps (f x).
true : eta bool.
def foo : etap ( forallK (X : type => p (bool))) :=
X:type => forall X (x:eta X => forallP (Y : type => forall Y (y:eta Y => true))).
\ No newline at end of file
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