X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Flibrary%2Fdecidable_kit%2Fdecidable.ma;h=b2b21ccd26aa50e693b4b3e88cbe424076cc03a5;hb=e880d6eab5e1700f4a625ddcd7d0fa8f0cce2dcc;hp=3aaa4a6ae51420415aeac5c8615214f847d4b8a3;hpb=680039d60c1d69521f84580ee0069cb2d6ff56ba;p=helm.git

diff --git a/helm/software/matita/library/decidable_kit/decidable.ma b/helm/software/matita/library/decidable_kit/decidable.ma
index 3aaa4a6ae..b2b21ccd2 100644
--- a/helm/software/matita/library/decidable_kit/decidable.ma
+++ b/helm/software/matita/library/decidable_kit/decidable.ma
@@ -12,8 +12,6 @@
 (*                                                                        *)
 (**************************************************************************)
 
-set "baseuri" "cic:/matita/decidable_kit/decidable/".
-
 (* classical connectives for decidable properties *)
 
 include "decidable_kit/streicher.ma".
@@ -56,6 +54,11 @@ intros (b); cases b; [ constructor 1; reflexivity | constructor 2;]
 unfold Not; intros (H); destruct H;
 qed.
 
+lemma prove_reflect : ∀P:Prop.∀b:bool.
+  (b = true → P) → (b = false → ¬P) → reflect P b.
+intros 2 (P b); cases b; intros; [left|right] [autobatch.|autobatch;]
+qed.   
+  
 (* ### standard connectives/relations with reflection predicate ### *)
 
 definition negb : bool → bool ≝ λb.match b with [ true ⇒ false | false ⇒ true].
@@ -69,22 +72,16 @@ definition andb : bool → bool → bool ≝
   λa,b:bool. match a with [ true ⇒ b | false ⇒ false ].
   
 lemma andbP : ∀a,b:bool. reflect (a = true ∧ b = true) (andb a b).
-intros (a b); 
-generalize in match (refl_eq ? (andb a b));
-generalize in match (andb a b) in ⊢ (? ? ? % → %); intros 1 (c);
-cases c; intros (H); [ apply reflect_true | apply reflect_false ];
-generalize in match H; clear H;
-cases a; simplify; 
-[1: intros (E); rewrite > E; split; reflexivity
-|2: intros (ABS); destruct ABS
-|3: intros (E); rewrite > E; unfold Not; intros (ABS); decompose;  destruct H1
-|4: intros (E); unfold Not; intros (ABS); decompose; destruct H]
+intros (a b); apply prove_reflect; cases a; cases b; simplify; intros (H);
+[1,2,3,4: rewrite > H; split; reflexivity;
+|5,6,7,8: unfold Not; intros (H1); cases H1; 
+          [destruct H|destruct H3|destruct H2|destruct H2]]
 qed.
 
 lemma andbPF : ∀a,b:bool. reflect (a = false ∨ b = false) (negb (andb a b)).
-intros (a b); cases a; cases b; simplify;
-[1: apply reflect_false | *: apply reflect_true ]
-[unfold Not; intros (H); cases H; destruct H1|right|left|left] reflexivity;
+intros (a b); apply prove_reflect; cases a; cases b; simplify; intros (H);
+[1,2,3,4: try rewrite > H; [1,2:right|3,4:left] reflexivity
+|5,6,7,8: unfold Not; intros (H1); [2,3,4: destruct H]; cases H1; destruct H2]
 qed.
 
 definition orb : bool → bool → bool ≝
@@ -97,7 +94,7 @@ intros (a b); cases a; cases b; simplify;
 qed. 
 
 lemma orbC : ∀a,b. orb a b = orb b a.
-intros (a b); cases a; cases b; auto. qed.
+intros (a b); cases a; cases b; autobatch. qed.
 
 lemma lebP: ∀x,y. reflect (x ≤ y) (leb x y).
 intros (x y); generalize in match (leb_to_Prop x y); 
@@ -110,7 +107,7 @@ intros (n); apply (p2bT ? ? (lebP ? ?)); apply le_n; qed.
 
 lemma lebW : ∀n,m. leb (S n) m = true → leb n m = true.
 intros (n m H); lapply (b2pT ? ? (lebP ? ?) H); clear H;
-apply (p2bT ? ? (lebP ? ?)); auto.
+apply (p2bT ? ? (lebP ? ?)); apply lt_to_le; assumption.
 qed. 
 
 definition ltb ≝ λx,y.leb (S x) y.
@@ -120,7 +117,7 @@ intros (x y); apply (lebP (S x) y);
 qed.
 
 lemma ltb_refl : ∀n.ltb n n = false.
-intros (n); apply (p2bF ? ? (ltbP ? ?)); auto; 
+intros (n); apply (p2bF ? ? (ltbP ? ?)); autobatch; 
 qed.
     
 (* ### = between booleans as <-> in Prop ### *)    
@@ -140,8 +137,8 @@ qed.
 
 lemma leb_eqb : ∀n,m. orb (eqb n m) (leb (S n) m) = leb n m.
 intros (n m); apply bool_to_eq; split; intros (H);
-[1:cases (b2pT ? ? (orbP ? ?) H); [2: auto] 
-   rewrite > (eqb_true_to_eq ? ? H1); auto
+[1:cases (b2pT ? ? (orbP ? ?) H); [2: (*autobatch type;*) apply lebW; assumption; ] 
+   rewrite > (eqb_true_to_eq ? ? H1); autobatch
 |2:cases (b2pT ? ? (lebP ? ?) H); 
    [ elim n; [reflexivity|assumption] 
    | simplify; rewrite > (p2bT ? ? (lebP ? ?) H1); rewrite > orbC ]
@@ -150,7 +147,8 @@ qed.
 
 
 (* OUT OF PLACE *)
-lemma ltW : ∀n,m. n < m → n < (S m). intros; auto. qed.
+lemma ltW : ∀n,m. n < m → n < (S m).
+intros; unfold lt; unfold lt in H; autobatch. qed.
 
 lemma ltbW : ∀n,m. ltb n m = true → ltb n (S m) = true.
 intros (n m H); letin H1 ≝ (b2pT ? ? (ltbP ? ?) H); clearbody H1;
@@ -170,7 +168,7 @@ intros (m n); apply bool_to_eq; split;
 [1: intros; cases (b2pT ? ? (orbP ? ?) H); [1: apply ltbW; assumption]
     rewrite > (eqb_true_to_eq ? ? H1); simplify; 
     rewrite > leb_refl; reflexivity  
-|2: generalize in match m; clear m; elim n 0;
+|2: elim n in m ⊢ % 0;
     [1: simplify; intros; cases n1; reflexivity;
     |2: intros 1 (m); elim m 0;
         [1: intros; apply (p2bT ? ? (orbP ? ?));