(** LNMItImp.v Version 2.6 July 2010 *) (** needs impredicative Set, runs under V8.3, tested with version rc1, 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 no longer conforms to the description in the article "An induction principle for nested datatypes in intensional type theory" by the author, that appeared in the Journal of Functional Programming, since it now uses type classes instead of the record [EFct] and the type [pEFct], as well as for [mon] and [NAT] 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. (** a device to parameterize the implementation *) Module Type LNMItParam. Parameter F: k2. (** the only general requirement: [F] preserves extensional functors *) Declare Instance FpEFct : pEFct F. (** the only axiom we want to use: proof irrelevance *) (** printing a1 %\ensuremath{a_1}% *) (** printing a2 %\ensuremath{a_2}% *) 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 *) (** printing c_k1 %\ensuremath{\subseteq}% *) 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 -> 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 *) Instance 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 f t)). Defined. (** the preliminary iterator with source [mu2E] does not iterate at all *) (** printing o %\ensuremath{\circ}% *) 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 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), (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 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. *) (** printing mu20 %\ensuremath{\mu_0}% *) Definition mu20 (A: Set) := {r: mu2E A | mu2Echeck r}. (** this is a convenient form to write [sig (mu2Echeck(A:= A))]. *) (** printing mu2 %\ensuremath{\mu}% *) 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: *) Instance mapmu2 : mon mu2. Proof. red. intros A B f r. destruct r as [r' p]. eexists (map 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 (map f r) = map 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 -> 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 -> NAT (pi1' j). 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 called [In] *) Definition In : InType. Proof. red. red. intros X ef j n A t. eexists (inE 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)(t: F G A)(B: Set)(f: A -> B), map f (In ef n t) = In ef n (m 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)(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), (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 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] *) (** printing r1 %\ensuremath{r_1}% *) (** printing r2 %\ensuremath{r_2}% *) 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 *) (** printing n1 %\ensuremath{n_1}% *) (** printing n2 %\ensuremath{n_2}% *) Lemma UNP : forall(X Y: k1)(j: X c_k1 Y)(mX: mon X)(mY: mon Y) (n1 n2: NAT j), 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 f t))(mapmu2 f (j' A t)) (n _ _ _ _)): NAT (Y:= mu2) j'). 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. f_equal. apply UNP. (** equates [n] and [pi1'pNAT n1] *) Qed. End LNMIt.