(* *)
(**************************************************************************)
-set "baseuri" "cic:/matita/decidable_kit/decidable/".
-
(* classical connectives for decidable properties *)
include "decidable_kit/streicher.ma".
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] auto.
+intros 2 (P b); cases b; intros; [left|right] [autobatch.|autobatch;]
qed.
(* ### standard connectives/relations with reflection predicate ### *)
lemma andbPF : ∀a,b:bool. reflect (a = false ∨ b = false) (negb (andb a b)).
intros (a b); apply prove_reflect; cases a; cases b; simplify; intros (H);
-[1,2,3,4: rewrite > H; [1,2:right|3,4:left] reflexivity
+[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.
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);
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 ### *)
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 ]
(* OUT OF PLACE *)
lemma ltW : ∀n,m. n < m → n < (S m).
-intros; unfold lt; unfold lt in H; auto. qed.
+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;
[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 ? ?));