(** EFlatCoqPred.v Version 2.1.1 December 2012 *) (** does not need impredicative Set, runs under V8.4, tested with 8.4pl1 *) (** Copyright Ralph Matthes, I.R.I.T., C.N.R.S. & University of Toulouse *) (** illustrates how Coq directly supports Lam and extends this to LamE that has explicit flattening *) (** this is code that conforms to the description in the article "An induction principle for nested datatypes in intensional type theory" by the author, to appear in the Journal of Functional Programming *) Set Implicit Arguments. Require Import LNMItPred. (** we use the direct support of heterogeneous families of datatypes that has been introduced into Coq V8.1 *) (** the standard representation of untyped lambda-calculus by a nested datatype *) Inductive Lam (A:Set) : Set := | var : A -> Lam A | app : Lam A -> Lam A -> Lam A | abs : Lam (option A) -> Lam A. (** the mapping operation for Lam *) Fixpoint lam (A B:Set)(f:A->B)(t:Lam A) : Lam B := match t with | var a => var (f a) | app t1 t2 => app (lam f t1)(lam f t2) | abs r => abs (lam (option_map f) r) end. Lemma lamext: ext lam. Proof. red. intros. generalize B f g H. clear B f g H. induction r; intros; simpl. rewrite H. reflexivity. rewrite (IHr1 B f g H). rewrite (IHr2 B f g H). reflexivity. rewrite (IHr (option B)(option_map f)(option_map g)). reflexivity. intro. change (option_map f a) with (m optionEFct f a). change (option_map g a) with (m optionEFct g a). apply (e optionEFct); assumption. Qed. Lemma lamfct1: fct1 lam. Proof. red. intros. induction x; simpl. reflexivity. rewrite IHx1. rewrite IHx2. reflexivity. f_equal. replace (lam (option_map (id (A:=A))) x) with (lam (id (A:=option A)) x). assumption. apply lamext. intro. set (H:=f1 optionEFct). unfold fct1 in H. simpl m in H. rewrite H. reflexivity. Qed. Lemma lamfct2 : fct2 lam. Proof. red. intros. generalize B C f g. clear B C f g. induction x; intros; simpl. reflexivity. rewrite IHx1. rewrite IHx2. reflexivity. rewrite <- IHx. f_equal. apply lamext. intro. unfold comp at 2. set (H:=f2 optionEFct). unfold fct2 in H. simpl m in H. apply H. Qed. (** towards substitution *) 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(A:=B)) (f a) end. Fixpoint subst (A B:Set)(f:A -> Lam B)(t:Lam A) :Lam B := match t with | var a => f a | app t1 t2 => app (subst f t1)(subst f t2) | abs r => abs (subst (lift f) r) end. Lemma liftext (A B:Set)(f g:A -> Lam B)(x:option A): (forall a, f a = g a) -> lift f x = lift g x. Proof. intros. destruct x. simpl. rewrite H. reflexivity. reflexivity. Qed. 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. generalize B f g H; clear B f g H. induction t; intros; simpl. apply H. rewrite (IHt1 B f g H). rewrite (IHt2 B f g H). reflexivity. rewrite (IHt (option B)(lift f)(lift g)). reflexivity. intro. apply liftext; assumption. Qed. (* a more fine-grained version of the substitution lemma, based on free variable occurrences *) Inductive occursFreeIn: forall (A:Set), A -> Lam A -> Prop := | occ_var: forall (A:Set)(a:A), occursFreeIn a (var a) | occ_appl: forall (A:Set)(a:A)(t1 t2:Lam A), occursFreeIn a t1 -> occursFreeIn a (app t1 t2) | occ_appr: forall (A:Set)(a:A)(t1 t2:Lam A), occursFreeIn a t2 -> occursFreeIn a (app t1 t2) | occ_abs: forall (A:Set)(a:A)(r:Lam(option A)), occursFreeIn (Some a) r -> occursFreeIn a (abs r). Infix "occ" := occursFreeIn (at level 90). (** an auxiliary lemma *) Lemma liftext' (A B:Set)(f g:A -> Lam B)(t:Lam(option A))(x:option A): x occ t -> (forall a, a occ (abs t) -> f a = g a) -> lift f x = lift g x. Proof. intros. destruct x. simpl. rewrite H0. reflexivity. apply occ_abs; assumption. reflexivity. Qed. 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. generalize B f g H; clear B f g H. induction t; intros; simpl. apply H. apply occ_var. (* app *) rewrite (IHt1 B f g). rewrite (IHt2 B f g). reflexivity. intros. apply H. apply occ_appr. assumption. intros. apply H. apply occ_appl. assumption. (* abs *) rewrite (IHt (option B)(lift f)(lift g)). reflexivity. intros. apply (liftext' f g H0 H). Qed. (** Remark: this lemma will not be needed in the sequel *) (** interaction of subst with lam *) Lemma substLaw1 (A B C:k0)(f: A -> B)(g:B -> Lam C)(t: Lam A): subst g (lam f t) = subst (g o f) t. Proof. intros. generalize B C f g; clear B C f g. induction t; intros; simpl. reflexivity. rewrite IHt1. rewrite IHt2. reflexivity. unfold k0 in B. (* this is necessary! *) f_equal. rewrite IHt. apply substext. intro. destruct a; reflexivity. Qed. (* a useful instance *) Lemma substLaw1Inst (A B:Set)(f: A -> Lam B)(t: Lam A): subst (id(A:=Lam B)) (lam f t) = subst f t. Proof. intros. rewrite substLaw1. apply substext. reflexivity. Qed. Lemma substLaw2: forall (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. intros. generalize B C f g; clear B C f g. induction t; intros; simpl. reflexivity. rewrite IHt1. rewrite IHt2. reflexivity. f_equal. rewrite IHt. apply substext. intro. destruct a. unfold comp. simpl. do 2 rewrite <- lamfct2. reflexivity. reflexivity. Qed. (** we use moncomp from LNMItPred.v *) Lemma substNAT (X:k1)(mX: mon X)(j:X c_k1 Lam)(n: NAT j mX lam): NAT (fun A=> subst (j A)) (moncomp lam mX) lam. Proof. red. intros. unfold moncomp. transitivity (subst (lam f o j A) t). rewrite substLaw1. apply substext. intro. unfold comp. apply n. (* the second part *) apply sym_eq. apply substLaw2. Qed. (** Just before embarking on explicit flattening, we verify the monad laws for substitution. *) Lemma substMonad1 (A B:Set)(f:A -> Lam B)(a:A): subst f (var a) = f a. Proof. reflexivity. Qed. Lemma substMonad2 (A:Set)(t:Lam A): subst (var(A:=A)) t = t. Proof. intros. induction t; simpl. reflexivity. rewrite IHt1. rewrite IHt2. reflexivity. f_equal. transitivity (subst (var(A:=option A)) t). apply substext. intro. destruct a; reflexivity. assumption. Qed. 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. intros. generalize B C f g; clear B C f g. induction t; intros; simpl. reflexivity. rewrite IHt1. rewrite IHt2. reflexivity. rewrite IHt. f_equal. apply substext. clear t IHt. intro. destruct a. unfold comp. simpl. rewrite substLaw2. rewrite substLaw1. apply substext. reflexivity. reflexivity. Qed. (** the monad laws will not be used in the sequel *) (** introduce explicit flattening that is not directly covered by Coq *) Definition LamEFlatF(X:k1)(A:Set) := (A + X A * X A + X(option A) + X (X A))%type. Definition lamEFlatpEFct : pEFct LamEFlatF. Proof. unfold LamEFlatF. apply sumpEFct. apply sumpEFct. apply sumpEFct. apply constpEFct. apply idEFct. apply prodpEFct. apply idpEFct_eta. apply idpEFct_eta. apply comppEFct. apply idpEFct. apply constpEFct. apply optionEFct. apply comppEFct. apply idpEFct. apply comppEFct. apply idpEFct. apply constpEFct. apply idEFct. Defined. Module Type LAME := LNMIt_Type with Definition F:=LamEFlatF with Definition FpEFct := lamEFlatpEFct. (** we base this on a hypothetical implementation of LAME *) Module EFlat (LamEBase:LAME). Module LamEM := LNMItDef LamEBase. Definition LamE : k1 := LamEBase.mu2. (** we just show the interesting new constructor for explicit flattening *) Definition flat (A:Set)(ee:LamE(LamE A)): LamE A := LamEM.InCan (inr _ ee). Definition lamE : mon LamE := LamEBase.mapmu2. (** evaluation of explicit flattening *) Definition eval: 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 (it A) (it (X A) ee)). Defined. (** the intended behaviour of eval on terms of the form flat ee *) Lemma evalFlat (A:Set)(ee:LamE(LamE A)): eval (flat ee) = subst (eval(A:=A)) (eval ee). Proof. intros. unfold eval at 1. unfold flat. rewrite LamEM.MItRedCan. reflexivity. Qed. (** eval is a natural transformation *) Lemma evalNAT: NAT eval lamE lam. Proof. unfold eval. apply LamEM.MItNAT. red. intros. destruct ef as [m0 e0 f01 f02]. simpl in H. destruct t as [[[a|(t1,t2)]|r]|ee]; simpl. reflexivity. do 2 rewrite H. reflexivity. unfold moncomp. rewrite H. reflexivity. unfold moncomp at 1. rewrite H. rewrite <- (substNAT H f (it (X A) ee)). f_equal. Qed. (** a less intended behaviour of eval on terms of the form flat ee; note that subst id is the "real" flattening operation on Lam *) Lemma evalNATcor (A:Set)(ee:LamE(LamE A)): eval (flat ee) = subst (id(A:= Lam A)) (eval (lamE (eval(A:=A)) ee)). Proof. intros. rewrite evalFlat. rewrite evalNAT. rewrite substLaw1Inst. reflexivity. Qed. End EFlat.