(** LNMItPred.v Version 2.01.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*) (** provides basic definitions and the predicative specification of LNMIt and infers general theorems from this specification. *) (** 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. (** the universe of all monotypes *) Definition k0 := Set. (** the type of all type transformations *) Definition k1 := k0 -> k0. (** the type of all rank-2 type transformations *) Definition k2 := k1 -> k1. (** polymorphic identity *) Definition id : forall (A:Set), A -> A := fun A x => x. (** composition *) Definition comp (A B C:Set)(g:B->C)(f:A->B) : A->C := fun x => g (f x). Infix "o" := comp (at level 90). (** standard notion of less than on type transformations, now in Type and no longer in Set that would require impredicative Set *) Definition sub_k1 (X Y:k1) : Type := forall A:Set, X A -> Y A. Infix "c_k1" := sub_k1 (at level 60). (** monotonicity *) Definition mon (X:k1) : Type := forall (A B:Set), (A -> B) -> X A -> X B. (** extensionality *) Definition ext (X:k1)(h: mon X): Prop := forall (A B:Set)(f g:A -> B), (forall a, f a = g a) -> forall r, h _ _ f r = h _ _ g r. (** first functor law *) Definition fct1 (X:k1)(m: mon X) : Prop := forall (A:Set)(x:X A), m _ _ (id(A:=A)) x = x. (** second functor law *) Definition fct2 (X:k1)(m: mon X) : Prop := forall (A B C:Set)(f:A -> B)(g:B -> C)(x:X A), m _ _ (g o f) x = m _ _ g (m _ _ f x). (** pack up the good properties of the approximation into the notion of an extensional functor *) Record EFct (X:k1) : Type := mkEFct { m : mon X; e : ext m; f1 : fct1 m; f2 : fct2 m }. (** preservation of extensional functors *) Definition pEFct (F:k2) : Type := forall (X:k1), EFct X -> EFct (F X). (** we show some closure properties of pEFct, depending on such properties for EFct *) Definition moncomp (X Y:k1)(mX:mon X)(mY:mon Y): mon (fun A => X(Y A)). Proof. red. intros A B f x. exact (mX (Y A)(Y B) (mY A B f) x). Defined. (** closure under composition *) Lemma compEFct (X Y:k1): EFct X -> EFct Y -> EFct (fun A => X(Y A)). Proof. intros ef1 ef2. apply (mkEFct(m:=moncomp (m ef1) (m ef2))); red; intros; unfold moncomp. (* prove ext *) apply (e ef1). intro. apply (e ef2); trivial. (* prove fct1 *) rewrite (e ef1 (m ef2 (id (A:=A))) (id(A:=Y A))). apply (f1 ef1). intro. apply (f1 ef2). (* prove fct2 *) rewrite (e ef1 (m ef2 (g o f))((m ef2 g)o(m ef2 f))). apply (f2 ef1). intro. unfold comp at 2. apply (f2 ef2). Defined. Corollary comppEFct (F G:k2): pEFct F -> pEFct G -> pEFct (fun X A => F X (G X A)). Proof. red. intros. apply compEFct; auto. Defined. (** This may now be used to prove that truly nested examples are instances of the theorems to come. *) (** closure under sums *) Lemma sumEFct (X Y:k1): EFct X -> EFct Y -> EFct (fun A => X A + Y A)%type. Proof. intros ef1 ef2. set (m12:=fun (A B:Set)(f:A->B) x => match x with | inl y => inl _ (m ef1 f y) | inr y => inr _ (m ef2 f y) end). apply (mkEFct(m:=m12)); red; intros. (* prove ext *) destruct r. simpl. f_equal. apply (e ef1); trivial. simpl. f_equal. apply (e ef2); trivial. (* prove fct1 *) destruct x. simpl. f_equal. apply (f1 ef1). simpl. f_equal. apply (f1 ef2). (* prove fct2 *) destruct x. simpl. rewrite (f2 ef1); reflexivity. simpl. rewrite (f2 ef2); reflexivity. Defined. Corollary sumpEFct (F G:k2): pEFct F -> pEFct G -> pEFct (fun X A => F X A + G X A)%type. Proof. red. intros. apply sumEFct; auto. Defined. (** closure under products *) Lemma prodEFct (X Y:k1): EFct X -> EFct Y -> EFct (fun A => X A * Y A)%type. Proof. intros ef1 ef2. set (m12:=fun (A B:Set)(f:A->B) x => match x with (x1,x2) => (m ef1 f x1, m ef2 f x2) end). apply (mkEFct(m:=m12)); red; intros. (* prove ext *) destruct r as [x1 x2]. simpl. apply injective_projections; simpl. apply (e ef1); trivial. apply (e ef2); trivial. (* prove fct1 *) destruct x as [x1 x2]. simpl. apply injective_projections; simpl. apply (f1 ef1). apply (f1 ef2). (* prove fct2 *) destruct x as [x1 x2]. simpl. apply injective_projections; simpl. apply (f2 ef1). apply (f2 ef2). Defined. Corollary prodpEFct (F G:k2): pEFct F -> pEFct G -> pEFct (fun X A => F X A * G X A)%type. Proof. red. intros. apply prodEFct; auto. Defined. (** the identity in k2 preserves extensional functors *) Lemma idpEFct: pEFct (fun X => X). Proof. red. intros. assumption. Defined. (** a variant for the eta-expanded identity *) Lemma idpEFct_eta: pEFct (fun X A => X A). Proof. red. intros X ef. destruct ef as [m0 e0 f01 f02]. change (mon X) with (mon (fun A => X A)) in m0. apply (mkEFct (m:=m0) e0 f01 f02). Defined. (** Is there any possibility to avoid the destruct command? *) (** the identity in k1 "is" an extensional functor *) Lemma idEFct: EFct (fun A => A). Proof. set (mId:=fun A B (f:A->B)(x:A) => f x). apply (mkEFct(m:=mId)). red. intros. unfold mId. apply H. red. reflexivity. red. reflexivity. Defined. (** constants in k2 *) Lemma constpEFct (X:k1): EFct X -> pEFct (fun _ => X). Proof. red. intros. assumption. Defined. (** constants in k1 *) Lemma constEFct (C:Set): EFct (fun _ => C). Proof. set (mC:=fun A B (f:A->B)(x:C) => x). apply (mkEFct(m:=mC)); red; intros; unfold mC; reflexivity. Defined. (** the option type *) Lemma optionEFct: EFct (fun (A:Set) => option A). apply (mkEFct (X:=fun (A:Set) => option A)(m:=option_map)); red; intros. destruct r. simpl. rewrite H. reflexivity. reflexivity. destruct x; reflexivity. destruct x; reflexivity. Defined. (** natural transformations from (X,mX) to (Y,mY) *) Definition NAT(X Y:k1)(j:X c_k1 Y)(mX:mon X)(mY:mon Y) : Prop := forall (A B:Set)(f:A->B)(t:X A), j B (mX A B f t) = mY _ _ f (j A t). (** a notion that plays a role in the uniqueness theorem for MIt *) Definition polyExtsub (X1 X2 Y1 Y2:k1)(t: X1 c_k1 X2 -> Y1 c_k1 Y2) : Prop := forall(f g: X1 c_k1 X2)(A:Set)(y: Y1 A), (forall (A:Set)(x: X1 A), f A x = g A x) -> t f A y = t g A y. (** a notion of monotonicity that is needed for "canonization" *) (** relativized basic monotonicity of rank 2 *) Definition mon2br (F:k2) := forall (X Y:k1), mon Y -> X c_k1 Y -> F X c_k1 F Y. (** the predicative specification of LNMIt *) Module Type LNMIt_Type. Parameter F:k2. Parameter FpEFct: pEFct F. Parameter mu20: k1. Definition mu2: k1:= fun A => mu20 A. (** the introduction of mu20 is a little twist that is not explained in the paper and not needed there *) Parameter mapmu2: mon mu2. Definition MItType: Type := forall G : k1, (forall X : k1, X c_k1 G -> F X c_k1 G) -> mu2 c_k1 G. Parameter MIt0 : MItType. (** we need just its eta-expansion MIt *) Definition MIt : MItType:= fun G s A t => MIt0 s t. Definition InType : Type := forall (X:k1)(ef:EFct X)(j: X c_k1 mu2), NAT j (m ef) mapmu2 -> F X c_k1 mu2. Parameter In : InType. Axiom mapmu2Red : forall (A:Set)(X:k1)(ef:EFct X)(j: X c_k1 mu2) (n: NAT j (m ef) mapmu2)(t: F X A)(B:Set)(f:A->B), mapmu2 f (In ef n t) = In ef n (m (FpEFct ef) f t). Axiom 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. 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. End LNMIt_Type. (** prove theorems about the components of LNMIt_Type *) Module LNMItDef(M:LNMIt_Type). Export M. (** we complete mapmu2 to an extensional functor; the order of the following three lemmas does not play a role; they only make shallow use of the induction principle in that they do not use the induction hypothesis *) Lemma mapmu2Ext : ext mapmu2. Proof. red. intros. generalize H; clear H. generalize f g; clear f g. generalize B; clear B. generalize A r; clear A r. apply (mu2Ind (fun A r => forall (B : Set) (f g : A -> B), (forall a : A, f a = g a) -> mapmu2 f r = mapmu2 g r)). intros. clear H (* the IH *). do 2 rewrite mapmu2Red. apply (f_equal (fun x=> In (A:=B) ef n x)). apply (e (FpEFct ef)); assumption. Defined. Lemma mapmu2Id: fct1 mapmu2. Proof. red. apply (mu2Ind (fun A r => mapmu2 (id(A:=A)) r = r)). intros. clear H (* the IH *). rewrite mapmu2Red. apply (f_equal (fun x=> In (A:=A) ef n x)). apply (f1 (FpEFct ef) _ t). Defined. Lemma mapmu2Comp : fct2 mapmu2. Proof. red. intros A B C f g r. generalize f g; clear f g. generalize B C; clear B C. generalize A r; clear A r. apply (mu2Ind (fun A r => forall (B C : Set) (f : A -> B) (g : B -> C), mapmu2 (g o f) r = mapmu2 g (mapmu2 f r))). intros. clear H (* the IH *). do 3 rewrite mapmu2Red. apply (f_equal (fun x=>In (A:=C) ef n x)). apply (f2 (FpEFct ef)); assumption. Defined. Lemma mapmu2EFct : EFct mu2. Proof. eapply mkEFct. eexact mapmu2Ext. exact mapmu2Id. exact mapmu2Comp. Defined. (* a reformulation of mapmu2Red *) Lemma mapmu2NAT(X:k1)(ef:EFct X)(j: X c_k1 mu2)(n:NAT j (m ef) mapmu2): NAT (In ef n) (m (FpEFct ef)) mapmu2. Proof. red. intros. apply sym_eq. apply mapmu2Red. Qed. (** the canonical constructor for mu2 uses mu2 as its own approximation *) Definition InCan : F mu2 c_k1 mu2 := fun A t => In mapmu2EFct (j:= fun _ x => x)(fun _ _ _ _ => refl_equal _) t. (** the behaviour for canonical elements *) Lemma MItRedCan : forall (G:k1)(s:forall X:k1, X c_k1 G ->F X c_k1 G) (A:Set)(t:F mu2 A), MIt s (InCan t) = s mu2 (MIt s) A t. Proof. intros. unfold InCan. rewrite MItRed. reflexivity. (* here, we needed the eta-expansion for MIt *) Qed. Lemma mapmu2RedCan : forall (A:Set)(B:Set)(f:A->B)(t: F mu2 A), mapmu2 f (InCan t) =InCan(m (FpEFct mapmu2EFct) f t). Proof. intros. unfold InCan. rewrite mapmu2Red. reflexivity. Qed. (* a reformulation of mapmu2RedCan *) Lemma mapmu2NATCan: NAT InCan (m (FpEFct mapmu2EFct)) mapmu2. Proof. red. intros. apply sym_eq. apply mapmu2RedCan. Qed. (** MItRed already characterizes MIt s under an extensionality assumption for s: *) Theorem MItUni: forall (G : k1)(s : forall X : k1, X c_k1 G -> F X c_k1 G) (h: mu2 c_k1 G), (forall (X:k1), polyExtsub(s X)) -> (forall (X : k1)(ef: EFct X)(j: X c_k1 mu2) (n:NAT j (m ef) mapmu2)(A:Set)(t:F X A), h A (In ef n t) = s X (fun A => (h A) o (j A)) A t) -> forall (A:Set)(r: mu2 A), h A r = MIt s r. Proof. intros G s h sExt H. apply (mu2Ind (fun A r => h A r = MIt s r)). intros X ef j n IH A t. rewrite H. rewrite MItRed. apply sExt. clear A t. intros. unfold comp. apply IH. Qed. (** provide naturality of MIt s *) Section MItNAT. Variable G:k1. Variable mG: mon G. Variable s: forall X : k1, X c_k1 G -> F X c_k1 G. Variable smGpNAT : forall (X:k1)(it: X c_k1 G)(ef: EFct X), NAT it (m ef) mG -> NAT (s it) (m (FpEFct ef)) mG. Theorem MItNAT : NAT (MIt 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), MIt s (mapmu2 f r) = mG f (MIt s r))). clear A r. intros X ef j n IH A t B f. rewrite mapmu2Red. do 2 rewrite MItRed. set (it:=fun A : Set => MIt s (A:=A) o j A). apply smGpNAT. clear A t B f. red. intros. unfold it at 1. unfold comp. rewrite n. rewrite IH. reflexivity. Qed. End MItNAT. Section Canonization. Variable Fmon2br: mon2br F. Definition canonize: mu2 c_k1 mu2 := MIt (fun (X : k1) (it : X c_k1 mu2) (A : Set) (t : F X A) => InCan (Fmon2br mapmu2 it t)). Definition OutCan: mu2 c_k1 F mu2 := MIt (fun X it A t => Fmon2br mapmu2 (fun A => InCan(A:=A) o (it A)) t). End Canonization. End LNMItDef.