X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2Fng_assembly%2Fnum%2Fbool_lemmas.ma;h=db5214c6d16fd5092ce33a1507b0bfaad9f3c9c1;hb=3e373f30525987b7b121ed74c8a1292dc71d185c;hp=b7b9096e871706bddcb98a46ce4b85db2221168c;hpb=9dc61a4f11210bccf34f63f48968afca4261c1b4;p=helm.git 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 b7b9096e8..db5214c6d 100755 --- a/helm/software/matita/contribs/ng_assembly/num/bool_lemmas.ma +++ b/helm/software/matita/contribs/ng_assembly/num/bool_lemmas.ma @@ -16,7 +16,7 @@ (* Progetto FreeScale *) (* *) (* Sviluppato da: Ing. Cosimo Oliboni, oliboni@cs.unibo.it *) -(* Ultima modifica: 05/08/2009 *) +(* Sviluppo: 2008-2010 *) (* *) (* ********************************************************************** *) @@ -26,6 +26,7 @@ include "num/bool.ma". (* BOOLEANI *) (* ******** *) +(* ndefinition bool_destruct_aux ≝ Πb1,b2:bool.ΠP:Prop.b1 = b2 → match eq_bool b1 b2 with [ true ⇒ P → P | false ⇒ P ]. @@ -37,6 +38,7 @@ ndefinition bool_destruct : bool_destruct_aux. nnormalize; napply (λx.x). nqed. +*) nlemma symmetric_eqbool : symmetricT bool bool eq_bool. #b1; #b2; @@ -103,7 +105,7 @@ nlemma eqbool_to_eq : ∀b1,b2:bool.(eq_bool b1 b2 = true) → (b1 = b2). ncases b2; nnormalize; ##[ ##1,4: #H; napply refl_eq - ##| ##*: #H; napply (bool_destruct … H) + ##| ##*: #H; ndestruct (*napply (bool_destruct … H)*) ##] nqed. @@ -113,7 +115,7 @@ nlemma eq_to_eqbool : ∀b1,b2.b1 = b2 → eq_bool b1 b2 = true. ncases b2; nnormalize; ##[ ##1,4: #H; napply refl_eq - ##| ##*: #H; napply (bool_destruct … H) + ##| ##*: #H; ndestruct (*napply (bool_destruct … H)*) ##] nqed. @@ -126,7 +128,7 @@ nlemma decidable_bool : ∀x,y:bool.decidable (x = y). ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); nnormalize; #H; napply False_ind; - napply (bool_destruct … H) + ndestruct (*napply (bool_destruct … H)*) ##] nqed. @@ -142,8 +144,8 @@ nlemma neqbool_to_neq : ∀b1,b2:bool.(eq_bool b1 b2 = false) → (b1 ≠ b2). ncases b1; ncases b2; nnormalize; - ##[ ##1,4: #H; napply (bool_destruct … H) - ##| ##*: #H; #H1; napply (bool_destruct … H1) + ##[ ##1,4: #H; ndestruct (*napply (bool_destruct … H)*) + ##| ##*: #H; #H1; ndestruct (*napply (bool_destruct … H1)*) ##] nqed. @@ -159,15 +161,15 @@ 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) + ##[ ##1: #H; ndestruct (*napply (bool_destruct … H)*) + ##| ##2: #H; nnormalize; #H1; ndestruct (*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) + ##[ ##1: #H; nnormalize; #H1; ndestruct (*napply (bool_destruct … H1)*) + ##| ##2: #H; ndestruct (*napply (bool_destruct … H)*) ##] nqed. @@ -191,7 +193,7 @@ nlemma andb_true_true_l: ∀b1,b2.(b1 ⊗ b2) = true → b1 = true. ncases b2; nnormalize; ##[ ##1,2: #H; napply refl_eq - ##| ##*: #H; napply (bool_destruct … H) + ##| ##*: #H; ndestruct (*napply (bool_destruct … H)*) ##] nqed. @@ -201,7 +203,7 @@ nlemma andb_true_true_r: ∀b1,b2.(b1 ⊗ b2) = true → b2 = true. ncases b2; nnormalize; ##[ ##1,3: #H; napply refl_eq - ##| ##*: #H; napply (bool_destruct … H) + ##| ##*: #H; ndestruct (*napply (bool_destruct … H)*) ##] nqed. @@ -212,7 +214,7 @@ nlemma andb_false2 ncases b1; ncases b2; nnormalize; - ##[ ##1: #H; napply (bool_destruct … H) + ##[ ##1: #H; ndestruct (*napply (bool_destruct … H)*) ##| ##2,4: #H; napply (or2_intro2 … H) ##| ##3: #H; napply (or2_intro1 … H) ##] @@ -226,7 +228,7 @@ nlemma andb_false3 ncases b2; ncases b3; nnormalize; - ##[ ##1: #H; napply (bool_destruct … H) + ##[ ##1: #H; ndestruct (*napply (bool_destruct … H)*) ##| ##5,6,7,8: #H; napply (or3_intro1 … H) ##| ##2,4: #H; napply (or3_intro3 … H) ##| ##3: #H; napply (or3_intro2 … H) @@ -242,7 +244,7 @@ nlemma andb_false4 ncases b3; ncases b4; nnormalize; - ##[ ##1: #H; napply (bool_destruct … H) + ##[ ##1: #H; ndestruct (*napply (bool_destruct … H)*) ##| ##9,10,11,12,13,14,15,16: #H; napply (or4_intro1 … H) ##| ##5,6,7,8: #H; napply (or4_intro2 … H) ##| ##3,4: #H; napply (or4_intro3 … H) @@ -260,7 +262,7 @@ nlemma andb_false5 ncases b4; ncases b5; nnormalize; - ##[ ##1: #H; napply (bool_destruct … H) + ##[ ##1: #H; ndestruct (*napply (bool_destruct … H)*) ##| ##17,18,19,20,21,22,23,24,25,26,27,28,29,30,31,32: #H; napply (or5_intro1 … H) ##| ##9,10,11,12,13,14,15,16: #H; napply (or5_intro2 … H) ##| ##5,6,7,8: #H; napply (or5_intro3 … H) @@ -307,7 +309,7 @@ nlemma orb_false_false_l : ∀b1,b2:bool.(b1 ⊕ b2) = false → b1 = false. ncases b2; nnormalize; ##[ ##4: #H; napply refl_eq - ##| ##*: #H; napply (bool_destruct … H) + ##| ##*: #H; ndestruct (*napply (bool_destruct … H)*) ##] nqed. @@ -317,6 +319,6 @@ nlemma orb_false_false_r : ∀b1,b2:bool.(b1 ⊕ b2) = false → b2 = false. ncases b2; nnormalize; ##[ ##4: #H; napply refl_eq - ##| ##*: #H; napply (bool_destruct … H) + ##| ##*: #H; ndestruct (*napply (bool_destruct … H)*) ##] nqed.