+++ /dev/null
-(**************************************************************************)
-(* ___ *)
-(* ||M|| *)
-(* ||A|| A project by Andrea Asperti *)
-(* ||T|| *)
-(* ||I|| Developers: *)
-(* ||T|| The HELM team. *)
-(* ||A|| http://helm.cs.unibo.it *)
-(* \ / *)
-(* \ / This file is distributed under the terms of the *)
-(* v GNU General Public License Version 2 *)
-(* *)
-(**************************************************************************)
-
-(* ********************************************************************** *)
-(* Progetto FreeScale *)
-(* *)
-(* Sviluppato da: Cosimo Oliboni, oliboni@cs.unibo.it *)
-(* Cosimo Oliboni, oliboni@cs.unibo.it *)
-(* *)
-(* ********************************************************************** *)
-
-include "freescale/theory.ma".
-include "freescale/bool.ma".
-
-(* ******** *)
-(* BOOLEANI *)
-(* ******** *)
-
-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 ]
- ].
-
-ndefinition bool_destruct : bool_destruct_aux.
- #b1; #b2; #P;
- 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)
- ##]
-nqed.
-
-nlemma symmetric_eqbool : symmetricT bool bool eq_bool.
- #b1; #b2;
- nelim b1;
- nelim b2;
- nnormalize;
- napply refl_eq.
-nqed.
-
-nlemma symmetric_andbool : symmetricT bool bool and_bool.
- #b1; #b2;
- nelim b1;
- nelim b2;
- nnormalize;
- napply refl_eq.
-nqed.
-
-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 symmetric_orbool : symmetricT bool bool or_bool.
- #b1; #b2;
- nelim b1;
- nelim b2;
- nnormalize;
- napply refl_eq.
-nqed.
-
-nlemma associative_orbool : ∀b1,b2,b3.((b1 ⊕ b2) ⊕ b3) = (b1 ⊕ (b2 ⊕ b3)).
- #b1; #b2; #b3;
- nelim b1;
- nelim b2;
- nelim b3;
- nnormalize;
- napply refl_eq.
-nqed.
-
-nlemma symmetric_xorbool : symmetricT bool bool xor_bool.
- #b1; #b2;
- nelim b1;
- nelim b2;
- nnormalize;
- napply refl_eq.
-nqed.
-
-nlemma associative_xorbool : ∀b1,b2,b3.((b1 ⊙ b2) ⊙ b3) = (b1 ⊙ (b2 ⊙ b3)).
- #b1; #b2; #b3;
- nelim b1;
- nelim b2;
- nelim b3;
- nnormalize;
- napply refl_eq.
-nqed.
-
-nlemma eqbool_to_eq : ∀b1,b2:bool.(eq_bool b1 b2 = true) → (b1 = b2).
- #b1; #b2;
- ncases b1;
- ncases b2;
- nnormalize;
- ##[ ##1,4: #H; napply refl_eq
- ##| ##*: #H; napply (bool_destruct … H)
- ##]
-nqed.
-
-nlemma eq_to_eqbool : ∀b1,b2.b1 = b2 → eq_bool b1 b2 = true.
- #b1; #b2;
- ncases b1;
- ncases b2;
- nnormalize;
- ##[ ##1,4: #H; napply refl_eq
- ##| ##*: #H; napply (bool_destruct … H)
- ##]
-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)
- ##]
-nqed.
-
-nlemma andb_true_true_r: ∀b1,b2.(b1 ⊗ b2) = true → b2 = true.
- #b1; #b2;
- ncases b1;
- ncases b2;
- nnormalize;
- ##[ ##1,3: #H; napply refl_eq
- ##| ##*: #H; napply (bool_destruct … H)
- ##]
-nqed.
-
-nlemma orb_false_false_l : ∀b1,b2:bool.(b1 ⊕ b2) = false → b1 = false.
- #b1; #b2;
- ncases b1;
- ncases b2;
- nnormalize;
- ##[ ##4: #H; napply refl_eq
- ##| ##*: #H; napply (bool_destruct … H)
- ##]
-nqed.
-
-nlemma orb_false_false_r : ∀b1,b2:bool.(b1 ⊕ b2) = false → b2 = false.
- #b1; #b2;
- ncases b1;
- ncases b2;
- nnormalize;
- ##[ ##4: #H; napply refl_eq
- ##| ##*: #H; napply (bool_destruct … H)
- ##]
-nqed.