(** 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.