(** LamFlatPred.v Version 1.4 October 2018 *) (** does not need impredicative Set, tested with version 8.8.2 *) (** Copyright Ralph Matthes, I.R.I.T., C.N.R.S. & University of Toulouse*) (** forms part of the code that came with a paper in the journal Science of Computer Programming *) Require Import LNMItPred. Require Import LNGMItPred. Require Import List. Set Implicit Arguments. Require Import Utf8. Require Import Setoid. Require Import Morphisms. Open Scope type_scope. Definition LambF(X: k1)(A: Set) := A + X A * X A + X(option A). Instance lambFpEFct : pEFct LambF. Proof. unfold LambF. typeclasses eauto. Defined. (* Print lambFpEFct. lambFpEFct = @sumpEFct (λ (X : k1) (A : k0), A + X A * X A) (@sumpEFct (λ (_ : k1) (A : k0), A) (@constpEFct (λ A : k0, A) idEFct) (λ (X : k1) (A : k0), X A * X A) (@prodpEFct (λ (X : k1) (A : k0), X A) idpEFct_eta (λ (X : k1) (A : k0), X A) idpEFct_eta)) (λ (X : k1) (A : k0), X (option A)) (@comppEFct (λ X : k1, X) idpEFct (λ (_ : k1) (A : k0), option A) (@constpEFct (λ A : k0, option A) optionEFct)) : pEFct LambF Expanded type for implicit arguments lambFpEFct : ∀ X : k1, EFct X → EFct (LambF X) Argument X is implicit *) Definition LamF(X: k1)(A: Set) := LambF X A + X (X A). Instance lamFpEFct_auto : pEFct LamF. Proof. unfold LamF. typeclasses eauto. Defined. (* Print lamFpEFct_auto. lamFpEFct_auto = @sumpEFct LambF lambFpEFct (λ (X : k1) (A : k0), X (X A)) (@comppEFct (λ X : k1, X) idpEFct (λ (X : k1) (A : k0), X A) idpEFct_eta) : pEFct LamF Expanded type for implicit arguments lamFpEFct_auto : ∀ X : k1, EFct X → EFct (LamF X) Argument X is implicit *) (** The following lemmas loosely correspond to the definition of the term of type [forall (X:k1), mon X -> mon(LamF X)] at the end of Section 4.1. Note the use of [idpEFct] and [idpEFct_eta] in the recursive descriptions. *) Definition pvar (X: k1)(A: Set)(a: A): LamF X A := inl (X (X A)) (inl (X (option A)) (inl (X A * X A) a)). (* short: inl _ (inl _ (inl _ a)) *) Lemma pvar_m_auto (X: k1)(ef: EFct X)(A B: Set)(f: A -> B)(a: A): m (EFct:= lamFpEFct_auto ef) f (pvar X a) = pvar X (f a). Proof. reflexivity. Qed. (** printing t1 %\ensuremath{t_1}% *) (** printing t2 %\ensuremath{t_2}% *) Definition papp (X: k1)(A: Set)(t1 t2: X A ): LamF X A := inl (X (X A)) (inl (X (option A)) (inr A (t1, t2))). (* short: inl _ (inl _ (inr _ (t1, t2))) *) Lemma papp_m_auto (X: k1)(ef: EFct X)(A B: Set)(f: A -> B)(t1 t2: X A): m (EFct:= lamFpEFct_auto ef) f (papp X A t1 t2) = papp X B (m (EFct:= idpEFct_eta ef) f t1) (m (EFct:= idpEFct_eta ef) f t2). Proof. reflexivity. Qed. Definition pabs (X: k1)(A: Set)(r: X (option A)): LamF X A := inl (X (X A)) (inr (A + X A * X A) r). (* short: inl _ (inr _ r) *) Lemma pabsE_m_auto (X: k1)(ef: EFct X)(A B: Set)(f: A -> B)(r: X (option A)): m (EFct:= lamFpEFct_auto ef) f (pabs X A r) = pabs X B (m (EFct:= idpEFct ef) (option_map f) r). Proof. reflexivity. Qed. Definition pflat (X: k1)(A: Set)(ee: X (X A)): LamF X A := inr (LambF X A) ee. (* short: inr _ ee *) Lemma pflat_m_auto (X: k1)(ef: EFct X)(A B: Set)(f: A -> B)(ee: X(X A)): m (EFct:= lamFpEFct_auto ef) f (pflat X A ee) = pflat X B (m (EFct:= idpEFct ef) (m (EFct:= idpEFct_eta ef) f) ee). Proof. reflexivity. Qed. (* the following will work perfectly well, but has the unnecessary expansions, as seen above: Instance lamFpEFct: pEFct LamF := lamFpEFct_auto. *) (** the by-hand definition at the end of Section 4.1 in the paper: *) Definition lamFpEFct_m (X: k1)(mX: mon X): mon (LamF X). Proof. red. (* intros X mX. *) red. red. intros A B f t. destruct t as [[[a|( t1, t2)]|r]|e]. - exact (pvar X (f a)). - exact (papp X B (mX A B f t1) (mX A B f t2)). - exact (pabs X B (mX (option A) (option B) (option_map f) r)). - exact (pflat X B (moncomp(mX:= mX)(mY:= mX) A B f e)). Defined. (* Print Instances pEFct. *) Definition lamFpEFct: pEFct LamF. Proof. intros X ef. exists (lamFpEFct_m (m(EFct:= ef))). - (* ext *) red. intros. destruct ef; destruct r as [[[a|( t1, t2)]|r]|ee]; simpl; unfold lamFpEFct_m; unfold LNMItPred.map; unfold LNMItPred.m. + rewrite H. reflexivity. + do 2 rewrite (e _ _ _ _ H). reflexivity. + assert (forall a: option A, option_map f a = option_map g a). { destruct a. * unfold option_map. simpl. rewrite H. reflexivity. * reflexivity. } rewrite (e _ _ _ _ H0). reflexivity. + f_equal. apply e. intro. apply e. assumption. - (* fct1 *) red. intros. destruct ef; destruct x as [[[a|( t1, t2)]|r]|ee]; simpl; unfold lamFpEFct_m; unfold LNMItPred.map; unfold LNMItPred.m. + reflexivity. + do 2 rewrite f1. reflexivity. + assert (forall a: option A, option_map id a = a). { destruct a. * unfold option_map. reflexivity. * reflexivity. } rewrite (e _ _ _ _ H). rewrite f1. reflexivity. + assert (forall x: X A, m A A id x = x) by (apply f1). fold (pflat X A ee). f_equal. unfold moncomp. rewrite (e _ _ _ _ H). apply f1. - (* fct2 *) red. intros. destruct ef; destruct x as [[[a|( t1, t2)]|r]|ee]; simpl; unfold lamFpEFct_m; unfold LNMItPred.map; unfold LNMItPred.m; simpl. + reflexivity. + do 2 rewrite f2. reflexivity. + assert (forall a: option A, option_map (g o f) a = ((option_map g) o (option_map f)) a). { destruct a. * unfold option_map. reflexivity. * reflexivity. } rewrite (e _ _ _ _ H). rewrite f2. reflexivity. + assert (forall x: X A, m A C (g o f) x = ((m B C g) o (m A B f)) x) by (apply f2). unfold moncomp. rewrite (e _ _ _ _ H). rewrite f2. reflexivity. Defined. Existing Instance lamFpEFct. (* Print Instances pEFct. *) (** the obvious consequence *) Lemma lamFpEFctlamFpEFct_m (X: k1)(ef: EFct X): @m _ (lamFpEFct ef) = lamFpEFct_m (@m _ ef). Proof. reflexivity. Qed. (** some preparations for lists *) (** [listk1] is needed because of sort polymorphism *) Definition listk1 (A: Set) : Set := list A. Fixpoint filterSome (A: Type)(l: list(option A)){struct l} : list A := match l with nil => nil | None :: rest => filterSome rest | Some a :: rest => a :: filterSome rest end. Lemma filterSomeIn (A: Type)(a: A)(l: list(option A)): In (Some a) l <-> In a (filterSome l). Proof. split. - intro. induction l. + inversion H. + destruct a0. * elim (in_inv H). -- intro. inversion H0. simpl. left. reflexivity. -- intro. simpl. right. apply IHl. assumption. * simpl. apply IHl. simpl in H. destruct H. -- inversion H. -- assumption. - (* the other direction *) 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. Instance listmap: LNMItPred.mon listk1. Proof. exact map. Defined. Definition optionk1 (A: Set) : Set := option A. Instance filterSomeNAT: NAT filterSome (mX:= moncomp(X:= listk1)(Y:= optionk1)(mX:= map)(mY:= option_map))(Y:= listk1). Proof. red. intros. unfold LNMItPred.map. induction t. (* if there are no arguments (X:=listk1)(Y:=optionk1), this will raise an error for bad typing: Error: Abstracting over the term "t" leads to a term "fun t : list (option A) => @filterSome B (@moncomp list (fun A B : Set => @map A B) option (fun A B : Set => @option_map A B) A B f t) = @listmap A B f (@filterSome A t)" which is ill-typed. This also holds of Coq 8.2-1. *) - reflexivity. - destruct a. + simpl. rewrite <- IHt. reflexivity. + simpl. rewrite <- IHt. reflexivity. Qed. (* if (Y:= listk1) is not given in the formulation of the lemma, this will raise a type error *) Lemma flat_mapext (A B: Set)(f g: A -> list B)(l: list A): (forall a, f a = g a) -> flat_map f l = flat_map g l. Proof. intros. induction l; intros; simpl. - reflexivity. - rewrite H. rewrite IHl. reflexivity. Qed. (** interaction of [flat_map] with [map] *) (** printing o %\ensuremath{\circ}% *) Lemma flat_mapLaw1 (A B C: Set)(f: A -> B)(g: B -> list C)(l: list A): flat_map g (map f l) = flat_map (g o f) l. Proof. induction l; intros; simpl. - reflexivity. - rewrite IHl. reflexivity. Qed. (** an instructive instance, but not needed in the sequel: *) Lemma flat_mapLaw1Inst (A B: Set)(f: A -> list B)(l: list A): flat_map (id(A:= list B)) (map f l) = flat_map f l. Proof. rewrite flat_mapLaw1. apply flat_mapext. reflexivity. Qed. Lemma flat_mapLaw2 (A B C : Set) (f : A -> list B) (g : B -> C) (l : list A): map g (flat_map f l) = flat_map (map g o f) l. Proof. induction l; intros; simpl. - reflexivity. - rewrite map_app. rewrite IHl. reflexivity. Qed. (** we use [moncomp] from [LNMItPred.v] *) (** printing c_k1 %\ensuremath{\subseteq}% *) Lemma flat_mapNAT (X: k1)(mX: mon X)(h: X c_k1 listk1)(n: NAT h (mX:= mX) (mY:= map)): NAT(Y:= listk1) (fun A => flat_map (h A)) (mX:= moncomp(X:= listk1)(mX:= map)(mY:= mX)) (mY:= map). Proof. red. intros. transitivity (flat_map (map f o h A) t). - unfold LNMItPred.map. unfold moncomp. rewrite flat_mapLaw1. apply (flat_mapext(B:= B) (h B o mX A B f) (map f o h A) t). intro. unfold comp. unfold NAT in n. exact (n A B f a). - apply sym_eq. exact (flat_mapLaw2 (h A) f t). Qed. Module Type LAM := LNGMIt_Type with Definition LNM.F:= LamF with Definition LNM.FpEFct := lamFpEFct. Module LamFlat (LamBase: LAM). Module LamM := LNGMItDef LamBase. Module LamMMItDef := LamM.LNMItDef. Definition Lam : k1 := LamBase.mu2. (** the canonical datatype constructors *) Definition var (A: Set)(a: A): Lam A := LamMMItDef.InCan (inl _ (inl _ (inl _ a))). (** printing t1 %\ensuremath{t_1}% *) (** printing t2 %\ensuremath{t_2}% *) Definition app (A: Set)(t1 t2: Lam A): Lam A := LamMMItDef.InCan (inl _ (inl _ (inr _ (t1, t2)))). (** there is a conflict with [List.app]! *) (** printing s1 %\ensuremath{s_1}% *) (** printing s2 %\ensuremath{s_2}% *) Lemma app_cong(A: Set)(s1 s2 t1 t2: Lam A): s1 = t1 -> s2 = t2 -> app s1 s2 = app t1 t2. Proof. intros. rewrite H. rewrite H0. reflexivity. Qed. Definition abs (A: Set)(r: Lam(option A)): Lam A := LamMMItDef.InCan (inl _ (inr _ r)). Definition flat (A: Set)(ee: Lam(Lam A)): Lam A := LamMMItDef.InCan (inr _ ee). (** lists of free variables of lambda terms, just with plain Mendler iteration see Section 2.2 in the paper *) Definition FV : Lam c_k1 listk1. Proof. refine (LamBase.MIt (fun (X: k1)(it: X c_k1 listk1)(A: Set)(t: LamF X A) => _)). destruct t as [[[a|( t1, t2)]|r]|e]. - exact (a::nil). - exact (it _ t1 ++ it _ t2). - exact (filterSome (it _ r)). - exact (flat_map(it A)(it (X A) e)). Defined. Definition sFV := fun (X : k1) (it : X c_k1 listk1) (A : Set) (t : LamF 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 => flat_map (it A) (it (X A) e) end. Lemma sFV_ok: FV = LamBase.MIt sFV. Proof. reflexivity. Qed. Lemma FV_var (A: Set)(a: A): FV(var a) = a :: nil. Proof. unfold var. unfold FV. rewrite LamMMItDef.MItRedCan. reflexivity. Qed. Lemma FV_app (A: Set)(t1 t2: Lam A): FV(app t1 t2) = FV t1 ++ FV t2. Proof. unfold app. unfold FV at 1. rewrite LamMMItDef.MItRedCan. reflexivity. Qed. Lemma FV_abs (A: Set)(r: Lam (option A)): FV(abs r) = filterSome (FV r). Proof. unfold abs. unfold FV at 1. rewrite LamMMItDef.MItRedCan. reflexivity. Qed. Lemma FV_flat (A: Set)(ee: Lam (Lam A)): FV(flat ee) = flat_map (FV(A:= A)) (FV ee). Proof. unfold flat. unfold FV at 1. rewrite LamMMItDef.MItRedCan. reflexivity. Qed. (** renaming, see Section 2.2 in the paper *) Instance lam : LNMItPred.mon Lam. (* it does not suffice with mon *) Proof. exact LamBase.mapmu2. Defined. (** behaviour of [lam] on canonical elements *) Lemma lam_var (A B: Set)(f: A -> B)(a: A) : lam f (var a) = var (f a). Proof. unfold lam at 1, var at 1; rewrite LamMMItDef.mapmu2RedCan. reflexivity. Qed. Lemma lam_app (A B: Set)(f: A -> B)(t1 t2: Lam A): lam f (app t1 t2) = app (lam f t1)(lam f t2). Proof. unfold lam at 1, app at 1; rewrite LamMMItDef.mapmu2RedCan. reflexivity. Qed. Lemma lam_abs (A B: Set)(f: A -> B)(r: Lam (option A)): lam f (abs r) = abs (lam (option_map f) r). Proof. unfold lam at 1, abs at 1; rewrite LamMMItDef.mapmu2RedCan. reflexivity. Qed. Lemma lam_flat (A B: Set)(f: A -> B)(ee: Lam (Lam A)): lam f (flat ee) = flat (lam (lam f) ee). Proof. unfold lam at 1, flat at 1. rewrite LamMMItDef.mapmu2RedCan. simpl. reflexivity. Qed. (** The "interesting question" at the end of Section 2.2 of the paper: *) Instance FVNAT: NAT FV. Proof. unfold FV. apply LamMMItDef.MItNAT. red. intros. destruct t as [[[a|( t1, t2)]|r]|ee]; induction ef; simpl; unfold LNMItPred.map. - (* var *) reflexivity. - (* app *) unfold listmap. rewrite map_app. do 2 rewrite H. reflexivity. - (* abs *) unfold moncomp. rewrite H. rewrite <- filterSomeNAT. reflexivity. - (* flat *) rewrite <- (flat_mapNAT(mX:= m)); try assumption. f_equal. unfold moncomp at 1. rewrite H. reflexivity. Qed. (** how renaming works on the list of free variables: *) Corollary FV_ok (A B: Set)(f: A -> B)(t: Lam A): FV(lam f t) = map f (FV t). Proof. apply FVNAT. Qed. (** towards substitution, see Section 2.3 of the paper *) Arguments Some {A}. Definition lift (A B: Set)(f: A -> Lam B)(x: option A): Lam(option B) := match x with | None => var None | Some a => lam Some (f a) end. Definition subst (A B: Set)(f: A -> Lam B)(t: Lam A): Lam B. Proof. revert A B f t. (* new for 8.3 *) refine (LamBase.GMIt (H:= Lam)(G:= Lam)(fun (X: k1)(it: X <_{ Lam } Lam) (A B: Set)(f: A -> Lam B)(t: LamF X A)=> _)). destruct t as [[[a|( t1, t2)]|r]|ee]. - exact (f a). - exact (app (it _ _ f t1)(it _ _ f t2)). - exact (abs (it _ _ (lift f) r)). - exact (flat (it (X A) (Lam B) (var(A:= Lam B) o (it A B f)) ee)). (* not: exact (flat (it (X A) (Lam B) (it A (Lam B) (var(A:= Lam B) o f)) ee)). *) Defined. (* the following definition is just by inspection of the defined subst *) Definition s_subst := fun (X : k1) (it : X <_{ Lam } Lam) (A B : Set) (f : A -> Lam B) (t : LamF X A) => match t with | inl (inl (inl a)) => f a | inl (inl (inr (pair t1 t2))) => app (it A B f t1) (it A B f t2) | inl (inr r) => abs (it (option A) (option B) (lift f) r) | inr ee => flat (it (X A) (Lam B) (var (A:= Lam B) o it A B f) ee) end. Lemma s_subst_ok: LamBase.GMIt s_subst = subst. Proof. reflexivity. Qed. Lemma subst_var (A B: Set)(f: A -> Lam B)(a: A): subst f (var a) = f a. Proof. change subst with (LamBase.GMIt s_subst). unfold var. rewrite LamM.GMItRedCan. reflexivity. Qed. Lemma substMonad1 (A B: Set)(f: A -> Lam B)(a: A): subst f (var a) = f a. Proof. apply subst_var. Qed. Lemma subst_app (A B: Set)(f: A -> Lam B)(t1 t2: Lam A): subst f (app t1 t2) = app (subst f t1)(subst f t2). Proof. change subst with (LamBase.GMIt s_subst). unfold app at 1. rewrite LamM.GMItRedCan. reflexivity. Qed. Lemma subst_abs (A B: Set)(f: A -> Lam B)(r: Lam (option A)): subst f (abs r) = abs (subst (lift f) r). Proof. change subst with (LamBase.GMIt s_subst). unfold abs at 1. rewrite LamM.GMItRedCan. reflexivity. Qed. Lemma subst_flat (A B: Set)(f: A -> Lam B)(ee: Lam(Lam A)): subst f (flat ee) = flat (subst (var(A:= Lam B) o (subst f)) ee). Proof. change subst with (LamBase.GMIt s_subst). unfold flat at 1. rewrite LamM.GMItRedCan. reflexivity. Qed. (** we would have liked to see [subst f (flat ee) = flat (lam (subst f) ee)], but this would need a full second monad law *) (** the generic properties of renaming: *) Lemma lamext: LNMItPred.ext(mX:= lam). Proof. exact LamMMItDef.mapmu2Ext. Qed. Lemma lamfct1: fct1(mX:= lam). Proof. exact LamMMItDef.mapmu2Id. Qed. Lemma lamfct2 : fct2(mX:= lam). Proof. exact LamMMItDef.mapmu2Comp. Qed. (** show that the definition of [subst] qualifies for Theorem 5 in the paper *) Lemma substpGext: forall (X : k1) (h : X <_{ Lam } Lam), gext h -> gext (s_subst 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) (lift f) (lift g)). + reflexivity. + destruct a. * simpl. rewrite H0. reflexivity. * reflexivity. - (* flat *) simpl. f_equal. apply H. clear ee. intro. unfold comp. f_equal. apply H. assumption. Qed. (** the first item in Theorem 1 in the paper: *) Lemma substext (A B: Set)(f g: A -> Lam B)(t: Lam A): (forall a, f a = g a) -> subst f t = subst g t. Proof. intros. change (subst f t) with (LamBase.GMIt s_subst B f t). rewrite (LamM.GMItsExt s_subst substpGext B f g H t). reflexivity. Qed. (* some preparations for the second item in Theorem 1 in the paper *) Lemma FV_var_gen (X : k1)(ef : EFct X)(j : X c_k1 Lam)(n : NAT j)(A : Set)(a : A): FV (LamBase.In ef n (pvar X a)) = a :: nil. Proof. unfold FV. rewrite LamBase.MItRed. reflexivity. Qed. Lemma FV_app_gen (X : k1)(ef : EFct X)(j : X c_k1 Lam)(n : NAT j)(A : Set)(t1 t2: X A): FV (LamBase.In ef n (papp X A t1 t2)) = FV (j A t1) ++ FV (j A t2). Proof. unfold FV at 1. rewrite LamBase.MItRed. reflexivity. Qed. Lemma FV_abs_gen (X : k1)(ef : EFct X)(j : X c_k1 Lam)(n : NAT j)(A : Set)(r: X (option A)): FV (LamBase.In ef n (pabs X A r)) = filterSome (FV (j (option A) r)). Proof. unfold FV at 1. rewrite LamBase.MItRed. reflexivity. Qed. Lemma FV_flat_gen (X : k1)(ef : EFct X)(j : X c_k1 Lam)(n : NAT j)(A : Set)(ee: X(X A)): FV (LamBase.In ef n (pflat X A ee)) = flat_map (FV(A:= A) o (j A)) (FV (j (X A) ee)). Proof. unfold FV at 1. rewrite LamBase.MItRed. reflexivity. Qed. Definition occursFreeIn(A: Set)(a: A)(t: Lam A): Prop := In a (FV t). Infix "occ" := occursFreeIn (at level 90). Lemma occ_var (X : k1)(ef : EFct X)(j : X c_k1 Lam)(n : NAT j)(A : Set)(a : A): a occ (LamBase.In ef n (pvar X a)). Proof. unfold occursFreeIn. rewrite FV_var_gen. left. reflexivity. Qed. Lemma occ_appl (X : k1)(ef : EFct X)(j : X c_k1 Lam)(n : NAT j)(A : Set)(a : A)(t1 t2 : X A): (a occ (j A t1)) -> a occ (LamBase.In ef n (papp X A t1 t2)). Proof. intros. unfold occursFreeIn. rewrite FV_app_gen. apply in_or_app. left. assumption. Qed. Lemma occ_appr (X : k1)(ef : EFct X)(j : X c_k1 Lam)(n : NAT j)(A : Set)(a : A)(t1 t2 : X A): (a occ (j A t2)) -> a occ (LamBase.In ef n (papp X A t1 t2)). Proof. intros. unfold occursFreeIn. rewrite FV_app_gen. apply in_or_app. right. assumption. Qed. Lemma occ_abs (X : k1)(ef : EFct X)(j : X c_k1 Lam)(n : NAT j)(A : Set)(a : A)(r: X (option A)): ((Some a) occ (j (option A) r)) -> a occ (LamBase.In ef n (pabs X A r)). Proof. intros. unfold occursFreeIn. rewrite FV_abs_gen. apply (proj1 (filterSomeIn _ _) H). Qed. (** printing a0 %\ensuremath{a_0}% *) Lemma occ_flat (X : k1)(ef : EFct X)(j : X c_k1 Lam)(n : NAT j)(A : Set)(a: X A)(ee: X(X A)): occursFreeIn a (j (X A) ee) -> forall a0 : A, occursFreeIn a0 (j A a) -> occursFreeIn a0 (LamBase.In ef n (pflat X A ee)). Proof. intros. unfold occursFreeIn. rewrite FV_flat_gen. apply (proj2(in_flat_map (FV(A:=A) o j A) (FV (j _ ee)) a0)). exists a. split; assumption. Qed. (** now the interpretation for canonical terms although not needed for Theorem 1: *) Lemma occCan_var (A: Set)(a: A): a occ (var a). Proof. unfold var, LamMMItDef.InCan. apply occ_var. Qed. Lemma occCan_appl (A: Set)(a: A)(t1 t2: Lam A): a occ t1 -> a occ (app t1 t2). Proof. intros. unfold app, LamMMItDef.InCan. apply occ_appl. assumption. Qed. Lemma occCan_appr (A: Set)(a: A)(t1 t2: Lam A): a occ t2 -> a occ (app t1 t2). Proof. intros. unfold app, LamMMItDef.InCan. apply occ_appr. assumption. Qed. Lemma occCan_abs (A: Set)(a: A)(r: Lam(option A)): (Some a) occ r -> a occ (abs r). Proof. intros. unfold abs, LamMMItDef.InCan. apply occ_abs. assumption. Qed. Lemma occCan_flat (A: Set)(a: A)(t: Lam A)(ee: Lam(Lam A)): a occ t -> t occ ee -> a occ (flat ee). Proof. intros. unfold flat, LamMMItDef.InCan. (* Check (occ_flat LamMMItDef.mapmu2EFct (j:= fun _ x => x) (fun _ _ _ _ => refl_equal _) t ee H0 a H). *) apply (occ_flat LamMMItDef.mapmu2EFct (j:= fun _ x => x) (fun _ _ _ _ => refl_equal _) t ee H0 a H). Qed. (** the second item in Theorem 1 in the paper: *) Lemma substext' (A B: Set)(f g: A -> Lam B)(t: Lam A): (forall a, a occ t -> f a = g a) -> subst f t = subst g t. Proof. intros. revert B f g H. revert A t. refine (LamBase.mu2Ind _ _). intros. destruct t as [[[a|( t1, t2)]|r]|ee]; change subst with (LamBase.GMIt s_subst); do 2 rewrite LamBase.GMItRed; simpl. - (* var *) apply H0. exact (occ_var ef n a). - (* app *) apply app_cong; change (LamBase.GMIt s_subst) with subst. + unfold comp. apply H. intros. apply H0. apply (occ_appl ef n a). assumption. + unfold comp. apply H. intros. apply H0. apply (occ_appr ef n a). assumption. - (* abs *) f_equal. change (LamBase.GMIt s_subst) with subst. unfold comp. apply H. intros. destruct a. + simpl. rewrite H0. * reflexivity. * generalize H1. apply (occ_abs ef n a). + reflexivity. - (* flat *) f_equal. change (LamBase.GMIt s_subst) with subst. unfold comp at 1 4. apply H. intros. unfold comp. f_equal. apply H. intros. apply H0. apply (occ_flat ef n a); assumption. Qed. (** the third item in Theorem 1 in the paper needs one extra lemma: *) Lemma lift_map (A B C: Set)(a: option A)(f: A -> Lam B)(g: B -> C): (lam (option_map g) o lift f) a = lift (lam g o f) a. Proof. destruct a. - unfold comp. simpl. do 2 rewrite <- lamfct2. apply lamext. reflexivity. - unfold comp. simpl. rewrite lam_var. reflexivity. Qed. (** the third item in Theorem 1 in the paper: *) Lemma substGnat1 (A B C : Set) (f : A -> Lam B) (g : B -> C) (t : Lam A): lam g (subst f t) = subst (lam g o f) t. Proof. apply (LamM.GMItsNat1 s_subst substpGext). red. intros. destruct x as [[[a|( t1, t2)]|r]|ee]. - simpl. reflexivity. - simpl s_subst. rewrite lam_app. do 2 rewrite H0. reflexivity. - simpl s_subst. rewrite lam_abs. rewrite H0. f_equal. apply H. intro. apply lift_map. - (* flat *) simpl s_subst. rewrite lam_flat. f_equal. rewrite H0. apply H. clear ee. intro. unfold comp at 1 2 3. rewrite lam_var. f_equal. rewrite H0. reflexivity. Qed. (** the fourth item in Theorem 1 in the paper: *) Lemma substGnat2 (A B C: Set)(f: A -> B)(g: B -> Lam C)(t: Lam A): subst g (lam f t) = subst (g o f) t. Proof. apply (LamM.GMItsNat2 s_subst substpGext). red. intros. destruct ef as [m0 e0 f01 f02]. destruct x as [[[a|( t1, t2)]|r]|ee]; simpl; unfold LNMItPred.map. - simpl. reflexivity. - do 2 rewrite H0. reflexivity. - unfold moncomp. rewrite H0. f_equal. apply H. intro. destruct a; reflexivity. - (* flat *) f_equal. unfold moncomp at 1. rewrite H0. apply H. clear ee. intro. unfold comp at 1 2 3. f_equal. unfold moncomp. rewrite H0. apply H. clear a. intro. reflexivity. Qed. (** just an instance *) Lemma substLaw (A B: Set)(f: A -> Lam B)(t: Lam A): subst id (lam f t) = subst f t. Proof. rewrite substGnat2. apply substext. reflexivity. Qed. (** a more elaborate formulation of naturality *) Instance substNAT (X: k1)(mX: mon X)(h: X c_k1 Lam)(n: NAT(mX:= mX) h): NAT (fun A => subst (h A)) (mX:= moncomp(mX:= lam)(mY:= mX)). Proof. red. intros. unfold LNMItPred.map. unfold moncomp. rewrite substGnat2. rewrite substGnat1. apply substext. intro. unfold comp. apply n. Qed. Corollary substNATCor (X: k1)(mX: mon X)(h: X c_k1 Lam)(n: NAT(mX:= mX) h) (A B: Set) (f: A -> B)(t : Lam (X A)): subst (h B) (lam (mX A B f) t) = lam f (subst (h A) t). Proof. intros. rewrite <- (substNAT n). reflexivity. Qed. Definition flatimpl: forall (A: Set), Lam(Lam A) -> Lam A := glessTosub subst. Instance flatimplNAT: NAT flatimpl (mX:= moncomp(mX:= lam)(mY:= lam)). Proof. apply gnat1gnat2NAT. - red; intros. apply substGnat1. - red; intros. apply substGnat2. Qed. (** the fifth item in Theorem 1 in the paper: *) Lemma substMonad3 (A B C: Set)(f: A -> Lam B)(g: B -> Lam C)(t: Lam A): subst g (subst f t) = subst ((subst g) o f) t. Proof. revert B C f g. revert A t. refine (LamBase.mu2Ind _ _). intros. destruct t as [[[a|( t1, t2)]|r]|ee]; change subst with (LamBase.GMIt s_subst); repeat rewrite LamBase.GMItRed; simpl; change (LamBase.GMIt s_subst) with subst. - (* var *) reflexivity. - (* app *) rewrite subst_app. unfold comp at 1 2. do 2 rewrite H. reflexivity. - (* abs *) rewrite subst_abs. unfold comp at 1. rewrite H. do 3 f_equal. unfold comp. apply substext. clear X ef j n H r. intro. destruct a. + simpl. rewrite substGnat1. rewrite substGnat2. reflexivity. + simpl. rewrite substMonad1. reflexivity. - (* flat *) rewrite subst_flat. f_equal. unfold comp at 2 5. rewrite H. apply substext. clear ee. intro. unfold comp. rewrite substMonad1. f_equal. rewrite H. (* this is an application of H deep inside the proof *) reflexivity. Qed. (** Section 5 of the paper *) (** preparations for the formula for the list of free variables of [subst f t] *) (** printing l1 %\ensuremath{l_1}% *) (** printing l2 %\ensuremath{l_2}% *) Lemma filterSomeAppend (A: Type)(l1 l2: list(option A)): filterSome (l1 ++ l2) = filterSome l1 ++ filterSome l2. Proof. induction l1. - reflexivity. - destruct a. + simpl. rewrite IHl1. reflexivity. + simpl. assumption. Qed. Lemma filterSomeMapSome (A: Type)(l: list A): filterSome (map (Some(A:= A)) l) = l. Proof. induction l. - reflexivity. - simpl. rewrite IHl. reflexivity. Qed. Lemma filterSomeFV (A: Set)(t: Lam A): filterSome (FV (lam Some t)) = FV t. Proof. rewrite FV_ok. apply filterSomeMapSome. Qed. (** this needed naturality of [FV] *) Lemma FVsubst_aux (A B: Set)(f: A -> Lam B)(t: list(option A)): filterSome(flat_map(FV(A:= option B) o lift f) t) = flat_map (FV(A:= B) o f)(filterSome t). Proof. induction t. - reflexivity. - destruct a. + simpl. unfold comp at 1. unfold lift at 1. rewrite <- IHt. rewrite filterSomeAppend. rewrite filterSomeFV. reflexivity. + simpl. rewrite <- IHt. rewrite filterSomeAppend. unfold comp at 1. simpl. rewrite FV_var. reflexivity. Qed. (** this needed naturality of [FV] through [filterSomeFV] *) (** further preparations for the last item of Theorem 1 in the paper: *) Lemma flat_map_app (A B: Set)(f: A -> list B)(l1 l2: list A): flat_map f (l1 ++ l2) = flat_map f l1 ++ flat_map f l2. Proof. induction l1. - reflexivity. - simpl. rewrite IHl1. rewrite app_ass. reflexivity. Qed. (** printing o %\ensuremath{\circ}% *) Lemma flat_mapMonad3 (A B C : Set) (f : A -> list B) (g : B -> list C) (l : list A): flat_map g (flat_map f l) = flat_map ((flat_map g) o f) l. Proof. induction l; intros. - reflexivity. - simpl. rewrite flat_map_app. rewrite IHl. reflexivity. Qed. (** the last item of Theorem 1 in the paper *) Lemma FVsubst (A B: Set)(f: A -> Lam B)(t: Lam A): FV (subst f t) = flat_map (FV(A:= B) o f) (FV t). Proof. revert B f. revert A t. refine (LamBase.mu2Ind _ _). intros. destruct t as [[[a|( t1, t2)]|r]|ee]; change subst with (LamBase.GMIt s_subst); rewrite LamBase.GMItRed; simpl; change (LamBase.GMIt s_subst) with subst. - (* var *) unfold LambF. fold (pvar X a). rewrite FV_var_gen. simpl. rewrite <- app_nil_end. reflexivity. - (* app *) unfold LambF. fold (papp X A t1 t2). rewrite FV_app_gen. rewrite FV_app. rewrite flat_map_app. unfold comp at 1 2. rewrite (H A t1 B f). rewrite (H A t2 B f). reflexivity. - (* abs *) unfold LambF. fold (pabs X A r). rewrite FV_abs_gen. rewrite FV_abs. unfold comp at 1. rewrite H. rewrite FVsubst_aux. (** here enters naturality of [FV] *) reflexivity. - (* flat *) fold (pflat X A ee). rewrite FV_flat_gen. rewrite FV_flat. unfold comp at 1. rewrite H. transitivity (flat_map (FV(A:= B)) (flat_map ((fun b: Lam B => b :: nil) o (subst f o j A)) (FV (j (X A) ee)))). + f_equal. apply flat_mapext. intro. unfold comp. apply FV_var. + do 2 rewrite flat_mapMonad3. apply flat_mapext. intro. unfold comp. simpl. rewrite <- app_nil_end. apply H. Qed. (** its consequence close to the end of Section 2.3 of the paper: *) Lemma subst_occ (A B: Set)(f: A -> Lam B)(t: Lam A)(b: B): b occ (subst f t) -> exists a: A, (a occ t) /\ (b occ f a). Proof. unfold occursFreeIn. intros. rewrite FVsubst in H. destruct (proj1 (in_flat_map (FV(A:= B) o f) (FV t) b) H). exists x. assumption. Qed. (** hereditarily canonical terms *) (** Definition 3 in the paper *) Inductive can : forall (A: Set), Lam A -> Prop := | can_var : forall (A: Set)(a: A), can (var a) | can_app : forall (A: Set)(t1 t2: Lam A), can t1 -> can t2 -> can(app t1 t2) | can_abs : forall (A: Set)(r: Lam(option A)), can r -> can (abs r) | can_flat: forall (A: Set)(ee: Lam(Lam A)), can ee -> (forall t:Lam A, t occ ee -> can t) -> can (flat ee). (** Here comes material that did not form part of the original submission of the SCP paper. It was stimulated by a question of one of the referees how [can] is related to what will be called [LamP] below. Many thanks to the anonymous referee for that. It was easy for me to answer that question since I had already studied binary versions of those unary predicates before. However, those developments would have led too far from the main issue of the paper. *) Definition optionpred (A: Type)(P: A -> Prop): option A -> Prop. Proof. intros x. induction x. - exact (P a). - exact True. Defined. (* a failed truly nested inductive definition in Coq: Inductive LamP : forall (A: Set), (A -> Prop) -> Lam A -> Prop := | LamP_var: forall (A: Set)(P: A -> Prop)(a: A), P a -> LamP P (var a) | LamP_app: forall (A: Set)(P: A -> Prop)(t1 t2: Lam A), LamP P t1 -> LamP P t2 -> LamP P (app t1 t2) | LamP_abs: forall (A: Set)(P: A -> Prop)(r: Lam(option A)), LamP (optionpred P) r -> LamP P (abs r) | LamP_flat: forall (A: Set)(P: A -> Prop)(ee: Lam(Lam A)), LamP (LamP P) ee -> LamP P (flat ee). yields: Error: Non strictly positive occurrence of "LamP" in "forall A : Set, forall P : A -> Prop, forall ee : Lam (Lam A), LamP (Lam A) (LamP A P) ee -> LamP A P (flat ee)". Without the last clause, this works well and yields the following induction principle: Check LamP_ind : forall Q : forall A : Set, (A -> Prop) -> Lam A -> Prop, (forall (A : Set) (P : A -> Prop) (a : A), P a -> Q A P (var a)) -> (forall (A : Set) (P : A -> Prop) (t1 t2 : Lam A), LamP P t1 -> Q A P t1 -> LamP P t2 -> Q A P t2 -> Q A P (app t1 t2)) -> (forall (A : Set) (P : A -> Prop) (r : Lam (option A)), LamP (optionpred P) r -> Q (option A) (optionpred P) r -> Q A P (abs r)) -> forall (A : Set) (P : A -> Prop) (t : Lam A), LamP P t -> Q A P t. *) (** an axiomatic definition of a truly nested inductive predicate on [Lam]: *) Parameter LamP: forall A: Set, (A -> Prop) -> Lam A -> Prop. Axiom LamP_var: forall (A: Set)(P: A -> Prop)(a: A), P a -> LamP P (var a). Axiom LamP_app: forall (A: Set)(P: A -> Prop)(t1 t2: Lam A), LamP P t1 -> LamP P t2 -> LamP P (app t1 t2). Axiom LamP_abs: forall (A: Set)(P: A -> Prop)(r: Lam(option A)), LamP (optionpred P) r -> LamP P (abs r). Axiom LamP_flat: forall (A: Set)(P: A -> Prop)(ee: Lam(Lam A)), LamP (LamP P) ee -> LamP P (flat ee). Axiom LamP_ind: forall (Q: forall A: Set, (A -> Prop) -> Lam A -> Prop), (forall (A: Set)(P: A -> Prop)(a: A), P a -> Q A P (var a)) -> (forall (A: Set)(P: A -> Prop)(t1 t2: Lam A), LamP P t1 -> Q A P t1 -> LamP P t2 -> Q A P t2 -> Q A P (app t1 t2)) -> (forall (A: Set)(P: A -> Prop)(r: Lam(option A)), LamP (optionpred P) r -> Q (option A) (optionpred P) r -> Q A P (abs r)) -> (forall (A: Set)(P: A -> Prop)(ee: Lam(Lam A)), LamP (LamP P) ee -> Q (Lam A) (Q A P) ee -> Q A P (flat ee)) -> forall (A: Set)(P: A -> Prop)(t: Lam A), LamP P t -> Q A P t. (** the last clause is in plain analogy with the other ones *) Definition univpred (A: Type): A -> Prop. Proof. intros. exact True. Defined. (** a variant that is accepted as inductive definition by Coq: *) Inductive LamP' : forall (A: Set), (A -> Prop) -> Lam A -> Prop := | LamP'_var: forall (A: Set)(P: A -> Prop)(a: A), P a -> LamP' P (var a) | LamP'_app: forall (A: Set)(P: A -> Prop)(t1 t2: Lam A), LamP' P t1 -> LamP' P t2 -> LamP' P (app t1 t2) | LamP'_abs: forall (A: Set)(P: A -> Prop)(r: Lam(option A)), LamP' (optionpred P) r -> LamP' P (abs r) | LamP'_flat: forall (A: Set)(P: A -> Prop)(ee: Lam(Lam A)), LamP' (@univpred (Lam A)) ee -> (forall t: Lam A, t occ ee -> LamP' P t) -> LamP' P (flat ee). Lemma LamP'ImpCan (A: Set)(P: A -> Prop)(t: Lam A): LamP' P t -> can t. Proof. intros. induction H. - apply can_var. - apply can_app; assumption. - apply can_abs; assumption. - apply can_flat; assumption. Qed. (* a failed attempt for an analogous lemma: Lemma LamPImpCan (A: Set)(P: A -> Prop)(t: Lam A): LamP P t -> can t. Proof. intros. revert A P t H. apply (LamP_ind (fun (A: Set)(P: A -> Prop)(t: Lam A) => can t)); intros. apply can_var. apply can_app; assumption. apply can_abs; assumption. apply can_flat; try assumption. intros. no hope! but the statement will follow later *) Definition subpredicate (A: Type)(P P': A -> Prop):= forall a:A, P a -> P' a. (* is this not part of the libraries? *) Add Parametric Morphism (A: Set): (LamP'(A:=A)) with signature (subpredicate(A:=A)) ==> (subpredicate(A:=Lam A)) as LamP'_monM. Proof. red. intros P P' Hsub t HP. induction HP. - apply LamP'_var. apply Hsub. assumption. - apply LamP'_app. + apply IHHP1; assumption. + apply IHHP2; assumption. - apply LamP'_abs. apply IHHP. red. intros. induction a. + simpl. apply Hsub. assumption. + exact I. - apply LamP'_flat. + assumption. + intros. apply H0; assumption. Qed. Lemma CanImpLamP'univ (A: Set)(t: Lam A): can t -> LamP' (@univpred A) t. Proof. intros. induction H. - apply LamP'_var. red. exact I. - apply LamP'_app; assumption. - apply LamP'_abs. assert (subpredicate (@univpred (option A)) (optionpred (@univpred A))). { red. intros. induction a; assumption. } apply (LamP'_monM H0). assumption. - apply LamP'_flat; assumption. Qed. (** thus, the relation between [can] and [LamP'] is rather trivial *) (* the following lemma will be needed even outside of this digression *) Lemma occ_var_inv (A: Set)(a b: A): a occ (var b) -> a = b. Proof. intros. unfold occursFreeIn in H. rewrite FV_var in H. destruct H. - apply sym_eq. assumption. - inversion H. Qed. Lemma occ_app_inv (A: Set)(a: A)(t1 t2: Lam A): a occ (app t1 t2) -> (a occ t1) \/ (a occ t2). Proof. intros. unfold occursFreeIn in H. rewrite FV_app in H. destruct (in_app_or (FV t1) (FV t2) _ H). - left. assumption. - right. assumption. Qed. Lemma occ_abs_inv (A: Set)(a: A)(r: Lam (option A)): a occ (abs r) -> Some a occ r. Proof. intros. unfold occursFreeIn in H. rewrite FV_abs in H. apply (proj2 (filterSomeIn _ _) H). Qed. Lemma occ_flat_inv (A: Set)(a: A)(ee: Lam (Lam A)): a occ (flat ee) -> exists t: Lam A, (a occ t) /\ (t occ ee). Proof. intros. unfold occursFreeIn in H. rewrite FV_flat in H. destruct (proj1 (in_flat_map (FV(A:=A)) (FV ee) a) H). exists x. destruct H0. split; assumption. Qed. (** an auxiliary lemma *) Lemma LamP'_FV (A: Set)(P: A -> Prop)(t: Lam A)(a: A): LamP' P t -> a occ t -> P a. Proof. intros. induction H. - apply occ_var_inv in H0. rewrite H0. assumption. - induction (occ_app_inv _ _ _ H0). + exact (IHLamP'1 a H2). + exact (IHLamP'2 a H2). - apply (occ_abs_inv a r) in H0. apply (IHLamP' (Some a) H0). - destruct (occ_flat_inv _ _ H0). destruct H3. apply (H2 x); assumption. Qed. (** for curiosity, an analogous lemma for [LamP]: *) Lemma LamP_FV (A: Set)(P: A -> Prop)(t: Lam A)(a: A): LamP P t -> a occ t -> P a. Proof. intros. revert a H0. revert A P t H. apply (LamP_ind (fun (A: Set)(P: A -> Prop)(t: Lam A) => forall a:A, a occ t -> P a)); intros. - apply occ_var_inv in H0. rewrite H0. assumption. - induction (occ_app_inv _ _ _ H3). + exact (H0 a H4). + exact (H2 a H4). - apply (occ_abs_inv a r) in H1. apply (H0 (Some a) H1). - destruct (occ_flat_inv _ _ H1). destruct H2. apply (H0 x); assumption. Qed. (** [LamP'] satisfies the last closure rule of [LamP]: *) Lemma LamP'_flat' (A: Set)(P: A -> Prop)(ee: Lam(Lam A)): LamP' (LamP' P) ee -> LamP' P (flat ee). Proof. intros. apply LamP'_flat. - assert (subpredicate (LamP' P) (@univpred (Lam A))). { red. intros. exact I. } apply (LamP'_monM H0). assumption. - intros. apply (LamP'_FV (t:=ee) t); assumption. Qed. Lemma LamPImpLamP' (A: Set)(P: A -> Prop)(t: Lam A): LamP P t -> LamP' P t. Proof. intros. refine (LamP_ind _ _ _ _ _ H); clear A P t H; intros. - apply LamP'_var; assumption. - apply LamP'_app; assumption. - apply LamP'_abs; assumption. - apply LamP'_flat'; assumption. Qed. (** another auxiliary lemma: *) Lemma CanImpLamP (A: Set)(t: Lam A): can t -> forall P: A -> Prop, (forall a: A, a occ t -> P a) -> LamP P t. Proof. intro Hyp. induction Hyp; intros. - apply LamP_var. apply H. apply occCan_var. - apply LamP_app. + apply IHHyp1. intros. apply H. apply occCan_appl. assumption. + apply IHHyp2. intros. apply H. apply occCan_appr. assumption. - apply LamP_abs. apply IHHyp. intros. induction a. + simpl. apply H. apply occCan_abs. assumption. + exact I. - apply LamP_flat. apply IHHyp. intros. apply H0. + assumption. + intros. apply H1. apply (occCan_flat a0 a); assumption. Qed. (** [LamP] satisfies the last closure rule of [LamP']: *) Lemma LamP_flat' (A: Set)(P: A -> Prop)(ee: Lam(Lam A)): LamP (@univpred (Lam A)) ee -> (forall t: Lam A, t occ ee -> LamP P t) -> LamP P (flat ee). Proof. intros. apply CanImpLamP. - apply can_flat. + apply (LamP'ImpCan(P:=@univpred (Lam A))). apply LamPImpLamP'. assumption. + intros. apply (LamP'ImpCan(P:= P)). apply LamPImpLamP'. apply H0. assumption. - intros. apply occ_flat_inv in H1. destruct H1. destruct H1. assert (LamP P x) by (apply H0; assumption). apply LamPImpLamP' in H3. apply (LamP'_FV a H3 H1). Qed. Lemma LamP'ImpLamP (A: Set)(P: A -> Prop)(t: Lam A): LamP' P t -> LamP P t. Proof. intros. refine (LamP'_ind _ _ _ _ _ H); clear A P t H; intros. - apply LamP_var; assumption. - apply LamP_app; assumption. - apply LamP_abs; assumption. - apply LamP_flat'; assumption. Qed. (** Section 5.1 of the paper *) (** we are only able to prove a weakened version of the second monad law, namely Lemma 8 in the paper: *) Lemma substMonad2 (A: Set)(t: Lam A): can t -> subst (var(A:= A)) t = t. Proof. intros H. induction H. - rewrite substMonad1. reflexivity. - (* app *) rewrite subst_app. rewrite IHcan1. rewrite IHcan2. reflexivity. - (* abs *) rewrite subst_abs. replace (subst (lift (var (A:= A))) r) with (subst (var (A:= option A)) r). 2: { apply substext. intro. destruct a. + simpl. rewrite lam_var. reflexivity. + reflexivity. } rewrite IHcan. reflexivity. - (* flat *) rewrite subst_flat. f_equal. transitivity (subst (var (A:= Lam A)) ee). + apply substext'. intros t Hyp. unfold comp. f_equal. apply H1. assumption. + assumption. Qed. Lemma lamext_refined (A B: Set)(f g: A -> B)(t: Lam A): can t -> (forall a, a occ t -> f a = g a) -> lam f t = lam g t. Proof. intros. revert B f g H0. (* induction over being canonical: *) induction H; intros. - do 2 rewrite lam_var. rewrite H0. + reflexivity. + apply occCan_var. - do 2 rewrite lam_app. apply app_cong. + apply IHcan1. intros. apply H1. apply occCan_appl. assumption. + apply IHcan2. intros. apply H1. apply occCan_appr. assumption. - do 2 rewrite lam_abs. f_equal. apply IHcan. intros. destruct a. + simpl. rewrite H0. * reflexivity. * apply occCan_abs. assumption. + reflexivity. - do 2 rewrite lam_flat. f_equal. apply IHcan. intros t Hyp. apply H1. + assumption. + intros. apply H2. eapply occCan_flat. * eexact H3. * assumption. Qed. Lemma lam_occ (A B: Set)(f: A -> B)(t: Lam A)(b: B): b occ (lam f t) -> exists a: A, (a occ t) /\ (b = f a). Proof. unfold occursFreeIn. intros. rewrite FV_ok in H. assert (exists a: A, f a = b /\ In a (FV t)) by (exact (proj1 (in_map_iff _ _ _) H)). destruct H0. destruct H0. exists x. split. - assumption. - symmetry. assumption. Qed. Lemma lam_can (A B: Set)(f: A -> B)(t: Lam A): can t -> can (lam f t). Proof. intros. revert B f. induction H; intros. - rewrite lam_var. apply can_var. - rewrite lam_app. apply can_app. + apply IHcan1. + apply IHcan2. - rewrite lam_abs. apply can_abs. apply IHcan. - (* flat *) rewrite lam_flat. apply can_flat. + apply IHcan. + intros. (* Check (lam_occ (fun t : Lam A => lam (fun x : A => f x) t) ee t H2). *) destruct (lam_occ _ _ t H2). destruct H3. rewrite H4. apply H1. assumption. Qed. (* now earlier in the file an auxiliary lemma for preservation of [can] by [subst]: Lemma occ_var_inv (A: Set)(a b: A): a occ (var b) -> a = b. Proof. intros. unfold occursFreeIn in H. rewrite FV_var in H. destruct H. apply sym_eq. assumption. inversion H. Qed. *) Lemma subst_can (A B: Set)(f: A -> Lam B)(t: Lam A): (forall a: A, a occ t -> can (f a)) -> can t -> can (subst f t). Proof. intros. revert B f H. induction H0; intros. - rewrite subst_var. apply H. apply occCan_var. - rewrite subst_app. apply can_app. + apply IHcan1. intros. apply H. apply occCan_appl. assumption. + apply IHcan2. intros. apply H. apply occCan_appr. assumption. - rewrite subst_abs. apply can_abs. apply IHcan. intros. destruct a. + simpl. apply lam_can. apply H. apply occCan_abs. assumption. + simpl. apply can_var. - (* flat *) rewrite subst_flat. apply can_flat. + apply IHcan. intros. unfold comp. apply can_var. + intros. (* Check (subst_occ _ ee _ H3). *) destruct (subst_occ _ ee _ H3). destruct H4. unfold comp in H5. (* Check (occ_var_inv t _ H5). *) rewrite (occ_var_inv t _ H5). apply H1. * assumption. * intros. apply H2. (* Check (occCan_flat a x _ H6 H4). *) exact (occCan_flat a x _ H6 H4). Qed. Lemma lam_is_subst (A B: Set)(f: A -> B)(t: Lam A): can t -> lam f t = subst (var(A:= B) o f) t. Proof. intros. rewrite <- substGnat2. apply sym_eq. apply substMonad2. apply lam_can. assumption. Qed. (** finally, we obtain the desired rewrite rule for [subst] in the case [flat], but only for canonical elements *) Lemma subst_flat' (A B: Set)(f: A -> Lam B)(ee: Lam(Lam A)): can ee -> subst f (flat ee) = flat (lam (subst f) ee). Proof. intros. rewrite subst_flat. f_equal. apply sym_eq. apply lam_is_subst. assumption. Qed. (** Section 5.2 of the paper *) Definition Lam' (A: Set) : Set := {t: Lam A| can t}. Inductive Lam'_ALT(A: Set): Set := existLam': forall t: Lam A, can t -> Lam'_ALT A. Definition Lam'_ALT_Lam' (A: Set): Lam'_ALT A -> Lam' A. Proof. intros. destruct H. exists t. assumption. Defined. Definition Lam'_Lam'_ALT (A: Set): Lam' A -> Lam'_ALT A. Proof. intros. destruct H. exists x. assumption. Defined. Lemma Lam'_ALT_bij_Lam' (A: Set): (forall t: Lam' A, Lam'_ALT_Lam' (Lam'_Lam'_ALT t) = t) /\ (forall t: Lam'_ALT A, Lam'_Lam'_ALT (Lam'_ALT_Lam' t) = t). Proof. split; intros; destruct t; reflexivity. Qed. Definition pi1: Lam' c_k1 Lam. Proof. red. intros. exact (proj1_sig H). Defined. Arguments pi1 {A}. Definition pi1_ALT: Lam'_ALT c_k1 Lam. Proof. red. intros. destruct H. assumption. Defined. Definition var' (A: Set)(a: A): Lam' A. Proof. red. exists (var a). apply can_var. Defined. (** printing t1' %\ensuremath{t'_1}% *) (** printing t2' %\ensuremath{t'_2}% *) (** printing p1 %\ensuremath{p_1}% *) (** printing p2 %\ensuremath{p_2}% *) Definition app' (A: Set)(t1 t2: Lam' A): Lam' A. Proof. destruct t1 as (t1', p1). destruct t2 as (t2', p2). exists (app t1' t2'). apply can_app; assumption. Defined. Definition abs' (A: Set)(r: Lam' (option A)): Lam' A. Proof. destruct r as (r, p). exists (abs r). apply can_abs; assumption. Defined. Definition flat' (A: Set)(ee: Lam'(Lam' A)): Lam' A. Proof. red. exists (flat (lam pi1 (pi1 ee))). destruct ee as (ee', p). simpl. apply can_flat. - apply lam_can. assumption. - intros. destruct (lam_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] *) Lemma flat'_ok (A: Set)(ee: Lam'(Lam' A)): pi1 (flat' ee) = flat(lam pi1 (pi1 ee)). Proof. reflexivity. Qed. Instance lam': LNMItPred.mon Lam'. Proof. red. intros A B f t. exists (lam f (pi1 t)). apply lam_can. unfold pi1. apply proj2_sig. Defined. Lemma lam'_ok (A B: Set)(f: A -> B)(t: Lam' A): pi1 (lam' f t) = lam f (pi1 t). Proof. reflexivity. Qed. Definition subst' (A B: Set)(f: A -> Lam' B)(t: Lam' A): Lam' B. Proof. red. exists (subst (fun a => pi1 (f a)) (pi1 t)). apply subst_can. - intros a _. unfold pi1. apply proj2_sig. - unfold pi1. apply proj2_sig. Defined. Lemma subst'_ok (A B: Set)(f: A -> Lam' B)(t: Lam' A): pi1 (subst' f t) = subst (pi1 o f) (pi1 t). Proof. reflexivity. Qed. Definition FV': Lam' c_k1 listk1. Proof. red. intros A t. apply FV. exact (pi1 t). Defined. Instance FV'NAT: NAT FV'. Proof. red. intros. unfold FV'. destruct t as (t', p). simpl. apply FVNAT. Qed. Corollary FV'_ok (A B: Set)(f: A -> B)(t: Lam' A): FV'(lam' f t) = map f (FV' t). Proof. apply FV'NAT. Qed. Lemma FV'_var (A: Set)(a: A): FV'(var' a) = a :: nil. Proof. unfold var'. unfold FV'. simpl. apply FV_var. Qed. Lemma FV'_app (A: Set)(t1 t2: Lam' A): FV'(app' t1 t2) = FV' t1 ++ FV' t2. Proof. destruct t1. destruct t2. unfold app'. unfold FV' at 1. simpl. rewrite FV_app. reflexivity. Qed. Lemma FV'_abs (A: Set)(r: Lam' (option A)): FV'(abs' r) = filterSome (FV' r). Proof. destruct r. unfold abs'. unfold FV' at 1. simpl. rewrite FV_abs. reflexivity. Qed. Lemma FV'_flat (A: Set)(ee: Lam' (Lam' A)): FV'(flat' ee) = flat_map (FV'(A:= A)) (FV' ee). Proof. destruct ee. unfold flat'. unfold FV' at 1. simpl. rewrite FV_flat. rewrite FV_ok. unfold FV'. simpl. rewrite flat_mapLaw1. reflexivity. Qed. (** item 6 of Theorem 1 for [Lam'] in place of [Lam]: *) Lemma FV'subst' (A B: Set)(f: A -> Lam' B)(t: Lam' A): FV'(subst' f t) = flat_map (FV'(A:= B) o f) (FV' t). Proof. unfold subst', FV'. destruct t as (t', p). simpl. rewrite FVsubst. unfold comp. reflexivity. Qed. Definition occursFreeIn' (A: Set)(a: A)(t: Lam' A): Prop := In a (FV' t). Infix "occ'" := occursFreeIn' (at level 90). Lemma lam'_occ (A B: Set)(f: A -> B)(t: Lam' A)(b: B): b occ' (lam' f t) -> exists a: A, (a occ' t) /\ (b = f a). Proof. unfold occursFreeIn'. intros. rewrite FV'_ok in H. assert (exists a: A, f a = b /\ In a (FV' t)) by (exact (proj1 (in_map_iff _ _ _) H)). destruct H0. destruct H0. exists x. split. - assumption. - rewrite H0. reflexivity. Qed. Lemma lam'_occ_ALT (A B: Set)(f: A -> B)(t: Lam' A)(b: B): b occ' (lam' f t) -> exists a: A, (a occ' t) /\ (b = f a). Proof. intros. destruct t. unfold occursFreeIn' in H. unfold FV' in H. rewrite lam'_ok in H. simpl in H. destruct (lam_occ _ _ _ H). exists x0. destruct H0. split. - unfold occursFreeIn'. assumption. - assumption. Qed. Lemma subst'_occ (A B: Set)(f: A -> Lam' B)(t: Lam' A)(b: B): b occ' (subst' f t) -> exists a: A, (a occ' t) /\ (b occ' f a). Proof. unfold occursFreeIn'. intros. rewrite FV'subst' in H. destruct (proj1 (in_flat_map (FV'(A:= B) o f) (FV' t) b) H). exists x. assumption. Qed. Lemma subst'_occ_ALT (A B: Set)(f: A -> Lam' B)(t: Lam' A)(b: B): b occ' (subst' f t) -> exists a: A, (a occ' t) /\ (b occ' f a). Proof. unfold occursFreeIn'. intros. unfold FV' in H. destruct t. rewrite subst'_ok in H. simpl in H. destruct (subst_occ _ _ _ H). exists x0. destruct H0. split; assumption. Qed. Definition EqLam' (A: Set)(t1 t2: Lam' A): Prop := pi1 t1 = pi1 t2. (** printing ~~ %\ensuremath{\equiv}% *) (* begin hide *) Infix "~~" := EqLam' (at level 60). (* end hide *) (** [EqLam'] is displayed as the infix $\equiv$#~~#. *) Lemma EqLam'_refl (A: Set)(t: Lam' A): t ~~ t. Proof. reflexivity. Qed. Lemma EqLam'_sym (A: Set)(t1 t2: Lam' A): t1 ~~ t2 -> t2 ~~ t1. Proof. intros. symmetry. assumption. Qed. (** printing t3 %\ensuremath{t_3}% *) Lemma EqLam'_trans (A: Set)(t1 t2 t3: Lam' A): t1 ~~ t2 -> t2 ~~ t3 -> t1 ~~ t3. Proof. intros. red. transitivity (pi1 t2); assumption. Qed. Add Parametric Relation (A: Set): (Lam' A) (EqLam'(A:= A)) reflexivity proved by (EqLam'_refl(A:= A)) symmetry proved by (EqLam'_sym(A:= A)) transitivity proved by (EqLam'_trans(A:= A)) as bisimilarRel. (** we do not impose the following axiomatically *) Definition proof_irrelevance := forall (P: Prop) (p1 p2: P), p1 = p2. Definition Lam'pirrProp := forall (A: Set)(t1 t2: Lam' A), t1 ~~ t2 -> t1 = t2. Lemma Lam'pirrFromPirr: proof_irrelevance -> Lam'pirrProp. Proof. intro pirr. red. intros. destruct t1 as [t1' H1]. destruct t2 as [t2' H2]. red in H. simpl in H. revert H1 H2. destruct H. intros. rewrite (pirr _ H1 H2). reflexivity. Qed. (** Theorem 9 in the paper *) (** item 1: *) Lemma subst'ext' (A B: Set)(f g: A -> Lam' B)(t: Lam' A): (forall a, a occ' t -> f a ~~ g a) -> subst' f t ~~ subst' g t. Proof. intros. destruct t as (t', p'). red. simpl. apply substext'. intros. red in H. rewrite H. - reflexivity. - unfold occursFreeIn', FV'. simpl. assumption. Qed. Corollary subst'ext (A B: Set)(f g: A -> Lam' B)(t: Lam' A): (forall a, f a ~~ g a) -> subst' f t ~~ subst' g t. Proof. intros. apply subst'ext'. intros. apply H. Qed. (** item 2: *) Lemma subst'Gnat1 (A B C : Set) (f : A -> Lam' B) (g : B -> C) (t : Lam' A): lam' g (subst' f t) ~~ subst' (lam' g o f) t. Proof. destruct t as (t', p'). red. simpl. rewrite substGnat1. apply substext. intro. unfold comp. reflexivity. Qed. (** item 3: *) Lemma subst'Gnat2 (A B C: Set)(f: A -> B)(g: B -> Lam' C)(t: Lam' A): subst' g (lam' f t) ~~ subst' (g o f) t. Proof. destruct t as (t', p'). red. simpl. rewrite substGnat2. reflexivity. Qed. (** item 4: *) Definition monad3Lam': Prop := forall (A B C : Set) (f : A -> Lam' B) (g : B -> Lam' C) (t : Lam' A), subst' g (subst' f t) ~~ subst' (subst' g o f) t. Lemma subst'Monad3: monad3Lam'. Proof. red. intros. red. destruct t as (t', p). simpl. rewrite substMonad3. apply substext. intro. unfold comp. destruct (f a) as (b', p'). simpl. reflexivity. Qed. (** the lemmas that no longer need an explicit relativization to hereditarily canonical elements *) (** item 5: *) Lemma subst'Monad2 (A: Set)(t: Lam' A): subst' (var'(A:= A)) t ~~ t. Proof. red. rewrite subst'_ok. transitivity (subst (var(A:= A)) (pi1 t)). - apply substext. reflexivity. - apply substMonad2. unfold pi1. apply proj2_sig. Qed. (** item 6: *) Lemma lam'_is_subst' (A B: Set)(f: A -> B)(t: Lam' A): lam' f t ~~ subst' (var'(A:= B) o f) t. Proof. red. rewrite lam'_ok. rewrite subst'_ok. rewrite lam_is_subst. - reflexivity. - unfold pi1. apply proj2_sig. Qed. (** item 7: *) Lemma subst'_flat' (A B: Set)(f: A -> Lam' B)(ee: Lam'(Lam' A)): subst' f (flat' ee) ~~ flat' (lam' (subst' f) ee). Proof. destruct ee as (ee', p). red. simpl. rewrite subst_flat'. - do 2 rewrite <- lamfct2. f_equal. - apply lam_can. assumption. Qed. (** This completes Theorem 9 of the paper. *) Lemma lam'_var (A B: Set)(f: A -> B)(a: A) : lam' f (var' a) ~~ var' (f a). Proof. red. simpl. apply lam_var. Qed. Lemma lam'_app (A B: Set)(f: A -> B)(t1 t2: Lam' A): lam' f (app' t1 t2) ~~ app' (lam' f t1)(lam' f t2). Proof. destruct t1 as [t1' p1]. destruct t2 as [t2' p2]. red. simpl. apply lam_app. Qed. Lemma lam'_abs (A B: Set)(f: A -> B)(r: Lam'(option A)): lam' f (abs' r) ~~ abs' (lam' (option_map f) r). Proof. destruct r as [r' p]. red. simpl. apply lam_abs. Qed. Lemma lam'_flat (A B: Set)(f: A -> B)(ee: Lam'(Lam' A)): lam' f (flat' ee) ~~ flat' (lam' (lam' f) ee). Proof. destruct ee as [ee' p]. red. simpl. rewrite lam_flat. f_equal. do 2 rewrite <- lamfct2. apply lamext. intro t. unfold comp. rewrite lam'_ok. reflexivity. Qed. Lemma lam'ext_refined (A B: Set)(f g: A -> B)(t: Lam' A): (forall a, a occ' t -> f a = g a) -> lam' f t ~~ lam' g t. Proof. intros. red. do 2 rewrite lam'_ok. apply lamext_refined. - destruct t. assumption. - assumption. Qed. Corollary lam'ext (A B: Set)(f g: A -> B): (forall a, f a = g a) -> forall r, lam' f r ~~ lam' g r. Proof. intros. apply lam'ext_refined. intros. apply H. Qed. Lemma lam'fct1 (A: Set)(t: Lam' A): lam' id t ~~ t. Proof. destruct t as (t', p). red. simpl. apply lamfct1. Qed. Lemma lam'fct2 (A B C : Set) (f : A -> B) (g : B -> C) (t : Lam' A): lam' (g o f) t ~~ lam' g (lam' f t). Proof. destruct t as (t', p). red. simpl. apply lamfct2. Qed. Definition lift' (A B: Set)(f: A -> Lam' B)(x: option A): Lam'(option B) := match x with | None => var' None | Some a => lam' Some (f a) end. Lemma lift'_ok (A B: Set)(f: A -> Lam' B)(x: option A): pi1 (lift' f x) = lift (pi1 o f) x. Proof. destruct x. - simpl. reflexivity. - reflexivity. Qed. Lemma subst'Monad1 (A B: Set)(f: A -> Lam' B)(a: A): subst' f (var' a) ~~ f a. Proof. red. simpl. rewrite subst_var. reflexivity. Qed. (* now just a repetition: *) Lemma subst'_var (A B: Set)(f: A -> Lam' B)(a: A): subst' f (var' a) ~~ f a. Proof. apply subst'Monad1. Qed. Lemma subst'_app (A B: Set)(f: A -> Lam' B)(t1 t2: Lam' A): subst' f (app' t1 t2) ~~ app' (subst' f t1)(subst' f t2). Proof. destruct t1 as [t1' p1]. destruct t2 as [t2' p2]. red. simpl. apply subst_app. Qed. Lemma subst'_abs (A B: Set)(f: A -> Lam' B)(r: Lam'(option A)): subst' f (abs' r) ~~ abs' (subst' (lift' f) r). Proof. destruct r as [r' p]. red. simpl. rewrite subst_abs. f_equal. apply substext. intro. rewrite lift'_ok. reflexivity. Qed. Lemma subst'_flat (A B: Set)(f: A -> Lam' B)(ee: Lam'(Lam' A)): subst' f (flat' ee) ~~ flat' (subst' (var'(A:= Lam' B) o (subst' f)) ee). Proof. destruct ee as [ee' p]. red. simpl. rewrite subst_flat. f_equal. rewrite substGnat1. rewrite substGnat2. apply substext. intro t. unfold comp. rewrite lam_var. destruct t as (t', p'). simpl. reflexivity. Qed. (* Is there a problem with the syntax here? Add Parametric Morphism (A: Set): (@flat' A) with signature (@EqLam'(Lam' A)) ==> (@EqLam' A) as flat'M. Proof. red. intros. simpl. f_equal. rewrite H. reflexivity. Qed. Lemma subst'_flat_ALT (A B: Set)(f: A -> Lam' B)(ee: Lam'(Lam' A)): subst' f (flat' ee) ~~ flat' (subst' (var'(A:= Lam' B) o (subst' f)) ee). Proof. intros. transitivity (flat' (lam' (subst' f) ee)). apply subst'_flat'. rewrite lam'_is_subst'. reflexivity. Qed. *) (** Section 5.3 of the paper *) Definition LamFmon2br: mon2br LamF. Proof. red. red. intros X Y mY f A t. destruct t as [[[a|( t1, t2)]|r]|ee]. - unfold LamF. left; left; left. assumption. - left; left; right. exact (f A t1, f A t2). - left; right. exact (f (option A) r). - exact (inr _ (mY _ _ (f A) (f (X A) ee))). Defined. Definition LamToCan: Lam c_k1 Lam := LamMMItDef.canonize LamFmon2br. Lemma LamToCan_var (A: Set)(a: A): LamToCan(var a) = var a. Proof. unfold var. unfold LamToCan. unfold LamMMItDef.canonize. rewrite LamMMItDef.MItRedCan. reflexivity. Qed. Lemma LamToCan_app (A: Set)(t1 t2: Lam A): LamToCan(app t1 t2) = app (LamToCan t1) (LamToCan t2). Proof. unfold app. unfold LamFlat.app. unfold LamToCan at 1. unfold LamMMItDef.canonize. rewrite LamMMItDef.MItRedCan. reflexivity. Qed. Lemma LamToCan_abs (A: Set)(r: Lam (option A)): LamToCan(abs r) = abs(LamToCan r). Proof. unfold abs. unfold LamToCan at 1. unfold LamMMItDef.canonize. rewrite LamMMItDef.MItRedCan. reflexivity. Qed. Lemma LamToCan_flat (A: Set)(ee: Lam (Lam A)): LamToCan(flat ee) = flat (lam (LamToCan(A:= A)) (LamToCan ee)). Proof. unfold flat. unfold LamToCan at 1. unfold LamMMItDef.canonize. rewrite LamMMItDef.MItRedCan. reflexivity. Qed. (** canonical elements are not changed by canonization *) Theorem LamToCan_invariant (A: Set)(t: Lam A): can t -> LamToCan t = t. Proof. intros. induction H. - apply LamToCan_var. - rewrite LamToCan_app. rewrite IHcan1. rewrite IHcan2. reflexivity. - rewrite LamToCan_abs. rewrite IHcan. reflexivity. - rewrite LamToCan_flat. rewrite IHcan. f_equal. transitivity (lam (id(A:= Lam A)) ee). + apply lamext_refined. * assumption. * intros t Hyp. apply H1. assumption. + apply lamfct1. Qed. (** canonization yields hereditarily canonical elements *) Theorem LamToCanCan (A: Set)(t: Lam A): can (LamToCan t). Proof. revert A t. (* new in 8.3 *) apply (LamBase.mu2Ind (fun A t => can (LamToCan t))). intros; destruct t as [[[a|( t1, t2)]|r]|ee]; unfold LamToCan; unfold LamMMItDef.canonize; rewrite LamBase.MItRed; simpl LamFmon2br. - assert (can (var a)) by (apply can_var). assumption. - assert (can (app (LamToCan (j A t1)) (LamToCan (j A t2)))) by (apply can_app; apply H). apply H0. - assert (can (abs (LamToCan (j (option A) r)))). { apply can_abs. apply H. } apply H0. - assert (can (flat (lam (LamToCan(A:= A) o j A) (LamToCan (j (X A) ee))))). { apply can_flat. + apply lam_can. apply H. + intros. destruct (lam_occ (LamToCan (A:= A) o j A) (LamToCan (j (X A) ee)) t H0). destruct H1. rewrite H2. unfold comp. apply H. } apply H0. Qed. (** canonization can be expressed as follows: *) Definition LamToLam': Lam c_k1 Lam'. Proof. red. intros A t. exists (LamToCan t). apply LamToCanCan. Defined. Lemma LamToLam'_ok (A: Set)(t: Lam A): pi1 (LamToLam' t) = LamToCan t. Proof. reflexivity. Qed. Scheme canInd := Induction for can Sort Prop. Definition IsConstructed' (A: Set)(t: Lam' A) : Prop := (exists a: A, t = var' a) \/ (exists t1, exists t2, t = app' t1 t2) \/ (exists r, t = abs' r) \/ (exists ee, t ~~ flat' ee). (* Note ~~ in the last disjunct! *) Lemma Lam'exhausted (A: Set)(t: Lam' A): IsConstructed' t. Proof. destruct t as (t', p). induction p using canInd. - (* var *) left. exists a. reflexivity. - (* app *) clear IHp1 IHp2. right; left. exists (exist (fun t : Lam A => can t) t1 p1). exists (exist (fun t : Lam A => can t) t2 p2). reflexivity. - (* abs *) clear IHp. right; right; left. exists (exist (fun t : Lam(option A) => can t) r p). reflexivity. - (* flat *) clear IHp H. right; right; right. set (ee0':= lam (LamToLam'(A:= A)) ee). set (p':= lam_can (LamToLam'(A:= A)) p: can ee0'). exists (exist (fun t : Lam (Lam' A) => can t) ee0' p'). red; simpl. f_equal. unfold ee0'. rewrite <- lamfct2. transitivity (lam (id(A:= Lam A)) ee). + rewrite lamfct1. reflexivity. + apply lamext_refined. * assumption. * intros t Hyp. unfold comp. rewrite LamToLam'_ok. rewrite LamToCan_invariant. -- reflexivity. -- exact (c t Hyp). Qed. End LamFlat.