-
Notifications
You must be signed in to change notification settings - Fork 80
/
lemmas.lean
153 lines (104 loc) · 4.67 KB
/
lemmas.lean
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
/-
Copyright (c) 2017 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Leonardo de Moura
-/
prelude
import init.data.bool.basic init.meta
attribute [simp] cond bor band bnot bxor
@[simp] lemma {u} cond_a_a {α : Type u} (b : bool) (a : α) : cond b a a = a :=
by cases b; simp
@[simp] lemma band_self (b : bool) : b && b = b :=
by cases b; simp
@[simp] lemma band_tt (b : bool) : b && tt = b :=
by cases b; simp
@[simp] lemma band_ff (b : bool) : b && ff = ff :=
by cases b; simp
@[simp] lemma tt_band (b : bool) : tt && b = b :=
by cases b; simp
@[simp] lemma ff_band (b : bool) : ff && b = ff :=
by cases b; simp
@[simp] lemma bor_self (b : bool) : b || b = b :=
by cases b; simp
@[simp] lemma bor_tt (b : bool) : b || tt = tt :=
by cases b; simp
@[simp] lemma bor_ff (b : bool) : b || ff = b :=
by cases b; simp
@[simp] lemma tt_bor (b : bool) : tt || b = tt :=
by cases b; simp
@[simp] lemma ff_bor (b : bool) : ff || b = b :=
by cases b; simp
@[simp] lemma bxor_self (b : bool) : bxor b b = ff :=
by cases b; simp
@[simp] lemma bxor_tt (b : bool) : bxor b tt = bnot b :=
by cases b; simp
lemma bxor_ff (b : bool) : bxor b ff = b :=
by cases b; simp
@[simp] lemma tt_bxor (b : bool) : bxor tt b = bnot b :=
by cases b; simp
lemma ff_bxor (b : bool) : bxor ff b = b :=
by cases b; simp
@[simp] lemma bnot_bnot (b : bool) : bnot (bnot b) = b :=
by cases b; simp
lemma tt_eq_ff_eq_false : ¬(tt = ff) :=
by contradiction
lemma ff_eq_tt_eq_false : ¬(ff = tt) :=
by contradiction
@[simp] lemma eq_ff_eq_not_eq_tt (b : bool) : (¬(b = tt)) = (b = ff) :=
by cases b; simp
@[simp] lemma eq_tt_eq_not_eq_ff (b : bool) : (¬(b = ff)) = (b = tt) :=
by cases b; simp
lemma eq_ff_of_not_eq_tt {b : bool} : (¬(b = tt)) → (b = ff) :=
eq.mp (eq_ff_eq_not_eq_tt b)
lemma eq_tt_of_not_eq_ff {b : bool} : (¬(b = ff)) → (b = tt) :=
eq.mp (eq_tt_eq_not_eq_ff b)
@[simp] lemma band_eq_true_eq_eq_tt_and_eq_tt (a b : bool) : (a && b = tt) = (a = tt ∧ b = tt) :=
by cases a; cases b; simp
@[simp] lemma bor_eq_true_eq_eq_tt_or_eq_tt (a b : bool) : (a || b = tt) = (a = tt ∨ b = tt) :=
by cases a; cases b; simp
@[simp] lemma bnot_eq_true_eq_eq_ff (a : bool) : (bnot a = tt) = (a = ff) :=
by cases a; simp
@[simp] lemma band_eq_false_eq_eq_ff_or_eq_ff (a b : bool) : (a && b = ff) = (a = ff ∨ b = ff) :=
by cases a; cases b; simp
@[simp] lemma bor_eq_false_eq_eq_ff_and_eq_ff (a b : bool) : (a || b = ff) = (a = ff ∧ b = ff) :=
by cases a; cases b; simp
@[simp] lemma bnot_eq_ff_eq_eq_tt (a : bool) : (bnot a = ff) = (a = tt) :=
by cases a; simp
@[simp] lemma coe_ff : ↑ff = false :=
show (ff = tt) = false, by simp
@[simp] lemma coe_tt : ↑tt = true :=
show (tt = tt) = true, by simp
@[simp] lemma coe_sort_ff : ↥ff = false :=
show (ff = tt) = false, by simp
@[simp] lemma coe_sort_tt : ↥tt = true :=
show (tt = tt) = true, by simp
@[simp] theorem to_bool_iff (p : Prop) [d : decidable p] : (to_bool p = tt) ↔ p :=
match d with
| is_true hp := ⟨λh, hp, λ_, rfl⟩
| is_false hnp := ⟨λh, bool.no_confusion h, λhp, absurd hp hnp⟩
end
theorem to_bool_true {p : Prop} [decidable p] : p → to_bool p := (to_bool_iff p).2
theorem to_bool_tt {p : Prop} [decidable p] : p → to_bool p = tt := to_bool_true
theorem of_to_bool_true {p : Prop} [decidable p] : to_bool p → p := (to_bool_iff p).1
theorem bool_iff_false {b : bool} : ¬ b ↔ b = ff := by cases b; exact dec_trivial
theorem bool_eq_false {b : bool} : ¬ b → b = ff := bool_iff_false.1
@[simp] theorem to_bool_ff_iff (p : Prop) [decidable p] : to_bool p = ff ↔ ¬p :=
bool_iff_false.symm.trans (not_congr (to_bool_iff _))
theorem to_bool_ff {p : Prop} [decidable p] : ¬p → to_bool p = ff := (to_bool_ff_iff p).2
theorem of_to_bool_ff {p : Prop} [decidable p] : to_bool p = ff → ¬p := (to_bool_ff_iff p).1
theorem to_bool_congr {p q : Prop} [decidable p] [decidable q] (h : p ↔ q) : to_bool p = to_bool q :=
begin
induction h' : to_bool q,
exact to_bool_ff (mt h.1 $ of_to_bool_ff h'),
exact to_bool_true (h.2 $ of_to_bool_true h')
end
@[simp] theorem bor_coe_iff (a b : bool) : a || b ↔ a ∨ b :=
by cases a; cases b; exact dec_trivial
@[simp] theorem band_coe_iff (a b : bool) : a && b ↔ a ∧ b :=
by cases a; cases b; exact dec_trivial
@[simp] theorem bxor_coe_iff (a b : bool) : bxor a b ↔ xor a b :=
by cases a; cases b; exact dec_trivial
@[simp] theorem ite_eq_tt_distrib (c : Prop) [decidable c] (a b : bool) : ((if c then a else b) = tt) = (if c then a = tt else b = tt) :=
by by_cases c; simp [*]
@[simp] theorem ite_eq_ff_distrib (c : Prop) [decidable c] (a b : bool) : ((if c then a else b) = ff) = (if c then a = ff else b = ff) :=
by by_cases c; simp [*]