From: Claudio Sacerdoti Coen Date: Sun, 28 Oct 2007 16:05:41 +0000 (+0000) Subject: New syntax for match patterns. X-Git-Tag: 0.4.95@7852~83 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=5f8818258f5de42780fbdbc95813bd36e124e096;p=helm.git New syntax for match patterns. New semantics for destruct. --- diff --git a/matita/library/decidable_kit/fintype.ma b/matita/library/decidable_kit/fintype.ma index ad71a4511..9002bab6a 100644 --- a/matita/library/decidable_kit/fintype.ma +++ b/matita/library/decidable_kit/fintype.ma @@ -88,8 +88,8 @@ cut (∀x:fsort. count fsort (cmp fsort x) enum = (S O)); generalize in match bound in ⊢ (% → ? → ? ? (? ? ? (? ? ? ? %)) ?); intros 1 (m); elim m (Hm Hn p IH Hm Hn); [ 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 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; @@ -169,7 +169,7 @@ 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; + destruct A'; rewrite < count_O_mem in H1; rewrite > Hcut in H1; destruct H1; |2: simplify; rewrite > cmp_refl; reflexivity;] |2: intros (Ul1); lapply (H Ul1); unfold Not; intros (A); apply Hletin; @@ -200,7 +200,7 @@ 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 +210,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;