(* Progetto FreeScale *)
(* *)
(* Sviluppato da: Ing. Cosimo Oliboni, oliboni@cs.unibo.it *)
-(* Ultima modifica: 05/08/2009 *)
+(* Sviluppo: 2008-2010 *)
(* *)
(* ********************************************************************** *)
(* BOOLEANI *)
(* ******** *)
+(*
ndefinition bool_destruct_aux ≝
Πb1,b2:bool.ΠP:Prop.b1 = b2 →
match eq_bool b1 b2 with [ true ⇒ P → P | false ⇒ P ].
nnormalize;
napply (λx.x).
nqed.
+*)
nlemma symmetric_eqbool : symmetricT bool bool eq_bool.
#b1; #b2;
ncases b2;
nnormalize;
##[ ##1,4: #H; napply refl_eq
- ##| ##*: #H; napply (bool_destruct … H)
+ ##| ##*: #H; ndestruct (*napply (bool_destruct … H)*)
##]
nqed.
ncases b2;
nnormalize;
##[ ##1,4: #H; napply refl_eq
- ##| ##*: #H; napply (bool_destruct … H)
+ ##| ##*: #H; ndestruct (*napply (bool_destruct … H)*)
##]
nqed.
##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …);
nnormalize; #H;
napply False_ind;
- napply (bool_destruct … H)
+ ndestruct (*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.
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.
##]
nqed.
+nlemma eqfalse_to_neqtrue : ∀x.x = false → x ≠ true.
+ #x; nelim x;
+ ##[ ##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; ndestruct (*napply (bool_destruct … H1)*)
+ ##| ##2: #H; ndestruct (*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;
ncases b2;
nnormalize;
##[ ##1,2: #H; napply refl_eq
- ##| ##*: #H; napply (bool_destruct … H)
+ ##| ##*: #H; ndestruct (*napply (bool_destruct … H)*)
##]
nqed.
ncases b2;
nnormalize;
##[ ##1,3: #H; napply refl_eq
- ##| ##*: #H; napply (bool_destruct … H)
+ ##| ##*: #H; ndestruct (*napply (bool_destruct … H)*)
##]
nqed.
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)
##]
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)
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)
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)
ncases b2;
nnormalize;
##[ ##4: #H; napply refl_eq
- ##| ##*: #H; napply (bool_destruct … H)
+ ##| ##*: #H; ndestruct (*napply (bool_destruct … H)*)
##]
nqed.
ncases b2;
nnormalize;
##[ ##4: #H; napply refl_eq
- ##| ##*: #H; napply (bool_destruct … H)
+ ##| ##*: #H; ndestruct (*napply (bool_destruct … H)*)
##]
nqed.