1 (**************************************************************************)
4 (* ||A|| A project by Andrea Asperti *)
6 (* ||I|| Developers: *)
7 (* ||T|| A.Asperti, C.Sacerdoti Coen, *)
8 (* ||A|| E.Tassi, S.Zacchiroli *)
10 (* \ / This file is distributed under the terms of the *)
11 (* v GNU Lesser General Public License Version 2.1 *)
13 (**************************************************************************)
15 include "basics/eq.ma".
16 include "basics/functions.ma".
18 ninductive bool: Type ≝
23 ntheorem bool_elim: \forall P:bool \to Prop. \forall b:bool.
25 \to (b = false \to P false)
29 [ apply H; reflexivity
30 | apply H1; reflexivity
34 (* ndestrcut does not work *)
35 ntheorem not_eq_true_false : true \neq false.
36 #Heq; nchange with match true with [true ⇒ False|false ⇒ True];
37 nrewrite > Heq; //; nqed.
39 ndefinition notb : bool → bool ≝
40 \lambda b:bool. match b with
44 interpretation "boolean not" 'not x = (notb x).
46 ntheorem notb_elim: ∀ b:bool.∀ P:bool → Prop.
49 | false ⇒ P true] → P (notb b).
50 #b; #P; nelim b; nnormalize; //; nqed.
52 ntheorem notb_notb: ∀b:bool. notb (notb b) = b.
53 #b; nelim b; //; nqed.
55 ntheorem injective_notb: injective bool bool notb.
56 #b1; #b2; #H; //; nqed.
58 ndefinition andb : bool → bool → bool ≝
59 \lambda b1,b2:bool. match b1 with
63 interpretation "boolean and" 'and x y = (andb x y).
65 ntheorem andb_elim: ∀ b1,b2:bool. ∀ P:bool → Prop.
68 | false ⇒ P false] → P (b1 ∧ b2).
69 #b1; #b2; #P; nelim b1; nnormalize; //; nqed.
72 ntheorem and_true: ∀ a,b:bool.
73 andb a b =true → a =true ∧ b= true.
74 #a; #b; ncases a; nnormalize;#H;napply conj;//;
76 [reflexivity|assumption]
78 apply not_eq_true_false.
84 ntheorem andb_true_l: ∀ b1,b2. (b1 ∧ b2) = true → b1 = true.
85 #b1; ncases b1; nnormalize; //; nqed.
87 ntheorem andb_true_r: \forall b1,b2. (b1 ∧ b2) = true → b2 = true.
88 #b1; ncases b1; nnormalize; //;
89 #b2; ncases b2; //; nqed.
91 ndefinition orb : bool → bool → bool ≝
97 interpretation "boolean or" 'or x y = (orb x y).
99 ntheorem orb_elim: ∀ b1,b2:bool. ∀ P:bool → Prop.
102 | false ⇒ P b2] → P (orb b1 b2).
103 #b1; #b2; #P; nelim b1; nnormalize; //; nqed.
105 ndefinition if_then_else: ∀A:Type. bool → A → A → A ≝
106 λA:Type.λb:bool.λ P,Q:A. match b with
110 ntheorem bool_to_decidable_eq:
111 ∀b1,b2:bool. decidable (b1=b2).
112 #b1; #b2; ncases b1; ncases b2; /2/;
115 ntheorem true_or_false:
116 ∀b:bool. b = true ∨ b = false.
117 #b; ncases b; /2/; nqed.
121 theorem P_x_to_P_x_to_eq:
122 \forall A:Set. \forall P: A \to bool.
123 \forall x:A. \forall p1,p2:P x = true. p1 = p2.
125 apply eq_to_eq_to_eq_p_q.
126 exact bool_to_decidable_eq.
130 (* some basic properties of and - or*)
131 theorem andb_sym: \forall A,B:bool.
132 (A \land B) = (B \land A).
140 theorem andb_assoc: \forall A,B,C:bool.
141 (A \land (B \land C)) = ((A \land B) \land C).
150 theorem orb_sym: \forall A,B:bool.
151 (A \lor B) = (B \lor A).
159 theorem true_to_true_to_andb_true: \forall A,B:bool.
160 A = true \to B = true \to (A \land B) = true.