(** LNGMItPred.v Version 1.0 January 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 basic definitions and the predicative specification of LNGMIt as an extension of LNMIt and infer general theorems from this specification. *) Require Import LNMItPred. Set Implicit Arguments. (** 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. Infix "<_k1" := less_k1 (at level 60). Definition mon (X:k1): Type := X <_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 <_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 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 <_k1 G), ext h = gext h. Proof. reflexivity. Qed. (** the first part of the naturality law for inhabitants of X <_k1 G *) Definition nat1 (X G: k1)(mG: mon G)(h: X<_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 <_k1 G), nat1 mG h = gnat1 monId mG h. Proof. reflexivity. Qed. (** the second part of the naturality law for inhabitants of X <_k1 G *) Definition nat2 (X G: k1)(mX: mon X)(h: X <_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 <_k1 G), nat2 mX h = gnat2 mX h. Proof. reflexivity. Qed. Definition lessTosub (X G: k1): X <_k1 G -> X c_k1 G. Proof. intros X G h A. exact (h A A (id(A:=A))). Defined. Lemma nat1nat2NAT(X G: k1)(mX: mon X)(mG: mon G)(h: X <_k1 G): nat1 mG h -> nat2 mX h -> NAT (lessTosub h) mX mG. 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(A:=H A))). Defined. Lemma glessTosubIsGen: forall (X G: k1)(h: X <_k1 G)(A: k0)(t: X A), glessTosub h A t = lessTosub h A t. Proof. reflexivity. Qed. (** The following lemma is Lemma 4 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) (moncomp mX mH) mG. Proof. intros. red. intros. unfold glessTosub. rewrite H0. unfold moncomp. unfold comp, id. rewrite H1. unfold comp. reflexivity. Qed. (** through instantiation, we can provide an alternative proof to nat1nat2NAT: *) Lemma nat1nat2NAT_ALT: forall (X G: k1)(mX: mon X)(mG: mon G)(h: X <_k1 G), nat1 mG h -> nat2 mX h -> NAT (lessTosub h) mX mG. 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)(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)(mH: mon H)(mG: mon G)(g: (fun A => X(H A)) c_k1 G): NAT g (moncomp mX mH) mG -> gnat1 mH mG (subTogless H mX g). Proof. red. intros. unfold subTogless. unfold comp at 1. rewrite <- H0. unfold moncomp. rewrite <- f2X. reflexivity. Qed. Lemma subToglessgnat2(X H G: k1)(mX: mon X)(f2X: fct2 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 *) Definition polyExtless (X1 X2 Y1 Y2:k1)(t: X1 <_k1 X2 -> Y1 <_k1 Y2): Prop := forall(g h: X1 <_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 <_k1 X2 -> Y1 <_k1 Y2): polyExtgless t = polyExtless t. Proof. reflexivity. Qed. 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. 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. 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 (m ef) mapmu2)(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 lemma is Lemma 2 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 (m ef) mapmu2)(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. generalize IH; clear IH. generalize B f; clear B f. generalize A r; clear A r. apply (mu2Ind (fun A r => forall (B : Set) (f : A -> H B), (forall (A0 B0 : Set) (f0 : A0 -> H B0) (X : k1) (ef : EFct X) (j : X c_k1 mu2) (n : NAT j (m ef) mapmu2) (t : F X A0), h A0 B0 f0 (In ef n t) = s (fun (A1 B1 : Set) (f1 : A1 -> H B1) => h A1 B1 f1 o j A1) f0 t) -> h A B f r = GMIt s B f r)). intros X ef j n IH A t B f Hyp. 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 lemma is Lemma 3 in the paper. *) Lemma GMItsExt: gext (GMIt s). Proof. intros A B f g Hyp r. generalize Hyp; clear Hyp. 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 -> H B), (forall a : A, f a = g a) -> GMIt s _ f r = GMIt s _ g r)). intros. do 2 rewrite GMItRed. apply spExt. red. intros. unfold comp. apply H0. assumption. assumption. Qed. End GMItsExt. 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 lemma is Lemma 5 in the paper. *) Lemma GMItsNat1: gnat1 mH mG (GMIt s). 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 -> H B) (g : B -> C), mG g (GMIt s _ f r) = GMIt s _ (mH g o f) r)). 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 ef) h -> gnat2 (m(FpEFct ef)) (s h). (** this is the part that needs the built-in naturality of LNGMIt *) (** The following lemma is Theorem 1 in the paper. *) Lemma GMItsNat2: gnat2 mapmu2 (GMIt s). 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 -> H C), GMIt s _ g (mapmu2 f r) = GMIt s _ (g o f) r)). 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 ef) h). clear A t B C f g. red. intros. unfold h at 1, comp at 1. 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 ef) h -> gnat2 (m(FpEFct ef)) (s h). Lemma GMItsNAT: NAT (glessTosub (GMIt s)) (moncomp mapmu2 mH) mG. Proof. simpl. apply gnat1gnat2NAT. exact (GMItsNat1 smGpgnat1). exact (GMItsNat2 smGpgnat2). Qed. End GMItsNAT. End GMIt. End LNGMItDef.