/
cc_lemmas.lean
117 lines (83 loc) · 4.55 KB
/
cc_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
/-
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.propext init.classical
/- Lemmas use by the congruence closure module -/
lemma iff_eq_of_eq_true_left {a b : Prop} (h : a = true) : (a ↔ b) = b :=
h.symm ▸ propext (true_iff _)
lemma iff_eq_of_eq_true_right {a b : Prop} (h : b = true) : (a ↔ b) = a :=
h.symm ▸ propext (iff_true _)
lemma iff_eq_true_of_eq {a b : Prop} (h : a = b) : (a ↔ b) = true :=
h ▸ propext (iff_self _)
lemma and_eq_of_eq_true_left {a b : Prop} (h : a = true) : (a ∧ b) = b :=
h.symm ▸ propext (true_and _)
lemma and_eq_of_eq_true_right {a b : Prop} (h : b = true) : (a ∧ b) = a :=
h.symm ▸ propext (and_true _)
lemma and_eq_of_eq_false_left {a b : Prop} (h : a = false) : (a ∧ b) = false :=
h.symm ▸ propext (false_and _)
lemma and_eq_of_eq_false_right {a b : Prop} (h : b = false) : (a ∧ b) = false :=
h.symm ▸ propext (and_false _)
lemma and_eq_of_eq {a b : Prop} (h : a = b) : (a ∧ b) = a :=
h ▸ propext (and_self _)
lemma or_eq_of_eq_true_left {a b : Prop} (h : a = true) : (a ∨ b) = true :=
h.symm ▸ propext (true_or _)
lemma or_eq_of_eq_true_right {a b : Prop} (h : b = true) : (a ∨ b) = true :=
h.symm ▸ propext (or_true _)
lemma or_eq_of_eq_false_left {a b : Prop} (h : a = false) : (a ∨ b) = b :=
h.symm ▸ propext (false_or _)
lemma or_eq_of_eq_false_right {a b : Prop} (h : b = false) : (a ∨ b) = a :=
h.symm ▸ propext (or_false _)
lemma or_eq_of_eq {a b : Prop} (h : a = b) : (a ∨ b) = a :=
h ▸ propext (or_self _)
lemma imp_eq_of_eq_true_left {a b : Prop} (h : a = true) : (a → b) = b :=
h.symm ▸ propext (iff.intro (λ h, h trivial) (λ h₁ h₂, h₁))
lemma imp_eq_of_eq_true_right {a b : Prop} (h : b = true) : (a → b) = true :=
h.symm ▸ propext (iff.intro (λ h, trivial) (λ h₁ h₂, h₁))
lemma imp_eq_of_eq_false_left {a b : Prop} (h : a = false) : (a → b) = true :=
h.symm ▸ propext (iff.intro (λ h, trivial) (λ h₁ h₂, false.elim h₂))
lemma imp_eq_of_eq_false_right {a b : Prop} (h : b = false) : (a → b) = not a :=
h.symm ▸ propext (iff.intro (λ h, h) (λ hna ha, hna ha))
/- Remark: the congruence closure module will only use the following lemma is
cc_config.em is tt. -/
lemma not_imp_eq_of_eq_false_right {a b : Prop} (h : b = false) : (not a → b) = a :=
h.symm ▸ propext (iff.intro (λ h', classical.by_contradiction (λ hna, h' hna)) (λ ha hna, hna ha))
lemma imp_eq_true_of_eq {a b : Prop} (h : a = b) : (a → b) = true :=
h ▸ propext (iff.intro (λ h, trivial) (λ h ha, ha))
lemma not_eq_of_eq_true {a : Prop} (h : a = true) : (not a) = false :=
h.symm ▸ propext not_true_iff
lemma not_eq_of_eq_false {a : Prop} (h : a = false) : (not a) = true :=
h.symm ▸ propext not_false_iff
lemma false_of_a_eq_not_a {a : Prop} (h : a = not a) : false :=
have not a, from λ ha, absurd ha (eq.mp h ha),
absurd (eq.mpr h this) this
universes u
lemma if_eq_of_eq_true {c : Prop} [d : decidable c] {α : Sort u} (t e : α) (h : c = true) : (@ite c d α t e) = t :=
if_pos (of_eq_true h)
lemma if_eq_of_eq_false {c : Prop} [d : decidable c] {α : Sort u} (t e : α) (h : c = false) : (@ite c d α t e) = e :=
if_neg (not_of_eq_false h)
lemma if_eq_of_eq (c : Prop) [d : decidable c] {α : Sort u} {t e : α} (h : t = e) : (@ite c d α t e) = t :=
match d with
| (is_true hc) := rfl
| (is_false hnc) := eq.symm h
end
lemma eq_true_of_and_eq_true_left {a b : Prop} (h : (a ∧ b) = true) : a = true :=
eq_true_intro (and.left (of_eq_true h))
lemma eq_true_of_and_eq_true_right {a b : Prop} (h : (a ∧ b) = true) : b = true :=
eq_true_intro (and.right (of_eq_true h))
lemma eq_false_of_or_eq_false_left {a b : Prop} (h : (a ∨ b) = false) : a = false :=
eq_false_intro (λ ha, false.elim (eq.mp h (or.inl ha)))
lemma eq_false_of_or_eq_false_right {a b : Prop} (h : (a ∨ b) = false) : b = false :=
eq_false_intro (λ hb, false.elim (eq.mp h (or.inr hb)))
lemma eq_false_of_not_eq_true {a : Prop} (h : (not a) = true) : a = false :=
eq_false_intro (λ ha, absurd ha (eq.mpr h trivial))
/- Remark: the congruence closure module will only use the following lemma is
cc_config.em is tt. -/
lemma eq_true_of_not_eq_false {a : Prop} (h : (not a) = false) : a = true :=
eq_true_intro (classical.by_contradiction (λ hna, eq.mp h hna))
lemma ne_of_eq_of_ne {α : Sort u} {a b c : α} (h₁ : a = b) (h₂ : b ≠ c) : a ≠ c :=
h₁.symm ▸ h₂
lemma ne_of_ne_of_eq {α : Sort u} {a b c : α} (h₁ : a ≠ b) (h₂ : b = c) : a ≠ c :=
h₂ ▸ h₁