Library MSetULamIHOL
Require Import Omega List Program.Equality.
Require Import Autosubst.
Inductive stp : Type :=
| o : stp
| i : stp
| na : stp
| ar : stp -> stp -> stp.
Inductive stm (e : nat -> stp) : stp -> Type :=
| SDB n : stm e (e n)
| SULam : stm e (ar (ar i i) i)
| SUAp : stm e (ar i (ar i i))
| SAp a b : stm e (ar a b) -> stm e a -> stm e b
| SLam a b : stm (a.:e) b -> stm e (ar a b)
| SImp : stm e o -> stm e o -> stm e o
| SAll a : stm (a.:e) o -> stm e o
| SEq a : stm e a -> stm e a -> stm e o.
Fixpoint push_stp_into_env (a:stp) (e:var -> stp) (j:nat) : var -> stp :=
match j with
| O => a.:e
| S j => (e 0).:(push_stp_into_env a (fun x => e (S x)) j)
end.
Fixpoint stmshift_var (j x:nat) : nat :=
match j with
| O => S x
| S j => match x with
| O => O
| S x => S (stmshift_var j x)
end
end.
Definition stmshift_var_eq a e j x : push_stp_into_env a e j (stmshift_var j x) = e x.
Defined.
Lemma stmshift_var_eq_match_eq a e j x :
match
stmshift_var_eq a e j x in (_ = y)
return
(push_stp_into_env a e j
(stmshift_var j x) = y)
with
| eq_refl => eq_refl
end
= stmshift_var_eq a e j x.
Lemma stmshift_var_eq_match_commutes a e j (x:nat) :
forall Y:stp -> Type, forall Z:stp -> Type, forall W, forall F:forall b, Y b -> Z b,
F (e x) (match stmshift_var_eq a e j x in (_ = y) return Y y with eq_refl => W end)
=
match stmshift_var_eq a e j x in (_ = y) return Z y with
eq_refl => F (push_stp_into_env a e j (stmshift_var j x)) W
end.
Definition stmshift_aux : forall e b, stm e b -> forall a j, stm (push_stp_into_env a e j) b.
Defined.
Definition stmshift : forall a e b, stm e b -> stm (a.:e) b.
Defined.
Definition pushsubstunder e e' a (theta:forall x, stm e' (e x)) : forall x, stm (a.:e') ((a.:e) x).
Defined.
Definition stmparsubst : forall e b e' (theta:forall x, stm e' (e x)), stm e b -> stm e' b.
Defined.
Definition stmsubst : forall a e b, stm (a.:e) b -> stm e a -> stm e b.
Defined.
Inductive conv_1 e : forall a, stm e a -> stm e a -> Prop :=
| conv_beta a b (s:stm (a.:e) b) (t:stm e a) :
conv_1 e b (SAp e a b (SLam e a b s) t) (stmsubst a e b s t)
| conv_eta a b (s:stm e (ar a b)) :
conv_1 e (ar a b) (SLam e a b (SAp (a.:e) a b (stmshift a e (ar a b) s) (SDB (a.:e) 0))) s
| conv_SApL a b (s1 s2:stm e (ar a b)) (t:stm e a) :
conv_1 e (ar a b) s1 s2 -> conv_1 e b (SAp e a b s1 t) (SAp e a b s2 t)
| conv_SApR a b (s:stm e (ar a b)) (t1 t2:stm e a) :
conv_1 e a t1 t2 -> conv_1 e b (SAp e a b s t1) (SAp e a b s t2)
| conv_SLam a b (s1 s2:stm (a.:e) b) :
conv_1 (a.:e) b s1 s2 -> conv_1 e (ar a b) (SLam e a b s1) (SLam e a b s2)
| conv_SImpL (s1 s2:stm e o) (t:stm e o) :
conv_1 e o s1 s2 -> conv_1 e o (SImp e s1 t) (SImp e s2 t)
| conv_SImpR (s:stm e o) (t1 t2:stm e o) :
conv_1 e o t1 t2 -> conv_1 e o (SImp e s t1) (SImp e s t2)
| conv_SAll a (s1 s2:stm (a.:e) o) :
conv_1 (a.:e) o s1 s2 -> conv_1 e o (SAll e a s1) (SAll e a s2)
| conv_SEqL a (s1 s2:stm e a) (t:stm e a) :
conv_1 e a s1 s2 -> conv_1 e o (SEq e a s1 t) (SEq e a s2 t)
| conv_SEqR a (s:stm e a) (t1 t2:stm e a) :
conv_1 e a t1 t2 -> conv_1 e o (SEq e a s t1) (SEq e a s t2)
.
Inductive conv e : forall a, stm e a -> stm e a -> Prop :=
| conv_one a (s t:stm e a) : conv_1 e a s t -> conv e a s t
| conv_ref a (s:stm e a) : conv e a s s
| conv_sym a (s t:stm e a) : conv e a s t -> conv e a t s
| conv_tra a (s t u:stm e a) : conv e a s t -> conv e a t u -> conv e a s u
.
Definition SFal e : stm e o :=
SAll e o (SDB (o.:e) 0).
Definition SLeibEq e a : stm e (ar a (ar a o)) :=
SLam e a (ar a o)
(SLam (a.:e) a o
(SAll (a.:a.:e) (ar a o)
(SImp (ar a o.:a.:a.:e)
(SAp (ar a o.:a.:a.:e) a o (SDB (ar a o.:a.:a.:e) 0) (SDB (ar a o.:a.:a.:e) 2))
(SAp (ar a o.:a.:a.:e) a o (SDB (ar a o.:a.:a.:e) 0) (SDB (ar a o.:a.:a.:e) 1))))).
Definition SLeibEqOp e a (s t:stm e a) : stm e o :=
SAp e a o (SAp e a (ar a o) (SLeibEq e a) s) t.
Definition SUApOp e (s t:stm e i) : stm e i :=
SAp e i i (SAp e i (ar i i) (SUAp e) s) t.
Definition SULamOp e (s:stm e (ar i i)) : stm e i :=
SAp e (ar i i) i (SULam e) s.
Inductive nd (e:nat -> stp) (G : stm e o -> Prop) : stm e o -> Prop :=
| ndH s : G s -> nd e G s
| ndConv s t : conv e o s t -> nd e G s -> nd e G t
| ndII s t : nd e (fun u => G u \/ u = s) t -> nd e G (SImp e s t)
| ndIE s t : nd e G (SImp e s t) -> nd e G s -> nd e G t
| ndAI a s : nd (a.:e) (fun u => exists v, G v /\ u = stmshift a e o v) s -> nd e G (SAll e a s)
| ndAE a s (t : stm e a) : nd e G (SAll e a s) -> nd e G (stmsubst a e o s t)
| ndEI a s : nd e G (SEq e a s s)
| ndEE a s t : nd e G (SEq e a s t) -> nd e G (SLeibEqOp e a s t)
| ndPropExt s t : nd e (fun u => G u \/ u = s) t -> nd e (fun u => G u \/ u = t) s -> nd e G (SEq e o s t)
| ndXi a b s t : nd (a.:e) (fun u => exists v, G v /\ u = stmshift a e o v) (SEq (a.:e) b s t) -> nd e G (SEq e (ar a b) (SLam e a b s) (SLam e a b t))
| ndApInj1 s1 s2 t : nd e G (SEq e i (SUApOp e s1 t) (SUApOp e s2 t)) -> nd e G (SEq e i s1 s2)
| ndApInj2 s t1 t2 : nd e G (SEq e i (SUApOp e s t1) (SUApOp e s t2)) -> nd e G (SEq e i t1 t2)
| ndLamInj s t : nd e G (SEq e i (SULamOp e s) (SULamOp e t)) -> nd e G (SEq e (ar i i) s t)
| ndApNotLam s t u : nd e G (SEq e i (SUApOp e s t) (SULamOp e u)) -> nd e G (SFal e)
.
Inductive term : Type :=
| Va (x : var)
| Ap (s t : term)
| La (s : {bind term}).
Instance Ids_term : Ids term.
Instance Rename_term : Rename term.
Instance Subst_term : Subst term.
Instance SubstLemmas_term : SubstLemmas term.
Definition RiId (X : (var -> term) -> Prop) : Prop :=
forall sigma, X sigma -> forall tau, X (sigma >> tau).
Lemma ActionRiId X (Xs:RiId X) sigma : RiId (fun tau => X (sigma >> tau)).
Record Mset : Type :=
mkMset {
Elt : Type;
Equ : Elt -> Elt -> Prop;
Action : Elt -> (var -> term) -> Elt;
EquSym : forall x y, Equ x y -> Equ y x;
EquTra : forall x y z, Equ x y -> Equ y z -> Equ x z;
ActionEqu : forall x y sigma, Equ x y -> Equ (Action x sigma) (Action y sigma);
ActionId : forall x y, Equ x y -> Equ (Action x ids) y;
ActionComp : forall x y sigma tau, Equ x y -> Equ (Action x (sigma >> tau)) (Action (Action y sigma) tau)
}.
Lemma EquRef1 (A:Mset) x y : Equ A x y -> Equ A x x.
Lemma EquRef2 (A:Mset) x y : Equ A x y -> Equ A y y.
Lemma ActionEqu1 (A:Mset) x sigma : Equ A x x -> Equ A (Action A x sigma) (Action A x sigma).
Definition Do : Mset.
Defined.
Definition Di : Mset.
Defined.
Definition Dnat : Mset.
Defined.
Definition Dar (A B:Mset) : Mset.
Defined.
Fixpoint tpinterp (a : stp) : Mset :=
match a with
| o => Do
| i => Di
| na => Dnat
| ar a b => Dar (tpinterp a) (tpinterp b)
end.
Fixpoint defaultelt (b:stp) : Elt (tpinterp b) :=
match b with
| o => fun sigma => False
| i => La (Va 0)
| na => 0
| ar a b => fun sigma x => defaultelt b
end.
Definition GlobalElt (A:Mset) (x:Elt A) : Prop :=
forall sigma:var -> term, Equ A (Action A x sigma) x.
Lemma defaultelt_GlobalElt (b:stp) : GlobalElt (tpinterp b) (defaultelt b).
Definition UAp : Elt (tpinterp (ar i (ar i i))) := fun sigma s => fun tau t => Ap (s.[tau]) t.
Definition ULam : Elt (tpinterp (ar (ar i i) i)) := fun sigma f => La (f (ren S) (Va 0)).
Lemma UAp_Global : GlobalElt (tpinterp (ar i (ar i i))) UAp.
Lemma UAp_OK : Equ _ UAp UAp.
Lemma ULam_Global : GlobalElt (tpinterp (ar (ar i i) i)) ULam.
Lemma ULam_OK : Equ (tpinterp (ar (ar i i) i)) ULam ULam.
Fixpoint eval (e : nat -> stp) (a : stp) (s : stm e a) (sigma:var -> term) (phi:forall n:nat, Elt (tpinterp (e n))) : Elt (tpinterp a) :=
match s with
| SDB n => phi n
| SULam => ULam
| SUAp => UAp
| SAp a b s t => eval e (ar a b) s sigma phi ids (eval e a t sigma phi)
| SLam a b s => fun (tau:var -> term) (x:Elt (tpinterp a)) =>
eval (a.:e) b s (sigma >> tau)
(fun n => match n with O => x | S n' => Action (tpinterp (e n')) (phi n') tau end)
| SImp s t => fun (tau:var -> term) =>
exists Z: (var -> term) -> Prop, RiId Z /\ Z tau /\
(forall mu, Z mu -> eval e o s (sigma >> mu) (fun n => Action _ (phi n) mu) ids
-> eval e o t (sigma >> mu) (fun n => Action _ (phi n) mu) ids)
| SAll a s => fun (tau:var -> term) =>
forall mu, forall x : Elt (tpinterp a), Equ (tpinterp a) x x ->
(eval (a.:e) o s (sigma >> tau >> mu)
(fun n => match n with O => x | S n' => Action (tpinterp (e n')) (phi n') (tau >> mu) end)) ids
| SEq a s t => fun (tau:var -> term) =>
Equ (tpinterp a)
(eval e a s (sigma >> tau) (fun n => Action _ (phi n) tau))
(eval e a t (sigma >> tau) (fun n => Action _ (phi n) tau))
end.
Theorem eval_thm1 (e : nat -> stp) (a : stp) (s : stm e a) (sigma tau:var -> term) (phi:forall n:nat, Elt (tpinterp (e n))) (psi:forall n:nat, Elt (tpinterp (e n))) :
(forall n, Equ (tpinterp (e n)) (phi n) (phi n)) ->
(forall n, Equ (tpinterp (e n)) (psi n) (Action (tpinterp (e n)) (phi n) tau)) ->
Equ (tpinterp a) (eval e a s sigma phi) (eval e a s sigma phi)
/\
Equ (tpinterp a) (Action (tpinterp a) (eval e a s sigma phi) tau) (eval e a s (sigma >> tau) psi).
Theorem eval_thm2 (e : nat -> stp) (a : stp) (s : stm e a) (sigma:var -> term) (phi psi:forall n:nat, Elt (tpinterp (e n))) :
(forall n, Equ (tpinterp (e n)) (phi n) (psi n)) ->
Equ (tpinterp a) (eval e a s sigma phi) (eval e a s sigma psi).
Theorem eval_thm3 (e : nat -> stp) (a : stp) (s : stm e a) (sigma:var -> term) (phi:forall n:nat, Elt (tpinterp (e n))) :
(forall n, Equ (tpinterp (e n)) (phi n) (phi n)) ->
Equ (tpinterp a) (eval e a s sigma phi) (eval e a s sigma phi).
Theorem eval_thm_ids e (phi:forall n, Elt (tpinterp (e n))) (Hphi:forall n, Equ (tpinterp (e n)) (phi n) (phi n)) (s:stm e o) sigma tau :
eval e o s (sigma >> tau) (fun n => Action _ (phi n) tau) ids
<->
eval e o s sigma phi tau.
Lemma eval_SImp_E e phi (Hphi:forall x, Equ (tpinterp (e x)) (phi x) (phi x)) (s t:stm e o) sigma tau :
eval e o (SImp e s t) sigma phi tau
->
(forall mu, eval e o s sigma phi (tau >> mu) -> eval e o t sigma phi (tau >> mu)).
Lemma eval_SImp_I e phi (Hphi:forall x, Equ (tpinterp (e x)) (phi x) (phi x)) (s t:stm e o) sigma tau :
(forall mu, eval e o s sigma phi (tau >> mu) -> eval e o t sigma phi (tau >> mu))
->
eval e o (SImp e s t) sigma phi tau.
Lemma eval_SEq_I e (phi: forall x, Elt (tpinterp (e x))) (Hphi:forall x, Equ (tpinterp (e x)) (phi x) (phi x)) a (s t:stm e a) sigma tau :
Equ (tpinterp a) (Action (tpinterp a) (eval e a s sigma phi) tau) (Action (tpinterp a) (eval e a t sigma phi) tau)
->
eval e o (SEq e a s t) sigma phi tau.
Lemma eval_SEq_E e (phi: forall x, Elt (tpinterp (e x))) (Hphi:forall x, Equ (tpinterp (e x)) (phi x) (phi x)) a (s t:stm e a) sigma tau :
eval e o (SEq e a s t) sigma phi tau
->
Equ (tpinterp a) (Action (tpinterp a) (eval e a s sigma phi) tau) (Action (tpinterp a) (eval e a t sigma phi) tau).
Lemma eval_SAll_I e (phi: forall x, Elt (tpinterp (e x))) a (s:stm (a.:e) o) sigma tau :
(forall mu z, Equ (tpinterp a) z z -> eval (a.:e) o s (sigma >> tau >> mu) (fun n => match n with O => z | S n' => Action _ (phi n') (tau >> mu) end) ids)
->
eval e o (SAll e a s) sigma phi tau.
Lemma eval_SAll_E e (phi: forall x, Elt (tpinterp (e x))) a (s:stm (a.:e) o) sigma tau :
eval e o (SAll e a s) sigma phi tau
->
(forall mu z, Equ (tpinterp a) z z -> eval (a.:e) o s (sigma >> tau >> mu) (fun n => match n with O => z | S n' => Action _ (phi n') (tau >> mu) end) ids).
Lemma eval_stmshift_aux e b (s:stm e b) a j sigma (phi:forall x, Elt (tpinterp (e x))) (psi:forall x, Elt (tpinterp (push_stp_into_env a e j x))) :
(forall x, Equ _ (psi x) (psi x)) ->
(forall x, Equ (tpinterp (e x)) (eq_rect (push_stp_into_env a e j (stmshift_var j x)) (fun a:stp => Elt (tpinterp a)) (psi (stmshift_var j x)) (e x) (stmshift_var_eq a e j x)) (phi x)) ->
Equ (tpinterp b) (eval (push_stp_into_env a e j) b (stmshift_aux e b s a j) sigma psi) (eval e b s sigma phi).
Lemma eval_stmshift a e b s sigma (phi:forall x, Elt (tpinterp (e x))) (psi:forall x, Elt (tpinterp ((a .: e) x))) :
(forall x, Equ _ (psi x) (psi x)) ->
(forall x, Equ (tpinterp (e x)) (phi x) (psi (S x))) ->
Equ (tpinterp b) (eval (a.:e) b (stmshift a e b s) sigma psi) (eval e b s sigma phi).
Lemma eval_stmparsubst e b (s:stm e b) e' (theta:forall x, stm e' (e x)) sigma (phi:forall x, Elt (tpinterp (e' x))) (psi:forall x, Elt (tpinterp (e x))) :
(forall x, Equ (tpinterp (e' x)) (phi x) (phi x)) ->
(forall x, Equ (tpinterp (e x)) (psi x) (eval e' (e x) (theta x) sigma phi)) ->
Equ (tpinterp b) (eval e' b (stmparsubst e b e' theta s) sigma phi) (eval e b s sigma psi).
Lemma eval_stmsubst a e b s t sigma (phi:forall x, Elt (tpinterp (e x))) (psi:forall x, Elt (tpinterp ((a .: e) x))) :
(forall x, Equ (tpinterp (e x)) (phi x) (psi (S x))) ->
(Equ (tpinterp a) (psi 0) (eval e a t sigma phi)) ->
Equ (tpinterp b) (eval e b (stmsubst a e b s t) sigma phi) (eval (a.:e) b s sigma psi).
Lemma eval_beta e phi (Hphi:forall x, Equ (tpinterp (e x)) (phi x) (phi x)) a b (s:stm (a.:e) b) (t:stm e a) sigma :
Equ (tpinterp b)
(eval e b (SAp e a b (SLam e a b s) t) sigma phi)
(eval e b (stmsubst a e b s t) sigma phi).
Lemma eval_eta e phi (Hphi:forall x, Equ (tpinterp (e x)) (phi x) (phi x)) a b (s:stm e (ar a b)) sigma :
Equ (tpinterp (ar a b))
(eval e (ar a b) (SLam e a b (SAp (a.:e) a b (stmshift a e (ar a b) s) (SDB (a.:e) 0))) sigma phi)
(eval e (ar a b) s sigma phi).
Lemma eval_conv_1 e phi (Hphi:forall x, Equ (tpinterp (e x)) (phi x) (phi x)) a (s t:stm e a) sigma :
conv_1 e a s t -> Equ (tpinterp a) (eval e a s sigma phi) (eval e a t sigma phi).
Lemma eval_conv e phi (Hphi:forall x, Equ (tpinterp (e x)) (phi x) (phi x)) a (s t:stm e a) sigma :
conv e a s t -> Equ (tpinterp a) (eval e a s sigma phi) (eval e a t sigma phi).
Lemma eval_SFal e sigma phi tau : ~ eval e o (SFal e) sigma phi tau.
Lemma SLeibEq_char e phi (Hphi:forall n, Equ _ (phi n) (phi n)) a x y sigma tau :
Equ (tpinterp a) x x ->
Equ (tpinterp a) y y ->
(eval e (ar a (ar a o)) (SLeibEq e a) sigma phi ids x ids y tau
<->
forall mu p, Equ (tpinterp (ar a o)) p p -> forall nu, p ids (Action _ x (tau >> mu)) nu -> p ids (Action _ y (tau >> mu)) nu).
Lemma eval_SLeibEq_I e phi (Hphi:forall n, Equ _ (phi n) (phi n)) a x y sigma tau :
Equ (tpinterp a) x x ->
Equ (tpinterp a) y y ->
Equ _ (Action (tpinterp a) x tau) (Action (tpinterp a) y tau)
->
eval e (ar a (ar a o)) (SLeibEq e a) sigma phi ids x ids y tau.
Lemma nd_sound e G s :
nd e G s ->
forall sigma phi, (forall x, Equ (tpinterp (e x)) (phi x) (phi x)) ->
forall tau,
(forall u, G u -> eval e o u sigma phi tau) ->
eval e o s sigma phi tau.
Lemma botRiId : RiId (fun _ => False).
Lemma topRiId : RiId (fun _ => True).
Lemma meetRiId X (Xs:RiId X) Y (Ys:RiId Y) : RiId (fun sigma => X sigma /\ Y sigma).
Lemma joinRiId X (Xs:RiId X) Y (Ys:RiId Y) : RiId (fun sigma => X sigma \/ Y sigma).
Lemma bigjoinRiId (C:((var -> term) -> Prop) -> Prop) (Cs:forall X, C X -> RiId X) : RiId (fun sigma => exists X, C X /\ X sigma).
Lemma impRiId X (Xs:RiId X) Y (Ys:RiId Y) : RiId (fun sigma => exists Z, (RiId Z /\ (forall tau, X tau -> Z tau -> Y tau)) /\ Z sigma).
Definition SNot e : stm e (ar o o) :=
SLam e o o (SImp (o.:e) (SDB (o.:e) 0) (SFal (o.:e))).
Definition SNotOp e (s : stm e o) : stm e o :=
SAp e o o (SNot e) s.
Lemma eval_SNot_E e phi (Hphi:forall x, Equ (tpinterp (e x)) (phi x) (phi x)) sigma s tau :
eval e o (SAp e o o (SNot e) s) sigma phi tau
->
forall mu, ~ eval e o s sigma phi (tau >> mu).
Lemma eval_SNot_I e phi (Hphi:forall x, Equ (tpinterp (e x)) (phi x) (phi x)) sigma s tau :
(forall mu, ~ eval e o s sigma phi (tau >> mu))
->
eval e o (SAp e o o (SNot e) s) sigma phi tau.
Lemma eval_SNotOp_E e phi (Hphi:forall x, Equ (tpinterp (e x)) (phi x) (phi x)) sigma s tau :
eval e o (SNotOp e s) sigma phi tau
->
forall mu, ~ eval e o s sigma phi (tau >> mu).
Lemma eval_SNotOp_I e phi (Hphi:forall x, Equ (tpinterp (e x)) (phi x) (phi x)) sigma s tau :
(forall mu, ~ eval e o s sigma phi (tau >> mu))
->
eval e o (SNotOp e s) sigma phi tau.
Definition charfn (a : stp) (p:Elt (tpinterp a) -> Prop) (sigma:var -> term) (x:Elt (tpinterp a)) tau : Prop :=
p (Action _ x tau).
Theorem charfnEqu (a : stp) (p:Elt (tpinterp a) -> Prop) :
(forall x sigma, p x -> p (Action _ x sigma))
->
(forall x y, p x -> Equ _ x y -> p y)
->
Equ (tpinterp (ar a o)) (charfn a p) (charfn a p).
Definition singfn (a : stp) (x:Elt (tpinterp a)) (sigma:var -> term) (z:Elt (tpinterp a)) tau : Prop :=
Equ (tpinterp a) (Action _ z tau) (Action _ x (sigma >> tau)).
Theorem singfnEqu (a : stp) (x:Elt (tpinterp a)) :
Equ _ x x
->
Equ (tpinterp (ar a o)) (singfn a x) (singfn a x).
Lemma SLeibEq_char1 e a phi (Hphi:forall n, Equ (tpinterp ((a.:a.:e) n)) (phi n) (phi n)) sigma tau :
eval (a.:a.:e) o
(SAll (a.:a.:e) (ar a o) (SImp (ar a o.:a.:a.:e)
(SAp (ar a o.:a.:a.:e) a o (SDB (ar a o.:a.:a.:e) 0) (SDB (ar a o.:a.:a.:e) 2))
(SAp (ar a o.:a.:a.:e) a o (SDB (ar a o.:a.:a.:e) 0) (SDB (ar a o.:a.:a.:e) 1)))) sigma phi tau
<->
forall mu p, Equ (tpinterp (ar a o)) p p -> forall nu, p ids (Action _ (phi 1) (tau >> mu)) nu -> p ids (Action _ (phi 0) (tau >> mu)) nu.
Lemma eval_SLeibEq_I' e phi (Hphi:forall n, Equ _ (phi n) (phi n)) a x y sigma tau :
Equ (tpinterp a) x y
->
eval e (ar a (ar a o)) (SLeibEq e a) sigma phi ids x ids y tau.
Lemma eval_SLeibEq_E e phi (Hphi:forall n, Equ _ (phi n) (phi n)) a x y sigma tau :
Equ (tpinterp a) x x ->
Equ (tpinterp a) y y ->
eval e (ar a (ar a o)) (SLeibEq e a) sigma phi ids x ids y tau ->
Equ _ (Action _ x tau) (Action _ y tau).
Lemma eval_SLeibEq_i e phi (Hphi:forall n, Equ _ (phi n) (phi n)) s t sigma :
eval e (ar i (ar i o)) (SLeibEq e i) sigma phi ids s ids t ids <->
s = t.
Lemma eval_SLeibEq_nat e phi (Hphi:forall n, Equ _ (phi n) (phi n)) n m sigma :
eval e (ar na (ar na o)) (SLeibEq e na) sigma phi ids n ids m ids <->
n = m.
Lemma eval_SLeibEq_o e phi (Hphi:forall n, Equ _ (phi n) (phi n)) P Q sigma :
RiId P -> RiId Q ->
(eval e (ar o (ar o o)) (SLeibEq e o) sigma phi ids P ids Q ids <->
forall tau, P tau <-> Q tau).
Lemma eval_SLeibEq_ar e phi (Hphi:forall n, Equ _ (phi n) (phi n)) a b f g sigma :
Equ (tpinterp (ar a b)) f f ->
Equ (tpinterp (ar a b)) g g ->
(eval e (ar (ar a b) (ar (ar a b) o)) (SLeibEq e (ar a b)) sigma phi ids f ids g ids <->
forall sigma x, Equ (tpinterp a) x x -> Equ (tpinterp b) (f sigma x) (g sigma x)).
Require Import Autosubst.
Inductive stp : Type :=
| o : stp
| i : stp
| na : stp
| ar : stp -> stp -> stp.
Inductive stm (e : nat -> stp) : stp -> Type :=
| SDB n : stm e (e n)
| SULam : stm e (ar (ar i i) i)
| SUAp : stm e (ar i (ar i i))
| SAp a b : stm e (ar a b) -> stm e a -> stm e b
| SLam a b : stm (a.:e) b -> stm e (ar a b)
| SImp : stm e o -> stm e o -> stm e o
| SAll a : stm (a.:e) o -> stm e o
| SEq a : stm e a -> stm e a -> stm e o.
Fixpoint push_stp_into_env (a:stp) (e:var -> stp) (j:nat) : var -> stp :=
match j with
| O => a.:e
| S j => (e 0).:(push_stp_into_env a (fun x => e (S x)) j)
end.
Fixpoint stmshift_var (j x:nat) : nat :=
match j with
| O => S x
| S j => match x with
| O => O
| S x => S (stmshift_var j x)
end
end.
Definition stmshift_var_eq a e j x : push_stp_into_env a e j (stmshift_var j x) = e x.
Defined.
Lemma stmshift_var_eq_match_eq a e j x :
match
stmshift_var_eq a e j x in (_ = y)
return
(push_stp_into_env a e j
(stmshift_var j x) = y)
with
| eq_refl => eq_refl
end
= stmshift_var_eq a e j x.
Lemma stmshift_var_eq_match_commutes a e j (x:nat) :
forall Y:stp -> Type, forall Z:stp -> Type, forall W, forall F:forall b, Y b -> Z b,
F (e x) (match stmshift_var_eq a e j x in (_ = y) return Y y with eq_refl => W end)
=
match stmshift_var_eq a e j x in (_ = y) return Z y with
eq_refl => F (push_stp_into_env a e j (stmshift_var j x)) W
end.
Definition stmshift_aux : forall e b, stm e b -> forall a j, stm (push_stp_into_env a e j) b.
Defined.
Definition stmshift : forall a e b, stm e b -> stm (a.:e) b.
Defined.
Definition pushsubstunder e e' a (theta:forall x, stm e' (e x)) : forall x, stm (a.:e') ((a.:e) x).
Defined.
Definition stmparsubst : forall e b e' (theta:forall x, stm e' (e x)), stm e b -> stm e' b.
Defined.
Definition stmsubst : forall a e b, stm (a.:e) b -> stm e a -> stm e b.
Defined.
Inductive conv_1 e : forall a, stm e a -> stm e a -> Prop :=
| conv_beta a b (s:stm (a.:e) b) (t:stm e a) :
conv_1 e b (SAp e a b (SLam e a b s) t) (stmsubst a e b s t)
| conv_eta a b (s:stm e (ar a b)) :
conv_1 e (ar a b) (SLam e a b (SAp (a.:e) a b (stmshift a e (ar a b) s) (SDB (a.:e) 0))) s
| conv_SApL a b (s1 s2:stm e (ar a b)) (t:stm e a) :
conv_1 e (ar a b) s1 s2 -> conv_1 e b (SAp e a b s1 t) (SAp e a b s2 t)
| conv_SApR a b (s:stm e (ar a b)) (t1 t2:stm e a) :
conv_1 e a t1 t2 -> conv_1 e b (SAp e a b s t1) (SAp e a b s t2)
| conv_SLam a b (s1 s2:stm (a.:e) b) :
conv_1 (a.:e) b s1 s2 -> conv_1 e (ar a b) (SLam e a b s1) (SLam e a b s2)
| conv_SImpL (s1 s2:stm e o) (t:stm e o) :
conv_1 e o s1 s2 -> conv_1 e o (SImp e s1 t) (SImp e s2 t)
| conv_SImpR (s:stm e o) (t1 t2:stm e o) :
conv_1 e o t1 t2 -> conv_1 e o (SImp e s t1) (SImp e s t2)
| conv_SAll a (s1 s2:stm (a.:e) o) :
conv_1 (a.:e) o s1 s2 -> conv_1 e o (SAll e a s1) (SAll e a s2)
| conv_SEqL a (s1 s2:stm e a) (t:stm e a) :
conv_1 e a s1 s2 -> conv_1 e o (SEq e a s1 t) (SEq e a s2 t)
| conv_SEqR a (s:stm e a) (t1 t2:stm e a) :
conv_1 e a t1 t2 -> conv_1 e o (SEq e a s t1) (SEq e a s t2)
.
Inductive conv e : forall a, stm e a -> stm e a -> Prop :=
| conv_one a (s t:stm e a) : conv_1 e a s t -> conv e a s t
| conv_ref a (s:stm e a) : conv e a s s
| conv_sym a (s t:stm e a) : conv e a s t -> conv e a t s
| conv_tra a (s t u:stm e a) : conv e a s t -> conv e a t u -> conv e a s u
.
Definition SFal e : stm e o :=
SAll e o (SDB (o.:e) 0).
Definition SLeibEq e a : stm e (ar a (ar a o)) :=
SLam e a (ar a o)
(SLam (a.:e) a o
(SAll (a.:a.:e) (ar a o)
(SImp (ar a o.:a.:a.:e)
(SAp (ar a o.:a.:a.:e) a o (SDB (ar a o.:a.:a.:e) 0) (SDB (ar a o.:a.:a.:e) 2))
(SAp (ar a o.:a.:a.:e) a o (SDB (ar a o.:a.:a.:e) 0) (SDB (ar a o.:a.:a.:e) 1))))).
Definition SLeibEqOp e a (s t:stm e a) : stm e o :=
SAp e a o (SAp e a (ar a o) (SLeibEq e a) s) t.
Definition SUApOp e (s t:stm e i) : stm e i :=
SAp e i i (SAp e i (ar i i) (SUAp e) s) t.
Definition SULamOp e (s:stm e (ar i i)) : stm e i :=
SAp e (ar i i) i (SULam e) s.
Inductive nd (e:nat -> stp) (G : stm e o -> Prop) : stm e o -> Prop :=
| ndH s : G s -> nd e G s
| ndConv s t : conv e o s t -> nd e G s -> nd e G t
| ndII s t : nd e (fun u => G u \/ u = s) t -> nd e G (SImp e s t)
| ndIE s t : nd e G (SImp e s t) -> nd e G s -> nd e G t
| ndAI a s : nd (a.:e) (fun u => exists v, G v /\ u = stmshift a e o v) s -> nd e G (SAll e a s)
| ndAE a s (t : stm e a) : nd e G (SAll e a s) -> nd e G (stmsubst a e o s t)
| ndEI a s : nd e G (SEq e a s s)
| ndEE a s t : nd e G (SEq e a s t) -> nd e G (SLeibEqOp e a s t)
| ndPropExt s t : nd e (fun u => G u \/ u = s) t -> nd e (fun u => G u \/ u = t) s -> nd e G (SEq e o s t)
| ndXi a b s t : nd (a.:e) (fun u => exists v, G v /\ u = stmshift a e o v) (SEq (a.:e) b s t) -> nd e G (SEq e (ar a b) (SLam e a b s) (SLam e a b t))
| ndApInj1 s1 s2 t : nd e G (SEq e i (SUApOp e s1 t) (SUApOp e s2 t)) -> nd e G (SEq e i s1 s2)
| ndApInj2 s t1 t2 : nd e G (SEq e i (SUApOp e s t1) (SUApOp e s t2)) -> nd e G (SEq e i t1 t2)
| ndLamInj s t : nd e G (SEq e i (SULamOp e s) (SULamOp e t)) -> nd e G (SEq e (ar i i) s t)
| ndApNotLam s t u : nd e G (SEq e i (SUApOp e s t) (SULamOp e u)) -> nd e G (SFal e)
.
Inductive term : Type :=
| Va (x : var)
| Ap (s t : term)
| La (s : {bind term}).
Instance Ids_term : Ids term.
Instance Rename_term : Rename term.
Instance Subst_term : Subst term.
Instance SubstLemmas_term : SubstLemmas term.
Definition RiId (X : (var -> term) -> Prop) : Prop :=
forall sigma, X sigma -> forall tau, X (sigma >> tau).
Lemma ActionRiId X (Xs:RiId X) sigma : RiId (fun tau => X (sigma >> tau)).
Record Mset : Type :=
mkMset {
Elt : Type;
Equ : Elt -> Elt -> Prop;
Action : Elt -> (var -> term) -> Elt;
EquSym : forall x y, Equ x y -> Equ y x;
EquTra : forall x y z, Equ x y -> Equ y z -> Equ x z;
ActionEqu : forall x y sigma, Equ x y -> Equ (Action x sigma) (Action y sigma);
ActionId : forall x y, Equ x y -> Equ (Action x ids) y;
ActionComp : forall x y sigma tau, Equ x y -> Equ (Action x (sigma >> tau)) (Action (Action y sigma) tau)
}.
Lemma EquRef1 (A:Mset) x y : Equ A x y -> Equ A x x.
Lemma EquRef2 (A:Mset) x y : Equ A x y -> Equ A y y.
Lemma ActionEqu1 (A:Mset) x sigma : Equ A x x -> Equ A (Action A x sigma) (Action A x sigma).
Definition Do : Mset.
Defined.
Definition Di : Mset.
Defined.
Definition Dnat : Mset.
Defined.
Definition Dar (A B:Mset) : Mset.
Defined.
Fixpoint tpinterp (a : stp) : Mset :=
match a with
| o => Do
| i => Di
| na => Dnat
| ar a b => Dar (tpinterp a) (tpinterp b)
end.
Fixpoint defaultelt (b:stp) : Elt (tpinterp b) :=
match b with
| o => fun sigma => False
| i => La (Va 0)
| na => 0
| ar a b => fun sigma x => defaultelt b
end.
Definition GlobalElt (A:Mset) (x:Elt A) : Prop :=
forall sigma:var -> term, Equ A (Action A x sigma) x.
Lemma defaultelt_GlobalElt (b:stp) : GlobalElt (tpinterp b) (defaultelt b).
Definition UAp : Elt (tpinterp (ar i (ar i i))) := fun sigma s => fun tau t => Ap (s.[tau]) t.
Definition ULam : Elt (tpinterp (ar (ar i i) i)) := fun sigma f => La (f (ren S) (Va 0)).
Lemma UAp_Global : GlobalElt (tpinterp (ar i (ar i i))) UAp.
Lemma UAp_OK : Equ _ UAp UAp.
Lemma ULam_Global : GlobalElt (tpinterp (ar (ar i i) i)) ULam.
Lemma ULam_OK : Equ (tpinterp (ar (ar i i) i)) ULam ULam.
Fixpoint eval (e : nat -> stp) (a : stp) (s : stm e a) (sigma:var -> term) (phi:forall n:nat, Elt (tpinterp (e n))) : Elt (tpinterp a) :=
match s with
| SDB n => phi n
| SULam => ULam
| SUAp => UAp
| SAp a b s t => eval e (ar a b) s sigma phi ids (eval e a t sigma phi)
| SLam a b s => fun (tau:var -> term) (x:Elt (tpinterp a)) =>
eval (a.:e) b s (sigma >> tau)
(fun n => match n with O => x | S n' => Action (tpinterp (e n')) (phi n') tau end)
| SImp s t => fun (tau:var -> term) =>
exists Z: (var -> term) -> Prop, RiId Z /\ Z tau /\
(forall mu, Z mu -> eval e o s (sigma >> mu) (fun n => Action _ (phi n) mu) ids
-> eval e o t (sigma >> mu) (fun n => Action _ (phi n) mu) ids)
| SAll a s => fun (tau:var -> term) =>
forall mu, forall x : Elt (tpinterp a), Equ (tpinterp a) x x ->
(eval (a.:e) o s (sigma >> tau >> mu)
(fun n => match n with O => x | S n' => Action (tpinterp (e n')) (phi n') (tau >> mu) end)) ids
| SEq a s t => fun (tau:var -> term) =>
Equ (tpinterp a)
(eval e a s (sigma >> tau) (fun n => Action _ (phi n) tau))
(eval e a t (sigma >> tau) (fun n => Action _ (phi n) tau))
end.
Theorem eval_thm1 (e : nat -> stp) (a : stp) (s : stm e a) (sigma tau:var -> term) (phi:forall n:nat, Elt (tpinterp (e n))) (psi:forall n:nat, Elt (tpinterp (e n))) :
(forall n, Equ (tpinterp (e n)) (phi n) (phi n)) ->
(forall n, Equ (tpinterp (e n)) (psi n) (Action (tpinterp (e n)) (phi n) tau)) ->
Equ (tpinterp a) (eval e a s sigma phi) (eval e a s sigma phi)
/\
Equ (tpinterp a) (Action (tpinterp a) (eval e a s sigma phi) tau) (eval e a s (sigma >> tau) psi).
Theorem eval_thm2 (e : nat -> stp) (a : stp) (s : stm e a) (sigma:var -> term) (phi psi:forall n:nat, Elt (tpinterp (e n))) :
(forall n, Equ (tpinterp (e n)) (phi n) (psi n)) ->
Equ (tpinterp a) (eval e a s sigma phi) (eval e a s sigma psi).
Theorem eval_thm3 (e : nat -> stp) (a : stp) (s : stm e a) (sigma:var -> term) (phi:forall n:nat, Elt (tpinterp (e n))) :
(forall n, Equ (tpinterp (e n)) (phi n) (phi n)) ->
Equ (tpinterp a) (eval e a s sigma phi) (eval e a s sigma phi).
Theorem eval_thm_ids e (phi:forall n, Elt (tpinterp (e n))) (Hphi:forall n, Equ (tpinterp (e n)) (phi n) (phi n)) (s:stm e o) sigma tau :
eval e o s (sigma >> tau) (fun n => Action _ (phi n) tau) ids
<->
eval e o s sigma phi tau.
Lemma eval_SImp_E e phi (Hphi:forall x, Equ (tpinterp (e x)) (phi x) (phi x)) (s t:stm e o) sigma tau :
eval e o (SImp e s t) sigma phi tau
->
(forall mu, eval e o s sigma phi (tau >> mu) -> eval e o t sigma phi (tau >> mu)).
Lemma eval_SImp_I e phi (Hphi:forall x, Equ (tpinterp (e x)) (phi x) (phi x)) (s t:stm e o) sigma tau :
(forall mu, eval e o s sigma phi (tau >> mu) -> eval e o t sigma phi (tau >> mu))
->
eval e o (SImp e s t) sigma phi tau.
Lemma eval_SEq_I e (phi: forall x, Elt (tpinterp (e x))) (Hphi:forall x, Equ (tpinterp (e x)) (phi x) (phi x)) a (s t:stm e a) sigma tau :
Equ (tpinterp a) (Action (tpinterp a) (eval e a s sigma phi) tau) (Action (tpinterp a) (eval e a t sigma phi) tau)
->
eval e o (SEq e a s t) sigma phi tau.
Lemma eval_SEq_E e (phi: forall x, Elt (tpinterp (e x))) (Hphi:forall x, Equ (tpinterp (e x)) (phi x) (phi x)) a (s t:stm e a) sigma tau :
eval e o (SEq e a s t) sigma phi tau
->
Equ (tpinterp a) (Action (tpinterp a) (eval e a s sigma phi) tau) (Action (tpinterp a) (eval e a t sigma phi) tau).
Lemma eval_SAll_I e (phi: forall x, Elt (tpinterp (e x))) a (s:stm (a.:e) o) sigma tau :
(forall mu z, Equ (tpinterp a) z z -> eval (a.:e) o s (sigma >> tau >> mu) (fun n => match n with O => z | S n' => Action _ (phi n') (tau >> mu) end) ids)
->
eval e o (SAll e a s) sigma phi tau.
Lemma eval_SAll_E e (phi: forall x, Elt (tpinterp (e x))) a (s:stm (a.:e) o) sigma tau :
eval e o (SAll e a s) sigma phi tau
->
(forall mu z, Equ (tpinterp a) z z -> eval (a.:e) o s (sigma >> tau >> mu) (fun n => match n with O => z | S n' => Action _ (phi n') (tau >> mu) end) ids).
Lemma eval_stmshift_aux e b (s:stm e b) a j sigma (phi:forall x, Elt (tpinterp (e x))) (psi:forall x, Elt (tpinterp (push_stp_into_env a e j x))) :
(forall x, Equ _ (psi x) (psi x)) ->
(forall x, Equ (tpinterp (e x)) (eq_rect (push_stp_into_env a e j (stmshift_var j x)) (fun a:stp => Elt (tpinterp a)) (psi (stmshift_var j x)) (e x) (stmshift_var_eq a e j x)) (phi x)) ->
Equ (tpinterp b) (eval (push_stp_into_env a e j) b (stmshift_aux e b s a j) sigma psi) (eval e b s sigma phi).
Lemma eval_stmshift a e b s sigma (phi:forall x, Elt (tpinterp (e x))) (psi:forall x, Elt (tpinterp ((a .: e) x))) :
(forall x, Equ _ (psi x) (psi x)) ->
(forall x, Equ (tpinterp (e x)) (phi x) (psi (S x))) ->
Equ (tpinterp b) (eval (a.:e) b (stmshift a e b s) sigma psi) (eval e b s sigma phi).
Lemma eval_stmparsubst e b (s:stm e b) e' (theta:forall x, stm e' (e x)) sigma (phi:forall x, Elt (tpinterp (e' x))) (psi:forall x, Elt (tpinterp (e x))) :
(forall x, Equ (tpinterp (e' x)) (phi x) (phi x)) ->
(forall x, Equ (tpinterp (e x)) (psi x) (eval e' (e x) (theta x) sigma phi)) ->
Equ (tpinterp b) (eval e' b (stmparsubst e b e' theta s) sigma phi) (eval e b s sigma psi).
Lemma eval_stmsubst a e b s t sigma (phi:forall x, Elt (tpinterp (e x))) (psi:forall x, Elt (tpinterp ((a .: e) x))) :
(forall x, Equ (tpinterp (e x)) (phi x) (psi (S x))) ->
(Equ (tpinterp a) (psi 0) (eval e a t sigma phi)) ->
Equ (tpinterp b) (eval e b (stmsubst a e b s t) sigma phi) (eval (a.:e) b s sigma psi).
Lemma eval_beta e phi (Hphi:forall x, Equ (tpinterp (e x)) (phi x) (phi x)) a b (s:stm (a.:e) b) (t:stm e a) sigma :
Equ (tpinterp b)
(eval e b (SAp e a b (SLam e a b s) t) sigma phi)
(eval e b (stmsubst a e b s t) sigma phi).
Lemma eval_eta e phi (Hphi:forall x, Equ (tpinterp (e x)) (phi x) (phi x)) a b (s:stm e (ar a b)) sigma :
Equ (tpinterp (ar a b))
(eval e (ar a b) (SLam e a b (SAp (a.:e) a b (stmshift a e (ar a b) s) (SDB (a.:e) 0))) sigma phi)
(eval e (ar a b) s sigma phi).
Lemma eval_conv_1 e phi (Hphi:forall x, Equ (tpinterp (e x)) (phi x) (phi x)) a (s t:stm e a) sigma :
conv_1 e a s t -> Equ (tpinterp a) (eval e a s sigma phi) (eval e a t sigma phi).
Lemma eval_conv e phi (Hphi:forall x, Equ (tpinterp (e x)) (phi x) (phi x)) a (s t:stm e a) sigma :
conv e a s t -> Equ (tpinterp a) (eval e a s sigma phi) (eval e a t sigma phi).
Lemma eval_SFal e sigma phi tau : ~ eval e o (SFal e) sigma phi tau.
Lemma SLeibEq_char e phi (Hphi:forall n, Equ _ (phi n) (phi n)) a x y sigma tau :
Equ (tpinterp a) x x ->
Equ (tpinterp a) y y ->
(eval e (ar a (ar a o)) (SLeibEq e a) sigma phi ids x ids y tau
<->
forall mu p, Equ (tpinterp (ar a o)) p p -> forall nu, p ids (Action _ x (tau >> mu)) nu -> p ids (Action _ y (tau >> mu)) nu).
Lemma eval_SLeibEq_I e phi (Hphi:forall n, Equ _ (phi n) (phi n)) a x y sigma tau :
Equ (tpinterp a) x x ->
Equ (tpinterp a) y y ->
Equ _ (Action (tpinterp a) x tau) (Action (tpinterp a) y tau)
->
eval e (ar a (ar a o)) (SLeibEq e a) sigma phi ids x ids y tau.
Lemma nd_sound e G s :
nd e G s ->
forall sigma phi, (forall x, Equ (tpinterp (e x)) (phi x) (phi x)) ->
forall tau,
(forall u, G u -> eval e o u sigma phi tau) ->
eval e o s sigma phi tau.
Lemma botRiId : RiId (fun _ => False).
Lemma topRiId : RiId (fun _ => True).
Lemma meetRiId X (Xs:RiId X) Y (Ys:RiId Y) : RiId (fun sigma => X sigma /\ Y sigma).
Lemma joinRiId X (Xs:RiId X) Y (Ys:RiId Y) : RiId (fun sigma => X sigma \/ Y sigma).
Lemma bigjoinRiId (C:((var -> term) -> Prop) -> Prop) (Cs:forall X, C X -> RiId X) : RiId (fun sigma => exists X, C X /\ X sigma).
Lemma impRiId X (Xs:RiId X) Y (Ys:RiId Y) : RiId (fun sigma => exists Z, (RiId Z /\ (forall tau, X tau -> Z tau -> Y tau)) /\ Z sigma).
Definition SNot e : stm e (ar o o) :=
SLam e o o (SImp (o.:e) (SDB (o.:e) 0) (SFal (o.:e))).
Definition SNotOp e (s : stm e o) : stm e o :=
SAp e o o (SNot e) s.
Lemma eval_SNot_E e phi (Hphi:forall x, Equ (tpinterp (e x)) (phi x) (phi x)) sigma s tau :
eval e o (SAp e o o (SNot e) s) sigma phi tau
->
forall mu, ~ eval e o s sigma phi (tau >> mu).
Lemma eval_SNot_I e phi (Hphi:forall x, Equ (tpinterp (e x)) (phi x) (phi x)) sigma s tau :
(forall mu, ~ eval e o s sigma phi (tau >> mu))
->
eval e o (SAp e o o (SNot e) s) sigma phi tau.
Lemma eval_SNotOp_E e phi (Hphi:forall x, Equ (tpinterp (e x)) (phi x) (phi x)) sigma s tau :
eval e o (SNotOp e s) sigma phi tau
->
forall mu, ~ eval e o s sigma phi (tau >> mu).
Lemma eval_SNotOp_I e phi (Hphi:forall x, Equ (tpinterp (e x)) (phi x) (phi x)) sigma s tau :
(forall mu, ~ eval e o s sigma phi (tau >> mu))
->
eval e o (SNotOp e s) sigma phi tau.
Definition charfn (a : stp) (p:Elt (tpinterp a) -> Prop) (sigma:var -> term) (x:Elt (tpinterp a)) tau : Prop :=
p (Action _ x tau).
Theorem charfnEqu (a : stp) (p:Elt (tpinterp a) -> Prop) :
(forall x sigma, p x -> p (Action _ x sigma))
->
(forall x y, p x -> Equ _ x y -> p y)
->
Equ (tpinterp (ar a o)) (charfn a p) (charfn a p).
Definition singfn (a : stp) (x:Elt (tpinterp a)) (sigma:var -> term) (z:Elt (tpinterp a)) tau : Prop :=
Equ (tpinterp a) (Action _ z tau) (Action _ x (sigma >> tau)).
Theorem singfnEqu (a : stp) (x:Elt (tpinterp a)) :
Equ _ x x
->
Equ (tpinterp (ar a o)) (singfn a x) (singfn a x).
Lemma SLeibEq_char1 e a phi (Hphi:forall n, Equ (tpinterp ((a.:a.:e) n)) (phi n) (phi n)) sigma tau :
eval (a.:a.:e) o
(SAll (a.:a.:e) (ar a o) (SImp (ar a o.:a.:a.:e)
(SAp (ar a o.:a.:a.:e) a o (SDB (ar a o.:a.:a.:e) 0) (SDB (ar a o.:a.:a.:e) 2))
(SAp (ar a o.:a.:a.:e) a o (SDB (ar a o.:a.:a.:e) 0) (SDB (ar a o.:a.:a.:e) 1)))) sigma phi tau
<->
forall mu p, Equ (tpinterp (ar a o)) p p -> forall nu, p ids (Action _ (phi 1) (tau >> mu)) nu -> p ids (Action _ (phi 0) (tau >> mu)) nu.
Lemma eval_SLeibEq_I' e phi (Hphi:forall n, Equ _ (phi n) (phi n)) a x y sigma tau :
Equ (tpinterp a) x y
->
eval e (ar a (ar a o)) (SLeibEq e a) sigma phi ids x ids y tau.
Lemma eval_SLeibEq_E e phi (Hphi:forall n, Equ _ (phi n) (phi n)) a x y sigma tau :
Equ (tpinterp a) x x ->
Equ (tpinterp a) y y ->
eval e (ar a (ar a o)) (SLeibEq e a) sigma phi ids x ids y tau ->
Equ _ (Action _ x tau) (Action _ y tau).
Lemma eval_SLeibEq_i e phi (Hphi:forall n, Equ _ (phi n) (phi n)) s t sigma :
eval e (ar i (ar i o)) (SLeibEq e i) sigma phi ids s ids t ids <->
s = t.
Lemma eval_SLeibEq_nat e phi (Hphi:forall n, Equ _ (phi n) (phi n)) n m sigma :
eval e (ar na (ar na o)) (SLeibEq e na) sigma phi ids n ids m ids <->
n = m.
Lemma eval_SLeibEq_o e phi (Hphi:forall n, Equ _ (phi n) (phi n)) P Q sigma :
RiId P -> RiId Q ->
(eval e (ar o (ar o o)) (SLeibEq e o) sigma phi ids P ids Q ids <->
forall tau, P tau <-> Q tau).
Lemma eval_SLeibEq_ar e phi (Hphi:forall n, Equ _ (phi n) (phi n)) a b f g sigma :
Equ (tpinterp (ar a b)) f f ->
Equ (tpinterp (ar a b)) g g ->
(eval e (ar (ar a b) (ar (ar a b) o)) (SLeibEq e (ar a b)) sigma phi ids f ids g ids <->
forall sigma x, Equ (tpinterp a) x x -> Equ (tpinterp b) (f sigma x) (g sigma x)).