(** LNMItPred.v Version 2.9.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 no longer conforms to the description in the article "An induction principle for nested datatypes in intensional type theory" by the author, that appeared in the Journal of Functional Programming, since it now uses type classes instead of the record [EFct] and the type [pEFct], as well as for [mon] and [NAT] forms part of the code that comes with a submission to the journal Science of Computer Programming *) Set Implicit Arguments. Require Import Utf8. (** 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. Implicit Arguments id [[A]]. (** composition: *) Definition comp (A B C: Type)(g: B -> C)(f: A -> B) : A -> C := fun x => g (f x). (** printing o %\ensuremath{\circ}% *) (* begin hide *) Infix "o" := comp (at level 90). (* end hide *) (** [comp] is displayed as the infix $\circ$#o#. *) (** standard notion of less than on type transformations, in Type and not in Set that would require impredicative Set *) Definition sub_k1 (X Y: k1) : Type := forall A: Set, X A -> Y A. (** printing c_k1 %\ensuremath{\subseteq}% *) (* begin hide *) Infix "c_k1" := sub_k1 (at level 60). (* end hide *) (** [sub_k1] is displayed as the infix $\subseteq$#c_k1#. *) (** monotonicity: *) Class mon (X: k1) : Type := map: forall (A B: Set), (A -> B) -> X A -> X B. (** extensionality: *) Definition ext (X: k1)`{mX: mon X}: Prop := forall (A B: Set)(f g: A -> B), (forall a, f a = g a) -> forall r, map f r = map g r. Require Import Setoid. Require Import Morphisms. (* Proper used to be Morphism: *) Definition ext' (X: k1)`{mX: mon X}: Prop := forall (A B: Set), Proper ((@eq A ==> @eq B) ==> @eq (X A) ==> @eq (X B)) (map(A:= A)(B:= B)). Lemma extEquiv (X: k1)`{mX: mon X}: ext <-> ext'. Proof. intros. split. red. intros. red. red. intros f g Hyp. red in Hyp. red. intros r r' Eq. rewrite <- Eq. apply H. intro. rewrite (Hyp a a); reflexivity. intro. red. intros. assert ((@eq A ==> @eq B)%signature f g). red. intros a a' Eq. rewrite <- Eq. apply H0. red in H. rewrite H1. reflexivity. Qed. (** first functor law: *) Definition fct1 (X: k1)`{mX: mon X}: Prop := forall (A: Set)(x: X A), map id x = x. (** second functor law: *) Definition fct2 (X: k1)`{mX: mon X}: Prop := forall (A B C: Set)(f: A -> B)(g: B -> C)(x: X A), map (g o f) x = map g (map f x). (** pack up the good properties of the approximation into the notion of an extensional functor: *) Class EFct (X: k1) := {m :> mon X; e: ext; f1: fct1; f2: fct2}. (** preservation of extensional functors: *) Class pEFct (F: k2) := pres:> forall (X: k1), EFct X -> EFct (F X). (** [:>] was suggested to me by Matthieu Sozeau on November 17, 2008 *) (** we show some closure properties of [pEFct], depending on such properties for [EFct] *) Instance moncomp `{X: k1, mX: mon X, Y: k1, mY: mon Y}: mon (fun A => X(Y A)). Proof. red. intros (* X mX Y mY *) A B f x. exact (mX (Y A)(Y B) (mY A B f) x). Defined. (** closure under composition: *) Instance compEFct `{X: k1, EFct X, Y: k1, EFct Y} : EFct (fun A => X(Y A)):= {m:= moncomp(mX:= map)(mY:= map)}. Proof. (* prove ext *) red; intros. apply e. apply e. trivial. (* prove fct1 *) red; intros; unfold moncomp. unfold map at 1. (* unintuitive numbering *) rewrite (e (map id) id); apply f1. (* prove fct2 *) red; intros; unfold moncomp. unfold map at 1. (* unintuitive numbering *) rewrite (e (map (g o f)) ((map g)o(map f))); apply f2. Defined. Instance comppEFct `{F: k2, pEFct F, G: k2, pEFct G}: pEFct (fun X A => F X (G X A)). Proof. red. intros. apply compEFct. Defined. (** This may now be used to prove that truly nested examples are instances of the theorems to come. *) (** closure under sums: *) Instance sumEFct `{X: k1, EFct X, Y: k1, EFct Y}: EFct (fun A => X A + Y A)%type:= {m:= (fun A B f x => match x with | inl y => inl _ (map f y) | inr y => inr _ (map f y) end): mon (fun A : Set => (X A + Y A)%type)}. Proof. (* prove ext *) red; intros. unfold map at 1 4. (* very unintuitive numbering *) destruct r; (f_equal; apply e; trivial). (* prove fct1 *) red; intros. unfold map at 1. (* unintuitive numbering *) destruct x; (f_equal; apply f1). (* prove fct2 *) red; intros. unfold map at 1. (* unintuitive numbering *) destruct x; (rewrite f2; reflexivity). Defined. Instance sumpEFct `{F: k2, pEFct F, G: k2, pEFct G}: pEFct (fun X A => F X A + G X A)%type. Proof. red. intros. apply sumEFct. Defined. (** closure under products: *) (** printing x1 %\ensuremath{x_1}% *) (** printing x2 %\ensuremath{x_2}% *) Instance prodEFct `{X: k1, EFct X, Y: k1, EFct Y}: EFct (fun A => X A * Y A)%type:= {m:= (fun A B f x => match x with (x1, x2) => (map f x1, map f x2) end): mon(fun A => X A * Y A)%type}. Proof. (* prove ext *) red; intros. unfold map at 1 4. (* very unintuitive numbering *) destruct r as [x1 x2]. apply injective_projections; (apply e; trivial). (* prove fct1 *) red; intros. unfold map at 1. (* unintuitive numbering *) destruct x as [x1 x2]. apply injective_projections; apply f1. (* prove fct2 *) red; intros. unfold map at 1 4. unfold map at 3. (* artistic numbering *) destruct x as [x1 x2]. apply injective_projections; apply f2. Defined. Instance prodpEFct `{F: k2, pEFct F, G: k2, pEFct G}: pEFct (fun X A => F X A * G X A)%type. Proof. red. intros. apply prodEFct. Defined. (** the identity in [k2] preserves extensional functors: *) Instance idpEFct: pEFct (fun X => X). Proof. red. intros. assumption. Defined. (** a variant for the eta-expanded identity: *) Instance 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 (Build_EFct (m:= m0) e0 f01 f02). Defined. (** Is there any possibility to avoid the destruct command? *) (** the identity in [k1] "is" an extensional functor: *) Instance idEFct: EFct (fun A => A) := {m:= fun A B (f: A -> B)(x: A) => f x}. Proof. red. intros. apply H. red. reflexivity. red. reflexivity. Defined. (** constants in [k2]: *) Instance constpEFct `{X: k1, EFct X}: pEFct (fun _ => X). Proof. red. intros. assumption. Defined. (** constants in [k1]: *) Instance constEFct(C: Set): EFct (fun _ => C):= {m:= fun A B (f: A -> B)(x: C) => x}. Proof. red; reflexivity. red; reflexivity. red; reflexivity. Defined. (** the option type: *) Instance optionEFct: EFct (fun A: Set => option A):= {m:= option_map}. red; destruct r; simpl; unfold map; simpl. rewrite H; reflexivity. reflexivity. red; destruct x; reflexivity. red; destruct x; reflexivity. Defined. (** natural transformations from [(X, mX)] to [(Y, mY)]: *) Class NAT(X Y: k1)(j: X c_k1 Y)`{mX: mon X, mY: mon Y} : Prop := naturality: forall (A B: Set)(f: A -> B)(t: X A), j B (map f t) = map f (j A t). (** a notion that plays a role in the uniqueness theorem for [MIt]: *) (** printing X1 %\ensuremath{X_1}% *) (** printing X2 %\ensuremath{X_2}% *) (** printing Y1 %\ensuremath{Y_1}% *) (** printing Y2 %\ensuremath{Y_2}% *) 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. Definition polyExtsub' (X1 X2 Y1 Y2: k1): (X1 c_k1 X2 -> Y1 c_k1 Y2) -> Prop := Proper (forall_relation (fun A: Set => @eq (X1 A) ==> @eq (X2 A)) ==> forall_relation (fun A: Set => @eq (Y1 A) ==> @eq (Y2 A))). Lemma polyExtsubEquiv (X1 X2 Y1 Y2: k1)(t: X1 c_k1 X2 -> Y1 c_k1 Y2): polyExtsub t <-> polyExtsub' t. Proof. intros. split. do 5 red. intros. red in H. rewrite H1. apply H. intros. do 2 red in H0. apply (H0 _ x1 x1). reflexivity. (* the other direction *) red. intros. apply H. do 2 red. intros. rewrite <- H1. apply H0. reflexivity. Qed. (* I did not see how to use setoid rewriting in the second half of the proof. *) (** 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. Declare Instance FpEFct: pEFct F. (* Declare is new keyword *) (** printing mu20 %\ensuremath{\mu_0}% *) Parameter mu20: k1. (** printing mu2 %\ensuremath{\mu}% *) Definition mu2: k1:= fun A => mu20 A. (** the introduction of [mu20] is a little twist that is mentioned in the paper, but only in a footnote and not relevant there *) Declare Instance mapmu2: mon mu2. (* Declare Instance instead of Parameter! *) 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 -> 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)(t: F X A)(B: Set)(f: A -> B), mapmu2 f (In ef n t) = In ef n (m 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)(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), (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(mX:= mapmu2). Proof. red. intros. revert H. revert f g. revert B. revert A r. refine (mu2Ind _ _). intros. clear H (* the IH *). do 2 rewrite mapmu2Red. f_equal. apply e; assumption. Defined. Lemma mapmu2Id: fct1(mX:= mapmu2). Proof. red. refine (mu2Ind _ _). intros. clear H (* the IH *). rewrite mapmu2Red. f_equal. apply f1. Defined. Lemma mapmu2Comp: fct2(mX:= mapmu2). Proof. red. intros A B C f g r. revert f g. revert B C. revert A r. refine (mu2Ind _ _). intros. clear H (* the IH *). do 3 rewrite mapmu2Red. f_equal. apply f2. Defined. Instance mapmu2EFct: EFct mu2 := {m:= mapmu2}. Proof. exact mapmu2Ext. exact mapmu2Id. exact mapmu2Comp. Defined. (* a reformulation of [mapmu2Red] *) Instance mapmu2NAT(X: k1)(ef: EFct X)(j: X c_k1 mu2)(n:NAT j): NAT (In ef n). 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 f t). Proof. intros. unfold InCan. rewrite mapmu2Red. reflexivity. Qed. (* a reformulation of [mapmu2RedCan] *) Instance mapmu2NATCan: NAT InCan. 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)(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. refine (mu2Ind _ _). 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 -> NAT (s it). Instance MItNAT : NAT (MIt s). Proof. red. intros A B f r. revert B f. revert A r. refine (mu2Ind _ _). 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.