(** EFlatCoqRecPred.v Version 1.0 January 2008 *) (** does not need impredicative Set, runs under V8.1, tested with 8.1pl3 *) (** We illustrate how MRec allows a different definition of eval but show that the new and the old eval agree on all arguments. *) (** Copyright Ralph Matthes, I.R.I.T., C.N.R.S. & University of Toulouse *) Set Implicit Arguments. Require Import LNMItPred. Require Import LNMRecPred. Require Import EFlatCoqPred. Module Type LAMERec := LNMRec_Type with Definition F:=LamEFlatF with Definition FpEFct := lamEFlatpEFct. (** we base this on a hypothetical implementation of LAMERec *) Module EFlatRec (LamERecBase:LAMERec). Import LamERecBase. Module LamERecDef := LNMRecDef LamERecBase. Import LamERecDef. Module LamEBase := LNMItFromRec LamERecBase. Module LamEDef := LNMItPred.LNMItDef LamEBase. Module EFlat := EFlat LamEBase. Import EFlat. (** for an even cleaner comparison, we define a slight variant eval1 of eval *) Definition eval1: LamE c_k1 Lam. Proof. refine (LamEBase.MIt (fun (X:k1)(it: X c_k1 Lam)(A:Set)(t:LamEFlatF 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 (id(A:=Lam A)) (lam (it A) (it (X A) ee))). Defined. (** note that subst id is the "real" flattening operation on Lam *) (** the intended behaviour of eval1 on terms of the form flat ee *) Lemma eval1Flat (A:Set)(ee:LamE(LamE A)): eval1 (flat ee) = subst (id(A:=Lam A)) (lam (eval1(A:=A)) (eval1 ee)). Proof. intros. unfold eval1 at 1. unfold flat. rewrite LamEM.MItRedCan. reflexivity. Qed. Lemma evaleval1 (A:Set)(t: LamE A): eval t = eval1 t. Proof. intros. unfold eval1. apply LamEDef.MItUni; clear A t. (* extensionality *) red. intros. destruct y as [[[a|(t1,t2)]|r]|ee]. reflexivity. do 2 rewrite H. reflexivity. rewrite H. reflexivity. rewrite H. rewrite (lamext (f A) (g A)). reflexivity. apply H. (* behaviour *) intros. destruct t as [[[a|(t1,t2)]|r]|ee]; try (unfold eval; rewrite LamEBase.MItRed; reflexivity). unfold eval at 1. rewrite LamEBase.MItRed. rewrite <- substLaw1Inst. reflexivity. Qed. Corollary eval1NAT: NAT eval1 lamE lam. Proof. red. intros. do 2 rewrite <- evaleval1. apply evalNAT. Qed. Lemma eval1NATcor (A:Set)(ee:LamE(LamE A)): eval1 (flat ee) = subst (id(A:= Lam A)) (eval1 (lamE (eval1(A:=A)) ee)). Proof. intros. rewrite eval1Flat. rewrite eval1NAT. reflexivity. Qed. (** evaluation of explicit flattening with access to the monotonicity witness for X *) Definition eval1': LamE c_k1 Lam. Proof. refine (LamERecBase.MRec (fun (X:k1)(mX:mon X)(j: X c_k1 LamE)(rec: X c_k1 Lam) (A:Set)(t:LamEFlatF X A) => _)). destruct t as [[[a|(t1,t2)]|r]|ee]. exact (var a). exact (app (rec _ t1)(rec _ t2)). exact (abs (rec _ r)). exact (subst (id(A:=Lam A)) (rec (Lam A) (mX (X A) (Lam A) (rec A) ee))). Defined. (** note that we do not use the j argument and hence do not make use of the primitive recursion facility *) (* Print eval1'. *) (** We discover the outcome of this interactive definition: *) Definition s_eval1'_base: forall (X:k1), mon X -> X c_k1 Lam -> LamEFlatF X c_k1 Lam:= fun (X : k1) (mX : mon X)(it : X c_k1 Lam) (A : Set) (t : LamEFlatF 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 (id (A:=Lam A)) (it (Lam A) (mX (X A) (Lam A) (it A) ee)) end. Lemma s_eval1'_base_ok: eval1' = MItpl s_eval1'_base. Proof. reflexivity. Qed. (** the intended behaviour of eval1' on terms of the form flat ee *) Lemma eval1'Flat (A:Set)(ee:LamE(LamE A)): eval1' (flat ee) = subst (id(A:=Lam A)) (eval1'(A:=Lam A) (lamE (eval1'(A:=A)) ee)). Proof. intros. unfold eval1' at 1. unfold flat. rewrite MRecRedCan. reflexivity. Qed. (** eval1' is a natural transformation *) Lemma eval1'NAT: NAT eval1' lamE lam. Proof. unfold eval1'. apply MRecNAT. red. intros. clear H. destruct ef as [m0 e0 f01 f02]. simpl in H0. destruct t as [[[a|(t1,t2)]|r]|ee]; simpl. reflexivity. do 2 rewrite H0. reflexivity. unfold moncomp. rewrite H0. reflexivity. unfold moncomp at 1. rewrite H0. unfold id at 2. rewrite <- (substNAT(mX:=lam)(j:=fun A r => r)). f_equal. unfold moncomp. do 2 rewrite H0. do 2 rewrite <- lamfct2. apply lamext. intro. unfold comp. rewrite H0. apply lamext. reflexivity. red. reflexivity. Qed. (** the now less intended behaviour of eval1' on terms of the form flat ee *) Lemma eval1'NATcor (A:Set)(ee:LamE(LamE A)): eval1' (flat ee) = subst (id(A:=Lam A)) (lam (eval1'(A:=A)) (eval1' ee)). Proof. intros. rewrite eval1'Flat. rewrite eval1'NAT. reflexivity. Qed. (** we first give a proof by help of MItUni *) Lemma eval1eval1' (A:Set)(t: LamE A): eval1 t = eval1' t. Proof. intros. apply sym_eq. unfold eval1. apply LamEDef.MItUni; clear A t. (* extensionality *) red. intros. destruct y as [[[a|(t1,t2)]|r]|ee]. reflexivity. do 2 rewrite H. reflexivity. rewrite H. reflexivity. rewrite H. rewrite (lamext (f A) (g A)). reflexivity. apply H. (* behaviour *) intros. destruct t as [[[a|(t1,t2)]|r]|ee]; try (unfold eval1'; rewrite MRecRed; reflexivity). (** we now need eval1'NATcor even for non-canonical elements *) transitivity (subst (id(A:=Lam A)) ((eval1'(A:=Lam A) o j (Lam A)) (m ef (eval1'(A:=A) o j A) ee))). unfold eval1' at 1. rewrite MRecRed. reflexivity. unfold comp at 1. rewrite n. rewrite eval1'NAT. reflexivity. Qed. (** alternatively, we can use uniqueness of eval1': *) Lemma eval1eval1'_ALT (A:Set)(t: LamE A): eval1 t = eval1' t. Proof. unfold eval1'. apply MRecUni. (* extensionality *) red. intros. destruct y as [[[a|(t1,t2)]|r]|ee]. reflexivity. do 2 rewrite H. reflexivity. rewrite H. reflexivity. rewrite H. rewrite (e ef (f A) (g A)). reflexivity. apply H. (* behaviour *) intros. destruct t as [[[a|(t1,t2)]|r]|ee]; try (unfold eval1; rewrite LamEBase.MItRed; reflexivity). (** we now need eval1NATcor even for non-canonical elements *) transitivity (subst (id (A:=Lam A)) (lam (eval1 (A:=A) o j A) ((eval1 (A:=X A) o j (X A)) ee))). unfold eval1 at 1. rewrite LamEBase.MItRed. reflexivity. unfold comp at 2. rewrite <- eval1NAT. unfold comp at 2. rewrite n. reflexivity. Qed. (** a test of MMIt *) Definition LamEFlatFmonbr2: mon2br LamEFlatF. Proof. red. red. intros X Y mY f A t. destruct t as [[[a|(t1,t2)]|r]|ee]. left. left. left. assumption. left. left. right. exact (f _ t1, f _ t2). left. right. exact (f _ r). right. exact (mY _ _ (f A) (f (X A) ee)). Defined. Definition eval1'': LamE c_k1 Lam := MMIt LamEFlatFmonbr2 lam s_eval1'_base. (** hence, all of the branches are as in the definition of eval1' *) (** we now see that eval1'' behaves nearly as eval1 *) Lemma eval1''_flat (A:Set)(ee:LamE(LamE A)): eval1'' (flat ee) = subst (id(A:=Lam A)) (lam (id (A:=Lam A)) (lam (eval1''(A:=A)) (eval1'' ee))). (* not exactly as eval1, i.e., subst (id(A:=Lam A)) (lam (eval1''(A:=A)) (eval1'' ee)) and not as eval1', i.e., subst (id(A:=Lam A)) (eval1''(A:=Lam A) (lamE (eval1''(A:=A)) ee)) *) Proof. intros. unfold eval1'' at 1. unfold flat. rewrite MMItRedCan. reflexivity. Qed. (** the behaviour of eval1 only comes with the first functor law for lam: *) Lemma eval1''_flat' (A:Set)(ee:LamE(LamE A)): eval1'' (flat ee) = subst (id(A:=Lam A)) (lam (eval1''(A:=A)) (eval1'' ee)). Proof. intros. rewrite eval1''_flat. rewrite lamfct1. (** this is an unfriendly artifact of the construction! *) reflexivity. Qed. (** alternatively, one could have used the second functor law and extensionality of lam *) (** here, we verify the suspicion that eval1'' and eval1 agree on all arguments; note that this cannot be the basis for a general theorem since eval1 is defined from a different step term *) Lemma eval1''eval1 (A:Set)(t: LamE A): eval1'' t = eval1 t. Proof. intros. unfold eval1. apply LamEDef.MItUni; clear A t. (* extensionality *) red. intros. destruct y as [[[a|(t1,t2)]|r]|ee]. reflexivity. do 2 rewrite H. reflexivity. rewrite H. reflexivity. rewrite H. rewrite (lamext (f A) (g A)). reflexivity. apply H. (* behaviour *) intros. destruct t as [[[a|(t1,t2)]|r]|ee]; try (unfold eval1''; unfold MMIt; rewrite LamEBase.MItRed; reflexivity). (** we now need eval1''_flat' even for non-canonical elements *) unfold eval1'' at 1. unfold MMIt. rewrite LamEBase.MItRed. unfold s_MMIt at 1; unfold LamEFlatFmonbr2 at 1. unfold s_eval1'_base at 1. change (fun x: Lam A => x) with (id(A:=Lam A)). rewrite lamfct1. (** again the artifact *) reflexivity. Qed. Definition lamEFct : EFct Lam := mkEFct lamext lamfct1 lamfct2. (** we now use the general result *) Lemma eval1''eval1' (A:Set)(t: LamE A): eval1'' t = eval1' t. Proof. intros. unfold eval1''. change eval1' with (MItpl s_eval1'_base). refine (MMItsMItpls _ _ _ lamEFct _ _ _ _ t); clear A t; try reflexivity. (* naturality *) red. intros. destruct t as [[[a|(t1,t2)]|r]|ee]. reflexivity. simpl lam. do 2 rewrite <- H. induction ef. reflexivity. simpl lam. rewrite <- H. reflexivity. induction ef. simpl. simpl in H. unfold moncomp. do 3 rewrite H. rewrite substLaw2. rewrite <- lamfct2. do 2 rewrite substLaw1. apply substext. intro. unfold comp. unfold id. transitivity (lam (fun x => f x) (it A a)). apply H. apply lamext. reflexivity. (* about LamEFlatFmonbr2 *) red. intros. destruct t as [[[a|(t1,t2)]|r]|ee]; simpl. reflexivity. induction ef. simpl. simpl in H. do 2 rewrite H. reflexivity. induction ef. simpl. simpl in H. unfold moncomp. rewrite H. reflexivity. induction ef. simpl. simpl in H. unfold moncomp. rewrite H. do 2 rewrite <- lamfct2. f_equal. apply lamext. intro. unfold comp. apply H. (* extensionality *) red. intros. destruct y as [[[a|(t1,t2)]|r]|ee]; unfold s_eval1'_base. reflexivity. do 2 rewrite H. reflexivity. rewrite H. reflexivity. rewrite H. rewrite (e ef (f A) (g A)). reflexivity. apply H. (* behaviour *) intros. destruct t as [[[a|(t1,t2)]|r]|ee]; try reflexivity. simpl. change (fun x : Lam A => x) with (id(A:=Lam A)). rewrite lamfct1. rewrite H. reflexivity. Qed. (** we have to reproduce the first two parts of the above proof in the following proof: *) Lemma eval1''NAT: NAT eval1'' lamE lam. Proof. unfold eval1''. refine (MMItsNAT(mG:=lam) LamEFlatFmonbr2 _ _ lamEFct (refl_equal _) _). (* about the step term *) red. intros. destruct t as [[[a|(t1,t2)]|r]|ee]. reflexivity. simpl lam. do 2 rewrite <- H. induction ef. reflexivity. simpl lam. rewrite <- H. reflexivity. induction ef. simpl. simpl in H. unfold moncomp. do 3 rewrite H. rewrite substLaw2. rewrite <- lamfct2. do 2 rewrite substLaw1. apply substext. intro. unfold comp. unfold id. transitivity (lam (fun x => f x) (it A a)). apply H. apply lamext. reflexivity. (* about LamEFlatFmonbr2 *) red. intros. destruct t as [[[a|(t1,t2)]|r]|ee]; simpl. reflexivity. induction ef. simpl. simpl in H. do 2 rewrite H. reflexivity. induction ef. simpl. simpl in H. unfold moncomp. rewrite H. reflexivity. induction ef. simpl. simpl in H. unfold moncomp. rewrite H. do 2 rewrite <- lamfct2. f_equal. apply lamext. intro. unfold comp. apply H. Qed. (** A direct naturality proof is much shorter: *) Lemma eval1''NAT_ALT: NAT eval1'' lamE lam. Proof. unfold eval1''. unfold MMIt. apply LamEDef.MItNAT. red. intros. destruct ef as [m0 e0 f01 f02]. simpl in H. destruct t as [[[a|(t1,t2)]|r]|ee]; unfold s_MMIt; unfold LamEFlatFmonbr2; simpl. reflexivity. do 2 rewrite H. reflexivity. unfold moncomp. rewrite H. reflexivity. unfold moncomp at 1. rewrite H. unfold id at 2. rewrite <- (substNAT(mX:=lam)(j:=fun A r => r)). f_equal. unfold moncomp. repeat rewrite <- lamfct2. apply lamext. intro. unfold comp. rewrite H. apply lamext. reflexivity. red. reflexivity. Qed. (** for the sake of completeness, the other datatype constructors are treated explicitly as well *) Definition varE (A:k0)(a:A): LamE A := LamEDef.InCan (inl _ (inl _ (inl _ a))). Definition appE (A:k0)(t1 t2:LamE A): LamE A := LamEDef.InCan (inl _ (inl _ (inr _ (t1,t2)))). Definition absE (A:k0)(r: LamE (option A)): LamE A := LamEDef.InCan (inl _ (inr _ r)). Lemma eval1'_var (A:k0)(a:A): eval1' (varE a) = var a. Proof. intros. unfold eval1'. unfold varE. rewrite MRecRedCan. reflexivity. Qed. Lemma eval1'_app (A:k0)(t1 t2:LamE A): eval1' (appE t1 t2) = app (eval1' t1) (eval1' t2). Proof. intros. unfold eval1' at 1. unfold appE. rewrite MRecRedCan. reflexivity. Qed. Lemma eval1'_abs (A:k0)(r:LamE (option A)): eval1' (absE r) = abs (eval1' r). Proof. intros. unfold eval1' at 1. unfold absE. rewrite MRecRedCan. reflexivity. Qed. Lemma eval1''_var (A:k0)(a:A): eval1'' (varE a) = var a. Proof. intros. unfold eval1''. unfold varE. rewrite MMItRedCan. reflexivity. Qed. Lemma eval1''_app (A:k0)(t1 t2:LamE A): eval1'' (appE t1 t2) = app (eval1'' t1) (eval1'' t2). Proof. intros. unfold eval1'' at 1. unfold appE. rewrite MMItRedCan. reflexivity. Qed. Lemma eval1''_abs (A:k0)(r:LamE (option A)): eval1'' (absE r) = abs (eval1'' r). Proof. intros. unfold eval1'' at 1. unfold absE. rewrite MMItRedCan. reflexivity. Qed. End EFlatRec.