(** BushImp.v Version 2.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 *) (** we enjoy that we have the rich notion of convertibility that comes from the implementation in LNMItImp.v *) (** 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. Require Import LNMItImp. Require Import BushPred. Axiom pirr: forall (A:Prop) (a1 a2:A), a1 = a2. (** here, we fix our parameters for the impredicative implementation *) Module BushParam : LNMItParam with Definition F:=BushF with Definition FpEFct:=bushpEFct with Definition pirr:=pirr. Definition F:=BushF. Definition FpEFct:=bushpEFct. Definition pirr:=pirr. End BushParam. (** the impredicative implementation is used *) Module BushBase := LNMIt BushParam. Module BushM := LNMItDef BushBase. (** we reuse the predicative development *) Module BushDef := Bush BushBase. Import BushDef. (* bush's behaviour for the general constructors *) Lemma bush_bnil_ (A B:k0)(f:A->B)(G : k1) (ef : EFct G) (j : G c_k1 Bush) (n:NAT j (m ef) BushBase.mapmu2): bush f (bnil_ A ef n) = bnil_ B ef n. Proof. reflexivity. Qed. (** We profit from the extended convertibility relation. *) Lemma bush_bcons_ (A B:k0)(f:A->B)(G : k1) (ef : EFct G) (j : G c_k1 Bush) (n:NAT j (m ef) BushBase.mapmu2)(a:A)(b:G(G A)): bush f (bcons_ ef n a b) = bcons_ ef n (f a) (m ef (m ef f) b). Proof. induction ef. (* necessary *) reflexivity. Qed. (* now for the canonical constructors *) Lemma bush_bnil (A B:k0)(f:A->B): bush f (bnil A) = bnil B. Proof. reflexivity. Qed. Lemma bush_bcons (A B:k0)(f:A->B)(a:A)(b:Bush(Bush A)): bush f (bcons a b) = bcons (f a) (bush (bush f) b). Proof. reflexivity. Qed. Import List. (* the behaviour of BushToList for the canonical constructors *) Lemma BushToList_bnil (A:k0): BushToList (bnil A) = nil(A:=A). Proof. reflexivity. Qed. Lemma BushToList_bcons (A:k0)(a:A)(b:Bush (Bush A)): BushToList (bcons a b) = a::flat_map(BushToList(A:=A))(BushToList b). Proof. reflexivity. Qed. (* the more general cases *) Lemma BushToList_bnil_ (A:k0)(G : k1) (ef : EFct G) (j : G c_k1 Bush) (n:NAT j (m ef) BushBase.mapmu2): BushToList (bnil_ A ef n) = nil(A:=A). Proof. reflexivity. Qed. Lemma BushToList_bcons_ (A:k0)(G : k1) (ef : EFct G) (j : G c_k1 Bush) (n:NAT j (m ef) BushBase.mapmu2)(a:A)(b:G(G A)): BushToList (bcons_ ef n a b) = a::flat_map ((BushToList(A:=A)) o (j A)) (BushToList (j _ b)). Proof. reflexivity. Qed. (** In the proof of BushToListNAT, we do not profit from the extended convertibility relation. *) (** in the manual proof, we profit in the bnil case: *) Lemma BushToList_ok_manually (A B: k0)(f:A->B)(t:Bush A): BushToList(bush f t) = map f (BushToList t). Proof. intros. generalize B f; clear B f. apply (BushBase.mu2Ind (fun A t => forall (B : Set) (f : A -> B), BushToList (bush f t) = map f (BushToList t))). clear A t. intros. destruct t as [u|(a,b)]. induction u. reflexivity. (* bcons *) change (BushBase.In ef n (inr unit (a,b))) with (bcons_ ef n a b). rewrite BushToList_bcons_. rewrite bush_bcons_. rewrite BushToList_bcons_. simpl map. apply (f_equal (fun x=> f a::x)). clear a. simpl. rewrite <- (flat_mapLaw1 (j B) (BushToList (A:=B))). rewrite flat_mapLaw2. rewrite n. rewrite H. rewrite map_map. rewrite flat_mapLaw1. apply flat_mapext. intro. unfold comp. rewrite <- H. rewrite n. reflexivity. Qed. (** for the [bcons] case, the extended convertibility relation does not help since [simpl] would obfuscate the goal *) (* the behaviour of BushToValue on the general constructors *) Lemma BushToValue_bnil_ (A:k0)(G : k1) (ef : EFct G) (j : G c_k1 Bush) (n:NAT j (m ef) BushBase.mapmu2)(f:A->nat): BushToValue (bnil_ A ef n) f = 0. Proof. reflexivity. Qed. Lemma BushToValue_bcons_ (A:k0)(G : k1) (ef : EFct G) (j : G c_k1 Bush) (n:NAT j (m ef) BushBase.mapmu2)(a:A)(b:G(G A))(f:A->nat): BushToValue (bcons_ ef n a b) f = f a + BushToValue (j _ b) (fun x => BushToValue (j _ x) f). Proof. reflexivity. Qed. (* the following two lemmas are only necessary for a direct proof that sizeDirect is invariant under bush *) Lemma BushToValueExt (A:k0)(t:Bush A)(f g:A->nat): (forall a, f a = g a) -> BushToValue t f = BushToValue t g. Proof. intros A t. apply (BushBase.mu2Ind (fun A t => forall f g : A -> nat, (forall a : A, f a = g a) -> BushToValue t f = BushToValue t g)). clear A t. intros. destruct t as [u|(a,b)]. induction u. reflexivity. (* bcons *) change (BushBase.In ef n (inr unit (a,b))) with (bcons_ ef n a b). do 2 rewrite BushToValue_bcons_. rewrite H0. apply (f_equal (fun x => g a+ x)). apply H. clear a b. intro. apply H. assumption. Qed. (** once again, enriched convertibility does not help for the [bcons] case *) (* this is a pointwise formulation of naturality: *) Lemma BushToValueNat (A B : k0) (f : A -> B) (t : Bush A)(g:B->nat): BushToValue (bush f t) g = BushToValue t (g o f). (* the right-hand side is natCont_mon f (BushToValue t) g *) Proof. intros. generalize B f g; clear B f g. apply (BushBase.mu2Ind (fun A t => forall (B : k0)(f : A -> B) (g : B -> nat), BushToValue (bush f t) g = BushToValue t (g o f))). clear A t. intros. destruct t as [u|(a,b)]. induction u. reflexivity. (* bcons *) change (BushBase.In ef n (inr unit (a,b))) with (bcons_ ef n a b). rewrite bush_bcons_. do 2 rewrite BushToValue_bcons_. apply (f_equal (fun x => g(f a) + x)). rewrite n. rewrite H. apply BushToValueExt. clear a b. intro. unfold comp at 1. rewrite <- H. rewrite n. reflexivity. Qed. Lemma values (A:k0)(t:Bush A)(f:A->nat): listToValue (BushToList t) f = BushToValue t f. Proof. apply (BushBase.mu2Ind (fun A t => forall (f : A -> nat), listToValue (BushToList t) f = BushToValue t f)). intros. destruct t as [u|(a,b)]. (* bnil *) induction u. induction ef. reflexivity. (* bcons *) change (BushBase.In ef n (inr unit (a, b))) with (bcons_ ef n a b). rewrite BushToValue_bcons_. rewrite BushToList_bcons_. simpl listToValue. apply (f_equal (fun x=> f a + x)). rewrite <- H. rewrite listToValueFlat_map. apply listToValueExt. clear a b. intro. unfold comp. apply H. Qed. Lemma BushToCan_bnil_ (A:k0)(G : k1) (ef : EFct G) (j : G c_k1 Bush) (n:NAT j (m ef) BushBase.mapmu2): BushToCan (bnil_ A ef n) = bnil A. Proof. reflexivity. Qed. Lemma BushToCan_bcons_ (A:k0)(G : k1) (ef : EFct G) (j : G c_k1 Bush) (n:NAT j (m ef) BushBase.mapmu2)(a:A)(b:G(G A)): BushToCan(bcons_ ef n a b) = bcons a (bush (BushToCan (A:=A) o j A) ((BushToCan (A:=G A) o j (G A)) b)). Proof. reflexivity. Qed. (** once more, the extended convertibility relation is most valuable for a fully automatic proof *) Lemma BushToCan_bnil (A:k0): BushToCan (bnil A) = bnil A. Proof. reflexivity. Qed. Lemma BushToCan_bcons (A:k0)(a:A)(b:Bush(Bush A)): BushToCan (bcons a b) = bcons a (bush (BushToCan (A:=A)) (BushToCan b)). Proof. reflexivity. Qed. (* the following lemma is restricted to canH t *) Lemma bushExt_refined (A B:k0)(f g:A->B)(t:Bush A): canH t -> (forall a, a elem t -> f a = g a) -> bush f t = bush g t. Proof. intros. generalize B f g H0; clear B f g H0. (* induction over being canonical: *) induction H; intros. reflexivity. (* a very small improvement *) do 2 rewrite bush_bcons. assert (f a = g a). apply H2. apply elem1. rewrite H3. apply (f_equal (fun x => bcons (g a) x)). apply IHcanH. intros. apply H0. assumption. intros. apply H2. exact (@elem2 A a b a1 a0 H5 H4). Qed. (* canonical elements are not changed by canonization *) Theorem BushToCan_invariant (A:k0)(t:Bush A): canH t -> BushToCan t = t. Proof. intros. induction H. reflexivity. (* a very small improvement *) rewrite BushToCan_bcons. apply (f_equal (fun x=> bcons a x)). change BushBase.mu2 with Bush. (* hidden in implicit parameters *) rewrite IHcanH. transitivity (bush (id(A:=Bush A)) b). apply bushExt_refined. assumption. assumption. apply BushM.mapmu2Id. Qed. (* a preparation for the next lemma *) Lemma BushToCanNAT: NAT BushToCan bush bush. Proof. unfold BushToCan. unfold BushM.canonize. apply BushM.MItNAT. red. intros. destruct t as [u|(a,b)]. (* bnil *) reflexivity. (* bcons *) simpl BushFmon2br. (* full simplification would obfuscate the goal *) transitivity (bush f (bcons a (bush (it A) (it (X A) b)))). rewrite bush_bcons. unfold bcons. apply (f_equal (fun x => BushM.InCan (inr unit (f a, x)))). unfold moncomp. rewrite H. do 2 rewrite <- BushM.mapmu2Comp. apply BushM.mapmu2Ext. clear a b. intro. unfold comp. rewrite <- H. induction ef. reflexivity. reflexivity. Qed. (* we also give a direct proof without the concept canH *) Lemma BushToCan_idempotent_DIRECT (A:k0)(t:Bush A): BushToCan(BushToCan t) = BushToCan t. Proof. unfold BushToCan at 3. unfold BushM.canonize. apply BushM.MItUni. (* alternatively, one could approach this by a direct inductive proof: apply (BushM.mu2Ind (fun A t => BushToCan(BushToCan t) = BushToCan t). *) (* polyExtsub *) red. intros. destruct y as [u|(a,b)]. reflexivity. simpl. apply (f_equal (fun x => BushM.InCan (inr unit (a, x)))). rewrite H. apply BushM.mapmu2Ext. apply H. (* behaviour *) intros. destruct t as [u|(a,b)]. (* bnil *) induction u. induction ef. reflexivity. (* bcons *) change (BushBase.In ef n (inr unit (a, b))) with (bcons_ ef n a b). rewrite BushToCan_bcons_. rewrite BushToCan_bcons. simpl. unfold bcons. apply (f_equal (fun x => BushM.InCan (inr unit (a, x)))). unfold comp at 2 4. rewrite BushToCanNAT. rewrite <- BushM.mapmu2Comp. unfold comp. reflexivity. Qed.