(no commit message)

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

diff --git a/helm/software/matita/contribs/ng_assembly/freescale/bool_lemmas.ma b/helm/software/matita/contribs/ng_assembly/freescale/bool_lemmas.ma
index 5c08f23f34a377db04f3fb540f1ee581965e5be6..5d05eb19575e34ee6197ca328355e9b14de26402 100755 (executable)
--- a/helm/software/matita/contribs/ng_assembly/freescale/bool_lemmas.ma
+++ b/helm/software/matita/contribs/ng_assembly/freescale/bool_lemmas.ma
@@ -31,32 +31,32 @@ include "freescale/bool.ma".
 (* BOOLEANI *)
 (* ******** *)
 
-ndefinition boolRelation : Type → Type ≝
-λA:Type.A → A → bool. 
-
-ndefinition boolSymmetric: ∀A:Type.∀R:boolRelation A.Prop ≝
-λA.λR.∀x,y:A.R x y = R y x.
-
-ntheorem bool_destruct_true_false : true ≠ false.
- nnormalize;
- #H;
- nchange with (match true with [ true ⇒ False | false ⇒ True]);
- nrewrite > H;
- nnormalize;
- napply I.
-nqed.
-
-ntheorem bool_destruct_false_true : false ≠ true.
+ndefinition bool_destruct :
+ Π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 ]
+  ].
+ #b1; #b2; #P;
+ nelim b1;
+ nelim b2;
  nnormalize;
  #H;
- nchange with (match true with [ true ⇒ False | false ⇒ True]);
- nrewrite < H;
- nnormalize;
- napply I.
+ ##[ ##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)
+ ##]
 nqed.
 
-nlemma bsymmetric_eqbool : boolSymmetric bool eq_bool.
- nnormalize;
+nlemma symmetric_eqbool : symmetricT bool bool eq_bool.
  #b1; #b2;
  nelim b1;
  nelim b2;
@@ -64,8 +64,7 @@ nlemma bsymmetric_eqbool : boolSymmetric bool eq_bool.
  napply (refl_eq ??).
 nqed.
 
-nlemma bsymmetric_andbool : boolSymmetric bool and_bool.
- nnormalize;
+nlemma symmetric_andbool : symmetricT bool bool and_bool.
  #b1; #b2;
  nelim b1;
  nelim b2;
@@ -73,17 +72,16 @@ nlemma bsymmetric_andbool : boolSymmetric bool and_bool.
  napply (refl_eq ??).
 nqed.
 
-nlemma bsymmetric_orbool : boolSymmetric bool or_bool.
- nnormalize;
- #b1; #b2;
+nlemma associative_andbool : ∀b1,b2,b3.((b1 ⊗ b2) ⊗ b3) = (b1 ⊗ (b2 ⊗ b3)).
+ #b1; #b2; #b3;
  nelim b1;
  nelim b2;
+ nelim b3;
  nnormalize;
  napply (refl_eq ??).
 nqed.
 
-nlemma bsymmetric_xorbool : boolSymmetric bool xor_bool.
- nnormalize;
+nlemma symmetric_orbool : symmetricT bool bool or_bool.
  #b1; #b2;
  nelim b1;
  nelim b2;
@@ -91,63 +89,94 @@ nlemma bsymmetric_xorbool : boolSymmetric bool xor_bool.
  napply (refl_eq ??).
 nqed.
 
-nlemma eqbool_to_eq : ∀b1,b2:bool.(eq_bool b1 b2 = true) → (b1 = b2).
- #b1; #b2;
+nlemma associative_orbool : ∀b1,b2,b3.((b1 ⊕ b2) ⊕ b3) = (b1 ⊕ (b2 ⊕ b3)).
+ #b1; #b2; #b3;
  nelim b1;
  nelim b2;
+ nelim b3;
  nnormalize;
- #H;
- ##[ ##2,3: nelim (bool_destruct_false_true H) ##]
  napply (refl_eq ??).
 nqed.
 
-nlemma eq_to_eqbool : ∀b1,b2.b1 = b2 → eq_bool b1 b2 = true.
+nlemma symmetric_xorbool : symmetricT bool bool xor_bool.
  #b1; #b2;
  nelim b1;
  nelim b2;
  nnormalize;
