From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Sun, 9 Sep 2007 19:00:57 +0000 (+0000)
Subject: ...
X-Git-Tag: make_still_working~6031
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=32d8d8d419e0b910435da275361bb55d49bc43a9;p=helm.git

...
---

diff --git a/helm/software/matita/library/decidable_kit/eqtype.ma b/helm/software/matita/library/decidable_kit/eqtype.ma
index ae0b07541..88721632f 100644
--- a/helm/software/matita/library/decidable_kit/eqtype.ma
+++ b/helm/software/matita/library/decidable_kit/eqtype.ma
@@ -90,20 +90,12 @@ interpretation "sub_eqType" 'sig x h =
 lemma sigma_eq_dec : ∀d:eqType.∀p.∀x,y:sigma d p. 
   eq_compatible ? x y (cmp ? (sval ? ? x) (sval ? ?y)).
 intros (d p x y);
-generalize in match (refl_eq ? (cmp d (sval d p x) (sval d p y)));
-generalize in match (cmp d (sval d p x) (sval d p y)) in ⊢ (? ? ? % → %); intros 1 (b);
-cases b; cases x (s ps); cases y (t pt); simplify; intros (Hcmp);
-[ constructor 1;
-  generalize in match (eqP d s t); intros (Est);
-  cases Est (H); clear Est;
-  [ generalize in match ps;
-    rewrite > H; intros (pt'); 
-    rewrite < (pirrel bool (p t) true pt pt' (eqType_decidable bool_eqType));
-    reflexivity;
-  | cases (H (b2pT ? ? (eqP d s t) Hcmp))
-  ]
-| constructor 2; unfold Not; intros (H); destruct H; 
-  rewrite > Hcut in Hcmp; rewrite > cmp_refl in Hcmp; destruct Hcmp;] 
+cases (eqP d (sval ? ? x) (sval ? ? y)); generalize in match H; clear H; 
+cases x (s ps); cases y (t pt); simplify; intros (Est); 
+[1: constructor 1; generalize in match ps; rewrite > Est; intros (pt');
+    rewrite < (pirrel ? ? ? pt pt' (eqType_decidable bool_eqType)); reflexivity;
+|2: constructor 2; unfold Not; intros (H); destruct H;
+    cases (Est); assumption;]  
 qed. 
 
 definition sub_eqType ≝ λd : eqType.λp. mk_eqType ? ? (sigma_eq_dec d p).
@@ -153,9 +145,13 @@ coercion cic:/matita/decidable_kit/eqtype/option_canonical_eqType.con.
 definition test_canonical_option_eqType ≝ 
   (eq (option_eqType nat_eqType) O (S O)).
 
-(* OUT OF PLACE *)       
-lemma eqbC : ∀x,y:nat. eqb x y = eqb y x.
-intros (x y); apply bool_to_eq; split; intros (H); 
-rewrite > (b2pT ? ? (eqbP ? ?) H); rewrite > (cmp_refl nat_eqType);
-reflexivity;
+lemma cmpP : ∀d:eqType.∀x,y:d.∀P:bool → Prop. 
+  (x=y → P true) → (cmp d x y = false → P false) → P (cmp d x y).
+intros; cases (eqP ? x y); [2:apply H1; apply (p2bF ? ? (eqP d ? ?))] autobatch;
+qed.
+
+lemma cmpC : ∀d:eqType.∀x,y:d. cmp d x y = cmp d y x.
+intros; apply (cmpP ? x y); apply (cmpP ? y x); [1,4: intros; reflexivity]
+[intros (H2 H1) | intros (H1 H2)] rewrite > H1 in H2; rewrite > cmp_refl in H2; 
+destruct H2.      
 qed.
diff --git a/helm/software/matita/library/decidable_kit/fgraph.ma b/helm/software/matita/library/decidable_kit/fgraph.ma
index b2aca796b..a024ada3d 100644
--- a/helm/software/matita/library/decidable_kit/fgraph.ma
+++ b/helm/software/matita/library/decidable_kit/fgraph.ma
@@ -144,12 +144,9 @@ lemma mem_multes :
 intros (d e l s); elim l (hd tl IH); [cases s;simplify;[2: rewrite > andbC] reflexivity]
 simplify; rewrite > IH; cases s; simplify; [reflexivity]
 unfold list_eqType; simplify;
-generalize in match (refl_eq ? (cmp d e s1)); generalize in match (cmp d e s1) in ⊢ (? ? ? % → %);
-intros 1 (b); cases b; clear b; intros (E); cases (lcmp d l1 hd); 
-[1,2: rewrite > (b2pT ? ? (eqP ? ? ?) E); simplify; rewrite > cmp_refl; reflexivity
-|3,4: rewrite > andbC; simplify; [2: reflexivity] rewrite > orbC; 
-      simplify; apply (p2bF ? ? (eqP ? ? ?)); unfold Not; intros (H); rewrite > H in E;
-      rewrite > cmp_refl in E; destruct E;]
+apply (cmpP ? e s1); cases (lcmp d l1 hd); intros (E); 
+[1,2: rewrite > E; simplify; rewrite > cmp_refl; reflexivity
+|3,4: rewrite > cmpC; rewrite > E; simplify; reflexivity;]
 qed.
 
 lemma mem_concat: 
@@ -166,15 +163,13 @@ lemma mem_multss :
   match x in list with [ Nil ⇒ false | (Cons he tl) ⇒ andb (mem ? he s) (mem ? tl l)].
 intros (d s l x); elim s; [cases x] simplify; try reflexivity; rewrite > mem_concat;
 rewrite > H; clear H; rewrite > mem_multes; cases x; simplify; [reflexivity]
-unfold list_eqType; simplify;
-generalize in match (refl_eq ? (cmp d t s1)); generalize in match (cmp d t s1) in ⊢ (? ? ? % → %);
-intros 1 (b); cases b; clear b; intros (E); cases (mem d s1 l1);
-[1,2: rewrite > (b2pT ? ? (eqP ? ? ?) E); rewrite > cmp_refl; simplify;
+unfold list_eqType; simplify; apply (cmpP ? t s1); intros (E); 
+cases (mem d s1 l1);
+[1,2: rewrite > E; rewrite > cmp_refl; simplify;
       [rewrite > orb_refl | rewrite > orbC ] reflexivity
 |3,4: simplify; rewrite > orbC; simplify; [reflexivity] symmetry;
       apply (p2bF ? ? (andbP ? ?)); unfold Not; intros (H); decompose;
-      rewrite > (b2pT ? ? (eqP ? ? ?) H1) in E; rewrite > cmp_refl in E;
-      destruct E]
+      rewrite > cmpC in H1; rewrite > E in H1; destruct H1;] 
 qed.   
 
 lemma mem_mkpermr_size : 
diff --git a/helm/software/matita/library/decidable_kit/fintype.ma b/helm/software/matita/library/decidable_kit/fintype.ma
index 9b2dbadb9..ad71a4511 100644
--- a/helm/software/matita/library/decidable_kit/fintype.ma
+++ b/helm/software/matita/library/decidable_kit/fintype.ma
@@ -39,10 +39,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 :
@@ -57,17 +56,11 @@ generalize in match (p t) in ⊢ (? ? ? % → %); intros 1 (b); cases b; clear b
 [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 t); 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 : 
@@ -78,9 +71,7 @@ generalize in match (refl_eq ? (p t));
 generalize in match (p t) 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] autobatch.
+   apply (cmpP d x t); [2: rewrite > H2;]; intros; reflexivity;
 |1:intros (H2); lapply (H1 t); [2:simplify; rewrite > cmp_refl; simplify; autobatch]
    rewrite > H2 in Hletin; simplify in Hletin; destruct Hletin]
 qed.    
@@ -99,24 +90,16 @@ cut (∀x:fsort. count fsort (cmp fsort x) enum = (S O));
    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;
+      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);
@@ -152,9 +135,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]
-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 t); intros (E); simplify ; rewrite > E; [reflexivity]
 rewrite > andbA; rewrite > andbC in ⊢ (? ? (? % ?) ?); rewrite < andbA;
 rewrite < H; rewrite > andbC in ⊢ (? ? ? (? % ?)); rewrite < andbA; reflexivity;
 qed.
@@ -169,25 +150,20 @@ intros (d l); apply prove_reflect; elim l; [1: destruct H1 | 3: 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: 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; 
+            rewrite > H2 in H4; destruct H4;
          |2: simplify; rewrite > H5; 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 t 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;
@@ -198,14 +174,11 @@ intros (d l); apply prove_reflect; elim l; [1: destruct H1 | 3: destruct H]
         |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 t); reflexivity]
+        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;]]
 qed.
     
 lemma mem_finType : ∀d:finType.∀x:d. mem d x (enum d) = true. 
@@ -228,36 +201,28 @@ cases (in_sub_eq d p t1); simplify;
    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; 
+   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]
        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; 
        [1: generalize in match H5; cases s; simplify; intros; clear H5; 
            unfold sub_eqType in ⊢ (? ? match ? (% ? ?) ? ? with [true⇒ ?|false⇒ ?] ?);
            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 ? t1 t2);
+           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 ? t1 t2);
+           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 t1); 
+   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 ≝