X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Flibrary%2Fdecidable_kit%2Ffintype.ma;h=e44b641977e2503d15308fcf4b6dd61b95ed2374;hb=5c10d402b5de7233bc83d7f685b274832e383212;hp=8f5de6e0aa85f5d9e445c2b86ed2b7705a4adba3;hpb=9af0ac16488f57149c7d02aa5bbee47a81c7c342;p=helm.git diff --git a/helm/software/matita/library/decidable_kit/fintype.ma b/helm/software/matita/library/decidable_kit/fintype.ma index 8f5de6e0a..e44b64197 100644 --- a/helm/software/matita/library/decidable_kit/fintype.ma +++ b/helm/software/matita/library/decidable_kit/fintype.ma @@ -12,8 +12,6 @@ (* *) (**************************************************************************) -set "baseuri" "cic:/matita/decidable_kit/fintype/". - include "decidable_kit/eqtype.ma". include "decidable_kit/list_aux.ma". @@ -39,10 +37,9 @@ definition segment_enum ≝ lemma iota_ltb : ∀x,p:nat. mem nat_eqType x (iota O p) = ltb x p. intros (x p); elim p; simplify;[reflexivity] -generalize in match (refl_eq ? (cmp ? x n)); -generalize in match (cmp ? x n) in ⊢ (? ? ? % → %); intros 1 (b); -cases b; simplify; intros (H1); rewrite > H; clear H; -rewrite < (leb_eqb x n); rewrite > H1; reflexivity; +apply (cmpP nat_eqType x n); intros (E); rewrite > H; clear H; simplify; +[1: symmetry; apply (p2bT ? ? (lebP ? ?)); rewrite > E; apply le_n; +|2: rewrite < (leb_eqb x n); rewrite > E; reflexivity;] qed. lemma mem_filter : @@ -52,36 +49,28 @@ lemma mem_filter : mem d2 x (filter d1 d2 p l) = false. intros 5 (d1 d2 x l p); elim l; simplify; [reflexivity] -generalize in match (refl_eq ? (p t)); -generalize in match (p t) in ⊢ (? ? ? % → %); intros 1 (b); cases b; clear b; intros (Hpt); +generalize in match (refl_eq ? (p a)); +generalize in match (p a) in ⊢ (? ? ? % → %); intros 1 (b); cases b; clear b; intros (Hpt); [1: apply H; intros (y Hyl); apply H1; simplify; rewrite > Hyl; rewrite > orbC; reflexivity; -|2: generalize in match (refl_eq ? (cmp ? x s)); - generalize in match (cmp ? x s) in ⊢ (? ? ? % → %); intros 1 (b); cases b; clear b; - [1: simplify; intros (Exs); - rewrite > orbC; rewrite > H; - [2: intros; apply H1; simplify; rewrite > H2; rewrite > orbC; reflexivity - |1: lapply (H1 t) as H2; [2: simplify; rewrite > cmp_refl; reflexivity] - rewrite > Hpt in H2; simplify in H2; rewrite > H2 in Exs; - destruct Exs;] - |2: intros (Dxs); simplify; rewrite > H; - [2: intros; apply (H1 y); simplify; rewrite > H2; rewrite > orbC; reflexivity - |1: rewrite > Dxs; reflexivity]]] +|2: simplify; apply (cmpP d2 x s); simplify; intros (E); + [1: rewrite < (H1 a); simplify; [rewrite > Hpt; rewrite > E] + simplify; rewrite > cmp_refl; reflexivity + |2: apply H; intros; apply H1; simplify; rewrite > H2; + rewrite > orbC; reflexivity]] qed. lemma count_O : ∀d:eqType.∀p:d→bool.∀l:list d. (∀x:d.mem d x l = true → notb (p x) = true) → count d p l = O. intros 3 (d p l); elim l; simplify; [1: reflexivity] -generalize in match (refl_eq ? (p t)); -generalize in match (p t) in ⊢ (? ? ? % → %); intros 1 (b); +generalize in match (refl_eq ? (p a)); +generalize in match (p a) in ⊢ (? ? ? % → %); intros 1 (b); cases b; simplify; [2:intros (Hpt); apply H; intros; apply H1; simplify; - generalize in match (refl_eq ? (cmp d x t)); - generalize in match (cmp d x t) in ⊢ (? ? ? % → %); intros 1 (b1); - cases b1; simplify; intros; [2:rewrite > H2] auto. -|1:intros (H2); lapply (H1 t); [2:simplify; rewrite > cmp_refl; simplify; auto] + apply (cmpP d x a); [2: rewrite > H2;]; intros; reflexivity; +|1:intros (H2); lapply (H1 a); [2:simplify; rewrite > cmp_refl; simplify; autobatch] rewrite > H2 in Hletin; simplify in Hletin; destruct Hletin] qed. @@ -93,36 +82,30 @@ cut (∀x:fsort. count fsort (cmp fsort x) enum = (S O)); [ apply (mk_finType fsort enum Hcut) | intros (x); cases x (n Hn); simplify in Hn; clear x; generalize in match Hn; generalize in match Hn; clear Hn; + unfold enum; unfold segment_enum; generalize in match bound in ⊢ (% → ? → ? ? (? ? ? (? ? ? ? %)) ?); - intros 1 (m); elim m (Hm Hn p IH Hm Hn); [ destruct Hm ] + intros 1 (m); elim m (Hm Hn p IH Hm Hn); [ simplify in Hm; destruct Hm ] simplify; cases (eqP bool_eqType (ltb p bound) true); simplify; - [1:unfold segment in ⊢ (? ? match ? % ? ? with [true⇒ ?|false⇒ ?] ?); - unfold nat_eqType in ⊢ (? ? match % with [true⇒ ?|false⇒ ?] ?); - simplify; - generalize in match (refl_eq ? (eqb n p)); - generalize in match (eqb n p) in ⊢ (? ? ? % → %); intros 1(b); cases b; clear b; - intros (Enp); simplify; - [2:rewrite > IH; [1,3: auto] + [1:unfold fsort; + unfold segment in ⊢ (? ? match ? % ? ? with [_ ⇒ ?|_ ⇒ ?] ?); + unfold nat_eqType in ⊢ (? ? match % with [_ ⇒ ?|_ ⇒ ?] ?); + simplify; apply (cmpP nat_eqType n p); intros (Enp); simplify; + [2:rewrite > IH; [1,3: autobatch] rewrite < ltb_n_Sm in Hm; rewrite > Enp in Hm; - generalize in match Hm; cases (ltb n p); intros; [reflexivity] - simplify in H1; destruct H1; + rewrite > orbC in Hm; assumption; |1:clear IH; rewrite > (count_O fsort); [reflexivity] - intros 1 (x); rewrite < (b2pT ? ? (eqP ? n ?) Enp); - cases x (y Hy); intros (ABS); clear x; - unfold segment; unfold notb; simplify; - generalize in match (refl_eq ? (cmp ? n y)); - generalize in match (cmp ? n y) in ⊢ (? ? ? % → %); intros 1 (b); cases b; clear b; - intros (Eny); simplify; [2:reflexivity] + intros 1 (x); rewrite < Enp; cases x (y Hy); + intros (ABS); clear x; unfold segment; unfold notb; simplify; + apply (cmpP ? n y); intros (Eny); simplify; [2:reflexivity] rewrite < ABS; symmetry; clear ABS; - generalize in match Hy; clear Hy; - rewrite < (b2pT ? ? (eqP nat_eqType ? ?) Eny); + generalize in match Hy; clear Hy;rewrite < Eny; simplify; intros (Hn); apply (mem_filter nat_eqType fsort); intros (w Hw); fold simplify (sort nat_eqType); (* CANONICAL?! *) cases (in_sub_eq nat_eqType (λx:nat_eqType.ltb x bound) w); simplify; [2: reflexivity] - generalize in match H1; clear H1; cases s; clear s; intros (H1); - unfold segment; simplify; simplify in H1; rewrite > H1; + generalize in match H1; clear H1; cases s (r Pr); clear s; intros (H1); + unfold fsort; unfold segment; simplify; simplify in H1; rewrite > H1; rewrite > iota_ltb in Hw; apply (p2bF ? ? (eqP nat_eqType ? ?)); unfold Not; intros (Enw); rewrite > Enw in Hw; rewrite > ltb_refl in Hw; destruct Hw] @@ -152,60 +135,50 @@ intros; cases a; cases b; reflexivity; qed. lemma uniq_tail : ∀d:eqType.∀x:d.∀l:list d. uniq d (x::l) = andb (negb (mem d x l)) (uniq d l). intros (d x l); elim l; simplify; [reflexivity] -generalize in match (refl_eq ? (cmp d x t)); -generalize in match (cmp d x t) in ⊢ (? ? ? % → %); intros 1 (b); cases b; clear b; -intros (E); simplify ; rewrite > E; [reflexivity] +apply (cmpP d x a); intros (E); simplify ; try rewrite > E; [reflexivity] rewrite > andbA; rewrite > andbC in ⊢ (? ? (? % ?) ?); rewrite < andbA; rewrite < H; rewrite > andbC in ⊢ (? ? ? (? % ?)); rewrite < andbA; reflexivity; qed. lemma count_O_mem : ∀d:eqType.∀x:d.∀l:list d.ltb O (count d (cmp d x) l) = mem d x l. -intros 3 (d x l); elim l [reflexivity] simplify; rewrite < H; cases (cmp d x t); +intros 3 (d x l); elim l [reflexivity] simplify; rewrite < H; cases (cmp d x a); reflexivity; qed. lemma uniqP : ∀d:eqType.∀l:list d. reflect (∀x:d.mem d x l = true → count d (cmp d x) l = (S O)) (uniq d l). -intros (d l); apply prove_reflect; elim l; [1: destruct H1 | 3: destruct H] +intros (d l); apply prove_reflect; elim l; [1: simplify in H1; destruct H1 | 3: simplify in H; destruct H] [1: generalize in match H2; simplify in H2; lapply (b2pT ? ? (orbP ? ?) H2) as H3; clear H2; cases H3; clear H3; intros; - [2: lapply (uniq_mem ? ? ? H1) as H4; - generalize in match (refl_eq ? (cmp d x t)); - generalize in match (cmp d x t) in ⊢ (? ? ? % → %); intros 1 (b); cases b; clear b; - intros (H5); - [1: simplify; rewrite > H5; simplify; rewrite > count_O; [reflexivity] - intros (y Hy); rewrite > (b2pT ? ? (eqP d ? ?) H5) in H2 H3 H4 ⊢ %; - clear H5; clear x; rewrite > H2 in H4; destruct H4; - |2: simplify; rewrite > H5; simplify; apply H; + [2: lapply (uniq_mem ? ? ? H1) as H4; simplify; apply (cmpP d x a); + intros (H5); simplify; + [1: rewrite > count_O; [reflexivity] + intros (y Hy); rewrite > H5 in H2 H3 ⊢ %; clear H5; clear x; + rewrite > H2 in H4; destruct H4; + |2: simplify; apply H; rewrite > uniq_tail in H1; cases (b2pT ? ? (andbP ? ?) H1); assumption;] |1: simplify; rewrite > H2; simplify; rewrite > count_O; [reflexivity] intros (y Hy); rewrite > (b2pT ? ? (eqP d ? ?) H2) in H3 ⊢ %; clear H2; clear x; lapply (uniq_mem ? ? ? H1) as H4; - generalize in match (refl_eq ? (cmp d t y)); - generalize in match (cmp d t y) in ⊢ (? ? ? % → %); intros 1 (b); cases b; clear b; intros (E); - [1: rewrite > (b2pT ? ? (eqP d ? ?) E) in H4; - rewrite > H4 in Hy; destruct Hy; - |2:intros; reflexivity]] -|2: rewrite > uniq_tail in H1; + apply (cmpP d a y); intros (E); [2: reflexivity]. + rewrite > E in H4; rewrite > H4 in Hy; destruct Hy;] +|2: rewrite > uniq_tail in H1; generalize in match (refl_eq ? (uniq d l1)); generalize in match (uniq d l1) in ⊢ (? ? ? % → %); intros 1 (b); cases b; clear b; [1: intros (E); rewrite > E in H1; rewrite > andbC in H1; simplify in H1; - unfold Not; intros (A); lapply (A t) as A'; + unfold Not; intros (A); lapply (A a) as A'; [1: simplify in A'; rewrite > cmp_refl in A'; simplify in A'; - destruct A'; clear A'; rewrite < count_O_mem in H1; - rewrite > Hcut in H1; destruct H1; + destruct A'; rewrite < count_O_mem in H1; + rewrite > Hcut in H1; simplify in H1; destruct H1; |2: simplify; rewrite > cmp_refl; reflexivity;] |2: intros (Ul1); lapply (H Ul1); unfold Not; intros (A); apply Hletin; intros (r Mrl1); lapply (A r); - [2: simplify; rewrite > Mrl1; cases (cmp d r t); reflexivity] - generalize in match (refl_eq ? (cmp d r t)); - generalize in match (cmp d r t) in ⊢ (? ? ? % → %); intros 1 (b); cases b; clear b; - [1: intros (E); simplify in Hletin1; rewrite > E in Hletin1; - destruct Hletin1; rewrite < count_O_mem in Mrl1; - rewrite > Hcut in Mrl1; destruct Mrl1; - |2: intros; simplify in Hletin1; rewrite > H2 in Hletin1; - simplify in Hletin1; apply (Hletin1);]]] + [2: simplify; rewrite > Mrl1; cases (cmp d r a); reflexivity] + generalize in match Hletin1; simplify; apply (cmpP d r a); + simplify; intros (E Hc); [2: assumption] + destruct Hc; rewrite < count_O_mem in Mrl1; + rewrite > Hcut in Mrl1; simplify in Mrl1; destruct Mrl1;]] qed. lemma mem_finType : ∀d:finType.∀x:d. mem d x (enum d) = true. @@ -222,42 +195,34 @@ lemma sub_enumP : ∀d:finType.∀p:d→bool.∀x:sub_eqType d p. intros (d p x); cases x (t Ht); clear x; generalize in match (mem_finType d t); generalize in match (uniq_fintype_enum d); -elim (enum d); [destruct H1] simplify; -cases (in_sub_eq d p t1); simplify; +elim (enum d); [simplify in H1; destruct H1] simplify; +cases (in_sub_eq d p a); simplify; [1:generalize in match H3; clear H3; cases s (r Hr); clear s; simplify; intros (Ert1); generalize in match Hr; clear Hr; rewrite > Ert1; clear Ert1; clear r; intros (Ht1); - unfold sub_eqType in ⊢ (? ? match ? (% ? ?) ? ? with [true⇒ ?|false⇒ ?] ?); - simplify; generalize in match (refl_eq ? (cmp d t t1)); - generalize in match (cmp d t t1) in ⊢ (? ? ? % → %); intros 1 (b); cases b; clear b; - intros (Ett1); simplify; + unfold sub_eqType in ⊢ (? ? match ? (% ? ?) ? ? with [_ ⇒ ?|_ ⇒ ?] ?); + simplify; apply (cmpP ? t a); simplify; intros (Ett1); [1: cut (count (sub_eqType d p) (cmp (sub_eqType d p) {t,Ht}) (filter d (sigma d p) (if_p d p) l) = O); [1:rewrite > Hcut; reflexivity] lapply (uniq_mem ? ? ? H1); generalize in match Ht; - rewrite > (b2pT ? ? (eqP d ? ?) Ett1); intros (Ht1'); clear Ht1; + rewrite > Ett1; intros (Ht1'); clear Ht1; generalize in match Hletin; elim l; [ reflexivity] - simplify; cases (in_sub_eq d p t2); simplify; + simplify; cases (in_sub_eq d p a1); simplify; [1: generalize in match H5; cases s; simplify; intros; clear H5; - unfold sub_eqType in ⊢ (? ? match ? (% ? ?) ? ? with [true⇒ ?|false⇒ ?] ?); + unfold sub_eqType in ⊢ (? ? match ? (% ? ?) ? ? with [_ ⇒ ?|_ ⇒ ?] ?); simplify; rewrite > H7; simplify in H4; - generalize in match H4; clear H4; - generalize in match (refl_eq ? (cmp d t1 t2)); - generalize in match (cmp d t1 t2) in ⊢ (? ? ? % → %); intros 1 (b); cases b; clear b; - simplify; intros; [1: destruct H5] apply H3; assumption; + generalize in match H4; clear H4; apply (cmpP ? a a1); + simplify; intros; [destruct H5] apply H3; assumption; |2: apply H3; - generalize in match H4; clear H4; simplify; - generalize in match (refl_eq ? (cmp d t1 t2)); - generalize in match (cmp d t1 t2) in ⊢ (? ? ? % → %); intros 1 (b); cases b; clear b; - simplify; intros; [1: destruct H6] assumption;] + generalize in match H4; clear H4; simplify; apply (cmpP ? a a1); + simplify; intros; [destruct H6] assumption;] |2: apply H; [ rewrite > uniq_tail in H1; cases (b2pT ? ? (andbP ? ?) H1); assumption] simplify in H2; rewrite > Ett1 in H2; simplify in H2; assumption] |2:rewrite > H; [1:reflexivity|2: rewrite > uniq_tail in H1; cases (b2pT ? ? (andbP ? ?) H1); assumption] - simplify in H2; generalize in match H2; generalize in match (refl_eq ? (cmp d t t1)); - generalize in match (cmp d t t1) in ⊢ (? ? ? % → %); intros 1 (b); cases b; clear b; - intros (E); [2:assumption] - lapply (b2pT ? ? (eqP d ? ?) E); clear H; rewrite > Hletin in Ht; - rewrite > Ht in H3; destruct H3;] + simplify in H2; generalize in match H2; apply (cmpP ? t a); + intros (E) [2:assumption] clear H; rewrite > E in Ht; rewrite > H3 in Ht; + destruct Ht;] qed. definition sub_finType : ∀d:finType.∀p:d→bool.finType ≝