- #H;
- ##[ ##2: nelim (bool_destruct_true_false H)
- ##| ##3: nelim (bool_destruct_false_true H) ##]
  napply (refl_eq ??).
 nqed.
 
-nlemma andb_true_true: ∀b1,b2.(b1 ⊗ b2) = true → b1 = true.
- #b1; #b2;
+nlemma associative_orbool : ∀b1,b2,b3.((b1 ⊙ b2) ⊙ b3) = (b1 ⊙ (b2 ⊙ b3)).
+ #b1; #b2; #b3;
  nelim b1;
  nelim b2;
+ nelim b3;
  nnormalize;
- #H;
- ##[ ##3,4: nelim (bool_destruct_false_true H) ##]
  napply (refl_eq ??).
 nqed.
 
+nlemma eqbool_to_eq : ∀b1,b2:bool.(eq_bool b1 b2 = true) → (b1 = b2).
+ #b1; #b2; #H;
+ nletin K ≝ (bool_destruct ?? (b1 = b2) H);
+ nelim b1 in K:(%) ⊢ %;
+ nelim b2;
+ nnormalize;
+ ##[ ##2,3: #H; napply H
+ ##| ##1,4: #H; napply (refl_eq ??)
+ ##]
+nqed.
+
+nlemma eq_to_eqbool : ∀b1,b2.b1 = b2 → eq_bool b1 b2 = true.
+ #b1; #b2; #H;
+ nletin K ≝ (bool_destruct ?? (eq_bool b1 b2 = true) H);
+ nelim b1 in K:(%) ⊢ %;
+ nelim b2;
+ nnormalize;
+ ##[ ##2,3: #H; napply H
+ ##| ##1,4: #H; napply (refl_eq ??)
+ ##]
+nqed.
+
+nlemma andb_true_true_l: ∀b1,b2.(b1 ⊗ b2) = true → b1 = true.
+ #b1; #b2; #H;
+ nletin K ≝ (bool_destruct ?? (b1 = true) H);
+ nelim b1 in K:(%) ⊢ %;
+ nelim b2;
+ nnormalize;
+ ##[ ##3,4: #H; napply H
+ ##| ##1,2: #H; napply (refl_eq ??)
+ ##]
+nqed.
+
 nlemma andb_true_true_r: ∀b1,b2.(b1 ⊗ b2) = true → b2 = true.
- #b1; #b2;
- nelim b1;
+ #b1; #b2; #H;
+ nletin K ≝ (bool_destruct ?? (b2 = true) H);
+ nelim b1 in K:(%) ⊢ %;
  nelim b2;
  nnormalize;
- #H;
- ##[ ##2,3,4: nelim (bool_destruct_false_true H) ##]
- napply (refl_eq ??).
+ ##[ ##2,4: #H; napply H
+ ##| ##1,3: #H; napply (refl_eq ??)
+ ##]
 nqed.
 
-nlemma orb_false_false : ∀b1,b2:bool.(b1 ⊕ b2) = false → b1 = false.
- #b1; #b2;
- nelim b1;
+nlemma orb_false_false_l : ∀b1,b2:bool.(b1 ⊕ b2) = false → b1 = false.
+ #b1; #b2; #H;
+ nletin K ≝ (bool_destruct ?? (b1 = false) H);
+ nelim b1 in K:(%) ⊢ %;
  nelim b2;
  nnormalize;
- #H;
- ##[ ##1,2: nelim (bool_destruct_true_false H) ##]
- napply (refl_eq ??).
+ ##[ ##1,2,3: #H; napply H
+ ##| ##4: #H; napply (refl_eq ??)
+ ##]
 nqed.
 
 nlemma orb_false_false_r : ∀b1,b2:bool.(b1 ⊕ b2) = false → b2 = false.
- #b1; #b2;
- nelim b1;
+ #b1; #b2; #H;
+ nletin K ≝ (bool_destruct ?? (b2 = false) H);
+ nelim b1 in K:(%) ⊢ %;
  nelim b2;
  nnormalize;
- #H;
- ##[ ##1,3: nelim (bool_destruct_true_false H) ##]
- napply (refl_eq ??).
+ ##[ ##1,2,3: #H; napply H
+ ##| ##4: #H; napply (refl_eq ??)
+ ##]
 nqed.