(** LNGMItImp.v Version 1.0 January 2008 *)
(** needs impredicative Set, runs under V8.1, tested with 8.1pl3 *)
(** Copyright Ralph Matthes, I.R.I.T.,  C.N.R.S. & University of Toulouse *)


(** this is the implementation part where impredicative methods justify LNGMIt by
     reduction to LNMIt *)

Set Implicit Arguments.

Require Import LNMItPred.
Require Import LNGMItPred.

(** right Kan extension along H *)
Definition GRan (H G:k1) :k1  := fun A => forall B:Set, (A -> H B) -> G B.

Definition toGRan (X H G:k1) : X <_{H} G -> X c_k1 GRan H G.
Proof.
  red.
  red.
  intros X H G h A x B f.
  exact (h A B f x).
Defined.

Definition fromGRan(X H G:k1) : X c_k1 GRan H G -> X <_{H} G .
Proof.
  red.
  intros X H G h A B f x.
  red in h.
  red in h.
  exact (h A x B f).
Defined.
  

(** end of preparations for the following module *)

Module LNGMItBaseImp(M:LNMIt_Type) <: LNGMIt_Type.
(* with "<:", we do not encapsulate the definitions *)

Import M.

(* we need to establish LNGMItBaseImp as a subtype of LNGMIt_Type *)
Module LNM:=M.
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.

Section GMIt0. 

Variables H G:k1.
Variable s: forall X:k1, X <_{H} G -> F X <_{H} G.

Definition sMItGMIt: forall X : k1, X c_k1 GRan H G -> F X c_k1 GRan H G.
Proof.
  intros X h.
  apply toGRan.
  apply s.
  apply fromGRan.
  assumption.
Defined.

(** The following definition corresponds to the definition in the proof of Lemma 1 in the paper. *)
Definition GMIt0 : mu2 <_{H} G := fromGRan (MIt sMItGMIt).

Lemma GMIt0Red : 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), 
                 GMIt0 f (In ef (j:=j) n t) = 
          s (fun (A B:Set) (f: A ->  H B) => (GMIt0 f)  o (j A)) f t.
Proof.
  intros.
  unfold GMIt0 at 1.
  unfold fromGRan.
  rewrite MItRed.
  reflexivity.
Qed.

End GMIt0.

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.

Lemma 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 B f (In ef (j:=j) n t) = 
          s X (fun (A B:Set) (f: A ->  H B) => (GMIt s B f)  o (j A)) A B f t.
Proof.
  intros.
  unfold GMIt at 1.
  rewrite GMIt0Red.
  reflexivity.
Qed.

End LNGMItBaseImp.

Require Import LNMItImp.

Module LNGMItDefImpImp(LNMP:LNMItParam).

Module LNMItBaseImp := LNMIt LNMP.
Module LNGMItBaseImpImp := LNGMItBaseImp LNMItBaseImp.

Import LNGMItBaseImpImp.

Lemma 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.
Proof.
  reflexivity.
Qed.


Module LNGMItDefImpImp := LNGMItDef LNGMItBaseImpImp.
Module LNMItDefImp := LNGMItDefImpImp.LNMItDef.

Import LNGMItDefImpImp.
Import LNMItDefImp.

(* ensure that the same equation is proven below by reflexivity:
Check GMItRedCan : forall(H G:k1)(s:forall X:k1, X <_{H} G -> F X <_{H} G)
  (A B:Set)(f: A-> H B)(t:F mu2 A),
   GMIt s _ f (InCan t) = s _ (GMIt s) _ _ f t.
*)
Lemma GMItRedCan : forall(H G:k1)(s:forall X:k1, X <_{H} G -> F X <_{H} G)
  (A B:Set)(f: A-> H B)(t:F mu2 A),
   GMIt s _ f (InCan t) = s _ (GMIt s) _ _ f t.
Proof.
  reflexivity.
Qed.

(** Hence, in the impredicative encoding, the additional reduction rules are
     part of the convertibility relation. *)

End LNGMItDefImpImp.