]> matita.cs.unibo.it Git - helm.git/blob - matitaB/matita/lib/basics/bool.ma
advances non lfsx ...
[helm.git] / matitaB / matita / lib / basics / bool.ma
1 (*
2     ||M||  This file is part of HELM, an Hypertextual, Electronic        
3     ||A||  Library of Mathematics, developed at the Computer Science     
4     ||T||  Department of the University of Bologna, Italy.                     
5     ||I||                                                                 
6     ||T||  
7     ||A||  
8     \   /  This file is distributed under the terms of the       
9      \ /   GNU General Public License Version 2   
10       V_______________________________________________________________ *)
11
12 include "basics/relations.ma".
13
14 (********** bool **********)
15 inductive bool: Type[0] ≝ 
16   | true : bool
17   | false : bool.
18
19 (* destruct does not work *)
20 theorem not_eq_true_false : true ≠ false.
21 @nmk #Heq change with match true with [true ⇒ False|false ⇒ True]
22 >Heq // qed.
23
24 definition notb : bool → bool ≝
25 λ b:bool. match b with [true ⇒ false|false ⇒ true ].
26
27 interpretation "boolean not" 'not x = (notb x).
28
29 theorem notb_elim: ∀ b:bool.∀ P:bool → Prop.
30 match b with
31 [ true ⇒ P false
32 | false ⇒ P true] → P (notb b).
33 #b #P elim b normalize // qed.
34
35 theorem notb_notb: ∀b:bool. notb (notb b) = b.
36 #b elim b // qed.
37
38 theorem injective_notb: injective bool bool notb.
39 #b1 #b2 #H // qed.
40
41 definition andb : bool → bool → bool ≝
42 λb1,b2:bool. match b1 with [ true ⇒ b2 | false ⇒ false ].
43
44 interpretation "boolean and" 'and x y = (andb x y).
45
46 theorem andb_elim: ∀ b1,b2:bool. ∀ P:bool → Prop.
47 match b1 with [ true ⇒ P b2 | false ⇒ P false] → P (b1 ∧ b2).
48 #b1 #b2 #P (elim b1) normalize // qed.
49
50 theorem andb_true_l: ∀ b1,b2. (b1 ∧ b2) = true → b1 = true.
51 #b1 (cases b1) normalize // qed.
52
53 theorem andb_true_r: ∀b1,b2. (b1 ∧ b2) = true → b2 = true.
54 #b1 #b2 (cases b1) normalize // (cases b2) // qed.
55
56 definition orb : bool → bool → bool ≝
57 λb1,b2:bool.match b1 with [ true ⇒ true | false ⇒ b2].
58  
59 interpretation "boolean or" 'or x y = (orb x y).
60
61 theorem orb_elim: ∀ b1,b2:bool. ∀ P:bool → Prop.
62 match b1 with [ true ⇒ P true | false ⇒ P b2] → P (orb b1 b2).
63 #b1 #b2 #P (elim b1) normalize // qed.
64
65 definition if_then_else: ∀A:Type[0]. bool → A → A → A ≝ 
66 λA.λb.λ P,Q:A. match b with [ true ⇒ P | false  ⇒ Q].
67
68 theorem bool_to_decidable_eq: 
69   ∀b1,b2:bool. decidable (b1=b2).
70 #b1 #b2 (cases b1) (cases b2) /2/ %2 /3/ qed.
71
72 theorem true_or_false:
73 ∀b:bool. b = true ∨ b = false.
74 #b (cases b) /2/ qed.
75
76