(** * Context *) Require Import Omega List Program.Equality. Require Import Autosubst. (*** Simple Types ***) Inductive stp : Type := | o : stp | i : stp | na : stp | ar : stp -> stp -> stp. (*** Simply Typed Terms ***) (*** SULam and SUAp are constants and could be generalized to having generic constants. SEq is a term constructor, but is equivalent to Leibniz Equality. Hence it could be omitted. It is included here because extensionality uses equality and so do the Untyped Lam Axioms. ***) 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. (*** Carefully written in order for some equations to hold with definitional equality: push_stp_into_env a e 0 is definitionally equal to a.:e ***) 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. revert e x. induction j as [|j IHj]; intros e x. - simpl. reflexivity. - simpl. destruct x as [|x]. + simpl. reflexivity. + simpl. rewrite <- (IHj (fun x => e (S x)) x). reflexivity. Defined. (*** The following two lemmas imply we can coerce using stmshift_var_eq with some safety. ***) 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. Proof. revert e x. induction j as [|j IHj]. - simpl. reflexivity. - simpl. intros e [|x]. + simpl. reflexivity. + simpl. unfold eq_ind. unfold eq_rect. rewrite (IHj (fun x => e (S x)) x) at 1. reflexivity. Qed. 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. Proof. intros Y Z W F. revert e x W. induction j as [|j IHj]. - simpl. reflexivity. - simpl. intros e [|x] W. + simpl. reflexivity. + simpl. unfold eq_ind. unfold eq_rect. simpl in W. rewrite stmshift_var_eq_match_eq. exact (IHj (fun x => e (S x)) x W). Qed. Definition stmshift_aux : forall e b, stm e b -> forall a j, stm (push_stp_into_env a e j) b. intros e b s. induction s as [e x| | |e b c s IHs t IHt|e b c s IHs|e s IHs t IHt|e b s IHs|e b s IHs t IHt]; intros a j. - rewrite <- (stmshift_var_eq a e j x). exact (SDB (push_stp_into_env a e j) (stmshift_var j x)). - apply SULam. - apply SUAp. - exact (SAp _ b c (IHs a j) (IHt a j)). - apply SLam. apply (IHs a (S j)). - exact (SImp _ (IHs a j) (IHt a j)). - apply SAll with (a := b). apply (IHs a (S j)). - apply SEq with (a := b). + exact (IHs a j). + exact (IHt a j). Defined. Definition stmshift : forall a e b, stm e b -> stm (a.:e) b. exact (fun a e b s => stmshift_aux e b s a 0). Defined. Definition pushsubstunder e e' a (theta:forall x, stm e' (e x)) : forall x, stm (a.:e') ((a.:e) x). intros [|x]. - simpl. exact (SDB (a.:e') 0). - simpl. exact (stmshift a e' (e x) (theta x)). Defined. Definition stmparsubst : forall e b e' (theta:forall x, stm e' (e x)), stm e b -> stm e' b. intros e b e' theta s. revert e' theta; induction s as [e x| | |e a b s IHs t IHt|e a b s IHs|e s IHs t IHt|e a s IHs|e a s IHs t IHt]; intros e' theta. - apply theta. - exact (SULam e'). - exact (SUAp e'). - exact (SAp e' a b (IHs e' theta) (IHt e' theta)). - apply SLam. apply (IHs (a.:e') (pushsubstunder e e' a theta)). - exact (SImp e' (IHs e' theta) (IHt e' theta)). - apply (SAll e' a). apply (IHs (a.:e') (pushsubstunder e e' a theta)). - exact (SEq e' a (IHs e' theta) (IHt e' theta)). Defined. Definition stmsubst : forall a e b, stm (a.:e) b -> stm e a -> stm e b. intros a e b s t. pose (e1 := a.:e). pose (theta := (fun n => match n as n' return stm e (e1 n') with O => t | S n' => SDB e n' end : stm e (e1 n))). exact (stmparsubst e1 b e theta s). 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 . (*** False ***) Definition SFal e : stm e o := SAll e o (SDB (o.:e) 0). (*** Leibniz equality ***) 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) (*** Equality rules, since we include it as a primitive term constructor. ***) | 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) (*** Extensionality Rules ***) | 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) (*** Since eta is included in conversion, the xi rule is enough to give full functional extensionality. ***) | 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)) (*** Rules for equational reasoning with untyped lambda terms represented in HOAS. A reasonable induction principle could probably be added. ***) | 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) . (*** Untyped lambda terms ***) Inductive term : Type := | Va (x : var) | Ap (s t : term) | La (s : {bind term}). Instance Ids_term : Ids term. derive. Defined. Instance Rename_term : Rename term. derive. Defined. Instance Subst_term : Subst term. derive. Defined. Instance SubstLemmas_term : SubstLemmas term. derive. Qed. (*** Right Ideals of Substitutions ***) 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)). Proof. intros tau H1 mu. generalize (Xs _ H1 mu). autosubst. Qed. (*** M-set with monoid M taken to be substitutions with ids and >> -- all relative to an equivalence relation ***) 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. Proof. intros H1. apply (EquTra A x y x H1). now apply EquSym. Qed. Lemma EquRef2 (A:Mset) x y : Equ A x y -> Equ A y y. Proof. intros H1. exact (EquTra A y x y (EquSym A x y H1) H1). Qed. Lemma ActionEqu1 (A:Mset) x sigma : Equ A x x -> Equ A (Action A x sigma) (Action A x sigma). Proof. intros H1. now apply ActionEqu. Qed. (*** Do : M-set of right ideals of substitutions ***) Definition Do : Mset. apply (mkMset ((var -> term) -> Prop) (fun X Y => RiId X /\ forall sigma, X sigma <-> Y sigma) (fun X sigma tau => X (sigma >> tau))). - intros X Y [H1 H2]. split. + intros sigma H3 tau. apply H2. apply H1. now apply H2. + intros sigma. split; now apply H2. - intros X Y Z [H1 H2] [H3 H4]. split. + assumption. + intros sigma. split. * intros H5. now apply H4, H2. * intros H5. now apply H2, H4. - intros X Y sigma [H1 H2]. split. + now apply ActionRiId. + intros tau. split; now apply H2. - intros X Y [H1 H2]. split. + now apply ActionRiId. + intros sigma. asimpl. apply H2. - intros X Y sigma tau [H1 H2]. split. + now apply ActionRiId. + intros mu. asimpl. apply H2. Defined. (*** Di : M-set of untyped lambda terms acted on by substitutions ***) Definition Di : Mset. apply (mkMset term (@eq term) (fun t sigma => t.[sigma])). - congruence. - congruence. - congruence. - autosubst. - intros s t sigma tau H1. subst t. autosubst. Defined. (*** Dnat : M-set of natural numbers with trivial action ***) Definition Dnat : Mset. apply (mkMset nat (@eq nat) (fun n sigma => n)); congruence. Defined. (*** Function space of two M-sets ***) Definition Dar (A B:Mset) : Mset. apply (mkMset ((var -> term) -> Elt A -> Elt B) (fun f g => (forall sigma x y tau, Equ A x y -> Equ B (Action B (f sigma x) tau) (f (sigma >> tau) (Action A y tau))) /\ forall sigma x y, Equ A x y -> Equ B (f sigma x) (g sigma y)) (fun f sigma tau x => f (sigma >> tau) x)). - intros f g [H1 H2]. split. + intros sigma x y tau H3. generalize (H1 sigma x y tau H3). intros H4. apply (EquTra B) with (y := (f (sigma >> tau) (Action A y tau))). * { apply (EquTra B) with (y := (Action B (f sigma x) tau)). - apply EquSym. apply ActionEqu. apply H2. revert H3. apply EquRef1. - assumption. } * apply H2. apply ActionEqu. revert H3. apply EquRef2. + intros sigma x y H3. apply EquSym. apply H2. now apply EquSym. - intros f g h [H1 H2] [H3 H4]. split. + exact H1. + intros sigma x y H5. apply EquTra with (y := (g sigma y)). * now apply H2. * apply H4. revert H5. apply EquRef2. - intros f g sigma [H1 H2]. split. + intros tau x y mu H3. generalize (H1 (sigma >> tau) x y mu H3). autosubst. + intros tau x y H3. now apply H2. - intros f g [H1 H2]. split. + intros sigma x y tau H3. generalize (H1 (ids >> sigma) x y tau H3). autosubst. + intros sigma x y H3. generalize (H2 sigma x y H3). autosubst. - intros f g sigma tau [H1 H2]. split. + intros mu x y nu H3. generalize (H1 (sigma >> tau >> mu) x y nu H3). autosubst. + intros mu x y H3. generalize (H2 (sigma >> tau >> mu) x y H3). autosubst. Defined. (*** M-set interpretation ***) 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. (*** The default elt is global at each type. ***) Lemma defaultelt_GlobalElt (b:stp) : GlobalElt (tpinterp b) (defaultelt b). Proof. induction b as [ | | |a _ b IHb]. - intros sigma. simpl. split. + intros tau. tauto. + tauto. - intros sigma. asimpl. reflexivity. - intros sigma. simpl. reflexivity. - intros sigma. split. + intros tau x y mu H1. simpl. apply IHb. + intros tau x y H1. simpl. generalize (IHb ids). apply EquRef2. Qed. (*** These will be the interpretations of the untyped application and abstraction ***) 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)). (*** What will be the interpretation of the untyped lambda application is global and hence OK ***) Lemma UAp_Global : GlobalElt (tpinterp (ar i (ar i i))) UAp. Proof. intros sigma. split. - intros tau x y mu H1. simpl. split. + intros nu w z xi H2. unfold UAp. asimpl. congruence. + intros nu w z H2. unfold UAp. asimpl. congruence. - intros tau x y H1. simpl. split. + intros mu w z nu H2. unfold UAp. asimpl. congruence. + intros mu w z H2. unfold UAp. congruence. Qed. Lemma UAp_OK : Equ _ UAp UAp. Proof. generalize (UAp_Global ids). apply EquRef2. Qed. (*** What will be the interpretation of the untyped lambda abstraction is global and hence OK ***) Lemma ULam_Global : GlobalElt (tpinterp (ar (ar i i) i)) ULam. Proof. intros sigma. simpl. unfold ULam. split. - intros _ f g tau [H1 H2]. rewrite (H1 (ren S) (Va 0) (Va 0) (up tau) (eq_refl (Va 0))). asimpl. rewrite <- (H2 (tau >> ren S) (Va 0) (Va 0) (eq_refl (Va 0))). autosubst. - intros _ f g [H1 H2]. rewrite (H2 (ren S) (Va 0) (Va 0) (eq_refl (Va 0))). reflexivity. Qed. Lemma ULam_OK : Equ (tpinterp (ar (ar i i) i)) ULam ULam. Proof. generalize (ULam_Global ids). apply EquRef2. Qed. (*** Evaluation function. This can be total because of the use of dependent types (i.e., stm e a). ***) 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) => (*** Implication in the Heyting Algebra ***) 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). Proof. revert sigma tau phi psi. induction s as [e n| | |e a b s IHs t IHt|e a b s IHs|e s IHs t IHt|e a s IHs|e a s IHs t IHt]; intros sigma tau phi psi H2a H2b. - simpl. split. + apply H2a. + apply EquSym. apply H2b. - split. + exact ULam_OK. + change (Equ (tpinterp (ar (ar i i) i)) (Action _ ULam tau) ULam). now apply ULam_Global. - split. + exact UAp_OK. + change (Equ _ (Action _ UAp tau) UAp). now apply UAp_Global. - simpl. split. + destruct (IHs sigma tau phi psi H2a H2b) as [[IHs1a IHs1b] IHs2]. destruct (IHt sigma tau phi psi H2a H2b) as [IHt1 IHt2]. apply IHs1b. apply IHt1. + apply EquTra with (y := ((Action (tpinterp (ar a b)) (eval e (ar a b) s sigma phi) tau) ids (Action (tpinterp a) (eval e a t sigma phi) tau))); fold tpinterp. * simpl. asimpl. assert (L1: (forall n : nat, Equ (tpinterp (e n)) (phi n) (Action (tpinterp (e n)) (phi n) ids))). { intros n. apply EquSym. apply ActionId. apply H2a. } destruct (IHs sigma (@ids term Ids_term) phi phi H2a L1) as [[IHs1 _] _]. generalize (IHs1 ids (eval e a t sigma phi) (eval e a t sigma phi) tau). asimpl. intros H3. apply H3. destruct (IHt sigma ids phi phi H2a L1) as [_ IHt2]. revert IHt2. asimpl. apply EquRef2. * destruct (IHs sigma tau phi psi H2a H2b) as [_ IHs2]. apply IHs2. now apply (IHt sigma tau phi psi H2a H2b). - split. + split. * intros mu x y nu H3. simpl. set (phi1 := fun n : nat => match n as n0 return (Elt (tpinterp match n0 with | 0 => a | S n' => e n' end)) with | 0 => x | S n' => Action (tpinterp (e n')) (phi n') mu end). set (psi1 := fun n : nat => match n as n0 return (Elt (tpinterp match n0 with | 0 => a | S n' => e n' end)) with | 0 => Action (tpinterp a) y nu | S n' => Action (tpinterp (e n')) (phi n') (mu >> nu) end). assert (L1: forall n : nat, Equ (tpinterp match n with | 0 => a | S n' => e n' end) (phi1 n) (phi1 n)). { intros [|n]. - simpl. revert H3. apply EquRef1. - simpl. apply ActionEqu. apply H2a. } assert (L2: forall n : nat, Equ (tpinterp match n with | 0 => a | S n' => e n' end) (psi1 n) (Action (tpinterp match n with | 0 => a | S n' => e n' end) (phi1 n) nu)). { intros [|n]. - simpl. apply ActionEqu. now apply EquSym. - simpl. apply ActionComp. apply H2a. } destruct (IHs (sigma >> mu) nu phi1 psi1 L1 L2) as [_ IHs2]. revert IHs2. autosubst. * intros mu x y H3. simpl. set (phi1 := fun n : nat => match n as n0 return (Elt (tpinterp match n0 with | 0 => a | S n' => e n' end)) with | 0 => x | S n' => Action (tpinterp (e n')) (phi n') mu end). set (psi1 := fun n : nat => match n as n0 return (Elt (tpinterp match n0 with | 0 => a | S n' => e n' end)) with | 0 => y | S n' => Action (tpinterp (e n')) (phi n') mu end). assert (L1: forall n : nat, Equ (tpinterp match n with | 0 => a | S n' => e n' end) (phi1 n) (phi1 n)). { intros [|n]. - simpl. revert H3. apply EquRef1. - simpl. apply ActionEqu. apply H2a. } assert (L2: forall n : nat, Equ (tpinterp match n with | 0 => a | S n' => e n' end) (psi1 n) (Action (tpinterp match n with | 0 => a | S n' => e n' end) (phi1 n) ids)). { intros [|n]. - simpl. apply EquSym. apply ActionId. assumption. - simpl. apply EquSym. apply ActionId. apply ActionEqu. apply H2a. } destruct (IHs (sigma >> mu) ids phi1 psi1 L1 L2) as [IHs1 IHs2]. revert IHs2. asimpl. intros IHs2. apply EquTra with (y := (Action (tpinterp b) (eval (a.:e) b s (sigma >> mu) phi1) ids)); try assumption. apply EquSym. apply ActionId. exact IHs1. + split. * intros mu x y nu H3. simpl. set (phi1 := fun n : nat => match n as n0 return (Elt (tpinterp match n0 with | 0 => a | S n' => e n' end)) with | 0 => x | S n' => Action (tpinterp (e n')) (phi n') (tau >> mu) end). set (psi1 := fun n : nat => match n as n0 return (Elt (tpinterp match n0 with | 0 => a | S n' => e n' end)) with | 0 => Action (tpinterp a) y nu | S n' => Action (tpinterp (e n')) (phi n') (tau >> (mu >> nu)) end). assert (L1: forall n : nat, Equ (tpinterp match n with | 0 => a | S n' => e n' end) (phi1 n) (phi1 n)). { intros [|n]. - simpl. revert H3. apply EquRef1. - simpl. apply ActionEqu. apply H2a. } assert (L2: forall n : nat, Equ (tpinterp match n with | 0 => a | S n' => e n' end) (psi1 n) (Action (tpinterp match n with | 0 => a | S n' => e n' end) (phi1 n) nu)). { intros [|n]. - simpl. apply ActionEqu. apply EquSym. assumption. - simpl. apply EquTra with (y := (Action (tpinterp (e n)) (phi n) (tau >> mu >> nu))). + asimpl. apply ActionEqu. apply H2a. + apply ActionComp. apply H2a. } destruct (IHs (sigma >> tau >> mu) nu phi1 psi1 L1 L2) as [_ IHs2]. revert IHs2. asimpl. intros IHs2. exact IHs2. * intros mu x y H3. simpl. set (phi1 := fun n : nat => match n as n0 return (Elt (tpinterp match n0 with | 0 => a | S n' => e n' end)) with | 0 => x | S n' => Action (tpinterp (e n')) (phi n') (tau >> mu) end). set (psi1 := fun n : nat => match n as n0 return (Elt (tpinterp match n0 with | 0 => a | S n' => e n' end)) with | 0 => y | S n' => Action (tpinterp (e n')) (psi n') mu end). assert (L1: forall n : nat, Equ (tpinterp match n with | 0 => a | S n' => e n' end) (phi1 n) (phi1 n)). { intros [|n]. - simpl. revert H3. apply EquRef1. - simpl. apply ActionEqu. apply H2a. } assert (L2: forall n : nat, Equ (tpinterp match n with | 0 => a | S n' => e n' end) (psi1 n) (Action (tpinterp match n with | 0 => a | S n' => e n' end) (phi1 n) ids)). { intros [|n]. - simpl. apply EquSym. apply EquTra with (y := x). + apply ActionId. revert H3. apply EquRef1. + assumption. - simpl. apply EquTra with (y := (Action (tpinterp (e n)) (phi n) (tau >> mu))). + apply EquTra with (y := (Action (tpinterp (e n)) (Action (tpinterp (e n)) (phi n) tau) mu)). * apply ActionEqu. apply H2b. * apply EquSym. apply ActionComp. apply H2a. + apply EquSym. apply ActionId. apply ActionEqu. apply H2a. } destruct (IHs (sigma >> tau >> mu) ids phi1 psi1 L1 L2) as [IHs1 IHs2]. revert IHs1 IHs2. asimpl. intros IHs1 IHs2. apply EquTra with (y := (Action (tpinterp b) (eval (fun n : nat => match n with | 0 => a | S n' => e n' end) b s (sigma >> (tau >> mu)) phi1) ids)); try assumption. apply EquSym. apply ActionId. exact IHs1. - split. + split. * intros mu [Z [H3 [H4 H5]]] nu. exists Z. repeat split; try assumption. now apply H3. * tauto. + split. * intros mu [Z [H3 [H4 H5]]] nu. exists Z. repeat split; try assumption. generalize (H3 (tau >> mu) H4 nu). autosubst. * { intros mu. split. - intros [Z [H3 [H4 H5]]]. exists (fun mu => Z (tau >> mu)). repeat split. + now apply ActionRiId. + assumption. + intros nu H6 H7. specialize (H5 _ H6). assert (L1: forall n : nat, Equ (tpinterp (e n)) (Action (tpinterp (e n)) (psi n) nu) (Action (tpinterp (e n)) (phi n) (tau >> nu))). { intros n. apply EquTra with (y := (Action _ (Action _ (phi n) tau) nu)). - apply ActionEqu. apply H2b. - apply EquSym. apply ActionComp. apply H2a. } destruct (IHs sigma (tau >> nu) phi (fun n => Action _ (psi n) nu) H2a L1) as [[IHs1a IHtsb] [IHs2a IHs2b]]. destruct (IHt sigma (tau >> nu) phi (fun n => Action _ (psi n) nu) H2a L1) as [[IHt1a IHt1b] [IHt2a IHt2b]]. assert (L2: forall n : nat, Equ (tpinterp (e n)) (Action (tpinterp (e n)) (phi n) (tau >> nu)) (Action (tpinterp (e n)) (phi n) (tau >> nu))). { intros n. apply ActionEqu. apply H2a. } destruct (IHs sigma (tau >> nu) phi (fun n => Action _ (phi n) (tau >> nu)) H2a L2) as [[IHs1a' IHs1b'] [IHs2a' IHs2b']]. destruct (IHt sigma (tau >> nu) phi (fun n => Action _ (phi n) (tau >> nu)) H2a L2) as [[IHt1a' IHt1b'] [IHt2a' IHt2b']]. generalize (IHt2b ids). asimpl. intros H8. apply H8. generalize (IHt2b' ids). asimpl. intros [H9 H10]. generalize (IHs2b' ids). asimpl. intros [H11 H12]. apply H10. apply H5. apply H11. generalize (IHs2b ids). asimpl. intros [_ H13]. revert H7. asimpl. intros H14. exact (H13 H14). - intros [Z [H3 [H4 H5]]]. exists (fun mu => exists nu, mu = (tau >> nu) /\ Z nu). repeat split. + intros nu [xi [H6 H7]] eta. exists (xi >> eta). split. * subst nu. autosubst. * now apply H3. + exists mu. tauto. + intros nu [xi [H6 H7]] H8. subst nu. generalize (H5 _ H7). asimpl. intros H9. destruct (IHs sigma (tau >> xi) phi (fun n => Action _ (phi n) (tau >> xi)) H2a (fun n => ActionEqu _ _ _ _ (H2a n))) as [_ [_ IHs1]]. destruct (IHt sigma (tau >> xi) phi (fun n => Action _ (phi n) (tau >> xi)) H2a (fun n => ActionEqu _ _ _ _ (H2a n))) as [_ [_ IHt1]]. generalize (IHt1 ids). asimpl. intros H10. apply H10. assert (L1: forall n : nat, Equ (tpinterp (e n)) (Action (tpinterp (e n)) (psi n) xi) (Action (tpinterp (e n)) (phi n) (tau >> xi))). { intros n. apply EquTra with (y := (Action _ (Action _ (phi n) tau) xi)). - apply ActionEqu. apply H2b. - apply EquSym. apply ActionComp. apply H2a. } destruct (IHs sigma (tau >> xi) phi (fun n => Action _ (psi n) xi) H2a L1) as [_ [_ IHs2]]. destruct (IHt sigma (tau >> xi) phi (fun n => Action _ (psi n) xi) H2a L1) as [_ [_ IHt2]]. generalize (IHt2 ids). asimpl. intros H11. apply H11. generalize (H5 _ H7). asimpl. intros H12. apply H12. generalize (IHs2 ids). asimpl. intros H13. apply H13. generalize (IHs1 ids). asimpl. intros H14. apply H14. exact H8. } - split. + split. * simpl. intros mu H3 nu xi x H4. generalize (H3 (nu >> xi) x H4). asimpl. intros H5. exact H5. * tauto. + simpl. split. * intros mu H3 nu xi x H4. generalize (H3 (nu >> xi) x H4). asimpl. intros H5. exact H5. * { intros mu. split. - intros H3 nu x H4. generalize (H3 nu x H4). set (phi1 := fun n : nat => match n as n0 return (Elt (tpinterp ((a .: e) n0))) with | 0 => x | S n' => Action (tpinterp (e n')) (phi n') (tau >> mu >> nu) end). set (phi2 := fun n : nat => match n as n0 return (Elt (tpinterp ((a .: e) n0))) with | 0 => x | S n' => Action (tpinterp (e n')) (psi n') (mu >> nu) end). assert (L1: forall n : nat, Equ (tpinterp ((a .: e) n)) (phi1 n) (phi1 n)). { intros [|n]. - simpl. assumption. - simpl. apply ActionEqu. apply H2a. } assert (L2: forall n : nat, Equ (tpinterp ((a .: e) n)) (phi2 n) (Action (tpinterp ((a .: e) n)) (phi1 n) ids)). { intros [|n]. - simpl. apply EquSym. now apply ActionId. - simpl. apply EquTra with (y := (Action (tpinterp (e n)) (Action (tpinterp (e n)) (phi n) tau) (mu >> nu))). + apply ActionEqu. apply H2b. + apply EquSym. apply EquTra with (y := Action (tpinterp (e n)) (phi n) (tau >> mu >> nu)). * apply ActionId. apply ActionEqu. apply H2a. * asimpl. apply ActionComp. apply H2a. } destruct (IHs (sigma >> tau >> mu >> nu) ids phi1 phi2 L1 L2) as [IHs1 [IHs2a IHs2b]]. revert IHs2b. asimpl. intros H5 H6. apply H5. exact H6. - intros H3 nu x H4. generalize (H3 nu x H4). set (phi1 := fun n : nat => match n as n0 return (Elt (tpinterp ((a .: e) n0))) with | 0 => x | S n' => Action (tpinterp (e n')) (phi n') (tau >> mu >> nu) end). set (phi2 := fun n : nat => match n as n0 return (Elt (tpinterp ((a .: e) n0))) with | 0 => x | S n' => Action (tpinterp (e n')) (psi n') (mu >> nu) end). assert (L1: forall n : nat, Equ (tpinterp ((a .: e) n)) (phi1 n) (phi1 n)). { intros [|n]. - simpl. assumption. - simpl. apply ActionEqu. apply H2a. } assert (L2: forall n : nat, Equ (tpinterp ((a .: e) n)) (phi2 n) (Action (tpinterp ((a .: e) n)) (phi1 n) ids)). { intros [|n]. - simpl. apply EquSym. now apply ActionId. - simpl. apply EquTra with (y := (Action (tpinterp (e n)) (Action (tpinterp (e n)) (phi n) tau) (mu >> nu))). + apply ActionEqu. apply H2b. + apply EquSym. apply EquTra with (y := Action (tpinterp (e n)) (phi n) (tau >> mu >> nu)). * apply ActionId. apply ActionEqu. apply H2a. * asimpl. apply ActionComp. apply H2a. } destruct (IHs (sigma >> tau >> mu >> nu) ids phi1 phi2 L1 L2) as [IHs1 [IHs2a IHs2b]]. revert IHs2b. asimpl. intros H5 H6. apply H5. exact H6. } - split. + simpl. split. * { intros mu H3 nu. assert (L1: forall n : nat, Equ (tpinterp (e n)) (Action (tpinterp (e n)) (phi n) mu) (Action (tpinterp (e n)) (phi n) mu)). { intros n. apply ActionEqu. apply H2a. } assert (L2: forall n : nat, Equ (tpinterp (e n)) (Action (tpinterp (e n)) (phi n) (mu >> nu)) (Action (tpinterp (e n)) (Action (tpinterp (e n)) (phi n) mu) nu)). { intros n. apply ActionComp. apply H2a. } generalize (IHs (sigma >> mu) nu (fun n => Action _ (phi n) mu) (fun n => Action _ (phi n) (mu >> nu)) L1 L2). asimpl. intros [_ IHs2]. generalize (IHt (sigma >> mu) nu (fun n => Action _ (phi n) mu) (fun n => Action _ (phi n) (mu >> nu)) L1 L2). asimpl. intros [_ IHt2]. apply EquTra with (y := (Action (tpinterp a) (eval e a s (sigma >> mu) (fun n : nat => Action (tpinterp (e n)) (phi n) mu)) nu)). - apply EquSym. exact IHs2. - apply EquTra with (y := (Action (tpinterp a) (eval e a t (sigma >> mu) (fun n : nat => Action (tpinterp (e n)) (phi n) mu)) nu)). + apply ActionEqu. exact H3. + exact IHt2. } * intros mu. tauto. + simpl. split. * { intros mu H3 nu. assert (L1: forall n : nat, Equ (tpinterp (e n)) (Action (tpinterp (e n)) (phi n) (tau >> mu)) (Action (tpinterp (e n)) (phi n) (tau >> mu))). { intros n. apply ActionEqu. apply H2a. } assert (L2: forall n : nat, Equ (tpinterp (e n)) (Action (tpinterp (e n)) (phi n) (tau >> mu >> nu)) (Action (tpinterp (e n)) (Action (tpinterp (e n)) (phi n) (tau >> mu)) nu)). { intros n. apply ActionComp. apply H2a. } generalize (IHs (sigma >> (tau >> mu)) nu (fun n => Action _ (phi n) (tau >> mu)) (fun n => Action _ (phi n) (tau >> mu >> nu)) L1 L2). asimpl. intros [_ IHs2]. generalize (IHt (sigma >> (tau >> mu)) nu (fun n => Action _ (phi n) (tau >> mu)) (fun n => Action _ (phi n) (tau >> mu >> nu)) L1 L2). asimpl. intros [_ IHt2]. apply EquTra with (y := (Action (tpinterp a) (eval e a s (sigma >> (tau >> mu)) (fun n : nat => Action (tpinterp (e n)) (phi n) (tau >> mu))) nu)). - apply EquSym. exact IHs2. - apply EquTra with (y := (Action (tpinterp a) (eval e a t (sigma >> (tau >> mu)) (fun n : nat => Action (tpinterp (e n)) (phi n) (tau >> mu))) nu)). + apply ActionEqu. exact H3. + exact IHt2. } * { intros mu. asimpl. split. - intros H3. assert (L1: forall n : nat, Equ (tpinterp (e n)) (Action (tpinterp (e n)) (phi n) tau) (Action (tpinterp (e n)) (phi n) tau)). { intros n. apply ActionEqu. apply H2a. } assert (L2: forall n : nat, Equ (tpinterp (e n)) (Action (tpinterp (e n)) (psi n) mu) (Action (tpinterp (e n)) (Action (tpinterp (e n)) (phi n) tau) mu)). { intros n. apply ActionEqu. apply H2b. } generalize (IHs (sigma >> tau) mu (fun n => Action _ (phi n) tau) (fun n => Action _ (psi n) mu) L1 L2). asimpl. intros [_ IHs2]. generalize (IHt (sigma >> tau) mu (fun n => Action _ (phi n) tau) (fun n => Action _ (psi n) mu) L1 L2). asimpl. intros [_ IHt2]. apply EquTra with (y := (Action (tpinterp a) (eval e a s (sigma >> tau) (fun n : nat => Action (tpinterp (e n)) (phi n) tau)) mu)). + apply EquSym. exact IHs2. + apply EquTra with (y := (Action (tpinterp a) (eval e a t (sigma >> tau) (fun n : nat => Action (tpinterp (e n)) (phi n) tau)) mu)). * { assert (L3: forall n : nat, Equ (tpinterp (e n)) (Action (tpinterp (e n)) (phi n) (tau >> mu)) (Action (tpinterp (e n)) (Action (tpinterp (e n)) (phi n) tau) mu)). { intros n. apply ActionComp. apply H2a. } generalize (IHs (sigma >> tau) mu (fun n => Action _ (phi n) tau) (fun n => Action _ (phi n) (tau >> mu)) L1 L3). asimpl. intros [_ IHs3]. generalize (IHt (sigma >> tau) mu (fun n => Action _ (phi n) tau) (fun n => Action _ (phi n) (tau >> mu)) L1 L3). asimpl. intros [_ IHt3]. apply EquTra with (y := eval e a s (sigma >> (tau >> mu)) (fun n : nat => Action (tpinterp (e n)) (phi n) (tau >> mu))). - exact IHs3. - apply EquTra with (y := eval e a t (sigma >> (tau >> mu)) (fun n : nat => Action (tpinterp (e n)) (phi n) (tau >> mu))). + exact H3. + apply EquSym. exact IHt3. } * exact IHt2. - intros H3. assert (L1: forall n : nat, Equ (tpinterp (e n)) (Action (tpinterp (e n)) (phi n) tau) (Action (tpinterp (e n)) (phi n) tau)). { intros n. apply ActionEqu. apply H2a. } assert (L2: forall n : nat, Equ (tpinterp (e n)) (Action (tpinterp (e n)) (psi n) mu) (Action (tpinterp (e n)) (Action (tpinterp (e n)) (phi n) tau) mu)). { intros n. apply ActionEqu. apply H2b. } generalize (IHs (sigma >> tau) mu (fun n => Action _ (phi n) tau) (fun n => Action _ (psi n) mu) L1 L2). asimpl. intros [_ IHs2]. generalize (IHt (sigma >> tau) mu (fun n => Action _ (phi n) tau) (fun n => Action _ (psi n) mu) L1 L2). asimpl. intros [_ IHt2]. assert (L3: forall n : nat, Equ (tpinterp (e n)) (Action (tpinterp (e n)) (phi n) (tau >> mu)) (Action (tpinterp (e n)) (Action (tpinterp (e n)) (phi n) tau) mu)). { intros n. apply ActionComp. apply H2a. } generalize (IHs (sigma >> tau) mu (fun n => Action _ (phi n) tau) (fun n => Action _ (phi n) (tau >> mu)) L1 L3). asimpl. intros [_ IHs3]. generalize (IHt (sigma >> tau) mu (fun n => Action _ (phi n) tau) (fun n => Action _ (phi n) (tau >> mu)) L1 L3). asimpl. intros [_ IHt3]. apply EquTra with (y := (Action (tpinterp a) (eval e a s (sigma >> tau) (fun n : nat => Action (tpinterp (e n)) (phi n) tau)) mu)). + apply EquSym. exact IHs3. + apply EquTra with (y := (Action (tpinterp a) (eval e a t (sigma >> tau) (fun n : nat => Action (tpinterp (e n)) (phi n) tau)) mu)). * { apply EquTra with (y := eval e a s (sigma >> (tau >> mu)) (fun n : nat => Action (tpinterp (e n)) (psi n) mu)). - exact IHs2. - apply EquTra with (y := eval e a t (sigma >> (tau >> mu)) (fun n : nat => Action (tpinterp (e n)) (psi n) mu)). + exact H3. + apply EquSym. exact IHt2. } * exact IHt3. } Qed. 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). Proof. intros H2. assert (L1:forall n : nat, Equ (tpinterp (e n)) (phi n) (phi n)). { intros n. generalize (H2 n). apply EquRef1. } assert (L2:forall n : nat, Equ (tpinterp (e n)) (psi n) (Action (tpinterp (e n)) (phi n) ids)). { intros n. apply EquSym. apply ActionId. apply H2. } destruct (eval_thm1 e a s sigma ids phi psi L1 L2) as [H3 H4]. asimpl in H4. apply EquTra with (y := (Action (tpinterp a) (eval e a s sigma phi) ids)). - apply EquSym. apply ActionId. exact H3. - exact H4. Qed. 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). Proof. intros H2. apply eval_thm2; assumption. Qed. (*** We can use eval_thm1 to reduce questions about when tau is in eval e a s sigma phi to when ids is in eval e a s (sigma >> tau) "phi tau". ***) 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. Proof. destruct (eval_thm1 e o s sigma tau phi (fun n => Action _ (phi n) tau) Hphi (fun n => ActionEqu _ _ _ _ (Hphi n))) as [_ [_ H1]]. generalize (H1 ids). simpl. asimpl. tauto. Qed. (*** The following lemmas are sometimes a more convenient way of reasoning about eval of implications and equations than the definition. ***) 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)). Proof. intros [Z [H1 [H2 H3]]] mu H4. apply (eval_thm_ids e phi Hphi). apply H3. - now apply H1. - apply (eval_thm_ids e phi Hphi). assumption. Qed. 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. Proof. intros H1. simpl. exists (fun mu => exists nu, mu = tau >> nu). repeat split. - intros mu [nu H2] xi. exists (nu >> xi). subst mu. autosubst. - exists ids. autosubst. - intros mu [nu H2]. subst mu. intros H2. apply (eval_thm_ids e phi Hphi). apply H1. apply (eval_thm_ids e phi Hphi). exact H2. Qed. 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. Proof. intros H1. simpl. destruct (eval_thm1 e a s sigma tau phi (fun n => Action _ (phi n) tau) Hphi (fun n => ActionEqu _ _ _ _ (Hphi n))) as [_ H2]. destruct (eval_thm1 e a t sigma tau phi (fun n => Action _ (phi n) tau) Hphi (fun n => ActionEqu _ _ _ _ (Hphi n))) as [_ H3]. apply EquTra with (y := Action (tpinterp a) (eval e a s sigma phi) tau). - apply EquSym. exact H2. - apply EquTra with (y := Action (tpinterp a) (eval e a t sigma phi) tau). + exact H1. + exact H3. Qed. 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). Proof. simpl. intros H1. destruct (eval_thm1 e a s sigma tau phi (fun n => Action _ (phi n) tau) Hphi (fun n => ActionEqu _ _ _ _ (Hphi n))) as [_ H2]. destruct (eval_thm1 e a t sigma tau phi (fun n => Action _ (phi n) tau) Hphi (fun n => ActionEqu _ _ _ _ (Hphi n))) as [_ H3]. apply EquTra with (y := eval e a s (sigma >> tau) (fun n : nat => Action (tpinterp (e n)) (phi n) tau)). - exact H2. - apply EquTra with (y := eval e a t (sigma >> tau) (fun n : nat => Action (tpinterp (e n)) (phi n) tau)). + exact H1. + apply EquSym. exact H3. Qed. (*** The following lemmas are essentially just the definition of eval of foralls put into lemma form. These are sometimes more convenient than the definition of eval simply to avoid having too much simplification. ***) 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. Proof. intros H1. exact H1. Qed. 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). Proof. intros H1. exact H1. Qed. 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). Proof. revert a j sigma phi psi. induction s as [e x| | |e c d s IHs t IHt|e c d s IHs|e s IHs t IHt|e c s IHs|e c s IHs t IHt]; intros a j sigma phi psi H1a H1b. - generalize (H1b x). simpl. intros H2. assert (E1: Equ (tpinterp (e x)) (eval (push_stp_into_env a e j) (e x) (eq_rec (push_stp_into_env a e j (stmshift_var j x)) (fun s : stp => stm (push_stp_into_env a e j) s) (SDB (push_stp_into_env a e j) (stmshift_var j x)) (e x) (stmshift_var_eq a e j x)) sigma psi) (eq_rect (push_stp_into_env a e j (stmshift_var j x)) (fun a0 : stp => Elt (tpinterp a0)) (psi (stmshift_var j x)) (e x) (stmshift_var_eq a e j x))). { unfold eq_rec, eq_rect. rewrite (stmshift_var_eq_match_commutes a e j x (fun b => stm (push_stp_into_env a e j) b) (fun b => Elt (tpinterp b)) (SDB (push_stp_into_env a e j) (stmshift_var j x)) (fun b (u:stm (push_stp_into_env a e j) b) => eval (push_stp_into_env a e j) b u sigma psi)). simpl. revert H2. unfold eq_rect. apply EquRef1. } apply EquTra with (y := (eq_rect (push_stp_into_env a e j (stmshift_var j x)) (fun a0 : stp => Elt (tpinterp a0)) (psi (stmshift_var j x)) (e x) (stmshift_var_eq a e j x))). + exact E1. + exact H2. - change (Equ (tpinterp (ar (ar i i) i)) ULam ULam). exact ULam_OK. - change (Equ (tpinterp (ar i (ar i i))) UAp UAp). exact UAp_OK. - simpl. destruct (IHs a j sigma phi psi H1a H1b) as [IHs1 IHs2]. apply IHs2. exact (IHt a j sigma phi psi H1a H1b). - simpl. split. + intros tau x y mu H2. set (psi1 := fun n : nat => match n as n0 return (Elt (tpinterp ((c .: push_stp_into_env a e j) n0))) with | 0 => x | S n' => Action (tpinterp (push_stp_into_env a e j n')) (psi n') tau end). set (psi2 := fun n : nat => match n as n0 return (Elt (tpinterp ((c .: push_stp_into_env a e j) n0))) with | 0 => Action (tpinterp c) y mu | S n' => Action (tpinterp (push_stp_into_env a e j n')) (psi n') (tau >> mu) end). set (phi1 := fun n => match n as n' return Elt (tpinterp ((c .: e) n')) with O => x | S n' => Action _ (phi n') tau end). set (phi2 := fun n => Action _ (phi1 n) mu). assert (L1: forall z : var, Equ (tpinterp (push_stp_into_env a (c .: e) (S j) z)) (psi1 z) (psi1 z)). { intros [|z]. - simpl. revert H2. apply EquRef1. - simpl. apply ActionEqu. apply H1a. } assert (L2: forall z : nat, Equ (tpinterp ((c .: e) z)) (eq_rect (push_stp_into_env a (c .: e) (S j) (stmshift_var (S j) z)) (fun a0 : stp => Elt (tpinterp a0)) (psi1 (stmshift_var (S j) z)) ((c .: e) z) (stmshift_var_eq a (c .: e) (S j) z)) (phi1 z)). { intros [|z]. - simpl. revert H2. apply EquRef1. - simpl. unfold eq_rect, eq_ind. unfold eq_rect. rewrite stmshift_var_eq_match_eq. generalize (stmshift_var_eq_match_commutes a e j z (fun b => Elt (tpinterp b)) (fun b => Elt (tpinterp b)) (psi (stmshift_var j z)) (fun b u => Action (tpinterp b) u tau)). intros E1. apply (fun H => @eq_ind (Elt (tpinterp (e z))) _ (fun u => Equ (tpinterp (e z)) u (Action (tpinterp (e z)) (phi z) tau)) H _ E1). apply ActionEqu. apply H1b. } assert (L3: forall z : var, Equ (tpinterp (push_stp_into_env a (c .: e) (S j) z)) (psi2 z) (psi2 z)). { intros [|z]. - simpl. apply ActionEqu. revert H2. apply EquRef2. - simpl. apply ActionEqu. apply H1a. } assert (L4: forall z : nat, Equ (tpinterp ((c .: e) z)) (eq_rect (push_stp_into_env a (c .: e) (S j) (stmshift_var (S j) z)) (fun a0 : stp => Elt (tpinterp a0)) (psi2 (stmshift_var (S j) z)) ((c .: e) z) (stmshift_var_eq a (c .: e) (S j) z)) (phi2 z)). { intros [|z]. - simpl. unfold phi2. unfold phi1. apply ActionEqu. apply EquSym. exact H2. - simpl. unfold eq_rect. unfold eq_ind. unfold eq_rect. rewrite stmshift_var_eq_match_eq. generalize (stmshift_var_eq_match_commutes a e j z (fun b => Elt (tpinterp b)) (fun b => Elt (tpinterp b)) (psi (stmshift_var j z)) (fun b u => Action (tpinterp b) u (tau >> mu))). intros E1. apply (fun H => @eq_ind (Elt (tpinterp (e z))) _ (fun u => Equ (tpinterp (e z)) u (phi2 (S z))) H _ E1). unfold phi2. simpl. apply EquTra with (y := (Action _ (phi z) (tau >> mu))). + apply ActionEqu. apply H1b. + apply ActionComp. generalize (H1b z). apply EquRef2. } generalize (IHs a (S j) (sigma >> tau) phi1 psi1 L1 L2). intros IHs1. generalize (IHs a (S j) (sigma >> (tau >> mu)) phi2 psi2 L3 L4). intros IHs2. apply EquTra with (y := (Action _ (eval (c .: e) d s (sigma >> tau) phi1) mu)). * apply ActionEqu. exact IHs1. * { apply EquTra with (y := (eval (c .: e) d s (sigma >> (tau >> mu)) phi2)). - generalize (eval_thm1 (c.:e) d s (sigma >> tau) mu phi1 phi2). asimpl. intros H4. apply H4. + intros [|n]. * simpl. revert H2. apply EquRef1. * simpl. apply ActionEqu. generalize (H1b n). apply EquRef2. + intros [|n]. * simpl. unfold phi2. simpl. apply ActionEqu. revert H2. apply EquRef1. * simpl. unfold phi2. simpl. apply ActionEqu. apply ActionEqu. generalize (H1b n). apply EquRef2. - apply EquSym. exact IHs2. } + intros tau x y H2. set (psi1 := fun n : nat => match n as n0 return (Elt (tpinterp ((c .: push_stp_into_env a e j) n0))) with | 0 => x | S n' => Action (tpinterp (push_stp_into_env a e j n')) (psi n') tau end). set (phi1 := fun n : nat => match n as n0 return (Elt (tpinterp ((c .: e) n0))) with | 0 => y | S n' => Action _ (phi n') tau end). assert (L1: forall y : var, Equ (tpinterp (push_stp_into_env a (c .: e) (S j) y)) (psi1 y) (psi1 y)). { intros [|z]. - simpl. revert H2. apply EquRef1. - simpl. apply ActionEqu. apply H1a. } assert (L2: forall y : nat, Equ (tpinterp ((c .: e) y)) (eq_rect (push_stp_into_env a (c .: e) (S j) (stmshift_var (S j) y)) (fun a0 : stp => Elt (tpinterp a0)) (psi1 (stmshift_var (S j) y)) ((c .: e) y) (stmshift_var_eq a (c .: e) (S j) y)) (phi1 y)). { intros [|z]. - simpl. assumption. - simpl. unfold eq_rect. unfold eq_ind. unfold eq_rect. rewrite stmshift_var_eq_match_eq. generalize (stmshift_var_eq_match_commutes a (fun z => e z) j z (fun b => Elt (tpinterp b)) (fun b => Elt (tpinterp b)) (psi (stmshift_var j z)) (fun b u => Action (tpinterp b) u tau)). intros E1. apply (fun H => @eq_ind (Elt (tpinterp (e z))) _ (fun u => Equ (tpinterp (e z)) u (Action (tpinterp (e z)) (phi z) tau)) H _ E1). apply ActionEqu. apply H1b. } exact (IHs a (S j) (sigma >> tau) phi1 psi1 L1 L2). - destruct (IHs a j sigma phi psi H1a H1b) as [IHs1 IHs2]. destruct (IHt a j sigma phi psi H1a H1b) as [IHt1 IHt2]. split. + intros tau [Z [H3 [H4 H5]]] mu. exists Z. repeat split. * assumption. * apply H3. assumption. * { intros nu H6 H7. apply H5. - exact H6. - exact H7. } + intros tau. assert (Hphi: forall n, Equ _ (phi n) (phi n)). { intros n. generalize (H1b n). apply EquRef2. } split. * { intros [Z [H2 [H3 H4]]]. exists Z. repeat split. - assumption. - assumption. - intros mu H5 H6. apply (eval_thm_ids e phi Hphi). apply IHt2. apply eval_thm_ids. + exact H1a. + apply H4. * assumption. * { apply eval_thm_ids. - exact H1a. - apply IHs2. apply (eval_thm_ids e phi Hphi). assumption. } } * { intros [Z [H2 [H3 H4]]]. exists Z. repeat split. - assumption. - assumption. - intros mu H5 H6. apply eval_thm_ids. + exact H1a. + apply IHt2. apply (eval_thm_ids e phi Hphi). apply H4. * assumption. * { apply (eval_thm_ids e phi Hphi). apply IHs2. apply eval_thm_ids. - exact H1a. - assumption. } } - split. + intros tau H2 mu. simpl. intros nu x H3. simpl in H2. generalize (H2 (mu >> nu) x H3). asimpl. intros H4. exact H4. + intros tau. split. * simpl. intros H2 mu x H3. generalize (H2 mu x H3). set (psi1 := fun n : nat => match n as n' return (Elt (tpinterp ((c .: push_stp_into_env a e j) n'))) with | 0 => x | S n' => Action (tpinterp (push_stp_into_env a e j n')) (psi n') (tau >> mu) end). set (phi1 := fun n => match n as n' return Elt (tpinterp ((c .: e) n')) with O => x | S n' => Action _ (phi n') (tau >> mu) end). asimpl. intros H4. assert (L1: forall y : var, Equ (tpinterp (push_stp_into_env a (c .: e) (S j) y)) (psi1 y) (psi1 y)). { intros [|y]. - simpl. assumption. - simpl. apply ActionEqu. apply H1a. } assert (L2: forall y : nat, Equ (tpinterp ((c .: e) y)) (eq_rect (push_stp_into_env a (c .: e) (S j) (stmshift_var (S j) y)) (fun a0 : stp => Elt (tpinterp a0)) (psi1 (stmshift_var (S j) y)) ((c .: e) y) (stmshift_var_eq a (c .: e) (S j) y)) (phi1 y)). { intros [|y]. - simpl. assumption. - simpl. unfold eq_rect, eq_ind. unfold eq_rect. rewrite stmshift_var_eq_match_eq. rewrite <- (stmshift_var_eq_match_commutes a e j y (fun b => Elt (tpinterp b)) (fun b => Elt (tpinterp b)) (psi (stmshift_var j y)) (fun b u => Action (tpinterp b) u (tau >> mu))). apply ActionEqu. apply H1b. } destruct (IHs a (S j) (sigma >> (tau >> mu)) phi1 psi1 L1 L2) as [IHs1 IHs2]. generalize (IHs2 ids). simpl. intros IHs2a. apply IHs2a. exact H4. * simpl. intros H2 mu x H3. generalize (H2 mu x H3). set (psi1 := fun n : nat => match n as n' return (Elt (tpinterp ((c .: push_stp_into_env a e j) n'))) with | 0 => x | S n' => Action (tpinterp (push_stp_into_env a e j n')) (psi n') (tau >> mu) end). set (phi1 := fun n => match n as n' return Elt (tpinterp ((c .: e) n')) with O => x | S n' => Action _ (phi n') (tau >> mu) end). asimpl. intros H4. assert (L1: forall y : var, Equ (tpinterp (push_stp_into_env a (c .: e) (S j) y)) (psi1 y) (psi1 y)). { intros [|y]. - simpl. assumption. - simpl. apply ActionEqu. apply H1a. } assert (L2: forall y : nat, Equ (tpinterp ((c .: e) y)) (eq_rect (push_stp_into_env a (c .: e) (S j) (stmshift_var (S j) y)) (fun a0 : stp => Elt (tpinterp a0)) (psi1 (stmshift_var (S j) y)) ((c .: e) y) (stmshift_var_eq a (c .: e) (S j) y)) (phi1 y)). { intros [|y]. - simpl. assumption. - simpl. unfold eq_rect, eq_ind. unfold eq_rect. rewrite stmshift_var_eq_match_eq. rewrite <- (stmshift_var_eq_match_commutes a e j y (fun b => Elt (tpinterp b)) (fun b => Elt (tpinterp b)) (psi (stmshift_var j y)) (fun b u => Action (tpinterp b) u (tau >> mu))). apply ActionEqu. apply H1b. } destruct (IHs a (S j) (sigma >> (tau >> mu)) phi1 psi1 L1 L2) as [IHs1 IHs2]. generalize (IHs2 ids). simpl. intros IHs2a. apply IHs2a. exact H4. - generalize (IHs a j sigma phi psi H1a H1b). intros IHs1. generalize (IHt a j sigma phi psi H1a H1b). intros IHt1. split. + destruct (eval_thm3 (push_stp_into_env a e j) o (stmshift_aux e o (SEq e c s t) a j) sigma psi H1a) as [H2 _]. exact H2. + intros tau. split. * { intros H3. apply eval_SEq_I. - intros n. generalize (H1b n). apply EquRef2. - apply EquTra with (y := Action _ (eval (push_stp_into_env a e j) c (stmshift_aux e c s a j) sigma psi) tau). + apply ActionEqu. apply EquSym. exact IHs1. + apply EquTra with (y := Action _ (eval (push_stp_into_env a e j) c (stmshift_aux e c t a j) sigma psi) tau). * revert H3. apply eval_SEq_E. exact H1a. * apply ActionEqu. exact IHt1. } * { intros H3. change (eval (push_stp_into_env a e j) o (SEq (push_stp_into_env a e j) c (stmshift_aux e c s a j) (stmshift_aux e c t a j)) sigma psi tau). apply eval_SEq_I. - exact H1a. - apply EquTra with (y := Action _ (eval e c s sigma phi) tau). + apply ActionEqu. exact IHs1. + apply EquTra with (y := Action _ (eval e c t sigma phi) tau). * revert H3. apply eval_SEq_E. intros n. generalize (H1b n). apply EquRef2. * apply ActionEqu. apply EquSym. exact IHt1. } Qed. 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). Proof. intros H1a H1b. unfold stmshift. apply (eval_stmshift_aux e b s a 0 sigma phi psi H1a). simpl. intros x. apply EquSym. apply H1b. Qed. 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). Proof. revert e' theta sigma phi psi. induction s as [e x| | |e c d s IHs t IHt|e c d s IHs|e s IHs t IHt|e c s IHs|e c s IHs t IHt]; intros e' theta sigma phi psi H1a H1b. - simpl. apply EquSym. apply H1b. - change (Equ _ ULam ULam). apply ULam_OK. - change (Equ _ UAp UAp). apply UAp_OK. - simpl. destruct (IHs e' theta sigma phi psi H1a H1b) as [IHs1 IHs2]. exact (IHs2 ids _ _ (IHt e' theta sigma phi psi H1a H1b)). - simpl. assert (L1: forall (tau : var -> term) (x y : Elt (tpinterp c)) (mu : var -> term), Equ (tpinterp c) x y -> Equ (tpinterp d) (Action (tpinterp d) (eval (c .: e') d (stmparsubst (c .: e) d (c .: e') (pushsubstunder e e' c theta) s) (sigma >> tau) (fun n : nat => match n as n0 return (Elt (tpinterp ((c .: e') n0))) with | 0 => x | S n' => Action (tpinterp (e' n')) (phi n') tau end)) mu) (eval (c .: e') d (stmparsubst (c .: e) d (c .: e') (pushsubstunder e e' c theta) s) (sigma >> (tau >> mu)) (fun n : nat => match n as n0 return (Elt (tpinterp ((c .: e') n0))) with | 0 => Action (tpinterp c) y mu | S n' => Action (tpinterp (e' n')) (phi n') (tau >> mu) end))). { intros tau x y mu H2. set (phi1 := (fun n : nat => match n as n0 return (Elt (tpinterp ((c .: e') n0))) with | 0 => x | S n' => Action (tpinterp (e' n')) (phi n') tau end)). set (phi2 := (fun n : nat => match n as n0 return (Elt (tpinterp ((c .: e') n0))) with | 0 => Action (tpinterp c) y mu | S n' => Action (tpinterp (e' n')) (phi n') (tau >> mu) end)). set (psi1 := (fun n : nat => match n as n0 return (Elt (tpinterp ((c.:e) n0))) with | 0 => x | S n' => Action (tpinterp (e n')) (psi n') tau end)). set (psi2 := (fun n : nat => match n as n0 return (Elt (tpinterp ((c.:e) n0))) with | 0 => Action _ y mu | S n' => Action (tpinterp (e n')) (psi n') (tau >> mu) end)). assert (L1a: Equ (tpinterp d) (eval (c .: e') d (stmparsubst (c .: e) d (c .: e') (pushsubstunder e e' c theta) s) (sigma >> tau) phi1) (eval (c .: e) d s (sigma >> tau) psi1)). { apply (IHs (c.:e') (pushsubstunder e e' c theta) (sigma >> tau) phi1 psi1). - intros [|z]. + simpl. revert H2. apply EquRef1. + simpl. apply ActionEqu. apply H1a. - intros [|z]. + simpl. revert H2. apply EquRef1. + simpl. apply EquTra with (y := (eval e' (e z) (theta z) (sigma >> tau) (fun w : var => Action (tpinterp (e' w)) (phi w) tau))). * { apply EquTra with (y := Action _ (eval e' (e z) (theta z) sigma phi) tau). - apply ActionEqu. apply H1b. - apply (eval_thm1 e' (e z) (theta z)). + assumption. + intros w. apply ActionEqu. apply H1a. } * { apply EquSym. apply (eval_stmshift c e' (e z) (theta z) (sigma >> tau) (fun w => Action _ (phi w) tau) phi1). - intros [|w]; simpl. + revert H2. apply EquRef1. + apply ActionEqu. apply H1a. - intros w. apply ActionEqu. apply H1a. } } assert (L1b:Equ (tpinterp d) (eval (c .: e') d (stmparsubst (c .: e) d (c .: e') (pushsubstunder e e' c theta) s) (sigma >> (tau >> mu)) phi2) (eval (c .: e) d s (sigma >> (tau >> mu)) psi2)). { apply (IHs (c.:e') (pushsubstunder e e' c theta) (sigma >> (tau >> mu)) phi2 psi2). - intros [|z]; simpl. + apply ActionEqu. revert H2. apply EquRef2. + apply ActionEqu. apply H1a. - intros [|z]; simpl. + apply ActionEqu. revert H2. apply EquRef2. + apply EquTra with (y := (eval e' (e z) (theta z) (sigma >> (tau >> mu)) (fun w : var => Action (tpinterp (e' w)) (phi w) (tau >> mu)))). * { apply EquTra with (y := Action _ (eval e' (e z) (theta z) sigma phi) (tau >> mu)). - apply ActionEqu. apply H1b. - apply (eval_thm1 e' (e z) (theta z)). + assumption. + intros w. apply ActionEqu. apply H1a. } * { apply EquSym. apply (eval_stmshift c e' (e z) (theta z) (sigma >> (tau >> mu)) (fun w => Action _ (phi w) (tau >> mu)) phi2). - intros [|w]; simpl. + apply ActionEqu. revert H2. apply EquRef2. + apply ActionEqu. apply H1a. - intros w. simpl. apply ActionEqu. apply H1a. } } apply EquTra with (y := Action _ (eval (c .: e) d s (sigma >> tau) psi1) mu). - apply ActionEqu. exact L1a. - apply EquTra with (y := (eval (c .: e) d s (sigma >> (tau >> mu)) psi2)). + generalize (eval_thm1 (c.:e) d s (sigma >> tau) mu psi1 psi2). asimpl. intros H3. apply H3. * { intros [|z]; simpl. - revert H2. apply EquRef1. - apply ActionEqu. generalize (H1b z). apply EquRef1. } * { intros [|z]; simpl. - apply ActionEqu. now apply EquSym. - apply ActionComp. generalize (H1b z). apply EquRef1. } + apply EquSym. exact L1b. } split. + exact L1. + intros tau x y H2. set (phi1 := (fun n : nat => match n as n0 return (Elt (tpinterp ((c .: e') n0))) with | 0 => x | S n' => Action (tpinterp (e' n')) (phi n') tau end)). set (psi1 := (fun n : nat => match n as n0 return (Elt (tpinterp ((c.:e) n0))) with | 0 => y | S n' => Action (tpinterp (e n')) (psi n') tau end)). generalize (L1 tau x y ids H2). asimpl. fold phi1. set (phi2 := (fun n : nat => match n as n0 return (Elt (tpinterp ((c .: e') n0))) with | 0 => Action _ y ids | S n' => Action (tpinterp (e' n')) (phi n') tau end)). assert (L2: Equ _ (eval (c .:e') d (stmparsubst (c .: e) d (c .: e') (pushsubstunder e e' c theta) s) (sigma >> tau) phi1) (eval (c .:e') d (stmparsubst (c .: e) d (c .: e') (pushsubstunder e e' c theta) s) (sigma >> tau) phi2)). { apply eval_thm2. intros [|z]; simpl. - apply EquTra with (y := y). + assumption. + apply EquSym. apply ActionId. revert H2. apply EquRef2. - apply ActionEqu. apply H1a. } intros H3. apply EquTra with (y := Action (tpinterp d) (eval (c .: e') d (stmparsubst (c .: e) d (c .: e') (pushsubstunder e e' c theta) s) (sigma >> tau) phi1) ids). * apply EquSym. apply ActionId. revert L2. apply EquRef1. * { apply EquTra with (y := eval (c .: e') d (stmparsubst (c .: e) d (c .: e') (pushsubstunder e e' c theta) s) (sigma >> tau) phi1). - apply ActionId. revert L2. apply EquRef1. - assert (L2a: Equ (tpinterp d) (eval (c .: e') d (stmparsubst (c .: e) d (c .: e') (pushsubstunder e e' c theta) s) (sigma >> tau) phi1) (eval (c .: e) d s (sigma >> tau) psi1)). { apply (IHs (c.:e') (pushsubstunder e e' c theta) (sigma >> tau) phi1 psi1). - intros [|z]. + simpl. revert H2. apply EquRef1. + simpl. apply ActionEqu. apply H1a. - intros [|z]. + simpl. now apply EquSym. + simpl. apply EquTra with (y := (eval e' (e z) (theta z) (sigma >> tau) (fun w : var => Action (tpinterp (e' w)) (phi w) tau))). * { apply EquTra with (y := Action _ (eval e' (e z) (theta z) sigma phi) tau). - apply ActionEqu. apply H1b. - apply (eval_thm1 e' (e z) (theta z)). + assumption. + intros w. apply ActionEqu. apply H1a. } * { apply EquSym. apply (eval_stmshift c e' (e z) (theta z) (sigma >> tau) (fun w => Action _ (phi w) tau) phi1). - intros [|w]; simpl. + revert H2. apply EquRef1. + apply ActionEqu. apply H1a. - intros w. apply ActionEqu. apply H1a. } } exact L2a. } - destruct (IHs e' theta sigma phi psi H1a H1b) as [IHs1 IHs2]. destruct (IHt e' theta sigma phi psi H1a H1b) as [IHt1 IHt2]. split. + intros tau H2 mu. change (eval e' o (SImp e' (stmparsubst e o e' theta s) (stmparsubst e o e' theta t)) sigma phi (tau >> mu)). apply (eval_SImp_I e' phi H1a). intros nu. asimpl. intros H3. apply (eval_SImp_E e' phi H1a (stmparsubst e o e' theta s) (stmparsubst e o e' theta t) sigma tau H2 (mu >> nu)). exact H3. + intros tau. split. * { intros H2. assert (Hpsi: forall x, Equ _ (psi x) (psi x)). { intros x. generalize (H1b x). apply EquRef1. } apply (eval_SImp_I e psi Hpsi). intros mu H3. apply IHt2. apply (eval_SImp_E e' phi H1a (stmparsubst e o e' theta s) (stmparsubst e o e' theta t) sigma tau H2 mu). now apply IHs2. } * { intros H2. assert (Hpsi: forall x, Equ _ (psi x) (psi x)). { intros x. generalize (H1b x). apply EquRef1. } change (eval e' o (SImp e' (stmparsubst e o e' theta s) (stmparsubst e o e' theta t)) sigma phi tau). apply (eval_SImp_I e' phi H1a). intros mu H3. apply IHt2. apply (eval_SImp_E e psi Hpsi s t sigma tau H2 mu). now apply IHs2. } - simpl. split. + intros tau H2 mu nu x H3. generalize (H2 (mu >> nu) x H3). asimpl. intros H4. exact H4. + intros tau. split. * { intros H2 mu x H3. set (phi1 := fun n : nat => match n as n0 return (Elt (tpinterp ((c .: e') n0))) with | 0 => x | S n' => Action (tpinterp (e' n')) (phi n') (tau >> mu) end). set (psi1 := fun n : nat => match n as n0 return (Elt (tpinterp ((c .: e) n0))) with | 0 => x | S n' => Action (tpinterp (e n')) (psi n') (tau >> mu) end). asimpl. apply (IHs (c .: e') (pushsubstunder e e' c theta) (sigma >> (tau >> mu)) phi1 psi1). - intros [|z]; simpl. + assumption. + apply ActionEqu. apply H1a. - intros [|z]; simpl. + assumption. + apply EquTra with (y := (eval e' (e z) (theta z) (sigma >> (tau >> mu)) (fun w => Action _ (phi w) (tau >> mu)))). * { apply EquTra with (y := (Action (tpinterp (e z)) (eval e' (e z) (theta z) sigma phi) (tau >> mu))). - apply ActionEqu. apply H1b. - generalize (eval_thm1 e' (e z) (theta z) sigma (tau >> mu) phi (fun w => Action _ (phi w) (tau >> mu))). asimpl. intros H4. apply H4. + apply H1a. + intros w. apply ActionEqu. apply H1a. } * { apply EquSym. apply (eval_stmshift c e' (e z) (theta z) (sigma >>(tau >> mu)) (fun w => Action _ (phi w) (tau >> mu)) phi1). - intros [|w]; simpl. + assumption. + apply ActionEqu. apply H1a. - intros w. simpl. asimpl. apply ActionEqu. apply H1a. } - generalize (H2 mu x H3). fold phi1. asimpl. intros H4. exact H4. } * { intros H2 mu x H3. set (phi1 := fun n : nat => match n as n0 return (Elt (tpinterp ((c .: e') n0))) with | 0 => x | S n' => Action (tpinterp (e' n')) (phi n') (tau >> mu) end). set (psi1 := fun n : nat => match n as n0 return (Elt (tpinterp ((c .: e) n0))) with | 0 => x | S n' => Action (tpinterp (e n')) (psi n') (tau >> mu) end). asimpl. apply (IHs (c .: e') (pushsubstunder e e' c theta) (sigma >> (tau >> mu)) phi1 psi1). - intros [|z]; simpl. + assumption. + apply ActionEqu. apply H1a. - intros [|z]; simpl. + assumption. + apply EquTra with (y := (eval e' (e z) (theta z) (sigma >> (tau >> mu)) (fun w => Action _ (phi w) (tau >> mu)))). * { apply EquTra with (y := (Action (tpinterp (e z)) (eval e' (e z) (theta z) sigma phi) (tau >> mu))). - apply ActionEqu. apply H1b. - generalize (eval_thm1 e' (e z) (theta z) sigma (tau >> mu) phi (fun w => Action _ (phi w) (tau >> mu))). asimpl. intros H4. apply H4. + apply H1a. + intros w. apply ActionEqu. apply H1a. } * { apply EquSym. apply (eval_stmshift c e' (e z) (theta z) (sigma >>(tau >> mu)) (fun w => Action _ (phi w) (tau >> mu)) phi1). - intros [|w]; simpl. + assumption. + apply ActionEqu. apply H1a. - intros w. simpl. asimpl. apply ActionEqu. apply H1a. } - generalize (H2 mu x H3). fold phi1. asimpl. intros H4. exact H4. } - split. + destruct (eval_thm3 e' o (stmparsubst e o e' theta (SEq e c s t)) sigma phi H1a) as [H2 _]. exact H2. + intros tau. change (eval e' o (SEq e' c (stmparsubst e c e' theta s) (stmparsubst e c e' theta t)) sigma phi tau <-> eval e o (SEq e c s t) sigma psi tau). generalize (IHs e' theta sigma phi psi H1a H1b). intros IHs1. generalize (IHt e' theta sigma phi psi H1a H1b). intros IHt1. split. * { intros H2. apply eval_SEq_I. - intros n. generalize (H1b n). apply EquRef1. - apply EquTra with (y := Action _ (eval e' c (stmparsubst e c e' theta s) sigma phi) tau). + apply ActionEqu. apply EquSym. exact IHs1. + apply EquTra with (y := Action _ (eval e' c (stmparsubst e c e' theta t) sigma phi) tau). * revert H2. apply eval_SEq_E. exact H1a. * apply ActionEqu. exact IHt1. } * { intros H2. apply (eval_SEq_I e' phi H1a). apply EquTra with (y := Action _ (eval e c s sigma psi) tau). + apply ActionEqu. exact IHs1. + apply EquTra with (y := Action _ (eval e c t sigma psi) tau). * revert H2. apply eval_SEq_E. intros n. generalize (H1b n). apply EquRef1. * apply ActionEqu. apply EquSym. exact IHt1. } Qed. 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). Proof. intros H1 H2. unfold stmsubst. set (theta := (fun n : var => match n as n' return (stm e ((a .: e) n')) with | 0 => t | S n' => SDB e n' end)). apply (eval_stmparsubst (a.:e) b s e theta sigma phi psi). - intros x. generalize (H1 x). apply EquRef1. - intros [|x]. + simpl. apply H2. + simpl. apply EquSym. apply H1. Qed. 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). Proof. simpl. asimpl. apply EquSym. apply eval_stmsubst. - intros x. apply EquSym. apply ActionId. apply Hphi. - apply eval_thm3. exact Hphi. Qed. 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). Proof. apply EquSym. split. - intros tau x y mu H1. destruct (eval_thm1 e (ar a b) s sigma tau phi (fun n => Action _ (phi n) tau) Hphi (fun n => ActionEqu _ _ _ _ (Hphi n))) as [_ [H2 _]]. generalize (H2 ids x y mu H1). asimpl. exact (fun H => H). - intros tau x y H1. simpl. set (psi := fun n : nat => match n as n0 return (Elt (tpinterp ((a .: e) n0))) with | 0 => y | S n' => Action (tpinterp (e n')) (phi n') tau end). assert (L1: forall z : var, Equ (tpinterp ((a .: e) z)) (psi z) (psi z)). { intros [|z]. - simpl. revert H1. apply EquRef2. - simpl. apply ActionEqu. apply Hphi. } assert (L2: forall z : var, Equ (tpinterp (e z)) (Action _ (phi z) tau) (psi (S z))). { intros z. simpl. apply ActionEqu. apply Hphi. } destruct (eval_stmshift a e (ar a b) s (sigma >> tau) (fun z => Action _ (phi z) tau) psi L1 L2) as [H2 H3]. apply EquTra with (y := eval e (ar a b) s (sigma >> tau) (fun z : var => Action (tpinterp (e z)) (phi z) tau) ids x). + change (Equ (tpinterp b) (eval e (ar a b) s sigma phi tau x) (eval e (ar a b) s (sigma >> tau) (fun z : var => Action (tpinterp (e z)) (phi z) tau) ids x)). destruct (eval_thm1 e (ar a b) s sigma tau phi (fun n => Action _ (phi n) tau) Hphi (fun n => ActionEqu _ _ _ _ (Hphi n))) as [_ [_ H4]]. generalize (H4 ids x x (EquRef1 _ _ _ H1)). simpl. asimpl. exact (fun H => H). + apply EquSym. apply (H3 ids y x (EquSym _ _ _ H1)). Qed. 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). Proof. intros D. revert phi Hphi sigma. induction D as [e a b s t|e a b s|e a b s1 s2 t D IHD|e a b s t1 t2 D IHD|e a b s1 s2 D IHD|e s1 s2 t D IHD|e s t1 t2 D IHD|e a s1 s2 D IHD|e a s1 s2 t D IHD|e a s t1 t2 D IHD]; intros phi Hphi sigma. - now apply eval_beta. - now apply eval_eta. - simpl. destruct (IHD phi Hphi sigma) as [IHD1 IHD2]. apply IHD2. now apply eval_thm3. - simpl. destruct (eval_thm3 e (ar a b) s sigma phi Hphi) as [H1 H2]. apply H2. now apply IHD. - simpl. split. + intros tau x y mu H1. set (phi1 := fun n : nat => match n as n0 return (Elt (tpinterp ((a .: e) n0))) with | 0 => x | S n' => Action (tpinterp (e n')) (phi n') tau end). set (phi2 := fun n : nat => match n as n0 return (Elt (tpinterp ((a .: e) n0))) with | 0 => Action (tpinterp a) y mu | S n' => Action (tpinterp (e n')) (phi n') (tau >> mu) end). generalize (eval_thm1 (a.:e) b s1 (sigma >> tau) mu phi1 phi2). asimpl. intros H2. apply H2. * { intros [|z]. - simpl. revert H1. apply EquRef1. - simpl. apply ActionEqu. apply Hphi. } * { intros [|z]. - simpl. apply ActionEqu. apply EquSym. exact H1. - simpl. apply ActionComp. apply Hphi. } + intros tau x y H1. set (phi1 := fun n : nat => match n as n0 return (Elt (tpinterp ((a .: e) n0))) with | 0 => x | S n' => Action (tpinterp (e n')) (phi n') tau end). set (phi2 := fun n : nat => match n as n0 return (Elt (tpinterp ((a .: e) n0))) with | 0 => y | S n' => Action (tpinterp (e n')) (phi n') tau end). assert (Hphi1: forall z, Equ _ (phi1 z) (phi1 z)). { intros [|z]. - simpl. revert H1. apply EquRef1. - simpl. apply ActionEqu. apply Hphi. } apply EquTra with (y := (eval (a .: e) b s2 (sigma >> tau) phi1)). * apply (IHD phi1 Hphi1 (sigma >> tau)). * { apply eval_thm2. intros [|z]. - simpl. assumption. - simpl. apply ActionEqu. apply Hphi. } - destruct (eval_thm3 e o (SImp e s1 t) sigma phi Hphi) as [H1 H2]. split. + intros tau H3 mu. now apply H1. + intros tau. split. * { intros H3. apply (eval_SImp_I e phi Hphi). intros mu H4. apply (eval_SImp_E e phi Hphi s1 t sigma). - exact H3. - destruct (IHD phi Hphi sigma) as [H5 H6]. apply H6. exact H4. } * { intros H3. apply (eval_SImp_I e phi Hphi). intros mu H4. apply (eval_SImp_E e phi Hphi s2 t sigma). - exact H3. - destruct (IHD phi Hphi sigma) as [H5 H6]. apply H6. exact H4. } - destruct (eval_thm3 e o (SImp e s t1) sigma phi Hphi) as [H1 H2]. split. + intros tau H3 mu. now apply H1. + intros tau. split. * { intros H3. apply (eval_SImp_I e phi Hphi). intros mu H4. destruct (IHD phi Hphi sigma) as [H5 H6]. apply H6. apply (eval_SImp_E e phi Hphi s t1 sigma). - exact H3. - exact H4. } * { intros H3. apply (eval_SImp_I e phi Hphi). intros mu H4. destruct (IHD phi Hphi sigma) as [H5 H6]. apply H6. apply (eval_SImp_E e phi Hphi s t2 sigma). - exact H3. - exact H4. } - destruct (eval_thm3 e o (SAll e a s1) sigma phi Hphi) as [H1 H2]. split. + intros tau H3 mu. now apply H1. + intros tau. split. * { simpl. intros H3 mu x H4. set (phi1 := fun n : nat => match n as n0 return (Elt (tpinterp ((a .: e) n0))) with | 0 => x | S n' => Action _ (phi n') (tau >> mu) end). assert (Hphi1: forall z, Equ _ (phi1 z) (phi1 z)). { intros [|z]. - simpl. assumption. - simpl. apply ActionEqu. apply Hphi. } destruct (IHD phi1 Hphi1 (sigma >> tau >> mu)) as [H5 H6]. apply H6. exact (H3 mu x H4). } * { simpl. intros H3 mu x H4. set (phi1 := fun n : nat => match n as n0 return (Elt (tpinterp ((a .: e) n0))) with | 0 => x | S n' => Action _ (phi n') (tau >> mu) end). assert (Hphi1: forall z, Equ _ (phi1 z) (phi1 z)). { intros [|z]. - simpl. assumption. - simpl. apply ActionEqu. apply Hphi. } destruct (IHD phi1 Hphi1 (sigma >> tau >> mu)) as [H5 H6]. apply H6. exact (H3 mu x H4). } - destruct (eval_thm3 e o (SEq e a s1 t) sigma phi Hphi) as [H1 _]. split. + intros tau H2 mu. now apply H1. + intros tau. split. * { intros H2. apply (eval_SEq_I e phi Hphi). apply EquTra with (y := Action (tpinterp a) (eval e a s1 sigma phi) tau). - apply EquSym. apply ActionEqu. apply IHD. exact Hphi. - revert H2. apply eval_SEq_E. exact Hphi. } * { intros H2. apply (eval_SEq_I e phi Hphi). apply EquTra with (y := Action (tpinterp a) (eval e a s2 sigma phi) tau). - apply ActionEqu. apply IHD. exact Hphi. - revert H2. apply eval_SEq_E. exact Hphi. } - destruct (eval_thm3 e o (SEq e a s t1) sigma phi Hphi) as [H1 _]. split. + intros tau H2 mu. now apply H1. + intros tau. split. * { intros H2. apply (eval_SEq_I e phi Hphi). apply EquTra with (y := Action (tpinterp a) (eval e a t1 sigma phi) tau). - revert H2. apply eval_SEq_E. exact Hphi. - apply ActionEqu. apply IHD. exact Hphi. } * { intros H2. apply (eval_SEq_I e phi Hphi). apply EquTra with (y := Action (tpinterp a) (eval e a t2 sigma phi) tau). - revert H2. apply eval_SEq_E. exact Hphi. - apply ActionEqu. apply EquSym. apply IHD. exact Hphi. } Qed. 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). Proof. intros D. induction D as [a s t D|a s|a s t D IHD|a s t u D IHD E IHE]. - now apply eval_conv_1. - now apply eval_thm3. - now apply EquSym. - now apply EquTra with (eval e a t sigma phi). Qed. Lemma eval_SFal e sigma phi tau : ~ eval e o (SFal e) sigma phi tau. Proof. simpl. intros H1. apply (H1 ids (fun mu => False)). split. - intros mu []. - tauto. Qed. (*** Characterization of when two semantic elts x and y are Leibniz equal. ***) 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). Proof. intros Hx Hy. split. - intros H1. set (e1 := a.:e). set (phi1 := fun n => match n as n' return Elt (tpinterp (e1 n')) with O => x | S n' => phi n' end). assert (Hphi1: forall n, Equ _ (phi1 n) (phi1 n)). { intros [|n]. - exact Hx. - simpl. apply Hphi. } set (e2 := a.:e1). set (phi2 := fun n => match n as n' return Elt (tpinterp (e2 n')) with O => y | S n' => Action _ (phi1 n') ids end). assert (Hphi2: forall n, Equ _ (phi2 n) (phi2 n)). { intros [|n]. - exact Hy. - simpl. apply ActionEqu. apply Hphi1. } set (e3 := ar a o.:e2). change (eval e2 o (SAll e2 (ar a o) (SImp e3 (SAp e3 a o (SDB e3 0) (SDB e3 2)) (SAp e3 a o (SDB e3 0) (SDB e3 1)))) sigma phi2 tau) in H1. intros mu p Hp. set (phi3 := fun n => match n as n' return Elt (tpinterp (e3 n')) with O => p | S n' => Action _ (phi2 n') (tau >> mu) end). assert (Hphi3: forall n, Equ _ (phi3 n) (phi3 n)). { intros [|n]. - exact Hp. - simpl. apply ActionEqu. apply Hphi2. } specialize (H1 mu p Hp). change (eval e3 o (SImp e3 (SAp e3 a o (SDB e3 0) (SDB e3 2)) (SAp e3 a o (SDB e3 0) (SDB e3 1))) (sigma >> (tau >> mu)) phi3 ids) in H1. intros nu H2. generalize (eval_SImp_E e3 phi3 Hphi3 (SAp e3 a o (SDB e3 0) (SDB e3 2)) (SAp e3 a o (SDB e3 0) (SDB e3 1)) (sigma >> (tau >> mu)) ids H1 nu). simpl. asimpl. intros H3. apply H3. destruct Hp as [Hp1 Hp2]. assert (L1: Equ (tpinterp a) (Action (tpinterp a) (Action (tpinterp a) x ids) (tau >> mu)) (Action (tpinterp a) x (tau >> mu))). { apply ActionEqu. apply ActionId. assumption. } destruct (Hp2 ids (Action (tpinterp a) (Action (tpinterp a) x ids) (tau >> mu)) (Action (tpinterp a) x (tau >> mu)) L1) as [H4 H5]. apply H5. exact H2. - intros H1. set (e1 := a.:e). set (phi1 := fun n => match n as n' return Elt (tpinterp (e1 n')) with O => x | S n' => phi n' end). assert (Hphi1: forall n, Equ _ (phi1 n) (phi1 n)). { intros [|n]. - exact Hx. - simpl. apply Hphi. } set (e2 := a.:e1). set (phi2 := fun n => match n as n' return Elt (tpinterp (e2 n')) with O => y | S n' => Action _ (phi1 n') ids end). assert (Hphi2: forall n, Equ _ (phi2 n) (phi2 n)). { intros [|n]. - exact Hy. - simpl. apply ActionEqu. apply Hphi1. } set (e3 := ar a o.:e2). change (eval e2 o (SAll e2 (ar a o) (SImp e3 (SAp e3 a o (SDB e3 0) (SDB e3 2)) (SAp e3 a o (SDB e3 0) (SDB e3 1)))) sigma phi2 tau). intros mu p Hp. set (phi3 := fun n => match n as n' return Elt (tpinterp (e3 n')) with O => p | S n' => Action _ (phi2 n') (tau >> mu) end). assert (Hphi3: forall n, Equ _ (phi3 n) (phi3 n)). { intros [|n]. - exact Hp. - simpl. apply ActionEqu. apply Hphi2. } change (eval e3 o (SImp e3 (SAp e3 a o (SDB e3 0) (SDB e3 2)) (SAp e3 a o (SDB e3 0) (SDB e3 1))) (sigma >> (tau >> mu)) phi3 ids). apply (eval_SImp_I e3 phi3 Hphi3). intros nu. asimpl. intros H2. apply (H1 mu p Hp nu). destruct Hp as [Hp1 Hp2]. assert (L1: Equ (tpinterp a) (Action (tpinterp a) (Action (tpinterp a) x ids) (tau >> mu)) (Action (tpinterp a) x (tau >> mu))). { apply ActionEqu. apply ActionId. assumption. } destruct (Hp2 ids (Action (tpinterp a) (Action (tpinterp a) x ids) (tau >> mu)) (Action (tpinterp a) x (tau >> mu)) L1) as [H3 H4]. apply H4. exact H2. Qed. 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. Proof. intros Hx Hy H1. apply (SLeibEq_char e phi Hphi). - assumption. - assumption. - intros mu p [Hp1 Hp2] nu. apply (Hp2 ids (Action _ x (tau >> mu)) (Action _ y (tau >> mu))). apply EquTra with (y := Action _ (Action (tpinterp a) x tau) mu). + apply ActionComp. assumption. + apply EquTra with (y := Action _ (Action (tpinterp a) y tau) mu). * apply ActionEqu. assumption. * apply EquSym. apply ActionComp. assumption. Qed. 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. intros D. induction D as [e G s H1|e G s t E D IHD|e G s t D IHD|e G s t D IHD E IHE|e G a s D IHD|e G a s t D IHD|e G a s|e G a s t D IHD|e G s t D IHD E IHE|e G a b s t D IHD|e G s1 s2 t D IHD|e G s t1 t2 D IHD|e G s t D IHD|e G s t u D IHD]. - intros sigma phi Hphi tau H2. apply H2. exact H1. - intros sigma phi Hphi tau H1. destruct (eval_conv e phi Hphi o s t sigma E) as [H2 H3]. apply H3. now apply IHD. - intros sigma phi Hphi tau H1. apply (eval_SImp_I e phi Hphi). intros mu H2. apply (IHD sigma phi Hphi). intros u [H3|H3]. + destruct (eval_thm3 e o u sigma phi Hphi) as [H4 _]. apply H4. now apply H1. + congruence. - intros sigma phi Hphi tau H1. generalize (eval_SImp_E e phi Hphi _ _ _ _ (IHD sigma phi Hphi tau H1) ids). asimpl. intros H2. apply H2. apply (IHE sigma phi Hphi tau H1). - intros sigma phi Hphi tau H1. simpl. intros mu x Hx. set (phi1 := fun n : nat => match n as n0 return (Elt (tpinterp ((a .: e) n0))) with | 0 => x | S n' => Action (tpinterp (e n')) (phi n') (tau >> mu) end). assert (L1: forall x : nat, Equ (tpinterp ((a .: e) x)) (phi1 x) (phi1 x)). { intros [|n]. - simpl. exact Hx. - simpl. apply ActionEqu. apply Hphi. } apply (IHD (sigma >> tau >> mu) phi1 L1 ids). intros u [v [H2 H3]]. subst u. generalize (H1 v H2). intros IHD1. set (phi2 := fun n => Action (tpinterp (e n)) (phi n) (tau >> mu)). assert (L2a: forall x : var, Equ _ (phi1 x) (phi1 x)). { intros [|y]. - simpl. assumption. - simpl. apply ActionEqu. apply Hphi. } assert (L2b: forall x : var, Equ (tpinterp (e x)) (phi2 x) (phi1 (S x))). { intros n. simpl. unfold phi2. apply ActionEqu. apply Hphi. } destruct (eval_stmshift a e o v (sigma >> tau >> mu) phi2 phi1 L2a L2b) as [H3 H4]. apply H4. assert (L3:forall n : nat, Equ (tpinterp (e n)) (phi2 n) (Action (tpinterp (e n)) (phi n) (tau >> mu))). { intros n. unfold phi2. apply ActionEqu. apply Hphi. } destruct (eval_thm1 e o v sigma (tau >> mu) phi phi2 Hphi L3) as [_ [_ H6]]. asimpl. apply H6. asimpl. destruct (eval_thm3 e o v sigma phi Hphi) as [H7 _]. apply (H7 tau). exact IHD1. - intros sigma phi Hphi tau H1. generalize (eval_thm3 e a t sigma phi Hphi). intros L0. assert (L0a: Equ (tpinterp a) (Action (tpinterp a) (eval e a t sigma phi) tau) (Action (tpinterp a) (eval e a t sigma phi) tau)). { apply ActionEqu. exact L0. } generalize (IHD sigma phi Hphi tau H1). asimpl. intros IHD1. generalize (IHD1 ids (Action (tpinterp a) (eval e a t sigma phi) tau) L0a). asimpl. set (psi := fun n => match n as n' return Elt (tpinterp ((a.:e) n')) with O => Action (tpinterp a) (eval e a t sigma phi) tau | S n' => Action (tpinterp (e n')) (phi n') tau end). intros IHD2. set (xi := fun n => match n as n' return Elt (tpinterp ((a.:e) n')) with O => eval e a t sigma phi | S n' => phi n' end). assert (L1: forall x : var, Equ (tpinterp (e x)) (phi x) (xi (S x))). { intros x. simpl. apply Hphi. } assert (L2: Equ (tpinterp a) (xi 0) (eval e a t sigma phi)). { simpl. exact L0. } destruct (eval_stmsubst a e o s t sigma phi xi L1 L2) as [H2 H3]. (*** substitution lemma ***) apply H3. assert (L3: (forall n : nat, Equ (tpinterp ((a .: e) n)) (xi n) (xi n))). { intros [|n]. - simpl. exact L0. - simpl. apply Hphi. } assert (L4: (forall n : nat, Equ (tpinterp ((a .: e) n)) (psi n) (Action (tpinterp ((a .: e) n)) (xi n) tau))). { intros [|n]. - simpl. exact L0a. - simpl. apply ActionEqu. apply Hphi. } destruct (eval_thm1 (a.:e) o s sigma tau xi psi L3 L4) as [_ [_ H4]]. generalize (H4 ids). asimpl. intros H5. apply H5. exact IHD2. - intros sigma phi Hphi tau H1. apply (eval_SEq_I e phi Hphi). apply ActionEqu. apply eval_thm3. exact Hphi. - intros sigma phi Hphi tau H1. change (eval e (ar a (ar a o)) (SLeibEq e a) sigma phi ids (eval e a s sigma phi) ids (eval e a t sigma phi) tau). apply (eval_SLeibEq_I e phi Hphi). + apply eval_thm3. exact Hphi. + apply eval_thm3. exact Hphi. + generalize (IHD sigma phi Hphi tau H1). apply eval_SEq_E. exact Hphi. - intros sigma phi Hphi tau H1. apply (eval_SEq_I e phi Hphi). split. + destruct (eval_thm3 e o s sigma phi Hphi) as [H2 _]. intros mu H3 nu. simpl. generalize (H2 (tau >> mu) H3 nu). asimpl. tauto. + intros mu. simpl. split. * { intros H2. apply (IHD sigma phi Hphi (tau >> mu)). intros u [H3|H3]. - destruct (eval_thm3 e o u sigma phi Hphi) as [H4 _]. apply H4. now apply H1. - subst u. exact H2. } * { intros H2. apply (IHE sigma phi Hphi (tau >> mu)). intros u [H3|H3]. - destruct (eval_thm3 e o u sigma phi Hphi) as [H4 _]. apply H4. now apply H1. - subst u. exact H2. } - intros sigma phi Hphi tau H1. apply (eval_SEq_I e phi Hphi). simpl. split. + intros mu x y nu H2. set (phi1 := fun n : nat => match n as n0 return (Elt (tpinterp ((a .: e) n0))) with | 0 => x | S n' => Action (tpinterp (e n')) (phi n') (tau >> mu) end). set (phi2 := fun n : nat => match n as n0 return (Elt (tpinterp ((a .: e) n0))) with | 0 => Action (tpinterp a) y nu | S n' => Action (tpinterp (e n')) (phi n') (tau >> (mu >> nu)) end). assert (L1: forall n : nat, Equ (tpinterp ((a .: e) n)) (phi1 n) (phi1 n)). { intros [|n]; simpl. - revert H2. apply EquRef1. - apply ActionEqu. apply Hphi. } assert (L2: forall n : nat, Equ (tpinterp ((a .: e) n)) (phi2 n) (Action (tpinterp ((a .: e) n)) (phi1 n) nu)). { intros [|n]; simpl. - apply ActionEqu. apply EquSym. exact H2. - apply EquTra with (y := (Action (tpinterp (e n)) (phi n) (tau >> mu >> nu))). + asimpl. apply ActionEqu. apply Hphi. + apply ActionComp. apply Hphi. } generalize (eval_thm1 (a.:e) b s (sigma >> (tau >> mu)) nu phi1 phi2 L1 L2). asimpl. intros [_ H3]. exact H3. + intros mu x y H2. set (phi1 := fun n : nat => match n as n0 return (Elt (tpinterp ((a .: e) n0))) with | 0 => x | S n' => Action (tpinterp (e n')) (phi n') (tau >> mu) end). set (phi2 := fun n : nat => match n as n0 return (Elt (tpinterp ((a .: e) n0))) with | 0 => y | S n' => Action (tpinterp (e n')) (phi n') (tau >> mu) end). apply EquTra with (y := eval (a .: e) b t (sigma >> (tau >> mu)) phi1). * { assert (L1: forall z : nat, Equ (tpinterp ((a .: e) z)) (phi1 z) (phi1 z)). { intros [|z]. - simpl. revert H2. apply EquRef1. - simpl. apply ActionEqu. apply Hphi. } assert (L2: forall z : var, Equ (tpinterp (e z)) (Action (tpinterp (e z)) (phi z) (tau >> mu)) (phi1 (S z))). { intros z. apply ActionEqu. apply Hphi. } assert (L3: forall u : stm (a .: e) o, (exists v : stm e o, G v /\ u = stmshift a e o v) -> eval (a .: e) o u (sigma >> (tau >> mu)) phi1 ids). { intros u [v [H3 H4]]. subst u. destruct (eval_stmshift a e o v (sigma >> (tau >> mu)) (fun z => Action _ (phi z) (tau >> mu)) phi1 L1 L2) as [H4 H5]. apply H5. generalize (H1 v H3). intros H6. destruct (eval_thm1 e o v sigma (tau >> mu) phi (fun z : var => Action (tpinterp (e z)) (phi z) (tau >> mu)) Hphi (fun z => ActionEqu _ _ _ _ (Hphi z))) as [[H7 _] [_ H8]]. apply H8. simpl. asimpl. apply H7. exact H6. } generalize (IHD (sigma >> (tau >> mu)) phi1 L1 ids L3). intros H3. generalize (eval_SEq_E (a.:e) phi1 L1 b s t (sigma >> (tau >> mu)) ids H3). intros H4. - apply EquTra with (Action (tpinterp b) (eval (a .: e) b s (sigma >> (tau >> mu)) phi1) ids). + apply EquSym. apply ActionId. apply eval_thm3. exact L1. + apply EquTra with (Action (tpinterp b) (eval (a .: e) b t (sigma >> (tau >> mu)) phi1) ids). * exact H4. * apply ActionId. apply eval_thm3. exact L1. } * { apply eval_thm2. intros [|n]. - simpl. exact H2. - simpl. apply ActionEqu. apply Hphi. } - intros sigma phi Hphi tau H1. apply (eval_SEq_I e phi Hphi). simpl. generalize (IHD sigma phi Hphi tau H1). intros H2. apply (eval_SEq_E e phi Hphi) in H2. simpl in H2. injection H2. asimpl. exact (fun H => H). - intros sigma phi Hphi tau H1. apply (eval_SEq_I e phi Hphi). simpl. generalize (IHD sigma phi Hphi tau H1). intros H2. apply (eval_SEq_E e phi Hphi) in H2. simpl in H2. injection H2. asimpl. exact (fun H => H). - intros sigma phi Hphi tau H1. apply (eval_SEq_I e phi Hphi). generalize (IHD sigma phi Hphi tau H1). intros H2. apply (eval_SEq_E e phi Hphi) in H2. simpl in H2. injection H2. intros H3. split. + intros mu x y nu H4. simpl. simpl in H4. subst y. destruct (eval_thm3 e (ar i i) s sigma phi Hphi) as [H5 _]. simpl in H5. generalize (H5 (tau >> mu) x x nu (eq_refl x)). asimpl. exact (fun H => H). + intros mu x y H4. simpl. (*** This is the cool case. ***) simpl in H4. subst y. assert (L1: ((eval e (ar i i) s sigma phi (ren S) (Va 0)).[up tau]).[x.:mu] = eval e (ar i i) s sigma phi (tau >> mu) x). { asimpl. destruct (eval_thm3 e (ar i i) s sigma phi Hphi) as [H4 _]. simpl in H4. generalize (H4 (ren S) (Va 0) (Va 0) (x.:tau >> mu) (eq_refl (Va 0))). intros H5. asimpl in H5. rewrite H5. autosubst. } assert (L2: ((eval e (ar i i) t sigma phi (ren S) (Va 0)).[up tau]).[x.:mu] = eval e (ar i i) t sigma phi (tau >> mu) x). { asimpl. destruct (eval_thm3 e (ar i i) t sigma phi Hphi) as [H4 _]. simpl in H4. generalize (H4 (ren S) (Va 0) (Va 0) (x.:tau >> mu) (eq_refl (Va 0))). intros H5. asimpl in H5. rewrite H5. autosubst. } rewrite <- L1. rewrite <- L2. rewrite H3. reflexivity. - intros sigma phi Hphi tau H1. exfalso. generalize (IHD sigma phi Hphi tau H1). intros H2. apply (eval_SEq_E e phi Hphi) in H2. simpl in H2. discriminate H2. Qed. (*** The remaining results are not needed, but may be interesting. ***) Lemma botRiId : RiId (fun _ => False). intros sigma []. Qed. Lemma topRiId : RiId (fun _ => True). intros sigma. tauto. Qed. Lemma meetRiId X (Xs:RiId X) Y (Ys:RiId Y) : RiId (fun sigma => X sigma /\ Y sigma). intros sigma [H1 H2] tau. split. - now apply Xs. - now apply Ys. Qed. Lemma joinRiId X (Xs:RiId X) Y (Ys:RiId Y) : RiId (fun sigma => X sigma \/ Y sigma). intros sigma [H|H] tau. - left. now apply Xs. - right. now apply Ys. Qed. Lemma bigjoinRiId (C:((var -> term) -> Prop) -> Prop) (Cs:forall X, C X -> RiId X) : RiId (fun sigma => exists X, C X /\ X sigma). intros sigma [X [H1 H2]] tau. exists X. split. - assumption. - now apply (Cs X H1). Qed. 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). apply bigjoinRiId with (C := fun Z => RiId Z /\ (forall tau, X tau -> Z tau -> Y tau)). tauto. Qed. (*** Not ***) 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). Proof. unfold SNot. destruct (eval_beta e phi Hphi o o (SImp (o.:e) (SDB (o.:e) 0) (SFal (o.:e))) s sigma) as [H1 H2]. intros H3. apply H2 in H3. change (eval e o (SImp e s (SFal e)) sigma phi tau) in H3. intros mu H4. generalize (eval_SImp_E _ phi Hphi s (SFal e) _ _ H3 mu H4). apply eval_SFal. Qed. 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. Proof. unfold SNot. intros H0. destruct (eval_beta e phi Hphi o o (SImp (o.:e) (SDB (o.:e) 0) (SFal (o.:e))) s sigma) as [H1 H2]. apply H2. change (eval e o (SImp e s (SFal e)) sigma phi tau). apply (eval_SImp_I e phi Hphi). intros mu H4. exfalso. apply (H0 mu). exact H4. Qed. 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). Proof. exact (eval_SNot_E e phi Hphi sigma s tau). Qed. 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. Proof. exact (eval_SNot_I e phi Hphi sigma s tau). Qed. 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). Proof. intros Hp1 Hp2. split. - intros tau x y mu H1. split. + simpl. unfold charfn. intros nu H2 xi. apply (Hp2 (Action _ (Action _ x (mu >> nu)) xi)). * apply Hp1. exact H2. * { apply EquTra with (y := Action (tpinterp a) x ((mu >> nu) >> xi)). - apply EquSym. apply ActionComp. revert H1. apply EquRef1. - asimpl. apply ActionEqu. revert H1. apply EquRef1. } + intros sigma. split. * { unfold charfn. simpl. intros H2. apply (Hp2 _ _ H2). apply EquTra with (y := Action (tpinterp a) y (mu >> sigma)). - apply ActionEqu. exact H1. - apply ActionComp. revert H1. apply EquRef2. } * { unfold charfn. simpl. intros H2. apply (Hp2 _ _ H2). apply EquTra with (y := Action (tpinterp a) y (mu >> sigma)). - apply EquSym. apply ActionComp. revert H1. apply EquRef2. - apply ActionEqu. now apply EquSym. } - intros sigma x y H1. unfold charfn. split. + intros tau H2 mu. apply (Hp2 (Action _ (Action _ x tau) mu)). * now apply Hp1. * apply EquSym. apply ActionComp. revert H1. apply EquRef1. + intros tau. split. * { intros H2. apply (Hp2 (Action _ x tau)). - exact H2. - now apply ActionEqu. } * { intros H2. apply (Hp2 (Action _ y tau)). - exact H2. - apply ActionEqu. now apply EquSym. } Qed. 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). Proof. intros Hx. unfold singfn. split. - intros sigma y z tau H1. split. + simpl. intros mu H2 nu. apply EquTra with (y := Action (tpinterp a) y (tau >> mu >> nu)). * asimpl. apply ActionEqu. revert H1. apply EquRef1. * { apply EquTra with (y := Action _ (Action (tpinterp a) y (tau >> mu)) nu). - apply ActionComp. revert H1. apply EquRef1. - apply EquTra with (y := Action _ (Action (tpinterp a) x (sigma >> (tau >> mu))) nu). + apply ActionEqu. assumption. + apply EquSym. apply EquTra with (y := Action (tpinterp a) x ((sigma >> (tau >> mu)) >> nu)). * asimpl. apply ActionEqu. assumption. * apply ActionComp. assumption. } + intros mu. simpl. split. * { intros H2. apply EquTra with (y := (Action _ y (tau >> mu))). - apply EquTra with (y := Action _ (Action _ y tau) mu). + apply ActionEqu. apply ActionEqu. now apply EquSym. + apply EquSym. apply ActionComp. revert H1. apply EquRef1. - asimpl. exact H2. } * { intros H2. apply EquTra with (y := (Action _ z (tau >> mu))). - apply ActionEqu. assumption. - apply EquTra with (y := Action _ (Action _ z tau) mu). + apply ActionComp. revert H1. apply EquRef2. + asimpl in H2. exact H2. } - intros sigma y z H1. split. + intros tau. simpl. intros H2 mu. apply EquTra with (y := Action _ (Action _ y tau) mu). * apply ActionComp. revert H1. apply EquRef1. * { apply EquTra with (y := Action _ (Action _ x (sigma >> tau)) mu). - apply ActionEqu. assumption. - apply EquSym. apply EquTra with (y := Action _ x ((sigma >> tau) >> mu)). + asimpl. apply ActionEqu. assumption. + apply ActionComp. assumption. } + intros tau. split. * { intros H2. apply EquTra with (y := (Action _ y tau)). - apply ActionEqu. now apply EquSym. - exact H2. } * { intros H2. apply EquTra with (y := (Action _ z tau)). - apply ActionEqu. assumption. - exact H2. } Qed. (*** Characterization of evaluation of "forall p:a->o, p x -> p y" under sigma and phi, where x is DB 1 and y is DB 0 ***) 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. Proof. split. - intros H1 mu p Hp nu H2. generalize (H1 mu p Hp). set (e1 := ar a o.:a.:a.:e). set (phi1 := fun n => match n as n' return Elt (tpinterp (e1 n')) with O => p | S n' => Action _ (phi n') (tau >> mu) end). assert (Hphi1: forall n, Equ _ (phi1 n) (phi1 n)). { intros [|n]. - exact Hp. - simpl. apply ActionEqu. apply Hphi. } intros H3. change (eval e1 o (SImp e1 (SAp e1 a o (SDB e1 0) (SDB e1 2)) (SAp e1 a o (SDB e1 0) (SDB e1 1))) (sigma >> tau >> mu) phi1 ids) in H3. apply (eval_SImp_E e1 phi1 Hphi1 (SAp e1 a o (SDB e1 0) (SDB e1 2)) (SAp e1 a o (SDB e1 0) (SDB e1 1)) (sigma >> tau >> mu) ids H3 nu). exact H2. - intros H1 mu p Hp. set (e1 := ar a o.:a.:a.:e). set (phi1 := fun n => match n as n' return Elt (tpinterp (e1 n')) with O => p | S n' => Action _ (phi n') (tau >> mu) end). assert (Hphi1: forall n, Equ _ (phi1 n) (phi1 n)). { intros [|n]. - exact Hp. - simpl. apply ActionEqu. apply Hphi. } change (eval e1 o (SImp e1 (SAp e1 a o (SDB e1 0) (SDB e1 2)) (SAp e1 a o (SDB e1 0) (SDB e1 1))) (sigma >> tau >> mu) phi1 ids). apply (eval_SImp_I e1 phi1 Hphi1). intros nu. apply H1. exact Hp. Qed. 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. Proof. intros H1. assert (Hx: Equ _ x x). { revert H1. apply EquRef1. } assert (Hy: Equ _ y y). { revert H1. apply EquRef2. } apply (eval_SLeibEq_I e phi Hphi a x y sigma tau Hx Hy). now apply ActionEqu. Qed. 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). Proof. intros Hx Hy H1. generalize (SLeibEq_char e phi Hphi a x y sigma tau Hx Hy). intros [H2 _]. set (p := singfn a x). assert (Hp : Equ (tpinterp (ar a o)) p p). { unfold p. apply singfnEqu. assumption. } assert (Hptau : Equ (tpinterp (ar a o)) (Action (tpinterp (ar a o)) p tau) (Action (tpinterp (ar a o)) p tau)). { apply ActionEqu. exact Hp. } generalize (H2 H1 ids (Action (tpinterp (ar a o)) p tau) Hptau ids). asimpl. intros H3. assert (H4: p tau (Action (tpinterp a) x tau) ids). { unfold p. unfold singfn. asimpl. apply ActionId. apply ActionEqu. assumption. } generalize (H3 H4). unfold p. unfold singfn. asimpl. intros H5. apply EquTra with (y := Action _ (Action (tpinterp a) y tau) ids). - now apply EquSym. - apply ActionId. apply ActionEqu. exact Hy. Qed. (*** At type i, two untyped lambda terms are Leibniz equal (i.e., the monoid identity ids is in "forall p. p s -> p t") if and only if they are the same untyped lambda term. ***) 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. Proof. split. - intros H1. apply (eval_SLeibEq_E e phi Hphi) in H1. + asimpl in H1. exact H1. + reflexivity. + reflexivity. - intros H1. subst t. apply (eval_SLeibEq_I' e phi Hphi). reflexivity. Qed. (*** At type nat, two naturals are Leibniz equal if they are the same. ***) 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. Proof. split. - intros H1. apply (eval_SLeibEq_E e phi Hphi) in H1. + simpl in H1. exact H1. + reflexivity. + reflexivity. - intros H1. subst m. apply (eval_SLeibEq_I' e phi Hphi). reflexivity. Qed. (*** At type o, P and Q are Leibniz equal if and only if they are the same right ideals. ***) 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). Proof. intros HP HQ. split. - intros H1. assert (L1: Equ (tpinterp o) P P) by (split; tauto). assert (L2: Equ (tpinterp o) Q Q) by (split; tauto). destruct (eval_SLeibEq_E e phi Hphi o P Q sigma ids L1 L2 H1) as [_ H2]. intros tau. generalize (H2 tau). asimpl. tauto. - intros H1. apply (eval_SLeibEq_I' e phi Hphi). split; assumption. Qed. (*** At function types a -> b, f and g are Leibniz equal if and only if they agree as functions. ***) 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)). Proof. intros Hf Hg. split. - intros H1. destruct (eval_SLeibEq_E e phi Hphi (ar a b) f g sigma ids Hf Hg H1) as [H2 H3]. intros tau x Hx. generalize (H3 tau x x Hx). asimpl. tauto. - intros H1. apply (eval_SLeibEq_I' e phi Hphi). split. destruct Hf as [Hf1 Hf2]. exact Hf1. intros tau x y H2. apply EquTra with (y := g tau x). + apply H1. revert H2. apply EquRef1. + destruct Hg as [Hg1 Hg2]. now apply Hg2. Qed.