From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Wed, 18 Apr 2007 10:08:40 +0000 (+0000)
Subject: more discriminate
X-Git-Tag: make_still_working~6377
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=9af0ac16488f57149c7d02aa5bbee47a81c7c342;p=helm.git

more discriminate
---

diff --git a/helm/software/matita/library/decidable_kit/eqtype.ma b/helm/software/matita/library/decidable_kit/eqtype.ma
index 97fdf8907..ae0b07541 100644
--- a/helm/software/matita/library/decidable_kit/eqtype.ma
+++ b/helm/software/matita/library/decidable_kit/eqtype.ma
@@ -102,11 +102,8 @@ cases b; cases x (s ps); cases y (t pt); simplify; intros (Hcmp);
     reflexivity;
   | cases (H (b2pT ? ? (eqP d s t) Hcmp))
   ]
-| constructor 2; unfold Not; intros (H);
-  (* XXX destruct H; *)
-  change in Hcmp with (cmp d (match {?,ps} with [(mk_sigma s _)⇒s]) t = false);
-  rewrite > H in Hcmp; simplify in Hcmp; rewrite > cmp_refl in Hcmp; destruct Hcmp;
-]
+| constructor 2; unfold Not; intros (H); destruct H; 
+  rewrite > Hcut in Hcmp; rewrite > cmp_refl in Hcmp; destruct Hcmp;] 
 qed. 
 
 definition sub_eqType ≝ λd : eqType.λp. mk_eqType ? ? (sigma_eq_dec d p).
@@ -143,12 +140,8 @@ cases a; cases b; simplify; intros (H);
 |2,3,5: destruct H;
 |4: rewrite > (b2pT ? ? (eqP d ? ?) H); reflexivity; 
 |6,7: unfold Not; intros (H1); destruct H1
-|8: unfold Not; intros (H1); 
-    (* ancora injection non va *)
-    cut (s = s1); [ rewrite > Hcut in H;  rewrite > cmp_refl in H;  destruct H;].
-    change with (match (Some d s) with
-                 [ None ⇒ s | (Some s) ⇒ s] = s1); rewrite > H1;
-                 simplify; reflexivity;] 
+|8: unfold Not; intros (H1); destruct H1; 
+    rewrite > Hcut in H;  rewrite > cmp_refl in H; destruct H;]
 qed.
 
 definition option_eqType : eqType → eqType ≝ λd:eqType.mk_eqType ? ? (ocmpP d).
diff --git a/helm/software/matita/library/decidable_kit/fintype.ma b/helm/software/matita/library/decidable_kit/fintype.ma
index ffd41d206..8f5de6e0a 100644
--- a/helm/software/matita/library/decidable_kit/fintype.ma
+++ b/helm/software/matita/library/decidable_kit/fintype.ma
@@ -46,7 +46,7 @@ rewrite < (leb_eqb x n); rewrite > H1; reflexivity;
 qed.
 
 lemma mem_filter :
-  ∀d1,d2:eqType.(*∀y:d1.*)∀x:d2.∀l:list d1.∀p:d1 → option d2.
+  ∀d1,d2:eqType.∀x:d2.∀l:list d1.∀p:d1 → option d2.
   (∀y.mem d1 y l = true → 
     match (p y) with [None ⇒ false | (Some q) ⇒ cmp d2 x q] = false) →
   mem d2 x (filter d1 d2 p l) = false.
diff --git a/helm/software/matita/library/decidable_kit/list_aux.ma b/helm/software/matita/library/decidable_kit/list_aux.ma
index d641d9018..b68858d68 100644
--- a/helm/software/matita/library/decidable_kit/list_aux.ma
+++ b/helm/software/matita/library/decidable_kit/list_aux.ma
@@ -96,13 +96,9 @@ cases c; intros (H); [ apply reflect_true | apply reflect_false ]
      | simplify;  intros;
        cases (b2pT ? ? (andbPF ? ?) (p2bT ? ? (negbP ?) H)); clear H;
        [ intros; lapply (b2pF ? ? (eqP d ? ?) H1) as H'; clear H1;
-         (* XXX destruct H; *)
-         change in H' with (Not ((match (x1::tl1) with [nil⇒x1|(cons x1 _) ⇒ x1]) = s));
-         rewrite > H in H'; simplify in H'; apply H'; reflexivity;
-       | intros; lapply (IH ? H1) as H';
-         (* XXX destruct H1 *)
-         change in H' with (Not ((match (x1::tl1) with [nil⇒tl1|(cons _ l) ⇒ l]) = l)); 
-         rewrite > H in H'; simplify in H'; apply H'; reflexivity;]]]]
+         destruct H; rewrite > Hcut in H'; apply H'; reflexivity;
+       | intros; lapply (IH ? H1) as H'; destruct H;
+         rewrite > Hcut1 in H'; apply H'; reflexivity;]]]]
 qed.
     
 definition list_eqType : eqType → eqType ≝ λd:eqType.mk_eqType ? ? (lcmpP d).