(** EFlatPred.v Version 1.0 January 2008 *) (** does not need impredicative Set, runs under V8.1, tested with 8.1pl3 *) (** Copyright Ralph Matthes, I.R.I.T., C.N.R.S. & University of Toulouse*) Set Implicit Arguments. Require Import LNMItPred. Require Import LNGMItPred. Require Import LamPred. Require Import List. Open Scope type_scope. Definition LamEF(X:k1)(A:k0) := LamF X A + X (X A). Definition lamEFpEFct : pEFct LamEF. Proof. unfold LamEF. apply sumpEFct. exact lampEFct. apply comppEFct. apply idpEFct. apply comppEFct. apply idpEFct. apply constpEFct. apply idEFct. Defined. (** flattening lists, with flat_map from the library *) Definition flatten : forall (A:k0), list(list A) -> list A := fun A => flat_map (id(A:=list A)). (** the usual rules for flatten hold in the strong form that both sides have the same normal form: *) Lemma flattenNil : forall (A:k0), flatten(A:=A) nil = nil. Proof. reflexivity. Qed. Lemma flattenCons: forall (A:k0)(a:list A)(l:list(list A)), flatten (a::l) = a ++ flatten l. Proof. reflexivity. Qed. Lemma flattenAppend (A:k0)(l1 l2:list(list A)): flatten (l1 ++ l2) = flatten l1 ++ flatten l2. Proof. intros. induction l1. reflexivity. rewrite flattenCons. rewrite app_ass. rewrite <- IHl1. reflexivity. Qed. (** naturality of flatten in the categorical sense *) Lemma mapflatten : forall (A B:k0)(f:A->B)(l:list (list A)), flatten(map(map f) l) = map f (flatten l). Proof. intros. induction l. reflexivity. simpl. rewrite flattenCons. rewrite IHl. rewrite <- map_app. reflexivity. Qed. Lemma flattenSingleton (A:k0)(l:list A): flatten (l::nil) = l. Proof. intros. unfold flatten. simpl. rewrite app_nil_end. reflexivity. Qed. Module Type LAME := LNGMIt_Type with Definition LNM.F:=LamEF with Definition LNM.FpEFct := lamEFpEFct. Module EFlat (LamEBase:LAME). Module LamEM := LNGMItDef LamEBase. Module LamEMMItDef := LamEM.LNMItDef. Definition LamE : k1 := LamEBase.mu2. Definition flatE (A:k0)(ee:LamE(LamE A)): LamE A := LamEMMItDef.InCan (inr _ ee). Definition lamE : mon LamE := LamEBase.mapmu2. (** We study the generic representation of substitution within the calculus with explicit flattening. *) Lemma lamEext: ext lamE. Proof. exact LamEMMItDef.mapmu2Ext. Qed. Lemma lamEfct1: fct1 lamE. Proof. exact LamEMMItDef.mapmu2Id. Qed. Lemma lamEfct2 : fct2 lamE. Proof. exact LamEMMItDef.mapmu2Comp. Qed. (** other canonical datatype constructors *) Definition varE (A:k0)(a:A): LamE A := LamEMMItDef.InCan (inl _ (inl _ (inl _ a))). Definition appE (A:k0)(t1 t2:LamE A): LamE A := LamEMMItDef.InCan (inl _ (inl _ (inr _ (t1,t2)))). Lemma appE_cong(A:k0)(s1 s2 t1 t2:LamE A): s1 = t1 -> s2 = t2 -> appE s1 s2 = appE t1 t2. Proof. intros. rewrite H. rewrite H0. reflexivity. Qed. Definition absE (A:k0)(r: LamE (option A)): LamE A := LamEMMItDef.InCan (inl _ (inr _ r)). (* lambda terms into lists of free variables, just with plain Mendler iteration *) Definition LamEToFV : LamE c_k1 listk1. Proof. refine (LamEBase.MIt (fun (X:k1)(it: X c_k1 listk1)(A:Set)(t:LamEF X A) => _)). destruct t as [[[a|(t1,t2)]|r]|e]. exact (a::nil). exact (it _ t1 ++ it _ t2). exact (filterSome (it _ r)). exact (flatten(map(it A)(it (X A) e))). Defined. Definition sLamEToFV := fun (X : k1) (it : X c_k1 listk1) (A : Set) (t : LamEF X A) => match t with | inl (inl (inl a)) => a :: nil | inl (inl (inr (pair t1 t2))) => it A t1 ++ it A t2 | inl (inr r) => filterSome (it (option A) r) | inr e => flatten (map (it A) (it (X A) e)) end. Lemma sLamEToFV_ok: LamEToFV = LamEBase.MIt sLamEToFV. Proof. reflexivity. Qed. Lemma LamEToFV_var (A:k0)(a:A): LamEToFV(varE a) = a::nil. Proof. intros. unfold varE. unfold LamEToFV. rewrite LamEMMItDef.MItRedCan. reflexivity. Qed. Lemma LamEToFV_app (A:k0)(t1 t2:LamE A): LamEToFV(appE t1 t2) = LamEToFV t1 ++ LamEToFV t2. Proof. intros. unfold appE. unfold LamEToFV at 1. rewrite LamEMMItDef.MItRedCan. reflexivity. Qed. Lemma LamEToFV_abs (A:k0)(r:LamE (option A)): LamEToFV(absE r) = filterSome (LamEToFV r). Proof. intros. unfold absE. unfold LamEToFV at 1. rewrite LamEMMItDef.MItRedCan. reflexivity. Qed. Lemma LamEToFV_flat (A:k0)(ee:LamE (LamE A)): LamEToFV(flatE ee) = flatten (map (LamEToFV(A:=A)) (LamEToFV ee)). Proof. intros. unfold flatE. unfold LamEToFV at 1. rewrite LamEMMItDef.MItRedCan. reflexivity. Qed. (** we are heading for closure properties of the free variables *) Definition occursFreeInE(A:k0)(a:A)(t:LamE A): Prop := In a (LamEToFV t). Infix "occE" := occursFreeInE (at level 90). (* the previous approach through an inductive definition Inductive occursFreeInE: forall (A:k0), A -> LamE A -> Prop := | occE_var: forall (X : k1) (ef : EFct X) (j : X c_k1 LamE) (n : NAT j (m ef) lamE) (A : Set) (a : A), occursFreeInE a (LamEBase.In ef n (inl (X (X A)) (inl (X (option A)) (inl (X A * X A) a)))) | occE_appl: forall (X : k1) (ef : EFct X) (j : X c_k1 LamE) (n : NAT j (m ef) lamE) (A : Set) (a : A)(t1 t2 : X A), (occursFreeInE a (j A t1)) -> occursFreeInE a (LamEBase.In ef n (inl (X (X A)) (inl (X (option A)) (inr A (t1, t2))))) | occE_appr: forall (X : k1) (ef : EFct X) (j : X c_k1 LamE) (n : NAT j (m ef) lamE) (A : Set) (a : A)(t1 t2 : X A), (occursFreeInE a (j A t2)) -> occursFreeInE a (LamEBase.In ef n (inl (X (X A)) (inl (X (option A)) (inr A (t1, t2))))) | occE_abs: forall (X : k1) (ef : EFct X) (j : X c_k1 LamE) (n : NAT j (m ef) lamE) (A : Set) (a : A)(r: X (option A)), (occursFreeInE (Some a)(j (option A) r)) -> occursFreeInE a (LamEBase.In ef n (inl (X (X A)) (inr (A + X A * X A) r))) | occE_flat: forall (X : k1) (ef : EFct X) (j : X c_k1 LamE) (n : NAT j (m ef) lamE) (A : Set)(a: X A)(ee: X(X A)), (occursFreeInE a (j (X A) ee)) -> forall a0 : A, (occursFreeInE a0 (j A a)) -> occursFreeInE a0 (LamEBase.In ef n (inr (LamF X A) ee)). Infix "occE" := occursFreeInE (at level 90). *) Lemma occE_var: forall (X : k1) (ef : EFct X) (j : X c_k1 LamE) (n : NAT j (m ef) lamE) (A : Set) (a : A), a occE (LamEBase.In ef n (inl (X (X A)) (inl (X (option A)) (inl (X A * X A) a)))). Proof. intros. unfold occursFreeInE. unfold LamEToFV. rewrite LamEBase.MItRed. simpl. left. reflexivity. Qed. Lemma occE_appl: forall (X : k1) (ef : EFct X) (j : X c_k1 LamE) (n : NAT j (m ef) lamE) (A : Set) (a : A)(t1 t2 : X A), (a occE (j A t1)) -> a occE (LamEBase.In ef n (inl (X (X A)) (inl (X (option A)) (inr A (t1, t2))))). Proof. intros. unfold occursFreeInE. unfold LamEToFV. rewrite LamEBase.MItRed. apply in_or_app. left. assumption. Qed. Lemma occE_appr: forall (X : k1) (ef : EFct X) (j : X c_k1 LamE) (n : NAT j (m ef) lamE) (A : Set) (a : A)(t1 t2 : X A), (a occE (j A t2)) -> a occE (LamEBase.In ef n (inl (X (X A)) (inl (X (option A)) (inr A (t1, t2))))). Proof. intros. unfold occursFreeInE. unfold LamEToFV. rewrite LamEBase.MItRed. apply in_or_app. right. assumption. Qed. Lemma occE_abs: forall (X : k1) (ef : EFct X) (j : X c_k1 LamE) (n : NAT j (m ef) lamE) (A : Set) (a : A)(r: X (option A)), ((Some a) occE (j (option A) r)) -> a occE (LamEBase.In ef n (inl (X (X A)) (inr (A + X A * X A) r))). Proof. intros. unfold occursFreeInE. unfold LamEToFV. rewrite LamEBase.MItRed. apply filterSomeIn. assumption. Qed. (* some preparation *) Lemma in_flatten (A:k0)(a:A)(aa:list A)(l:list(list A)): In a aa -> In aa l -> In a (flatten l). Proof. intros. unfold flatten. apply (proj2 (in_flat_map(A:=list A) (id (A:=list A)) l a)). exists aa. split; assumption. Qed. Lemma occE_flat: forall (X : k1) (ef : EFct X) (j : X c_k1 LamE) (n : NAT j (m ef) lamE) (A : Set)(a: X A)(ee: X(X A)), (occursFreeInE a (j (X A) ee)) -> forall a0 : A, (occursFreeInE a0 (j A a)) -> occursFreeInE a0 (LamEBase.In ef n (inr (LamF X A) ee)). Proof. intros. unfold occursFreeInE. unfold LamEToFV. rewrite LamEBase.MItRed. unfold occursFreeInE in H0. apply (in_flatten _ _ (map (LamEToFV(A:=A) o j A) (LamEToFV (j _ ee))) H0). apply (proj2 (in_map_iff (LamEToFV(A:=A) o j A) (LamEToFV (j _ ee)) (LamEToFV (j A a)))). exists a. split. reflexivity. assumption. Qed. (** now the interpretation for canonical terms *) Lemma occECan_var: forall(A:k0)(a:A), a occE (varE a). Proof. intros. unfold varE, LamEMMItDef.InCan. apply occE_var. Qed. Lemma occECan_appl: forall(A:k0)(a:A)(t1 t2:LamE A), a occE t1 -> a occE (appE t1 t2). Proof. intros. unfold appE, LamEMMItDef.InCan. apply occE_appl. assumption. Qed. Lemma occECan_appr: forall(A:k0)(a:A)(t1 t2:LamE A), a occE t2 -> a occE (appE t1 t2). Proof. intros. unfold appE, LamEMMItDef.InCan. apply occE_appr. assumption. Qed. Lemma occECan_abs: forall(A:k0)(a:A)(r:LamE(option A)), (Some a) occE r -> a occE (absE r). Proof. intros. unfold absE, LamEMMItDef.InCan. apply occE_abs. assumption. Qed. Lemma occECan_flat: forall(A:k0)(a:A)(t:LamE A)(ee:LamE(LamE A)), a occE t -> t occE ee -> a occE (flatE ee). Proof. intros. unfold flatE, LamEMMItDef.InCan. (* Check (occE_flat LamEMMItDef.mapmu2EFct (j:= fun _ x => x) (fun _ _ _ _ => refl_equal _) t ee H0 a H). *) apply (occE_flat LamEMMItDef.mapmu2EFct (j:= fun _ x => x) (fun _ _ _ _ => refl_equal _) t ee H0 a H). Qed. (* this is now easy from the direct definition of occE: *) Lemma occE_var_inv (A:k0)(a b:A): a occE (varE b) -> a = b. Proof. intros. unfold occursFreeInE, varE, LamEToFV in H. rewrite LamEMMItDef.MItRedCan in H. simpl in H. destruct H. apply sym_eq. assumption. inversion H. Qed. (* these other lemmas were needed with the former approach: *) Lemma occE_app_inv (A:k0)(a:A)(t1 t2:LamE A): a occE (appE t1 t2) -> (a occE t1) \/ (a occE t2). Proof. intros. unfold occursFreeInE, appE, LamEToFV in H. rewrite LamEMMItDef.MItRedCan in H. fold LamEToFV in H. destruct (in_app_or (LamEToFV t1) (LamEToFV t2) _ H). left. assumption. right. assumption. Qed. Lemma filterSomeIn' (A:Set)(a:A)(l:list(option A)): In a (filterSome l) -> In (Some a) l. Proof. intros. induction l. inversion H. destruct a0. simpl in H. destruct H. rewrite H. simpl. left. reflexivity. simpl. right. apply IHl. assumption. simpl. right. apply IHl. simpl in H. assumption. Qed. Lemma occE_abs_inv (A:k0)(a:A)(r:LamE (option A)): a occE (absE r) -> Some a occE r. Proof. intros. unfold occursFreeInE, absE, LamEToFV in H. rewrite LamEMMItDef.MItRedCan in H. fold LamEToFV in H. unfold occursFreeInE. apply filterSomeIn'. assumption. Qed. Lemma in_flatten_reverse: forall(A:k0)(a:A)(l:list(list A)), In a (flatten l) -> exists aa:list A, In a aa /\ In aa l. Proof. intros. unfold flatten in H. elim (proj1 (in_flat_map(A:=list A) (id (A:=list A)) l a) H). intro aa. intros. destruct H0. exists aa. split; assumption. Qed. Lemma occE_flat_inv (A:k0)(a:A)(ee:LamE (LamE A)): a occE (flatE ee) -> exists t:LamE A, (a occE t) /\ (t occE ee). Proof. intros. unfold occursFreeInE, flatE, LamEToFV in H. rewrite LamEMMItDef.MItRedCan in H. fold LamEToFV in H. destruct (in_flatten_reverse _ _ H). destruct H0. elim (proj1 (in_map_iff _ _ _) H1). intros t H2. destruct H2. exists t. split. rewrite <- H2 in H0. assumption. assumption. Qed. (* end of digression *) (** behaviour of lamE on canonical elements *) Lemma lamE_var (A B:k0)(f:A->B)(a:A) : lamE f (varE a) = varE (f a). Proof. intros. unfold lamE at 1, varE at 1; rewrite LamEMMItDef.mapmu2RedCan. reflexivity. Qed. Lemma lamE_app (A B:k0)(f:A->B)(t1 t2:LamE A): lamE f (appE t1 t2) = appE (lamE f t1)(lamE f t2). Proof. intros. unfold lamE at 1, appE at 1; rewrite LamEMMItDef.mapmu2RedCan. reflexivity. Qed. Lemma lamE_abs (A B:k0)(f:A->B)(r:LamE (option A)): lamE f (absE r) = absE (lamE (option_map f) r). Proof. intros. unfold lamE at 1, absE at 1; rewrite LamEMMItDef.mapmu2RedCan. reflexivity. Qed. Lemma lamE_flat (A B:k0)(f:A->B)(ee:LamE (LamE A)): lamE f (flatE ee) = flatE (lamE (fun t => lamE (fun x => f x) t) ee). Proof. intros. unfold lamE at 1, flatE at 1. rewrite LamEMMItDef.mapmu2RedCan. simpl. reflexivity. Qed. (** a more perspicuous version that is not included in convertibility of LNMIt: *) Lemma lamE_flat' (A B:k0)(f:A->B)(ee:LamE (LamE A)): lamE f (flatE ee) = flatE (lamE (lamE f) ee). Proof. intros. rewrite lamE_flat. simpl. (* the following command is not accepted: apply (f_equal (fun (x:LamE(LamE A)) => flatE x)). *) replace (lamE (fun t : LamE A => lamE (fun x : A => f x) t) ee) with (lamE (lamE f) ee). reflexivity. apply lamEext. intro. apply lamEext. reflexivity. Qed. (** some preparation *) Definition optionk1 (A:k0) : k0 := option A. Lemma filterSomeNAT: NAT (Y:=listk1) filterSome (moncomp(X:=listk1)(Y:=optionk1) map option_map) map. Proof. red. intros. induction t. reflexivity. destruct a. simpl. rewrite <- IHt. reflexivity. simpl. rewrite <- IHt. reflexivity. Qed. Lemma LamEToFVNAT: NAT LamEToFV lamE map. Proof. unfold LamEToFV. apply LamEMMItDef.MItNAT. red. intros. destruct t as [[[a|(t1,t2)]|r]|ee]; induction ef. (* var *) reflexivity. (* app *) simpl. rewrite map_app. do 2 rewrite H. reflexivity. (* abs *) simpl. unfold moncomp. rewrite H. rewrite <- filterSomeNAT. reflexivity. (* flat *) simpl. unfold moncomp at 1. rewrite H. rewrite <- mapflatten. apply (f_equal (fun x=> flatten(A:=B) x)). do 2 rewrite map_map. apply map_ext. clear ee; intro a. unfold moncomp. rewrite H. reflexivity. Qed. (** how renaming works on the lst of free variables: *) Corollary LamEToFV_ok (A B: k0)(f:A->B)(t:LamE A): LamEToFV(lamE f t) = map f (LamEToFV t). Proof. intros. apply LamEToFVNAT. Qed. (** towards substitution *) Definition liftE (A B:k0)(f:A -> LamE B)(x:option A): LamE(option B) := match x with | None => varE None | Some a => lamE (Some(A:=B)) (f a) end. Lemma liftE_map (A B C:k0)(a:option A)(f:A-> LamE B)(g:B->C): (lamE (option_map g) o liftE f) a = liftE (lamE g o f) a. Proof. intros. destruct a. unfold comp. simpl. do 2 rewrite <- lamEfct2. apply lamEext. reflexivity. unfold comp. simpl. rewrite lamE_var. reflexivity. Qed. Definition substE (A B:k0)(f:A -> LamE B)(t:LamE A) :LamE B. Proof. refine (LamEBase.GMIt (H:=LamE)(G:=LamE)(fun (X:k1)(it: X <_{LamE} LamE) (A B:k0)(f:A -> LamE B)(t:LamEF X A)=> _)). destruct t as [[[a|(t1,t2)]|r]|ee]. exact (f a). exact (appE (it _ _ f t1)(it _ _ f t2)). exact (absE (it _ _ (liftE f) r)). exact (flatE (it (X A) (LamE B) (varE(A:=LamE B) o (it A B f)) ee)). (* not: exact (flatE (it (X A) (LamE B) (it A (LamE B) (varE(A:=LamE B) o f)) ee)). *) Defined. (* the following definition is just by inspection of the defined substE *) Definition s_substE := fun (X : k1) (it : X <_{ LamE}LamE) (A B : k0) (f : A -> LamE B) (t : LamEF X A) => match t with | inl (inl (inl a)) => f a | inl (inl (inr (pair t1 t2))) => appE (it A B f t1) (it A B f t2) | inl (inr r) => absE (it (option A) (option B) (liftE f) r) | inr ee => flatE (it (X A) (LamE B) (varE (A:=LamE B) o it A B f) ee) end. Lemma s_substE_ok (A B:k0)(f:A -> LamE B)(t:LamE A): LamEBase.GMIt s_substE B f t = substE f t. Proof. reflexivity. Qed. Lemma substE_var (A B:k0)(f: A -> LamE B)(a:A): substE f (varE a) = f a. Proof. intros. change substE with (LamEBase.GMIt s_substE). unfold varE. rewrite LamEM.GMItRedCan. reflexivity. Qed. Lemma substEMonad1 (A B:k0)(f:A -> LamE B)(a:A): substE f (varE a) = f a. Proof. exact substE_var. Qed. Lemma substE_app (A B:k0)(f: A -> LamE B)(t1 t2:LamE A): substE f (appE t1 t2) = appE (substE f t1)(substE f t2). Proof. intros. change substE with (LamEBase.GMIt s_substE). unfold appE at 1. rewrite LamEM.GMItRedCan. reflexivity. Qed. Lemma substE_abs (A B:k0)(f: A -> LamE B)(r:LamE (option A)): substE f (absE r) = absE (substE (liftE f) r). Proof. intros. change substE with (LamEBase.GMIt s_substE). unfold absE at 1. rewrite LamEM.GMItRedCan. reflexivity. Qed. Lemma substE_flat (A B:k0)(f: A -> LamE B)(ee:LamE(LamE A)): substE f (flatE ee) = flatE (substE (varE(A:=LamE B) o (substE f)) ee). Proof. intros. change substE with (LamEBase.GMIt s_substE). unfold flatE at 1. rewrite LamEM.GMItRedCan. reflexivity. Qed. (* we would have liked to see substE f (flatE ee) = flatE (lamE (substE f) ee), but this would need a full second monad law *) (** show that the definition of substE qualifies for Lemma 3 in the paper *) Lemma substEpGext: forall (X : k1) (h : X <_{LamE} LamE), gext h -> gext (s_substE h). Proof. red. intros. destruct r as [[[a|(t1,t2)]|r]|ee]. simpl. apply H0. simpl. do 2 rewrite (H A B f g H0). reflexivity. simpl. rewrite (H (option A) (option B) (liftE f) (liftE g)). reflexivity. destruct a. simpl. rewrite H0. reflexivity. reflexivity. (* flat *) simpl. apply (f_equal (fun x => flatE(A:=B) x)). apply H. clear ee. intro. unfold comp. apply (f_equal (fun x=> varE(A:=LamE B) x)). apply H. assumption. Qed. (** the first item in the list in the paper *) Lemma substEext (A B:k0)(f g:A -> LamE B)(t:LamE A): (forall a, f a = g a) -> substE f t = substE g t. Proof. intros. change (substE f t) with (LamEBase.GMIt s_substE B f t). rewrite (LamEM.GMItsExt s_substE substEpGext B f g H t). reflexivity. Qed. (** the second item in the list in the paper *) Lemma substEext' (A B:k0)(f g:A -> LamE B)(t:LamE A): (forall a, a occE t -> f a = g a) -> substE f t = substE g t. Proof. intros. generalize B f g H; clear B f g H. generalize A t; clear A t. apply (LamEBase.mu2Ind (fun A t => forall (B : k0) (f g : A -> LamE B), (forall a : A, (a occE t) -> f a = g a) -> substE f t = substE g t)). intros. destruct t as [[[a|(t1,t2)]|r]|ee]; change substE with (LamEBase.GMIt s_substE); do 2 rewrite LamEBase.GMItRed; simpl. (* var *) apply H0. exact (occE_var ef n a). (* app *) apply appE_cong; change (LamEBase.GMIt s_substE) with substE. unfold comp. apply H. intros. apply H0. apply (occE_appl ef n a). assumption. unfold comp. apply H. intros. apply H0. apply (occE_appr ef n a). assumption. (* abs *) apply (f_equal (fun x => absE(A:=B) x)). change (LamEBase.GMIt s_substE) with substE. unfold comp. apply H. intros. destruct a. simpl. rewrite H0. reflexivity. generalize H1. apply (occE_abs ef n a). reflexivity. (* flat *) apply (f_equal (fun x => flatE(A:=B) x)). change (LamEBase.GMIt s_substE) with substE. unfold comp at 1 4. apply H. intros. unfold comp. apply (f_equal (fun x => varE(A:=LamE B) x)). apply H. intros. apply H0. apply (occE_flat ef n a); assumption. Qed. (** the third item in the list in the paper *) Lemma substEGnat1: forall (A B C : Set) (f : A -> LamE B) (g : B -> C) (t : LamE A), lamE g (substE f t) = substE (lamE g o f) t. Proof. apply (LamEM.GMItsNat1 s_substE substEpGext). red. intros. destruct x as [[[a|(t1,t2)]|r]|ee]. simpl. reflexivity. simpl s_substE. rewrite lamE_app. do 2 rewrite H0. reflexivity. simpl s_substE. rewrite lamE_abs. rewrite H0. apply (f_equal (fun x => absE(A:=C) x)). apply H. intro. apply liftE_map. (* flat *) simpl s_substE. rewrite lamE_flat'. apply (f_equal (fun x => flatE(A:=C) x)). rewrite H0. apply H. clear ee. intro. unfold comp at 1 2 3. rewrite lamE_var. apply (f_equal (fun x=> varE(A:=LamE C) x)). rewrite H0. reflexivity. Qed. (** the fourth item in the list in the paper *) Lemma substEGnat2 (A B C:k0)(f: A -> B)(g:B -> LamE C)(t: LamE A): substE g (lamE f t) = substE (g o f) t. Proof. apply (LamEM.GMItsNat2 s_substE substEpGext). red. intros. destruct ef as [m0 e0 f01 f02]. destruct x as [[[a|(t1,t2)]|r]|ee]. simpl. reflexivity. simpl. do 2 rewrite H0. reflexivity. simpl. unfold moncomp. rewrite H0. apply (f_equal (fun x => absE(A:=C) x)). apply H. intro. destruct a; reflexivity. (* flat *) simpl. apply (f_equal (fun x => flatE(A:=C) x)). unfold moncomp at 1. rewrite H0. apply H. clear ee. intro. unfold comp at 1 2 3. apply (f_equal (fun x=> varE(A:=LamE C) x)). unfold moncomp. rewrite H0. apply H. clear a. intro. reflexivity. Qed. (** just an instance *) Lemma substELaw (A B:k0)(f: A -> LamE B)(t: LamE A): substE (id(A:=LamE B)) (lamE f t) = substE f t. Proof. intros. rewrite substEGnat2. apply substEext. reflexivity. Qed. (** a more elaborate formulation of naturality *) Lemma substENAT (X:k1)(mX: mon X)(h:X c_k1 LamE)(n: NAT h mX lamE): NAT (fun A => substE (h A)) (moncomp lamE mX) lamE. Proof. intros. unfold moncomp. red. intros. rewrite substEGnat2. rewrite substEGnat1. apply substEext. intro. unfold comp. apply n. Qed. Corollary substENATCor (X:k1)(mX: mon X)(h:X c_k1 LamE)(n: NAT h mX lamE) (A B : Set) (f : A -> B)(t : LamE (X A)): substE (h B) (lamE (mX A B f) t) = lamE f (substE (h A) t). Proof. intros. rewrite <- (substENAT n). reflexivity. Qed. (** the fifth item in the list in the paper *) Lemma substEMonad3 (A B C:k0)(f: A -> LamE B)(g: B -> LamE C)(t:LamE A): substE g (substE f t) = substE ((substE g) o f) t. Proof. intros. generalize B C f g; clear B C f g. generalize A t; clear A t. apply (LamEBase.mu2Ind (fun A t => forall (B C : k0) (f : A -> LamE B) (g : B -> LamE C), substE g (substE f t) = substE (substE g o f) t)). intros. destruct t as [[[a|(t1,t2)]|r]|ee]; change substE with (LamEBase.GMIt s_substE); repeat rewrite LamEBase.GMItRed; simpl. (* var *) reflexivity. unfold appE. rewrite LamEM.GMItRedCan. simpl. change (LamEBase.GMIt s_substE) with substE. unfold comp at 1 2. do 2 rewrite H. reflexivity. unfold absE. rewrite LamEM.GMItRedCan. simpl. change (LamEBase.GMIt s_substE) with substE. unfold comp at 1. rewrite H. unfold absE. apply (f_equal (fun x => LamEMMItDef.InCan (inl (LamEBase.mu2 (LamEBase.mu2 C))(inr (C + LamEBase.mu2 C * LamEBase.mu2 C)x)))). unfold comp. apply substEext. clear X ef j n H r. intro. destruct a. simpl. rewrite substEGnat1. rewrite substEGnat2. reflexivity. simpl. rewrite substEMonad1. reflexivity. (* flat *) unfold flatE at 1. rewrite LamEM.GMItRedCan. simpl. apply (f_equal (fun x => flatE(A:=C) x)). unfold comp at 2 5. change (LamEBase.GMIt s_substE) with substE. rewrite H. apply substEext. clear ee. intro. unfold comp. rewrite substEMonad1. apply (f_equal (fun x => varE(A:=LamE C) x)). rewrite H. (* this is an application of H deep inside the proof *) reflexivity. Qed. (** preparations for the formula for the list of free variables of substE f t *) Lemma filterSomeAppend (A:k0)(l1 l2:list(option A)): filterSome (l1++l2) = filterSome l1 ++ filterSome l2. Proof. intros. induction l1. reflexivity. destruct a. simpl. rewrite IHl1. reflexivity. simpl. assumption. Qed. Lemma filterSomeMapSome (A:k0)(l:list A): filterSome (map (Some(A:=A)) l) = l. Proof. intros. induction l. reflexivity. simpl. rewrite IHl. reflexivity. Qed. Lemma filterSomeLamEToFV (A:k0)(t:LamE A): filterSome (LamEToFV (lamE (Some(A:=A)) t)) = LamEToFV t. Proof. intros. rewrite LamEToFV_ok. apply filterSomeMapSome. Qed. (** this needed naturality of LamEToFV *) Lemma aux_abs (A B:k0)(f:A -> LamE B)(t:list(option A)): filterSome(flatten(map(LamEToFV(A:=option B) o liftE f) t)) = flatten (map (LamEToFV(A:=B) o f)(filterSome t)). Proof. intros. rewrite <- filterSomeNAT. unfold moncomp. induction t. reflexivity. destruct a. simpl. unfold comp at 1. unfold liftE at 1. change (listk1 B) with (list B). rewrite flattenCons. change (listk1 (option B)) with (list (option B)). rewrite flattenCons. change (list B) with (listk1 B). rewrite <- IHt. simpl. rewrite filterSomeAppend. rewrite filterSomeLamEToFV. reflexivity. simpl. change (listk1 (option B)) with (list (option B)). rewrite flattenCons. rewrite <- IHt. unfold comp at 1. simpl. unfold LamEToFV at 1. unfold varE. rewrite LamEMMItDef.MItRedCan. rewrite filterSomeAppend. simpl. reflexivity. Qed. (** this needed naturality of LamEToFV through filterSomeLamEToFV *) Lemma flattenMapSingleton (A B:k0)(f:A->B)(l:list A): flatten (map (fun x => f x::nil) l) = map f l. Proof. intros. induction l. reflexivity. simpl. rewrite flattenCons. rewrite IHl. reflexivity. Qed. Lemma flattenMapFlatten (A B:k0)(f:A->list(list B))(l:list A): flatten (map (flatten(A:=B) o f) l) = flatten (flatten (map f l)). Proof. intros. induction l. reflexivity. simpl. do 2 rewrite flattenCons. rewrite flattenAppend. rewrite IHl. reflexivity. Qed. (** the last item in the list in the paper *) Lemma LamEToFVsubstE (A B:k0)(f: A -> LamE B)(t: LamE A): LamEToFV (substE f t) = flatten (map (LamEToFV(A:=B) o f) (LamEToFV t)). Proof. intros. generalize B f; clear B f. generalize A t; clear A t. apply (LamEBase.mu2Ind (fun A t => forall (B : k0) (f : A -> LamE B), LamEToFV (substE f t) = flatten (map (LamEToFV(A:=B) o f) (LamEToFV t)))). intros. destruct t as [[[a|(t1,t2)]|r]|ee]; change substE with (LamEBase.GMIt s_substE); rewrite LamEBase.GMItRed; simpl; unfold LamEToFV at 3; rewrite LamEBase.MItRed; simpl. (* var *) change (listk1 B) with (list B). rewrite flattenSingleton. reflexivity. (* app *) unfold LamEToFV at 1. unfold appE. rewrite LamEMMItDef.MItRedCan. rewrite map_app. change (listk1 B) with (list B). rewrite flattenAppend. change LamEBase.LNM.MIt with LamEBase.MIt. change (LamEBase.MIt (fun (X0 : k1) (it : X0 c_k1 listk1) (A0 : Set) (t : LamEF X0 A0) => match t with | inl (inl (inl a)) => a :: nil | inl (inl (inr (pair t3 t4))) => it A0 t3 ++ it A0 t4 | inl (inr r) => filterSome (it (option A0) r) | inr e => flatten (map (it A0) (it (X0 A0) e)) end)) with LamEToFV. unfold comp at 4 6. change (list B) with (listk1 B). rewrite <- (H A t1 B f). rewrite <- (H A t2 B f). reflexivity. (* abs *) unfold LamEToFV at 1. unfold absE. rewrite LamEMMItDef.MItRedCan. change LamEBase.LNM.MIt with LamEBase.MIt. change (LamEBase.MIt (fun (X0 : k1) (it : X0 c_k1 listk1) (A0 : Set) (t : LamEF X0 A0) => match t with | inl (inl (inl a)) => a :: nil | inl (inl (inr (pair t3 t4))) => it A0 t3 ++ it A0 t4 | inl (inr r) => filterSome (it (option A0) r) | inr e => flatten (map (it A0) (it (X0 A0) e)) end)) with LamEToFV. unfold comp at 3. change (LamEBase.GMIt s_substE) with substE. unfold comp at 1. rewrite H. rewrite aux_abs. (** here enters naturality of LamEToFV *) reflexivity. (* flat *) unfold LamEToFV at 1. unfold flatE. rewrite LamEMMItDef.MItRedCan. change LamEBase.LNM.MIt with LamEBase.MIt. change (LamEBase.MIt (fun (X0 : k1) (it : X0 c_k1 listk1) (A0 : Set) (t : LamEF X0 A0) => match t with | inl (inl (inl a)) => a :: nil | inl (inl (inr (pair t3 t4))) => it A0 t3 ++ it A0 t4 | inl (inr r) => filterSome (it (option A0) r) | inr e => flatten (map (it A0) (it (X0 A0) e)) end)) with LamEToFV. change (LamEBase.GMIt s_substE) with substE. unfold comp at 1. rewrite H. rewrite <- mapflatten. rewrite map_map. replace (@map (X A) (list (listk1 B)) (fun x : X A => @map (LamE B) (listk1 B) (@LamEToFV B) (@comp (X A) (LamE (LamE B)) (listk1 (LamE B)) (@LamEToFV (LamE B)) (@comp (X A) (LamE B) (LamE (LamE B)) (@varE (LamE B)) (@comp (X A) (LamEBase.mu2 A) (LamE B) (@substE A B f) (j A))) x)) (@LamEToFV (X A) (j (X A) ee))) with (map (fun x : X A => LamEToFV(substE f (j A x)) :: nil) (LamEToFV (j (X A) ee))). Focus 2. apply map_ext. intro. unfold comp. unfold LamEToFV at 3. unfold varE. rewrite LamEMMItDef.MItRedCan. reflexivity. (* back *) rewrite flattenMapSingleton. replace (@map (X A) (listk1 B) (fun x : X A => @LamEToFV B (@substE A B f (j A x))) (@LamEToFV (X A) (j (X A) ee))) with (map (fun x : X A => flatten (map (LamEToFV(A:=B) o f) (LamEToFV (j A x)))) (LamEToFV (j (X A) ee))). Focus 2. apply map_ext. intro. rewrite <- H. reflexivity. (* back *) rewrite <- mapflatten. rewrite map_map. unfold comp at 3. change (listk1 B) with (list B). rewrite <- flattenMapFlatten. unfold comp. reflexivity. Qed. Lemma substE_occ (A B:k0)(f: A -> LamE B)(t: LamE A)(b:B): b occE (substE f t) -> exists a:A, (a occE t) /\ (b occE f a). Proof. unfold occursFreeInE. intros. rewrite LamEToFVsubstE in H. destruct (in_flatten_reverse _ _ H). destruct H0. elim (proj1 (in_map_iff _ _ _) H1). intro a. intro. destruct H2. exists a. split. assumption. unfold comp in H2. rewrite H2. assumption. Qed. (** hereditarily canonical elements *) (** Definition 3 in the paper *) Inductive canE : forall (A:Set), LamE A -> Prop := | canE_var : forall(A:Set)(a:A), canE (varE a) | canE_app : forall(A:Set)(t1 t2:LamE A), canE t1 -> canE t2 -> canE(appE t1 t2) | canE_abs : forall(A:Set)(r:LamE(option A)), canE r -> canE (absE r) | canE_flat: forall(A:Set)(ee:LamE(LamE A)), canE ee -> (forall t:LamE A, t occE ee -> canE t) -> canE (flatE ee). (** we are only able to prove a weakened version of the second monad law *) Lemma substEMonad2 (A:k0)(t:LamE A): canE t -> substE (varE(A:=A)) t = t. Proof. intros A t H. induction H. rewrite substEMonad1. reflexivity. (* app *) rewrite substE_app. rewrite IHcanE1. rewrite IHcanE2. reflexivity. (* abs *) rewrite substE_abs. replace (substE (liftE (varE (A:=A))) r) with (substE (varE (A:= option A)) r). Focus 2. apply substEext. intro. destruct a. simpl. rewrite lamE_var. reflexivity. reflexivity. (* back *) rewrite IHcanE. reflexivity. (* flat *) rewrite substE_flat. apply (f_equal (fun x => flatE(A:=A) x)). transitivity (substE (varE (A:=LamE A)) ee). apply substEext'. intros t Hyp. unfold comp. apply (f_equal (fun x => varE(A:=LamE A) x)). apply H1. assumption. assumption. Qed. (* now the lemma that needed so much inversion properties with the inductive definition of occE *) Lemma lamE_occ (A B:k0)(f: A -> B)(t: LamE A)(b:B): b occE (lamE f t) -> exists a:A, (a occE t) /\ (b = f a). Proof. unfold occursFreeInE. intros. rewrite LamEToFV_ok in H. assert (exists a:A, f a =b /\ In a (LamEToFV t)). exact (proj1 (in_map_iff _ _ _) H). destruct H0. destruct H0. exists x. split. assumption. rewrite H0. reflexivity. Qed. Lemma lamE_can (A B:k0)(f: A -> B)(t: LamE A): canE t -> canE (lamE f t). Proof. intros. generalize B f; clear B f. induction H; intros. rewrite lamE_var. apply canE_var. rewrite lamE_app. apply canE_app. apply IHcanE1. apply IHcanE2. rewrite lamE_abs. apply canE_abs. apply IHcanE. (* flat *) rewrite lamE_flat. apply canE_flat. apply IHcanE. intros. (* Check (lamE_occ (fun t : LamE A => lamE (fun x : A => f x) t) ee t H2). *) destruct (lamE_occ _ _ t H2). destruct H3. rewrite H4. apply H1. assumption. Qed. Lemma substE_can (A B:k0)(f: A -> LamE B)(t: LamE A): (forall a:A, a occE t -> canE (f a)) -> canE t -> canE (substE f t). Proof. intros. generalize B f H; clear B f H. induction H0; intros. rewrite substE_var. apply H. apply occECan_var. rewrite substE_app. apply canE_app. apply IHcanE1. intros. apply H. apply occECan_appl. assumption. apply IHcanE2. intros. apply H. apply occECan_appr. assumption. rewrite substE_abs. apply canE_abs. apply IHcanE. intros. destruct a. simpl. apply lamE_can. apply H. apply occECan_abs. assumption. simpl. apply canE_var. (* flat *) rewrite substE_flat. apply canE_flat. apply IHcanE. intros. unfold comp. apply canE_var. intros. (* Check (substE_occ _ ee _ H3). *) destruct (substE_occ _ ee _ H3). destruct H4. unfold comp in H5. (* Check (occE_var_inv t _ H5). *) rewrite (occE_var_inv t _ H5). apply H1. assumption. intros. apply H2. (* Check (occECan_flat a x _ H6 H4). *) exact (occECan_flat a x _ H6 H4). Qed. Lemma lamE_is_substE (A B:k0)(f: A -> B)(t: LamE A): canE t -> lamE f t = substE (varE(A:=B) o f) t. Proof. intros. rewrite <- substEGnat2. apply sym_eq. apply substEMonad2. apply lamE_can. assumption. Qed. (** finally, we obtain the desired rewrite rule for substE in the case flatE, but only for standard elements *) Lemma substE_flat' (A B:k0)(f: A -> LamE B)(ee:LamE(LamE A)): canE ee -> substE f (flatE ee) = flatE (lamE (substE f) ee). Proof. intros. rewrite substE_flat. apply (f_equal (fun x => flatE(A:=B) x)). apply sym_eq. apply lamE_is_substE. assumption. Qed. (** We now cast this purely in terms of hereditarily canonical elements. *) Definition LamEC (A:k0) : k0 := {t:LamE A| canE t}. Definition varEC (A:k0)(a:A) : LamEC A. Proof. intros. red. exists (varE a). apply canE_var. Defined. Definition appEC (A:k0)(t1 t2:LamEC A): LamEC A. Proof. intros. destruct t1 as (t1',p1). destruct t2 as (t2',p2). exists (appE t1' t2'). apply canE_app; assumption. Defined. Definition absEC (A:k0)(r: LamEC (option A)): LamEC A. Proof. intros. destruct r as (r,p). exists (absE r). apply canE_abs; assumption. Defined. Definition pi1: LamEC c_k1 LamE. Proof. red. intros. exact (proj1_sig H). Defined. Definition flatEC (A:k0)(ee:LamEC(LamEC A)): LamEC A. Proof. intros. red. exists (flatE (lamE (pi1(A:=A)) (pi1 ee))). destruct ee as (ee',p). apply canE_flat. apply lamE_can. assumption. intros. destruct (lamE_occ _ _ _ H). destruct x as (t',p'). simpl in H0. destruct H0. rewrite H1. assumption. Defined. (** unfortunately, this definition has to do something on terms, namely renaming using pi1 *) Definition lamEC: mon LamEC. Proof. red. red. red. intros A B f t. destruct t as (t',p). exists (lamE f t'). apply lamE_can. assumption. Defined. Definition substEC(A B:k0)(f:A -> LamEC B)(t:LamEC A): LamEC B. Proof. intros. red. destruct t as (t',p). exists (substE (fun a => pi1 (f a)) t'). apply substE_can. intros a _. unfold pi1. apply proj2_sig. assumption. Defined. Definition LamECToFV : LamEC c_k1 listk1. Proof. red. intros A t. apply LamEToFV. exact (pi1 t). Defined. Definition occursFreeInEC(A:k0)(a:A)(t:LamEC A): Prop := In a (LamECToFV t). Infix "occEC" := occursFreeInEC (at level 90). Lemma occEC_var: forall(A:k0)(a:A), a occEC (varEC a). Proof. intros. unfold varEC, occursFreeInEC, LamECToFV. simpl. apply occECan_var. Qed. Lemma occEC_appl: forall(A:k0)(a:A)(t1 t2:LamEC A), a occEC t1 -> a occEC (appEC t1 t2). Proof. intros. unfold appEC, occursFreeInEC, LamECToFV. destruct t1 as [t1' p1]. destruct t2 as [t2' p2]. simpl. apply occECan_appl. assumption. Qed. Lemma occEC_appr: forall(A:k0)(a:A)(t1 t2:LamEC A), a occEC t2 -> a occEC (appEC t1 t2). Proof. intros. unfold appEC, occursFreeInEC, LamECToFV. destruct t1 as [t1' p1]. destruct t2 as [t2' p2]. simpl. apply occECan_appr. assumption. Qed. Lemma occEC_abs: forall(A:k0)(a:A)(r:LamEC(option A)), (Some a) occEC r -> a occEC (absEC r). Proof. intros. unfold absEC, occursFreeInEC, LamECToFV. destruct r as [r' p]. simpl. apply occECan_abs. assumption. Qed. Lemma occEC_flat: forall(A:k0)(a:A)(t:LamEC A)(ee:LamEC(LamEC A)), a occEC t -> t occEC ee -> a occEC (flatEC ee). Proof. intros. unfold flatEC, occursFreeInEC, LamECToFV. destruct ee as (ee',p). destruct t as (t',p'). simpl. unfold occursFreeInEC, LamECToFV in H. simpl in H. unfold occursFreeInEC, LamECToFV in H0. simpl in H0. apply (occECan_flat a t' (lamE (pi1(A:=A)) ee')). assumption. unfold occursFreeInE. rewrite LamEToFVNAT. change t' with (pi1(exist (fun t : LamE A => canE t) t' p')). apply in_map. assumption. Qed. Lemma occEC_var_inv (A:k0)(a b:A): a occEC (varEC b) -> a = b. Proof. intros. unfold occursFreeInEC, varEC, LamECToFV in H. simpl in H. apply (occE_var_inv _ _ H). Qed. Lemma occEC_app_inv (A:k0)(a:A)(t1 t2:LamEC A): a occEC (appEC t1 t2) -> (a occEC t1) \/ (a occEC t2). Proof. intros. unfold occursFreeInEC, appEC, LamECToFV in H. destruct t1 as [t1' p1]. destruct t2 as [t2' p2]. simpl in H. destruct (occE_app_inv _ _ _ H). left. unfold occursFreeInEC, LamECToFV. simpl. assumption. right. unfold occursFreeInEC, LamECToFV. simpl. assumption. Qed. Lemma occEC_abs_inv (A:k0)(a:A)(r:LamEC (option A)): a occEC (absEC r) -> Some a occEC r. Proof. intros. unfold occursFreeInEC, appEC, LamECToFV in H. destruct r as [r' p]. simpl in H. unfold occursFreeInEC, LamECToFV. simpl. apply occE_abs_inv. assumption. Qed. Lemma occEC_flat_inv (A:k0)(a:A)(ee:LamEC (LamEC A)): a occEC (flatEC ee) -> exists t:LamEC A, (a occEC t) /\ (t occEC ee). Proof. intros. unfold occursFreeInEC, appEC, LamECToFV in H. destruct ee as (ee',p). simpl in H. destruct (occE_flat_inv _ _ H) as (t,H0). destruct H0. unfold occursFreeInE in H1. rewrite LamEToFVNAT in H1. destruct (proj1 (in_map_iff _ _ _) H1). destruct H2. destruct x as (t',p'). simpl in H2. exists (exist (fun t1 : LamE A => canE t1) t' p'). split. unfold occursFreeInEC, LamECToFV. simpl. rewrite H2. assumption. unfold occursFreeInEC, LamECToFV. simpl. assumption. Qed. Lemma LamECToFVNAT: NAT LamECToFV lamEC map. Proof. red. intros. unfold LamECToFV. destruct t as (t',p). simpl. apply LamEToFVNAT. Qed. Corollary LamECToFV_ok (A B: k0)(f:A->B)(t:LamEC A): LamECToFV(lamEC f t) = map f (LamECToFV t). Proof. intros. apply LamECToFVNAT. Qed. Lemma lamEC_occ (A B:k0)(f: A -> B)(t: LamEC A)(b:B): b occEC (lamEC f t) -> exists a:A, (a occEC t) /\ (b = f a). Proof. unfold occursFreeInEC. intros. rewrite LamECToFV_ok in H. assert (exists a:A, f a =b /\ In a (LamECToFV t)). exact (proj1 (in_map_iff _ _ _) H). destruct H0. destruct H0. exists x. split. assumption. rewrite H0. reflexivity. Qed. (** item 6 for LamEC *) Lemma LamECToFVsubstEC (A B:k0)(f: A -> LamEC B)(t: LamEC A): LamECToFV (substEC f t) = flatten (map (LamECToFV(A:=B) o f) (LamECToFV t)). Proof. intros. unfold substEC, LamECToFV. destruct t as (t',p). simpl. rewrite LamEToFVsubstE. unfold comp. reflexivity. Qed. Lemma substEC_occ (A B:k0)(f: A -> LamEC B)(t: LamEC A)(b:B): b occEC (substEC f t) -> exists a:A, (a occEC t) /\ (b occEC f a). Proof. unfold occursFreeInEC. intros. rewrite LamECToFVsubstEC in H. destruct (in_flatten_reverse _ _ H). destruct H0. elim (proj1 (in_map_iff _ _ _) H1). intro a. intro. destruct H2. exists a. split. assumption. unfold comp in H2. rewrite H2. assumption. Qed. Definition proof_irrelevance := forall (P:Prop) (p1 p2:P), p1 = p2. (** this is the only axiom we need *) Axiom pirr : proof_irrelevance. (** the only consequence we use *) Lemma LamECpirr : forall (A:k0)(t1 t2:LamEC A), pi1 t1 = pi1 t2 -> t1 = t2. Proof. intros. destruct t1 as [t1' H1]. destruct t2 as [t2' H2]. simpl in H. generalize H1 H2; clear H1 H2. destruct H. intros. rewrite (pirr H1 H2). reflexivity. Qed. (** item 1 *) Lemma substECext (A B:k0)(f g:A -> LamEC B)(t:LamEC A): (forall a, f a = g a) -> substEC f t = substEC g t. Proof. intros. destruct t as (t',p'). apply LamECpirr. simpl. apply substEext. intro. rewrite H. reflexivity. Qed. (** item 2 *) Lemma substECext' (A B:k0)(f g:A -> LamEC B)(t:LamEC A): (forall a, a occEC t -> f a = g a) -> substEC f t = substEC g t. Proof. intros. destruct t as (t',p'). apply LamECpirr. simpl. apply substEext'. intros. rewrite H. reflexivity. unfold occursFreeInEC, LamECToFV. simpl. assumption. Qed. (** item 3 *) Lemma substECGnat1: forall (A B C : Set) (f : A -> LamEC B) (g : B -> C) (t : LamEC A), lamEC g (substEC f t) = substEC (lamEC g o f) t. Proof. intros. destruct t as (t',p'). apply LamECpirr. simpl. rewrite substEGnat1. apply substEext. intro. unfold comp. destruct (f a). simpl. reflexivity. Qed. (** item 4 *) Lemma substECGnat2 (A B C:k0)(f: A -> B)(g:B -> LamEC C)(t: LamEC A): substEC g (lamEC f t) = substEC (g o f) t. Proof. intros. destruct t as (t',p'). apply LamECpirr. simpl. rewrite substEGnat2. apply substEext. reflexivity. Qed. Lemma substECLaw (A B:k0)(f: A -> LamEC B)(t: LamEC A): substEC (id(A:=LamEC B)) (lamEC f t) = substEC f t. Proof. intros. rewrite substECGnat2. apply substECext. reflexivity. Qed. Lemma substECNAT (X:k1)(mX: mon X)(h:X c_k1 LamEC)(n: NAT h mX lamEC): NAT (fun A=> substEC (h A)) (moncomp lamEC mX) lamEC. Proof. intros. unfold moncomp. red. intros. rewrite substECGnat2. rewrite substECGnat1. apply substECext. intro. unfold comp. apply n. Qed. Corollary substECNATCor (X:k1)(mX: mon X)(h:X c_k1 LamEC)(n: NAT h mX lamEC) (A B : Set) (f : A -> B)(t : LamEC (X A)): substEC (h B) (lamEC (mX A B f) t) = lamEC f (substEC (h A) t). Proof. intros. rewrite <- (substECNAT n). reflexivity. Qed. (** item 5 *) Lemma substECMonad3: monad3 LamEC substEC. Proof. red. intros. apply LamECpirr. destruct t as (t',p). simpl. rewrite substEMonad3. apply substEext. intro. unfold comp. destruct (f a) as (b',p'). simpl. reflexivity. Qed. Lemma lamEC_var (A B:k0)(f:A->B)(a:A) : lamEC f (varEC a) = varEC (f a). Proof. intros. apply LamECpirr. simpl. apply lamE_var. Qed. Lemma lamEC_app (A B:k0)(f:A->B)(t1 t2:LamEC A): lamEC f (appEC t1 t2) = appEC (lamEC f t1)(lamEC f t2). Proof. intros. apply LamECpirr. destruct t1 as [t1' p1]. destruct t2 as [t2' p2]. simpl. apply lamE_app. Qed. Lemma lamEC_abs (A B:k0)(f:A->B)(r:LamEC (option A)): lamEC f (absEC r) = absEC (lamEC (option_map f) r). Proof. intros. apply LamECpirr. destruct r as [r' p]. simpl. apply lamE_abs. Qed. Lemma lamEC_flat (A B:k0)(f:A->B)(ee:LamEC (LamEC A)): lamEC f (flatEC ee) = flatEC (lamEC (fun t => lamEC (fun x => f x) t) ee). Proof. intros. apply LamECpirr. destruct ee as [ee' p]. simpl. rewrite lamE_flat. apply (f_equal (fun x => flatE(A:=B) x)). do 2 rewrite <- lamEfct2. apply lamEext. intro t. unfold comp. destruct t as (t',p'). reflexivity. Qed. (** the following proof works precisely the same way *) Lemma lamEC_flat' (A B:k0)(f:A->B)(ee:LamEC (LamEC A)): lamEC f (flatEC ee) = flatEC (lamEC (lamEC f) ee). Proof. intros. apply LamECpirr. destruct ee as [ee' p]. simpl. rewrite lamE_flat'. apply (f_equal (fun x => flatE(A:=B) x)). do 2 rewrite <- lamEfct2. apply lamEext. intro t. unfold comp. destruct t as (t',p'). reflexivity. Qed. Lemma lamECext: ext lamEC. Proof. red. intros. apply LamECpirr. destruct r as [r' p]. simpl. apply lamEext. assumption. Qed. Lemma lamECfct1: fct1 lamEC. Proof. red. intros. destruct x as (t,p). apply LamECpirr. simpl. apply lamEfct1. Qed. Lemma lamECfct2 : fct2 lamEC. Proof. red. intros. destruct x as (t,p). apply LamECpirr. simpl. apply lamEfct2. Qed. (** the lemmas that no longer need a relativization to hereditarily canonical elements: *) Lemma substECMonad2: monad2 LamEC varEC substEC. Proof. red. intros. apply LamECpirr. destruct t as (t',p). simpl. replace (substE (fun a : A => varE a) t') with (substE (varE(A:=A)) t'). apply substEMonad2. assumption. apply substEext. reflexivity. Qed. Lemma lamEC_is_substEC (A B:k0)(f: A -> B)(t: LamEC A): lamEC f t = substEC (varEC(A:=B) o f) t. Proof. intros. apply LamECpirr. destruct t as (t',p). simpl. change (substE (fun a : A => varE (f a))) with (substE (varE(A:=B) o f)). apply lamE_is_substE. assumption. Qed. Lemma substEC_flat' (A B:k0)(f: A -> LamEC B)(ee:LamEC(LamEC A)): substEC f (flatEC ee) = flatEC (lamEC (substEC f) ee). Proof. intros. apply LamECpirr. destruct ee as (ee',p). simpl. rewrite substE_flat'. do 2 rewrite <- lamEfct2. apply (f_equal (fun x => flatE(A:=B) x)). apply lamEext. intro t. unfold comp. destruct t as (t',p'). simpl. reflexivity. apply lamE_can. assumption. Qed. (** finally, the recursive description of substEC: *) Lemma substECMonad1: monad1 LamEC varEC substEC. Proof. red. intros. apply LamECpirr. simpl. rewrite substE_var. reflexivity. Qed. Lemma substEC_var (A B:k0)(f: A -> LamEC B)(a:A): substEC f (varEC a) = f a. Proof. intros. apply substECMonad1. Qed. Lemma substEC_app (A B:k0)(f: A -> LamEC B)(t1 t2:LamEC A): substEC f (appEC t1 t2) = appEC (substEC f t1)(substEC f t2). Proof. intros. apply LamECpirr. destruct t1 as [t1' p1]. destruct t2 as [t2' p2]. simpl. apply substE_app. Qed. Definition liftEC (A B:k0)(f:A -> LamEC B)(x:option A): LamEC(option B) := match x with | None => varEC None | Some a => lamEC (Some(A:=B)) (f a) end. Lemma substEC_abs (A B:k0)(f: A -> LamEC B)(r:LamEC (option A)): substEC f (absEC r) = absEC (substEC (liftEC f) r). Proof. intros. apply LamECpirr. destruct r as [r' p]. simpl. rewrite substE_abs. apply (f_equal (fun x => absE(A:=B) x)). apply substEext. intro. destruct a. simpl. destruct (f a). simpl. reflexivity. reflexivity. Qed. (** the following lemma is way more difficult than the abs case *) Lemma substEC_flat (A B:k0)(f: A -> LamEC B)(ee:LamEC(LamEC A)): substEC f (flatEC ee) = flatEC (substEC (varEC(A:=LamEC B) o (substEC f)) ee). Proof. intros. apply LamECpirr. destruct ee as [ee' p]. simpl. rewrite substE_flat. apply (f_equal (fun x => flatE(A:=B) x)). rewrite substEGnat1. rewrite substEGnat2. apply substEext. intro t. unfold comp. rewrite lamE_var. destruct t as (t',p'). simpl. reflexivity. Qed. End EFlat. (** evaluation as another example of the use of plain Mendler iteration *) Module Eval (LamBase:LAM)(LamEBase:LAME). Module LamM := LNGMItDef LamBase. (* Module LamMMItBase := LamBase.LNM. *) Module LamMMItDef := LamM.LNMItDef. Module Lam := Lam LamBase. Import Lam. Module LamEM := LNGMItDef LamEBase. Module LamEMMItDef := LamEM.LNMItDef. Module EFlat := EFlat LamEBase. Import EFlat. Definition eval (A:k0): LamE A -> Lam A. Proof. refine (LamEBase.MIt (fun (X:k1)(it: X c_k1 Lam)(A:k0)(t:LamEF X A)=> _)). destruct t as [[[a|(t1,t2)]|r]|ee]. exact (var a). exact (app (it _ t1)(it _ t2)). exact (abs (it _ r)). exact (subst (it A) (it (X A) ee)). Defined. (* the following definition is just by inspection of the defined eval *) Definition s_eval := fun (X : k1) (it : X c_k1 Lam) (A : k0) (t : LamEF X A) => match t with | inl (inl (inl a)) => var a | inl (inl (inr (pair t1 t2))) => app (it A t1) (it A t2) | inl (inr r) => abs (it (option A) r) | inr ee => subst (it A) (it (X A) ee) end. Lemma evalFlat (A:k0)(ee:LamE(LamE A)): eval (flatE ee) = subst (eval(A:=A)) (eval ee). Proof. intros. unfold eval at 1, flatE. rewrite LamEMMItDef.MItRedCan. reflexivity. Qed. Lemma evalNAT: NAT eval lamE lam. Proof. apply (LamEMMItDef.MItNAT(mG:=lam) s_eval). red. intros. destruct ef as [m0 e0 f01 f02]. simpl in H. destruct t as [[[a|(t1,t2)]|r]|ee]; simpl. rewrite lam_var. reflexivity. do 2 rewrite H. rewrite lam_app. reflexivity. unfold moncomp. rewrite H. rewrite lam_abs. reflexivity. unfold moncomp. rewrite H. rewrite <- (substNAT H f (it (X A) ee)). apply (f_equal (fun y => subst (it B) y)). unfold moncomp. apply lamext. intro. apply e0. reflexivity. Qed. Lemma evalNATcor (A:k0)(ee:LamE(LamE A)): eval (flatE ee) = subst (id(A:= Lam A)) (eval (lamE (eval(A:=A)) ee)). Proof. intros. rewrite evalFlat. rewrite evalNAT. rewrite substLaw. reflexivity. Qed. End Eval.