(** LNGMItImp.v Version 1.3a March 2009 *) (** needs 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 *) (** this is the implementation part where impredicative methods justify [LNGMIt] by reduction to [LNMIt] forms part of the code that comes with a submission to the journal Science of Computer Programming *) Set Implicit Arguments. Require Import Utf8. 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. (** printing c_k1 %\ensuremath{\subseteq}% *) Definition LeqRan (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 RanLeq(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 that represents the proof of Proposition 1 of the paper *) 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. (** 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. 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 LeqRan. apply s. apply RanLeq. assumption. Defined. (** The following definition corresponds to the definition in the proof of Proposition 1 in the paper. *) Definition GMIt0 : mu2 <_{H} G := RanLeq (MIt sMItGMIt). (** printing o %\ensuremath{\circ}% *) Lemma GMIt0Red : 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), 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 RanLeq. 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)(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)(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.