X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=inline;f=helm%2Fsoftware%2Fmatita%2Flibrary%2Fdecidable_kit%2Ffintype.ma;h=82d54131bb494901801a8d3162382a76281b7fd6;hb=c640262bd3affd2a689ce401f4f48baca6421c53;hp=ad71a4511dd6d7583a5de136dd5b39dd3ffd1287;hpb=32d8d8d419e0b910435da275361bb55d49bc43a9;p=helm.git diff --git a/helm/software/matita/library/decidable_kit/fintype.ma b/helm/software/matita/library/decidable_kit/fintype.ma index ad71a4511..82d54131b 100644 --- a/helm/software/matita/library/decidable_kit/fintype.ma +++ b/helm/software/matita/library/decidable_kit/fintype.ma @@ -84,12 +84,14 @@ 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⇒ ?] ?); + [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; @@ -104,8 +106,8 @@ cut (∀x:fsort. count fsort (cmp fsort x) enum = (S O)); 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] @@ -135,7 +137,7 @@ 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] -apply (cmpP d x t); intros (E); simplify ; rewrite > E; [reflexivity] +apply (cmpP d x t); intros (E); simplify ; try rewrite > E; [reflexivity] rewrite > andbA; rewrite > andbC in ⊢ (? ? (? % ?) ?); rewrite < andbA; rewrite < H; rewrite > andbC in ⊢ (? ? ? (? % ?)); rewrite < andbA; reflexivity; qed. @@ -146,16 +148,16 @@ 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; simplify; apply (cmpP d x t); intros (H5); simplify; [1: rewrite > count_O; [reflexivity] - intros (y Hy); rewrite > H5 in H2 H3 H4 ⊢ %; clear H5; clear x; + intros (y Hy); rewrite > H5 in H2 H3 ⊢ %; clear H5; clear x; rewrite > H2 in H4; destruct H4; - |2: simplify; rewrite > H5; simplify; apply H; + |2: simplify; apply H; rewrite > uniq_tail in H1; cases (b2pT ? ? (andbP ? ?) H1); assumption;] |1: simplify; rewrite > H2; simplify; rewrite > count_O; [reflexivity] @@ -169,8 +171,8 @@ intros (d l); apply prove_reflect; elim l; [1: destruct H1 | 3: destruct H] [1: intros (E); rewrite > E in H1; rewrite > andbC in H1; simplify in H1; unfold Not; intros (A); lapply (A t) 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); @@ -178,7 +180,7 @@ intros (d l); apply prove_reflect; elim l; [1: destruct H1 | 3: destruct H] generalize in match Hletin1; simplify; apply (cmpP d r t); simplify; intros (E Hc); [2: assumption] destruct Hc; rewrite < count_O_mem in Mrl1; - rewrite > Hcut in Mrl1; destruct Mrl1;]] + rewrite > Hcut in Mrl1; simplify in Mrl1; destruct Mrl1;]] qed. lemma mem_finType : ∀d:finType.∀x:d. mem d x (enum d) = true. @@ -195,12 +197,12 @@ 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; +elim (enum d); [simplify in H1; destruct H1] simplify; cases (in_sub_eq d p t1); 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⇒ ?] ?); + unfold sub_eqType in ⊢ (? ? match ? (% ? ?) ? ? with [_ ⇒ ?|_ ⇒ ?] ?); simplify; apply (cmpP ? t t1); 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] @@ -210,7 +212,7 @@ cases (in_sub_eq d p t1); simplify; generalize in match Hletin; elim l; [ reflexivity] simplify; cases (in_sub_eq d p t2); 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; apply (cmpP ? t1 t2); simplify; intros; [destruct H5] apply H3; assumption;