(** LNMRecPred.v Version 1.01 March 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*) (** We provide the predicative specification of LNMRec, discover it as an extension of LNMIt and infer general theorems from this specification. *) Require Import LNMItPred. Set Implicit Arguments. Module Type LNMRec_Type. (** the following are taken from LNMIt_Type: *) Parameter F:k2. Parameter FpEFct: pEFct F. Parameter mu20: k1. Definition mu2: k1:= fun A => mu20 A. Parameter mapmu2: mon mu2. Definition InType : Type := forall (G:k1)(ef:EFct G)(j: G c_k1 mu2), NAT j (m ef) mapmu2 -> F G c_k1 mu2. Parameter In : InType. Axiom mapmu2Red : forall (A:Set)(G:k1)(ef:EFct G)(j: G c_k1 mu2) (n: NAT j (m ef) mapmu2)(t: F G A)(B:Set)(f:A->B), mapmu2 f (In ef n t) =In ef n (m (FpEFct ef) f t). Definition mu2IndType : Prop := forall (P : (forall A : Set, mu2 A -> Prop)), (forall (X : k1)(ef:EFct X)(j : X c_k1 mu2)(n: NAT j (m ef) mapmu2), (forall (A : Set) (x : X A), P A (j A x)) -> forall (A:Set)(t : F X A), P A (In ef n t)) -> forall (A : Set) (r : mu2 A), P A r. Axiom mu2Ind : mu2IndType. (** the following are extensions of elements from LNMIt_Type: *) Definition MRecType: Type := forall G : k1, (forall X : k1, mon X -> X c_k1 mu2 -> X c_k1 G -> F X c_k1 G) -> mu2 c_k1 G. Parameter MRec0 : MRecType. (** we need just its eta-expansion MRec *) Definition MRec : MRecType := fun G s A t => MRec0 s t. Axiom MRecRed : forall (G : k1) (s : forall X : k1, mon X -> X c_k1 mu2 -> X c_k1 G -> F X c_k1 G)(X : k1)(ef:EFct X)(j: X c_k1 mu2) (n: NAT j (m ef) mapmu2)(A:Set)(t:F X A), MRec s (In ef n t) = s X (m ef) j (fun A => (MRec s (A:=A)) o (j A)) A t. End LNMRec_Type. Module LNMItFromRec(M:LNMRec_Type) <: LNMIt_Type. Import M. (* we need to establish LNMItFromRec as a subtype of LNMIt_Type *) Module LNM <: LNMIt_Type. Definition F:=F. Definition FpEFct:= FpEFct. Definition mu20 := mu20. Definition mu2 := mu2. Definition mapmu2 := mapmu2. Definition InType := InType. Definition In := In. Definition mapmu2Red:=mapmu2Red. Definition mu2IndType:=mu2IndType. Definition mu2Ind:=mu2Ind. Definition MItType: Type := forall G : k1, (forall X : k1, X c_k1 G -> F X c_k1 G) -> mu2 c_k1 G. Definition MIt0 := fun (G:k1) s (A:k0) => MRec(G:=G)(A:=A) (fun X m j => s X). Definition MIt : MItType:= fun G s A t => MIt0 s t. Lemma MItRed : forall (G : k1) (s : forall X : k1, X c_k1 G -> F X c_k1 G)(X : k1)(ef:EFct X)(j: X c_k1 mu2) (n: NAT j (m ef) mapmu2)(A:Set)(t:F X A), MIt s (In ef n t) = s X (fun A => (MIt s (A:=A)) o (j A)) A t. Proof. intros. unfold MIt. unfold MIt0. rewrite MRecRed. reflexivity. Qed. End LNM. Import LNM. Definition F:=F. Definition FpEFct:= FpEFct. Definition mu20 := mu20. Definition mu2 := mu2. Definition mapmu2 := mapmu2. Definition MItType:= MItType. Definition MIt0 := MIt0. Definition MIt := MIt. Definition InType := InType. Definition In := In. Definition mapmu2Red:=mapmu2Red. Definition MItRed:=MItRed. Definition mu2IndType:=mu2IndType. Definition mu2Ind:=mu2Ind. End LNMItFromRec. Module LNMRecDef (M:LNMRec_Type). Import M. Module LNMItBase := LNMItFromRec M. Module LNMItDef := LNMItDef LNMItBase. Import LNMItDef. Section MRec. (** the behaviour for canonical elements *) Lemma MRecRedCan : forall (G:k1)(s:forall X:k1, mon X -> X c_k1 mu2 -> X c_k1 G -> F X c_k1 G) (A:Set)(t:F mu2 A), MRec s (InCan t) = s mu2 mapmu2 (fun A r=> r) (MRec s) A t. Proof. intros. unfold InCan. rewrite MRecRed. reflexivity. (* here, we needed the eta-expansion for MRec *) Qed. (** MRecRed already characterizes MRec s under an extensionality assumption for s: *) Theorem MRecUni: forall (G : k1)(s : forall X : k1, mon X -> X c_k1 mu2 -> X c_k1 G -> F X c_k1 G) (h: mu2 c_k1 G), (forall (X:k1)(ef:EFct X)(j: X c_k1 mu2), polyExtsub(s X (m ef) j)) -> (forall (A : Set)(X : k1)(ef: EFct X)(j: X c_k1 mu2) (n:NAT j (m ef) mapmu2)(t:F X A), h A (In ef n t) = s X (m ef) j (fun A => (h A) o (j A)) A t) -> forall (A:Set)(r: mu2 A), h A r = MRec s r. Proof. intros G s h sExt H. apply (mu2Ind (fun A r => h A r = MRec s r)). intros X ef j n IH A t. rewrite H. rewrite MRecRed. apply sExt. clear A t. intros. unfold comp. apply IH. Qed. (** provide naturality of MRec s *) Section MRecNAT. Variable G:k1. Variable s: forall X : k1, mon X -> X c_k1 mu2 -> X c_k1 G -> F X c_k1 G. Variable mG: mon G. Variable smGpNAT : forall (X:k1)(ef: EFct X)(j: X c_k1 mu2)(rec: X c_k1 G), NAT j (m ef) mapmu2 -> NAT rec (m ef) mG -> NAT (s (m ef) j rec) (m (FpEFct ef)) mG. Theorem MRecNAT : NAT (MRec s) mapmu2 mG. Proof. red. intros A B f r. generalize B f; clear B f. apply (mu2Ind (fun A r => forall (B : Set) (f : A -> B), MRec s (mapmu2 f r) = mG f (MRec s r))). clear A r. intros X ef j n IH A t B f. rewrite mapmu2Red. do 2 rewrite MRecRed. apply (smGpNAT(rec:=fun A0 : Set => MRec s (A:=A0) o j A0) ef n). clear A t B f. red. intros. unfold comp. rewrite n. apply IH. Qed. End MRecNAT. End MRec. Section MMIt. (** Mendler iteration with access to monotonocity *) Variable Fmon2br : mon2br F. Variable G:k1. Variable mG: mon G. Variable s: forall X:k1, mon X -> X c_k1 G -> F X c_k1 G. (** The idea for the following definition arose when studying the TLCA '07 paper by Johann and Ghani. In that paper, instead of mon2br F, an unrelativized version was used that cannot treat truly nested datatypes. Moreover, G was restricted to be a right Kan extension, and only an algebra - of type F G c_k1 G - was constructed. *) Definition s_MMIt : forall X:k1, X c_k1 G -> F X c_k1 G. Proof. red. intros X it A t. exact (s mG (fun A x => x) (Fmon2br mG it t)). Defined. Definition MMIt: mu2 c_k1 G := MIt s_MMIt. (** the unperspicuous behaviour *) Lemma MMItRedCan (A:k0)(t:F mu2 A): MMIt (InCan t) = s mG (fun A x => x) (Fmon2br mG MMIt t). Proof. intros. unfold MMIt. rewrite MItRedCan. reflexivity. Qed. (** here, we only want to forget the j argument *) Definition s_MItpl: forall X:k1, mon X -> X c_k1 mu2 -> X c_k1 G -> F X c_k1 G. Proof. intros X mX j rec. exact (s mX rec). Defined. (** the instance of MRec without the j argument *) Definition MItpl: mu2 c_k1 G := MRec s_MItpl. (** the intended behaviour *) Lemma MItplRedCan (A:k0)(t:F mu2 A): MItpl (InCan t) = s mapmu2 MItpl t. Proof. intros. unfold MItpl. rewrite MRecRedCan. reflexivity. Qed. Variable smGpNAT : forall (X:k1)(ef: EFct X)(it: X c_k1 G), NAT it (m ef) mG -> NAT (s (m ef) it) (m (FpEFct ef)) mG. Lemma s_MItplmGpNAT : forall (X:k1)(ef: EFct X)(j: X c_k1 mu2)(rec: X c_k1 G), NAT j (m ef) mapmu2 -> NAT rec (m ef) mG -> NAT (s_MItpl (m ef) j rec) (m (FpEFct ef)) mG. Proof. red. intros. unfold s_MItpl. apply smGpNAT. assumption. Qed. Lemma MItplsNAT : NAT MItpl mapmu2 mG. Proof. unfold MItpl. apply MRecNAT. apply s_MItplmGpNAT. Qed. Variable GEFct : EFct G. Hypothesis mGOk : m GEFct = mG. Hypothesis Fmon2brpNAT : forall (X:k1)(ef: EFct X)(it: X c_k1 G), NAT it (m ef) (m GEFct) -> NAT (Fmon2br (m GEFct) it) (m(FpEFct ef)) (m(FpEFct GEFct)). Lemma MMItsNAT : NAT MMIt mapmu2 mG. Proof. unfold MMIt. apply MItNAT. unfold s_MMIt. red. intros. rewrite <- mGOk. rewrite Fmon2brpNAT. rewrite (smGpNAT GEFct (it:=fun A x => x)). rewrite <- mGOk. reflexivity. rewrite <- mGOk. red. intros. reflexivity. rewrite mGOk. assumption. Qed. Hypothesis spolyExtsub: forall (X : k1) (ef : EFct X), polyExtsub (s (m ef)). Hypothesis sFmon2br: forall(X:k1)(ef:EFct X)(it:X c_k1 G), NAT it (m ef) mG -> forall(A:k0)(t: F X A), s (m ef) it t = s mG (fun (A0 : Set) (x : G A0) => x) (Fmon2br mG it t). Theorem MMItsMItpls: forall (A:k0)(t:mu2 A), MMIt t = MItpl t. Proof. unfold MItpl. apply MRecUni. (* extensionality *) red. intros. unfold s_MItpl. apply spolyExtsub. assumption. (* behaviour *) intros. unfold MMIt at 1. rewrite MItRed. change (LNM.MIt s_MMIt) with MMIt. unfold s_MMIt. unfold s_MItpl. rewrite sFmon2br. reflexivity. red. intros. unfold comp. rewrite n. rewrite MMItsNAT. reflexivity. Qed. (** just for curiosity: for the proof of MMItsMItpls, smGpNAT is only used in MMItsNAT, and there in the form smGpNAT GEFct (it:=fun A x => x). The question is whether full smGpNAT is implied by this version together with the other assumptions: *) Lemma smGpNATspecial: NAT (s mG (fun (A : Set) (x : G A) => x)) (m (FpEFct GEFct)) mG -> forall (X:k1)(ef: EFct X)(it: X c_k1 G), NAT it (m ef) mG -> NAT (s (m ef) it) (m (FpEFct ef)) mG. Proof. intros. clear smGpNAT. (* !! *) red. intros. rewrite sFmon2br; try assumption. rewrite <- mGOk. rewrite Fmon2brpNAT. rewrite mGOk. rewrite H. rewrite sFmon2br; try assumption. reflexivity. rewrite mGOk. assumption. Qed. (** To conclude, instead of smGpNAT, one should have assumed only NAT (s mG (fun (A : Set) (x : G A) => x)) (m (FpEFct GEFct)) mG. With the present development, there is thus some repetition of work. *) End MMIt. End LNMRecDef.