(** LNGMItPred.v Version 1.5 March 2009 *) (** does not need impredicative Set, runs under V8.2, later tested with version 8.2pl1 *) (** Copyright Ralph Matthes, I.R.I.T., C.N.R.S. & University of Toulouse*) (** We provide basic definitions and the predicative specification of LNGMIt as an extension of LNMIt and infer general theorems from this specification. *) (** forms part of the code that comes with a submission to the journal Science of Computer Programming *) Require Import LNMItPred. Set Implicit Arguments. Require Import Utf8. (** refined notion of less than on type transformations: *) Definition less_k1 (X G: k1): Type := forall (A B: Set), (A -> B) -> X A -> G B. (* begin hide *) Infix "lt_k1" := less_k1 (at level 60). (* end hide *) (** printing lt_k1 %\ensuremath{\leq}% *) (** [less_k1] is displayed as the infix $\leq$#<_k1#. *) Class mon (X: k1): Type := map: X lt_k1 X. Lemma monOk: mon = LNMItPred.mon. Proof. reflexivity. Qed. (** generalized refined containment: *) Definition gless_k1 (X H G: k1): Type := forall (A B: Set), (A -> H B) -> X A -> G B. Notation "X <_{ H } G" := (gless_k1 X H G) (at level 60). Definition ext (X G: k1)(h: X lt_k1 G): Prop := forall (A B: Set)(f g: A -> B), (forall a, f a = g a) -> forall r, h _ _ f r = h _ _ g r. Lemma extOk (X: k1)`{m: mon X}: ext m = LNMItPred.ext(mX:= m). Proof. reflexivity. Qed. Definition gext (H X G: k1)(h: X <_{H} G): Prop := forall (A B: Set)(f g: A -> H B), (forall a, f a = g a) -> forall r, h _ _ f r = h _ _ g r. Lemma gextIsGen: forall(X G: k1)(h: X lt_k1 G), ext h = gext h. Proof. reflexivity. Qed. Require Import Setoid. Require Import Morphisms. Definition gext' (H X G: k1)(h: X <_{H} G): Prop := forall (A B: Set), Morphism ((@eq A ==> @eq (H B)) ==> @eq (X A) ==> @eq (G B)) (h A B). Lemma gextEquiv (H X G: k1)(h: X <_{H} G): gext h <-> gext' h. Proof. intros. split. red. intros. red. red. intros f g Hyp. red in Hyp. red. intros r r' Eq. rewrite <- Eq. apply H0. intro. rewrite (Hyp a a); reflexivity. intro. red. intros. assert ((@eq A ==> @eq (H B))%signature f g). red. intros a a' Eq. rewrite <- Eq. apply H1. red in H0. rewrite H2. reflexivity. Qed. (** This was essentially the same proof as that for [LNMItPred.extEquiv]. *) (** the first part of the naturality law for inhabitants of [X lt_k1 G] (Definition 1/2 in the paper): *) (** printing o %\ensuremath{\circ}% *) (* recalled from LNMItPred.v *) Definition nat1 (X G: k1)(mG: mon G)(h: X lt_k1 G): Prop := forall (A B C: Set)(f: A -> B)(g: B -> C)(x: X A), mG B C g (h A B f x) = h A C (g o f) x. (** the same generalized to monotone [H]: *) Definition gnat1 (X H G: k1)(mH: mon H)(mG: mon G)(h: X <_{H} G): Prop := forall (A B C: Set)(f: A -> H B)(g: B -> C)(x: X A), mG B C g (h A B f x) = h A C ((mH _ _ g) o f) x. Definition monId: mon (fun A => A) := fun A B f x => f x. Lemma gnat1IsGen: forall (X G: k1)(mG: mon G)(h: X lt_k1 G), nat1 mG h = gnat1 monId mG h. Proof. reflexivity. Qed. (** the second part of the naturality law for inhabitants of [X lt_k1 G] (Definition 1/2 in the paper): *) Definition nat2 (X G: k1)(mX: mon X)(h: X lt_k1 G): Prop := forall (A B C: Set)(f: A -> B)(g: B -> C)(x: X A), h B C g (mX A B f x) = h A C (g o f) x. Definition gnat2 (X H G: k1)(mX: mon X)(h: X <_{H} G): Prop := forall (A B C: Set)(f: A -> B)(g: B -> H C)(x: X A), h B C g (mX A B f x) = h A C (g o f) x. Lemma gnat2IsGen: forall (X G: k1)(mX: mon X)(h: X lt_k1 G), nat2 mX h = gnat2 mX h. Proof. reflexivity. Qed. (** printing c_k1 %\ensuremath{\subseteq}% *) (* recalled from LNMItPred.v *) Definition lessTosub (X G: k1): X lt_k1 G -> X c_k1 G. Proof. intros X G h A. exact (h A A id). Defined. Lemma nat1nat2NAT(X G: k1)(mX: mon X)(mG: mon G)(h: X lt_k1 G): nat1 mG h -> nat2 mX h -> NAT(mX:= mX)(mY:= mG) (lessTosub h). Proof. intros. red. intros. unfold lessTosub. rewrite H0. unfold comp, id. rewrite H. unfold comp. reflexivity. Qed. Definition glessTosub (X H G: k1): X <_{H} G -> (fun A => X(H A)) c_k1 G. Proof. intros X H G h A. exact (h (H A) A id). Defined. Lemma glessTosubIsGen: forall (X G: k1)(h: X lt_k1 G)(A: Set)(t: X A), glessTosub h A t = lessTosub h A t. Proof. reflexivity. Qed. (** The following is Lemma 2 in the paper. *) Lemma gnat1gnat2NAT(X H G: k1)(mX: mon X)(mH: mon H)(mG: mon G)(h: X <_{H} G): gnat1 mH mG h -> gnat2 mX h -> NAT (glessTosub h) (mX:= moncomp(mX:= mX)(mY:= mH))(mY:= mG). Proof. intros. red. intros. unfold glessTosub. rewrite H0. unfold moncomp. unfold comp, id. unfold LNMItPred.map. rewrite H1. unfold comp. reflexivity. Qed. (** through instantiation, we can provide an alternative proof to [nat1nat2NAT]: *) Instance nat1nat2NAT_ALT: forall (X G: k1)(mX: mon X)(mG: mon G)(h: X lt_k1 G), nat1 mG h -> nat2 mX h -> NAT(mX:= mX)(mY:= mG) (lessTosub h). Proof. red. intros. do 2 rewrite <- glessTosubIsGen. set (aux:= gnat1gnat2NAT H H0). unfold moncomp in aux. apply aux. Qed. (** As a digression, we develop a partial inverse of [gnat1gnat2NAT] (extending Mac Lane's exercise): *) Definition subTogless (X H G: k1)(mX: mon X): (fun A => X(H A)) c_k1 G -> X <_{H} G. intros X H G mX g A B f. exact ((g B) o (mX A (H B) f)). Defined. Lemma subToglessTosub (X H G: k1)(mX: mon X)(f1X: fct1(mX:= mX))(g: (fun A => X(H A)) c_k1 G)(A: Set)(x: X(H A)): glessTosub (subTogless H mX g) A x = g A x. Proof. intros. unfold glessTosub. unfold subTogless. unfold comp. rewrite f1X. reflexivity. Qed. Lemma NATgnat1(X H G: k1)(mX: mon X)(f2X: fct2(mX:= mX))(mH: mon H)(mG: mon G)(g: (fun A => X(H A)) c_k1 G): NAT g (mX:= moncomp(mX:= mX)(mY:= mH))(mY:= mG) -> gnat1 mH mG (subTogless H mX g). Proof. red. intros. unfold subTogless. unfold comp at 1. rewrite <- H0. unfold LNMItPred.map. unfold moncomp. rewrite <- f2X. reflexivity. Qed. Lemma subToglessgnat2(X H G: k1)(mX: mon X)(f2X: fct2(mX:= mX))(g: (fun A => X(H A)) c_k1 G): gnat2 mX (subTogless H mX g). Proof. red. intros. unfold subTogless at 1. unfold comp at 1. rewrite <- f2X. reflexivity. Qed. (** because of the previous lemma, the condition on [gnat2] seems unavoidable in the following: *) Lemma glessTosubTogless (X H G: k1)(mX: mon X)(h: X <_{H} G)(A B: Set)(f: A -> H B)(x: X A): gext h -> gnat2 mX h -> subTogless H mX (glessTosub h) B f x = h A B f x. Proof. intros. unfold subTogless. unfold glessTosub. unfold comp. rewrite H1. apply H0. reflexivity. Qed. (** end of digression *) (** printing X1 %\ensuremath{X_1}% *) (** printing X2 %\ensuremath{X_2}% *) (** printing Y1 %\ensuremath{Y_1}% *) (** printing Y2 %\ensuremath{Y_2}% *) (* recalled from LNMItPred.v *) Definition polyExtless (X1 X2 Y1 Y2: k1)(t: X1 lt_k1 X2 -> Y1 lt_k1 Y2): Prop := forall(g h: X1 lt_k1 X2)(A B: Set)(f: A -> B)(y: Y1 A), (forall (A B: Set)(f: A -> B)(x: X1 A), g A B f x = h A B f x) -> t g A B f y = t h A B f y. Definition polyExtgless (H X1 X2 Y1 Y2: k1)(t: X1 <_{H} X2 -> Y1 <_{H} Y2): Prop := forall(g h: X1 <_{H} X2)(A B: Set)(f: A -> H B)(y: Y1 A), (forall (A B: Set)(f: A -> H B)(x: X1 A), g A B f x = h A B f x) -> t g A B f y = t h A B f y. Lemma polyExtlessOk (X1 X2 Y1 Y2: k1)(t: X1 lt_k1 X2 -> Y1 lt_k1 Y2): polyExtgless t = polyExtless t. Proof. reflexivity. Qed. Definition polyExtgless' (H X1 X2 Y1 Y2: k1): (X1 <_{H} X2 -> Y1 <_{H} Y2) -> Prop := Morphism ((forall_relation (fun A: Set => forall_relation (fun B: Set => (@eq (A -> H B)) ==> @eq (X1 A) ==> @eq (X2 B)))) ==> (forall_relation (fun A: Set => forall_relation (fun B: Set => (@eq (A -> H B)) ==> @eq (Y1 A) ==> @eq (Y2 B)))))%signature. Lemma polyExtglessEquiv (H X1 X2 Y1 Y2: k1)(t: X1 <_{H} X2 -> Y1 <_{H} Y2): polyExtgless t <-> polyExtgless' t. Proof. intros. split. do 7 red. intros. rewrite H3. rewrite H2. apply H0. intros. apply H1; reflexivity. (* the other direction *) red. intros. apply H0; try reflexivity. do 4 red. intros. rewrite H2. rewrite H3. apply H1; reflexivity. Qed. (** for curiosity, we define a variant of [polyExtgless] *) Definition polyExtgless'' (H X1 X2 Y1 Y2: k1): (X1 <_{H} X2 -> Y1 <_{H} Y2) -> Prop := Morphism ((forall_relation (fun A: Set => forall_relation (fun B: Set => (@eq A ==> @eq (H B)) ==> @eq (X1 A) ==> @eq (X2 B)))) ==> (forall_relation (fun A: Set => forall_relation (fun B: Set => (@eq A ==> @eq (H B)) ==> @eq (Y1 A) ==> @eq (Y2 B)))))%signature. Module Type LNGMIt_Type. Declare Module Import LNM: LNMIt_Type. (* we need to establish LNGMIt_Type as a subtype of LNMIt_Type *) Definition F:= F. Definition FpEFct:= FpEFct. (** printing mu20 %\ensuremath{\mu_0}% *) Definition mu20 := mu20. (** printing mu2 %\ensuremath{\mu}% *) 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. Parameter GMIt0: forall (H G: k1), (forall X: k1, X <_{H} G -> F X <_{H} G) -> mu2 <_{H} G. Definition GMIt: forall (H G: k1), (forall X: k1, X <_{H} G -> F X <_{H} G) -> mu2 <_{H} G := fun (H G: k1) s (A: Set) B f t => GMIt0(H:= H)(G:= G)(A:= A) s B f t. Axiom GMItRed : forall (H G: k1)(s: forall X: k1, X <_{H} G -> F X <_{H} G)(A B: Set)(f: A -> H B)(X: k1)(ef: EFct X)(j: X c_k1 mu2)(n: NAT j)(t: F X A), GMIt s _ f (In ef (j:= j) n t) = s X (fun (A B: Set) (f: A -> H B) => (GMIt s _ f) o (j A)) A B f t. End LNGMIt_Type. (** prove theorems about the components of [LNGMIt_Type] *) Module LNGMItDef(M: LNGMIt_Type). Import M. Module LNMItDef := LNMItDef M. Import LNMItDef. Section GMIt. Variables H G: k1. Variable s: forall X: k1, X <_{H} G -> F X <_{H} G. (** the behaviour for canonical elements: *) Lemma GMItRedCan : forall (A B: Set)(f: A-> H B)(t: F mu2 A), GMIt s _ f (InCan t) = s (GMIt s) f t. Proof. intros. unfold InCan. rewrite GMItRed. unfold comp. reflexivity. Qed. (** The following is Theorem 4 in the paper. *) Lemma GMItUni: forall (h: mu2 <_{H} G), (forall (X: k1), polyExtgless(s(X:= X))) -> (forall (A B: Set)(f: A -> H B)(X: k1)(ef: EFct X)(j: X c_k1 mu2)(n: NAT j)(t: F X A), h A B f (In ef n t) = s (fun (A B: Set) (f: A -> H B) => (h A B f) o (j A)) f t) -> forall (A B: Set)(f: A -> H B)(r: mu2 A), h A B f r = GMIt s _ f r. Proof. intros h sExt Hyp A B f r. revert B f. revert A r. refine (mu2Ind _ _). intros X ef j n IH A t B f. rewrite Hyp. rewrite GMItRed. apply sExt. intros. unfold comp. apply IH; assumption. Qed. (** For the remainder, we require the following: *) Hypothesis spExt : forall (X: k1)(h: X <_{H} G), gext h -> gext (s h). Section GMItsExt. (** GMIt s only depends on the extension of its functional argument *) (** The following is Theorem 5 in the paper. *) Lemma GMItsExt: gext (GMIt s). Proof. intros A B f g Hyp r. revert Hyp. revert f g. revert B. revert A r. refine (mu2Ind _ _). intros. do 2 rewrite GMItRed. apply spExt. red. intros. unfold comp. apply H0. assumption. assumption. Qed. End GMItsExt. (** for curiosity, we can now prove the variant of [GMItUni] that uses [polyExtgless''] instead of [polyExtgless], but this is under the extra assumption [spExt] of the enclosing section [GMIt] *) Lemma GMItUni'': forall (h: mu2 <_{H} G), (forall (X: k1), polyExtgless''(s(X:= X))) -> (forall (A B: Set)(f: A -> H B)(X: k1)(ef: EFct X)(j: X c_k1 mu2)(n: NAT j)(t: F X A), h A B f (In ef n t) = s (fun (A B: Set) (f: A -> H B) => (h A B f) o (j A)) f t) -> forall (A B: Set)(f: A -> H B)(r: mu2 A), h A B f r = GMIt s _ f r. Proof. intros h sExt IH A B f r. revert IH. revert B f. revert A r. refine (mu2Ind _ _). intros X ef j n IH A t B f Hyp. rewrite Hyp. rewrite GMItRed. apply sExt; try reflexivity. do 4 red. intros. unfold comp. rewrite H1. transitivity (GMIt s a0 x (j a y0)). apply IH; assumption. apply GMItsExt. intros. apply H0; reflexivity. Qed. Section GMItsNat1. Variable mH: mon H. Variable mG: mon G. Hypothesis smGpgnat1: forall (X: k1)(h: X<_{H} G), EFct X -> gext h -> gnat1 mH mG h -> gnat1 mH mG (s h). (** The following is Theorem 6 in the paper. *) Lemma GMItsNat1: gnat1 mH mG (GMIt s). Proof. red. intros A B C f g r. revert f g. revert B C. revert A r. refine (mu2Ind _ _). intros. do 2 rewrite GMItRed. clear n. (* we do not need the built-in naturality of j *) set (h := fun (A0 B0 : Set) (f0 : A0 -> H B0) => GMIt s _ f0 o j A0). assert (hext: gext h). unfold h. red. intros. unfold comp. apply GMItsExt. assumption. apply (smGpgnat1 ef hext). red. intros. unfold h, comp at 1 2. apply H0. Qed. End GMItsNat1. Section GMItsNat2. Hypothesis smGpgnat2: forall (X: k1)(h: X<_{H} G)(ef: EFct X), gext h -> gnat2 m h -> gnat2 m (s h). (** this is the part that needs the built-in naturality of [LNGMIt] *) (** The following is Theorem 7 in the paper. *) Lemma GMItsNat2: gnat2 mapmu2 (GMIt s). Proof. red. intros A B C f g r. revert f g. revert B C. revert A r. refine (mu2Ind _ _). intros. rewrite mapmu2Red. do 2 rewrite GMItRed. set (h := fun (A B : Set) (f : A -> H B) => GMIt s _ f o j A). assert (hnat2 : gnat2 m h). clear A t B C f g. red. intros. unfold h at 1, comp at 1. unfold m. rewrite n. (* !! *) unfold h, comp at 1. apply H0. (** now we may use the assertion *) apply smGpgnat2; try assumption. clear A t B C f g. unfold h. red. intros. unfold comp. apply GMItsExt. assumption. Qed. End GMItsNat2. Section GMItsNAT. Variable mH: mon H. Variable mG: mon G. Hypothesis smGpgnat1: forall (X: k1)(h: X<_{H} G), EFct X -> gext h -> gnat1 mH mG h -> gnat1 mH mG (s h). Hypothesis smGpgnat2: forall (X: k1)(h: X<_{H} G)(ef: EFct X), gext h -> gnat2 m h -> gnat2 m (s h). Lemma GMItsNAT: NAT (glessTosub (GMIt s)) (mX:= moncomp(mX:= mapmu2)(mY:= mH))(mY:= mG). Proof. simpl. apply gnat1gnat2NAT. exact (GMItsNat1 smGpgnat1). exact (GMItsNat2 smGpgnat2). Qed. End GMItsNAT. End GMIt. End LNGMItDef.