From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Sun, 18 May 2008 18:31:45 +0000 (+0000)
Subject: Dummy dependent types are no longer cleaned in inductive type arities.
X-Git-Tag: make_still_working~5163
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=d9faaa76c5c1a3f679ff78a8757d59a9fd07fcbc;p=helm.git

Dummy dependent types are no longer cleaned in inductive type arities.
---

diff --git a/helm/software/matita/library/decidable_kit/fgraph.ma b/helm/software/matita/library/decidable_kit/fgraph.ma
index 5b28071dc..2d02d113d 100644
--- a/helm/software/matita/library/decidable_kit/fgraph.ma
+++ b/helm/software/matita/library/decidable_kit/fgraph.ma
@@ -152,7 +152,7 @@ qed.
 lemma mem_concat: 
   ∀d:eqType. ∀x.∀l1,l2:list d.
     mem d x (l1 @ l2) = orb (mem d x l1) (mem d x l2).
-intros; elim l1; [reflexivity] simplify; cases (cmp d x t); simplify; [reflexivity|assumption]
+intros; elim l1; [reflexivity] simplify; cases (cmp d x a); simplify; [reflexivity|assumption]
 qed.
 
 lemma orb_refl : ∀x.orb x x = x. intros (x); cases x; reflexivity; qed. 
@@ -163,7 +163,7 @@ 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; apply (cmpP ? t s1); intros (E); 
+unfold list_eqType; simplify; apply (cmpP ? a s1); intros (E); 
 cases (mem d s1 l1);
 [1,2: rewrite > E; rewrite > cmp_refl; simplify;
       [rewrite > orb_refl | rewrite > orbC ] reflexivity
diff --git a/helm/software/matita/library/decidable_kit/fintype.ma b/helm/software/matita/library/decidable_kit/fintype.ma
index 82d54131b..9d6b30e59 100644
--- a/helm/software/matita/library/decidable_kit/fintype.ma
+++ b/helm/software/matita/library/decidable_kit/fintype.ma
@@ -51,13 +51,13 @@ 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: simplify; apply (cmpP d2 x s); simplify; intros (E);
-    [1: rewrite < (H1 t); simplify; [rewrite > Hpt; rewrite > 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]]
@@ -67,12 +67,12 @@ 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;
-   apply (cmpP d x t); [2: rewrite > H2;]; intros; reflexivity;
-|1:intros (H2); lapply (H1 t); [2:simplify; rewrite > cmp_refl; simplify; autobatch]
+   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.    
     
@@ -137,13 +137,13 @@ 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 ; try 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. 
@@ -152,7 +152,7 @@ intros (d l); apply prove_reflect; elim l; [1: simplify in H1; destruct H1 | 3:
 [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);  
+    [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; 
@@ -163,21 +163,21 @@ intros (d l); apply prove_reflect; elim l; [1: simplify in H1; destruct H1 | 3:
     |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;
-        apply (cmpP d t y); intros (E); [2: reflexivity].
+        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'; 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 Hletin1; simplify; apply (cmpP d r t); 
+          [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;]]
@@ -198,31 +198,31 @@ 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); [simplify in H1; destruct H1] simplify;  
-cases (in_sub_eq d p t1); 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 [_ ⇒ ?|_ ⇒ ?] ?); 
-   simplify; apply (cmpP ? t t1); simplify; intros (Ett1);
+   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 > 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 [_ ⇒ ?|_ ⇒ ?] ?);
            simplify; rewrite > H7; simplify in H4;
-           generalize in match H4; clear H4; apply (cmpP ? t1 t2);
+           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; apply (cmpP ? t1 t2);
+           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; apply (cmpP ? t t1); 
+   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.