]> matita.cs.unibo.it Git - helm.git/blob - matita/matita/re_complete/basics/bool.ma
arithmetics for λδ
[helm.git] / matita / matita / re_complete / basics / bool.ma
1 include "basics/relations.ma".
2
3 (********** bool **********)
4 inductive bool: Type[0] ≝ 
5   | true : bool
6   | false : bool.
7
8 theorem not_eq_true_false : true ≠ false.
9 @nmk #Heq destruct
10 qed.
11
12 definition notb : bool → bool ≝
13 λ b:bool. match b with [true ⇒ false|false ⇒ true ].
14
15 interpretation "boolean not" 'not x = (notb x).
16
17 theorem notb_elim: ∀ b:bool.∀ P:bool → Prop.
18 match b with
19 [ true ⇒ P false
20 | false ⇒ P true] → P (notb b).
21 #b #P elim b normalize // qed.
22
23 theorem notb_notb: ∀b:bool. notb (notb b) = b.
24 #b elim b // qed.
25
26 theorem injective_notb: injective bool bool notb.
27 #b1 #b2 #H <(notb_notb b1) <(notb_notb b2) @eq_f // qed.
28
29 theorem noteq_to_eqnot: ∀b1,b2. b1 ≠ b2 → b1 = notb b2.
30 * * // #H @False_ind /2/
31 qed.
32
33 theorem eqnot_to_noteq: ∀b1,b2. b1 = notb b2 → b1 ≠ b2.
34 * * normalize // #H @(not_to_not … not_eq_true_false) //
35 qed.
36
37 definition andb : bool → bool → bool ≝
38 λb1,b2:bool. match b1 with [ true ⇒ b2 | false ⇒ false ].
39
40 interpretation "boolean and" 'and x y = (andb x y).
41
42 theorem andb_elim: ∀ b1,b2:bool. ∀ P:bool → Prop.
43 match b1 with [ true ⇒ P b2 | false ⇒ P false] → P (b1 ∧ b2).
44 #b1 #b2 #P (elim b1) normalize // qed.
45
46 theorem andb_true_l: ∀ b1,b2. (b1 ∧ b2) = true → b1 = true.
47 #b1 (cases b1) normalize // qed.
48
49 theorem andb_true_r: ∀b1,b2. (b1 ∧ b2) = true → b2 = true.
50 #b1 #b2 (cases b1) normalize // (cases b2) // qed.
51
52 theorem andb_true: ∀b1,b2. (b1 ∧ b2) = true → b1 = true ∧ b2 = true.
53 /3/ qed.
54
55 definition orb : bool → bool → bool ≝
56 λb1,b2:bool.match b1 with [ true ⇒ true | false ⇒ b2].
57  
58 interpretation "boolean or" 'or x y = (orb x y).
59
60 theorem orb_elim: ∀ b1,b2:bool. ∀ P:bool → Prop.
61 match b1 with [ true ⇒ P true | false ⇒ P b2] → P (orb b1 b2).
62 #b1 #b2 #P (elim b1) normalize // qed.
63
64 lemma orb_true_r1: ∀b1,b2:bool. 
65   b1 = true → (b1 ∨ b2) = true.
66 #b1 #b2 #H >H // qed.
67
68 lemma orb_true_r2: ∀b1,b2:bool. 
69   b2 = true → (b1 ∨ b2) = true.
70 #b1 #b2 #H >H cases b1 // qed.
71
72 lemma orb_true_l: ∀b1,b2:bool. 
73   (b1 ∨ b2) = true → (b1 = true) ∨ (b2 = true).
74 * normalize /2/ qed.
75
76 definition xorb : bool → bool → bool ≝
77 λb1,b2:bool.
78  match b1 with
79   [ true ⇒  match b2 with [ true ⇒ false | false ⇒ true ]
80   | false ⇒  match b2 with [ true ⇒ true | false ⇒ false ]].
81
82 notation > "'if' term 46 e 'then' term 46 t 'else' term 46 f" non associative with precedence 46
83  for @{ match $e in bool with [ true ⇒ $t | false ⇒ $f]  }.
84 notation < "hvbox('if' \nbsp term 46 e \nbsp break 'then' \nbsp term 46 t \nbsp break 'else' \nbsp term 49 f \nbsp)" non associative with precedence 46
85  for @{ match $e with [ true ⇒ $t | false ⇒ $f]  }.
86
87 theorem bool_to_decidable_eq: 
88   ∀b1,b2:bool. decidable (b1=b2).
89 #b1 #b2 (cases b1) (cases b2) /2/ %2 /3/ qed.
90
91 theorem true_or_false:
92 ∀b:bool. b = true ∨ b = false.
93 #b (cases b) /2/ qed.
94
95