freescale porting, work in progress

[helm.git] / helm / software / matita / contribs / ng_assembly / num / bool_lemmas.ma

diff --git a/helm/software/matita/contribs/ng_assembly/num/bool_lemmas.ma b/helm/software/matita/contribs/ng_assembly/num/bool_lemmas.ma
index 9190adda8e40f22174decaae0d3abfa2be6d3d52..b7b9096e871706bddcb98a46ce4b85db2221168c 100755 (executable)
--- a/helm/software/matita/contribs/ng_assembly/num/bool_lemmas.ma
+++ b/helm/software/matita/contribs/ng_assembly/num/bool_lemmas.ma
@@ -28,29 +28,14 @@ include "num/bool.ma".
 
 ndefinition bool_destruct_aux ≝
 Πb1,b2:bool.ΠP:Prop.b1 = b2 →
- match b1 with
-  [ true ⇒ match b2 with [ true ⇒ P → P | false ⇒ P ]
-  | false ⇒ match b2 with [ true ⇒ P | false ⇒ P → P ]
-  ].
+ match eq_bool b1 b2 with [ true ⇒ P → P | false ⇒ P ].
 
 ndefinition bool_destruct : bool_destruct_aux.
- #b1; #b2; #P;
+ #b1; #b2; #P; #H;
+ nrewrite < H;
  nelim b1;
- nelim b2;
  nnormalize;
- #H;
- ##[ ##2: napply False_ind;
-          nchange with (match true with [ true ⇒ False | false ⇒ True]);
-          nrewrite > H;
-          nnormalize;
-          napply I
- ##| ##3: napply False_ind;
-          nchange with (match true with [ true ⇒ False | false ⇒ True]);
-          nrewrite < H;
-          nnormalize;
-          napply I
- ##| ##1,4: napply (λx:P.x)
- ##]
+ napply (λx.x).
 nqed.
 
 nlemma symmetric_eqbool : symmetricT bool bool eq_bool.
@@ -138,7 +123,17 @@ nlemma decidable_bool : ∀x,y:bool.decidable (x = y).
  nelim x;
  nelim y;
  ##[ ##1,4: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
- ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); nnormalize; #H; napply False_ind; napply (bool_destruct … H)
+ ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …);
+          nnormalize; #H;
+          napply False_ind;
+          napply (bool_destruct … H)
+ ##]
+nqed.
+
+nlemma decidable_bexpr : ∀x.(x = true) ∨ (x = false).
+ #x; ncases x;
+ ##[ ##1: napply (or2_intro1 (true = true) (true = false) (refl_eq …))
+ ##| ##2: napply (or2_intro2 (false = true) (false = false) (refl_eq …))
  ##]
 nqed.
 
@@ -162,6 +157,34 @@ nlemma neq_to_neqbool : ∀b1,b2.b1 ≠ b2 → eq_bool b1 b2 = false.
  ##]
 nqed.
 
+nlemma eqfalse_to_neqtrue : ∀x.x = false → x ≠ true.
+ #x; nelim x;
+ ##[ ##1: #H; napply (bool_destruct … H)
+ ##| ##2: #H; nnormalize; #H1; napply (bool_destruct … H1)
+ ##]
+nqed.
+
+nlemma eqtrue_to_neqfalse : ∀x.x = true → x ≠ false.
+ #x; nelim x;
+ ##[ ##1: #H; nnormalize; #H1; napply (bool_destruct … H1)
+ ##| ##2: #H; napply (bool_destruct … H)
+ ##]
+nqed.
+
+nlemma neqfalse_to_eqtrue : ∀x.x ≠ false → x = true.
+ #x; nelim x;
+ ##[ ##1: #H; napply refl_eq
+ ##| ##2: nnormalize; #H; nelim (H (refl_eq …))
+ ##]
+nqed.
+
+nlemma neqtrue_to_eqfalse : ∀x.x ≠ true → x = false.
+ #x; nelim x;
+ ##[ ##1: nnormalize; #H; nelim (H (refl_eq …))
+ ##| ##2: #H; napply refl_eq
+ ##]
+nqed.
+
 nlemma andb_true_true_l: ∀b1,b2.(b1 ⊗ b2) = true → b1 = true.
  #b1; #b2;
  ncases b1;