(** LNMItImp.v Version 2.0 January 2008 *)
(** needs impredicative Set, runs under V8.1, tested with 8.1pl3, also runs under V8.4, tested with 8.4pl1 *)

(** Copyright Ralph Matthes, I.R.I.T.,  C.N.R.S. & University of Toulouse *)

(** this is the implementation part where impredicative methods justify LNMIt, 
    based on ideas of Venanzio Capretta to represent simultaneous
    inductive-recursive definitions  *)

(** this is code that conforms to the description in the article
    "An induction principle for nested datatypes in intensional type theory"
    by the author, to appear in the Journal of Functional Programming *)

Set Implicit Arguments.

Require Import LNMItPred.

(** a device to parameterize the implementation *)
Module Type LNMItParam.

Parameter F:k2.

(** the only general requirement: F preserves extensional functors *)
Parameter FpEFct : pEFct F.

(** the only axiom we want to use: proof irrelevance *)
Axiom pirr :  forall (A:Prop) (a1 a2:A), a1 = a2.

End LNMItParam.

(** the implementation of LNMIt for a given F and FpEFct *)
Module LNMIt(LNMP:LNMItParam) <: LNMIt_Type with Definition F:=LNMP.F
     with Definition FpEFct:=LNMP.FpEFct.
(* with "<:", we do not encapsulate the definitions *)

Import LNMP.

Definition F:= F.
Definition FpEFct:= FpEFct.
Definition pirr:= pirr.

(** the type of the iterator, parameterized over the source constructor *)
Definition MItPretype (S:k1) : Type :=
  forall G : k1, (forall X : k1, X c_k1 G -> F X c_k1 G) -> S c_k1 G.


