Commit 7ef448d7 authored by Valentin Blot's avatar Valentin Blot
Browse files

simplification of stack substitution

parent 54333a96
......@@ -132,7 +132,7 @@ Inductive logterm : Type :=
| LAbs : logterm -> logterm
| LApp : logterm -> logtermlist -> logterm
| LMetavar : nat -> logterm
| LMetasubst : logterm -> nat -> logtermlist -> logterm
| LMetasubst : logterm -> logtermlist -> logterm
with logtermlist : Type :=
| LLVar : nat -> logtermlist
| LLList : list logterm -> logtermlist.
......@@ -156,7 +156,7 @@ Fixpoint logterm_liftt (n : nat) (t : logterm) : logterm :=
| LAbs t => LAbs (logterm_liftt n t)
| LApp t p => LApp (logterm_liftt n t) (logtermlist_liftt n p)
| LMetavar m => if m <? n then LMetavar m else LMetavar (S m)
| LMetasubst t m p => LMetasubst (logterm_liftt n t) m (logtermlist_liftt n p)
| LMetasubst t p => LMetasubst (logterm_liftt n t) (logtermlist_liftt n p)
end
with logtermlist_liftt (n : nat) (p : logtermlist) : logtermlist :=
match p with
......@@ -172,7 +172,7 @@ Fixpoint logterm_liftp (n : nat) (t : logterm) : logterm :=
| LAbs t => LAbs (logterm_liftp n t)
| LApp t p => LApp (logterm_liftp n t) (logtermlist_liftp n p)
| LMetavar m => LMetavar m
| LMetasubst t m p => LMetasubst (logterm_liftp n t) m (logtermlist_liftp n p)
| LMetasubst t p => LMetasubst (logterm_liftp n t) (logtermlist_liftp n p)
end
with logtermlist_liftp (n : nat) (p : logtermlist) : logtermlist :=
match p with
......@@ -193,7 +193,7 @@ Fixpoint logterm_substt (n : nat) (t : logterm) (u : logterm) : logterm :=
| Eq => u
| Gt => LMetavar (pred m)
end
| LMetasubst t m p => LMetasubst (logterm_substt n t u) m (logtermlist_substt n p u)
| LMetasubst t p => LMetasubst (logterm_substt n t u) (logtermlist_substt n p u)
end
with logtermlist_substt (n : nat) (p : logtermlist) (u : logterm) : logtermlist :=
match p with
......@@ -209,7 +209,7 @@ Fixpoint logterm_substp (n : nat) (t : logterm) (p : logtermlist) : logterm :=
| LAbs t => LAbs (logterm_substp n t p)
| LApp t q => LApp (logterm_substp n t p) (logtermlist_substp n q p)
| LMetavar m => LMetavar m
| LMetasubst t m q => LMetasubst (logterm_substp n t p) m (logtermlist_substp n q p)
| LMetasubst t q => LMetasubst (logterm_substp n t p) (logtermlist_substp n q p)
end
with logtermlist_substp (n : nat) (q : logtermlist) (p : logtermlist) : logtermlist :=
match q with
......@@ -233,10 +233,10 @@ Fixpoint logterm_to_term (t : logterm) : term :=
| LLList p => fold_right (fun u t => App t u) (logterm_to_term t) (map logterm_to_term p)
end
| LMetavar m => Var 0
| LMetasubst t m p =>
| LMetasubst t p =>
match p with
| LLVar m => Var 0
| LLList p => term_subst m (logterm_to_term t) (map logterm_to_term p)
| LLList p => term_subst 0 (logterm_to_term t) (map logterm_to_term p)
end
end.
......@@ -345,7 +345,7 @@ Definition redcand : form :=
)
(FForallt (FForallt (FForallp
(FImp
(FIn (LApp (LMetasubst (LMetavar 1) 0 (LLList [LMetavar 0])) (LLVar 0)) 0)
(FIn (LApp (LMetasubst (LMetavar 1) (LLList [LMetavar 0])) (LLVar 0)) 0)
(FIn (LApp (LApp (LAbs (LMetavar 1)) (LLList [LMetavar 0])) (LLVar 0)) 0)
)
))).
......
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