(** the following inductive definition is only a record *)
Inductive mu2E:Set -> Set :=
   inE : forall (G:k1)(ef:EFct G)(G':k1)(m':mon G')
          (it:MItPretype G')(j: G c_k1 G'), NAT j (m ef) m' ->
          F G c_k1 mu2E.
(** the rough intention is that we only want to use inE with G':=mu2,
     m':=mapmu2 and it:=MIt. *)

(** We do not want to have j as implicit argument due to eta-problems. *)
Implicit Arguments inE [G G' m' A].

(** the preliminary map term *)
Definition mapmu2E : mon mu2E.
Proof.
  red.
  intros A B f r.
  destruct r as [G ef G' m' it j n A t].
  exact  (inE(A:=B) ef it j n (m (FpEFct ef) f t)).
Defined.

(** the preliminary iterator with source mu2E does not iterate at all *)
Definition MItE : MItPretype mu2E.
Proof.
  red.
  intros G s A r.
  destruct r as [G0 ef G' m' it j n A t].
  exact (s G0 (fun A => (it G s A) o (j A)) A t).
Defined.

Lemma MItERed : forall (G:k1)(s:forall X : k1, X c_k1 G -> F X c_k1 G)(A:Set)
  (X:k1)(ef:EFct X)(G':k1)(m':mon G')(it:MItPretype G') 
   (j: X c_k1 G') n (t:F X A),
   MItE s (inE (m':=m') ef it j n t) = s X (fun A => (it G s A) o (j A)) A t.
Proof.
  reflexivity.
Qed.

(** single out the good elements of mu2E A *)
Inductive mu2Echeck : forall (A:Set), mu2E A -> Prop :=
   inEcheck : forall (G:k1)(ef:EFct G)(j: G c_k1 mu2E)
       (n: NAT j (m ef) mapmu2E),
       (forall (A:Set)(t:G A), mu2Echeck (j A t)) ->
     forall (A: Set)(t:F G A),
       mu2Echeck (inE ef MItE (fun A t => j A t) n t).
(** this expansion of j will later be needed *)

Implicit Arguments inEcheck [G A].

(*
Check mu2Echeck_ind : forall P : forall A : Set, mu2E A -> Prop,
       (forall (G : k1) (ef : EFct G) (j : G c_k1 mu2E)
          (n : NAT j (m ef) mapmu2E),
        (forall (A : Set) (t : G A), mu2Echeck (j A t)) ->
        (forall (A : Set) (t : G A), P A (j A t)) ->
        forall (A : Set) (t : F G A),
        P A
          (inE ef MItE (fun (A: Set) (t : G A) => j A t) n t)) ->
       forall (A : Set) (r : mu2E A), mu2Echeck r -> P A r.
*)

Definition mu20 (A:Set) := {r:mu2E A | mu2Echeck r}.
(** this is a convenient form to write sig (mu2Echeck(A:=A)). *)

Definition mu2 : k1 := fun A => mu20 A.

Definition mu2cons (A:Set)(r:mu2E A)(p:mu2Echeck r) : mu2 A :=
  exist (fun r : mu2E A => mu2Echeck r) r p.

Implicit Arguments mu2cons [A].

(** a non-iterative definition of the monotonicity witness *)
Definition mapmu2 : mon mu2.
Proof.
  red.
  intros A B f r.
  destruct r as [r' p].
  eexists (mapmu2E f r').
  destruct p.
  simpl.
  apply inEcheck.
  assumption.
Defined.


(** the usual projections from a sig are proj1_sig and proj2_sig *)
Definition pi1 : mu2 c_k1 mu2E.
Proof.
  red.
  intros A r.
  exact (proj1_sig r).
Defined.

Definition MItType: Type := MItPretype mu2.

Definition MIt0 : MItType.
Proof.
  intros G s A r.
  exact (MItE s (pi1 r)).
Defined.
(** This has been very easy since mu2 is only the source type 
      of the transformation. Therefore, we did not even need "destruct r".
      Had we used it nevertheless, we would have encountered problems
      with eta. *)

(** the specification dictates this second eta-expansion *)
Definition MIt : MItPretype mu2 := fun G s A r => MIt0 s r.

Lemma pi2 : forall(A:Set)(r:mu2 A), mu2Echeck (pi1 r).
Proof.
  intros.
  exact (proj2_sig r).
Qed.

(** first projection commutes with the maps *)
Lemma pi1mapmu2 : forall (A B:Set)(f:A->B)(r:mu2 A),
  pi1 (mapmu2 f r) = mapmu2E f (pi1 r).
Proof.
  intros.
  destruct r.
  reflexivity.
Qed.

(** the type of the future datatype constructor In *)
Definition InType : Type := 
    forall (X:k1)(ef:EFct X)(j: X c_k1 mu2), NAT j (m ef) mapmu2 ->
        F X c_k1 mu2.

Definition pi1' (X:k1)(j: X c_k1 mu2): X c_k1 mu2E.
Proof.
  red.
  intros.
  exact (pi1 (j A H)).
Defined.

Lemma pi1'pNAT : forall (X:k1)(m:mon X)(j: X c_k1 mu2), 
  NAT j m mapmu2 -> NAT (pi1' j) m mapmu2E.
Proof.
  red.
  intros.
  unfold pi1'.
  rewrite H.
  apply pi1mapmu2.
Qed. 

Lemma pi2' : forall(X:k1)(j: X c_k1 mu2)(A:Set)(t: X A), 
             mu2Echeck (pi1' j A t).
Proof.
  intros.
  exact (pi2 (j A t)).
Qed.

(** in is reserved for Coq, so the datatype constructor will be In *)
Definition In : InType.
Proof.
  red.
  red.
  intros X ef j n A t.
  eexists (inE(A:=A)(m':=mapmu2E) ef MItE (pi1' j) (pi1'pNAT n) t).
  unfold pi1'.
  change   (fun (A0 : Set) (H : X A0) => pi1 (j A0 H)) with
  (fun A0 H => (fun A0 H => pi1 (j A0 H)) A0 H).
  apply inEcheck.
  exact (pi2' j). 
Defined.

Lemma mapmu2Red : forall (A:Set)(G:k1)(ef:EFct G)(j: G c_k1 mu2)
    (n: NAT j (m ef) mapmu2)(t: F G A)(B:Set)(f:A->B), 
             mapmu2 f (In ef n t) = In ef n (m (FpEFct ef) f t).
Proof.
  reflexivity.  
Qed.

Lemma MItRed : forall (G : k1)
  (s : forall X : k1, X c_k1 G -> F X c_k1 G)(X : k1)(ef:EFct X)(j: X c_k1 mu2)
      (n: NAT j (m ef) mapmu2)(A:Set)(t:F X A),
     MIt s (In ef n t) = s X (fun A => (MIt s (A:=A)) o (j A)) A t.
Proof.
(* for a proof "by hand", do the following:
  intros.
  unfold MIt at 1.
  unfold MIt0.
  unfold In.
  simpl pi1.
  simpl MItE.
  unfold MIt.
  unfold MIt0.
  unfold pi1'.
  unfold comp.
*)
  reflexivity.
Qed.

(** our desired induction principle, first just as a proposition *)
Definition mu2IndType : Prop :=
  forall P : (forall A : Set, mu2 A -> Prop),
       (forall (X : k1)(ef:EFct X)(j : X c_k1 mu2)(n: NAT j (m ef) mapmu2),
          (forall (A : Set) (x : X A), P A (j A x)) ->
        forall (A:Set)(t : F X A), P A (In ef n t)) ->
    forall (A : Set) (r : mu2 A), P A r.

Scheme mu2EcheckInd := Induction for mu2Echeck Sort Prop.

(*
Check mu2EcheckInd : 
      forall P : forall (A : Set) (r' : mu2E A), mu2Echeck r' -> Prop,
       (forall (G : k1) (ef : EFct G) (j : G c_k1 mu2E)
          (n : NAT j (m ef) mapmu2E)
          (k : forall (A : Set) (t : G A), mu2Echeck (j A t)),
        (forall (A : Set) (t : G A), P A (j A t) (k A t)) ->
        forall (A : Set) (t : F G A),
        P A
          (inE ef MItE (fun (A0 : Set) (t0 : G A0) => j A0 t0) n t)
          (inEcheck ef j n k t)) ->
       forall (A : Set) (r' : mu2E A) (p : mu2Echeck r'), P A r' p.
*)

(** the first consequence of proof irrelevance we will use is injectivity of pi1 *)
Lemma mu2pirr : forall (A:Set)(r1 r2:mu2 A), pi1 r1 = pi1 r2 -> r1 = r2.
Proof.
  intros.
  destruct r1 as [r1' H1].
  destruct r2 as [r2' H2].
  simpl in H.
  generalize H1 H2; clear H1 H2.
  destruct H.
  intros.
  rewrite (pirr H1 H2).
  reflexivity.
Qed.

(** the second consequence of proof irrelevance we will use: uniqueness of
      naturality proofs  *)
Lemma UNP : forall(X Y:k1)(j:X c_k1 Y)(mX:mon X)(mY:mon Y)
    (n1 n2: NAT j mX mY), n1 = n2.
Proof.
  intros.
  apply pirr.
Qed.

(** the main theorem of the whole approach *)
Lemma mu2Ind : mu2IndType.
Proof.
  red.
  intros P s A r.
  destruct r as [r' p].
  change (P A (exist (fun r : mu2E A => mu2Echeck r) r' p)) with 
    (P A (mu2cons r' p)).
  induction p using mu2EcheckInd.
  rename m into k.
  set (j':=fun (A : Set) (t : G A) => mu2cons(j A t)(k A t)).
  change (forall (A : Set) (t : G A), P A (mu2cons (j A t) (k A t)))
    with (forall (A : Set) (t : G A), P A (j' A t)) in H.
(* the following would be an interactive version of the later setting of n1,
    and it would work equally well in the proof:
  assert (n1 : NAT (Y:=mu2) j' (LNMItPred.m ef) mapmu2).
  red. 
  clear A t. 
  intros.
  apply mu2pirr.
  simpl.
  apply n.
*)
  set (n1:=(fun(A B : Set) (f : A -> B) (t : G A) => 
      mu2pirr (j' B (LNMItPred.m ef f t))(mapmu2 f (j' A t)) (n _ _ _ _)): 
      NAT (Y:=mu2) j' (LNMItPred.m ef) mapmu2).
  set (p:=s G ef j' n1 H A t : P A (In ef n1 t)).
  apply (eq_ind _ (fun r => P A r) p).
  apply mu2pirr. 
  simpl.
  apply (f_equal (fun x : NAT (fun A t => j A t) (LNMItPred.m ef) mapmu2E 
                               => inE ef MItE _ x t)).
  apply UNP. (** equates n and pi1'pNAT n1 *)
Qed.

End LNMIt.