e513b0ead4
The convention is this: we use e.g. nat.is_inhabited and nat.has_decidable_eq for these two purposes only, to avoid clashing with "inhabited" and "decidable_eq" in a namespace. Otherwise, we use "decidable_foo" and "inhabited_foo".
151 lines
5.3 KiB
Text
151 lines
5.3 KiB
Text
/-
|
||
Copyright (c) 2014 Microsoft Corporation. All rights reserved.
|
||
Released under Apache 2.0 license as described in the file LICENSE.
|
||
|
||
Module: logic.identities
|
||
Authors: Jeremy Avigad, Leonardo de Moura
|
||
|
||
Useful logical identities. Since we are not using propositional extensionality, some of the
|
||
calculations use the type class support provided by logic.instances.
|
||
-/
|
||
import logic.connectives logic.instances logic.quantifiers logic.cast
|
||
open relation decidable relation.iff_ops
|
||
|
||
theorem or.right_comm (a b c : Prop) : (a ∨ b) ∨ c ↔ (a ∨ c) ∨ b :=
|
||
calc
|
||
(a ∨ b) ∨ c ↔ a ∨ (b ∨ c) : or.assoc
|
||
... ↔ a ∨ (c ∨ b) : {or.comm}
|
||
... ↔ (a ∨ c) ∨ b : iff.symm or.assoc
|
||
|
||
theorem or.left_comm (a b c : Prop) : a ∨ (b ∨ c) ↔ b ∨ (a ∨ c) :=
|
||
calc
|
||
a ∨ (b ∨ c) ↔ (a ∨ b) ∨ c : iff.symm or.assoc
|
||
... ↔ (b ∨ a) ∨ c : {or.comm}
|
||
... ↔ b ∨ (a ∨ c) : or.assoc
|
||
|
||
theorem and.right_comm (a b c : Prop) : (a ∧ b) ∧ c ↔ (a ∧ c) ∧ b :=
|
||
calc
|
||
(a ∧ b) ∧ c ↔ a ∧ (b ∧ c) : and.assoc
|
||
... ↔ a ∧ (c ∧ b) : {and.comm}
|
||
... ↔ (a ∧ c) ∧ b : iff.symm and.assoc
|
||
|
||
theorem and.left_comm (a b c : Prop) : a ∧ (b ∧ c) ↔ b ∧ (a ∧ c) :=
|
||
calc
|
||
a ∧ (b ∧ c) ↔ (a ∧ b) ∧ c : iff.symm and.assoc
|
||
... ↔ (b ∧ a) ∧ c : {and.comm}
|
||
... ↔ b ∧ (a ∧ c) : and.assoc
|
||
|
||
theorem not_not_iff {a : Prop} [D : decidable a] : (¬¬a) ↔ a :=
|
||
iff.intro
|
||
(assume H : ¬¬a,
|
||
by_cases (assume H' : a, H') (assume H' : ¬a, absurd H' H))
|
||
(assume H : a, assume H', H' H)
|
||
|
||
theorem not_not_elim {a : Prop} [D : decidable a] (H : ¬¬a) : a :=
|
||
iff.mp not_not_iff H
|
||
|
||
theorem not_true_iff_false : ¬true ↔ false :=
|
||
iff.intro (assume H, H trivial) false.elim
|
||
|
||
theorem not_false_iff_true : ¬false ↔ true :=
|
||
iff.intro (assume H, trivial) (assume H H', H')
|
||
|
||
theorem not_or_iff_not_and_not {a b : Prop} [Da : decidable a] [Db : decidable b] :
|
||
¬(a ∨ b) ↔ ¬a ∧ ¬b :=
|
||
iff.intro
|
||
(assume H, or.elim (em a)
|
||
(assume Ha, absurd (or.inl Ha) H)
|
||
(assume Hna, or.elim (em b)
|
||
(assume Hb, absurd (or.inr Hb) H)
|
||
(assume Hnb, and.intro Hna Hnb)))
|
||
(assume (H : ¬a ∧ ¬b) (N : a ∨ b),
|
||
or.elim N
|
||
(assume Ha, absurd Ha (and.elim_left H))
|
||
(assume Hb, absurd Hb (and.elim_right H)))
|
||
|
||
theorem not_and_iff_not_or_not {a b : Prop} [Da : decidable a] [Db : decidable b] :
|
||
¬(a ∧ b) ↔ ¬a ∨ ¬b :=
|
||
iff.intro
|
||
(assume H, or.elim (em a)
|
||
(assume Ha, or.elim (em b)
|
||
(assume Hb, absurd (and.intro Ha Hb) H)
|
||
(assume Hnb, or.inr Hnb))
|
||
(assume Hna, or.inl Hna))
|
||
(assume (H : ¬a ∨ ¬b) (N : a ∧ b),
|
||
or.elim H
|
||
(assume Hna, absurd (and.elim_left N) Hna)
|
||
(assume Hnb, absurd (and.elim_right N) Hnb))
|
||
|
||
theorem imp_iff_not_or {a b : Prop} [Da : decidable a] : (a → b) ↔ ¬a ∨ b :=
|
||
iff.intro
|
||
(assume H : a → b, (or.elim (em a)
|
||
(assume Ha : a, or.inr (H Ha))
|
||
(assume Hna : ¬a, or.inl Hna)))
|
||
(assume (H : ¬a ∨ b) (Ha : a),
|
||
or_resolve_right H (not_not_iff⁻¹ ▸ Ha))
|
||
|
||
theorem not_implies_iff_and_not {a b : Prop} [Da : decidable a] [Db : decidable b] :
|
||
¬(a → b) ↔ a ∧ ¬b :=
|
||
calc
|
||
¬(a → b) ↔ ¬(¬a ∨ b) : {imp_iff_not_or}
|
||
... ↔ ¬¬a ∧ ¬b : not_or_iff_not_and_not
|
||
... ↔ a ∧ ¬b : {not_not_iff}
|
||
|
||
theorem peirce {a b : Prop} [D : decidable a] : ((a → b) → a) → a :=
|
||
assume H, by_contradiction (assume Hna : ¬a,
|
||
have Hnna : ¬¬a, from not_not_of_not_implies (mt H Hna),
|
||
absurd (not_not_elim Hnna) Hna)
|
||
|
||
theorem forall_not_of_not_exists {A : Type} {P : A → Prop} [D : ∀x, decidable (P x)]
|
||
(H : ¬∃x, P x) : ∀x, ¬P x :=
|
||
take x, or.elim (em (P x))
|
||
(assume Hp : P x, absurd (exists.intro x Hp) H)
|
||
(assume Hn : ¬P x, Hn)
|
||
|
||
theorem exists_not_of_not_forall {A : Type} {P : A → Prop} [D : ∀x, decidable (P x)]
|
||
[D' : decidable (∃x, ¬P x)] (H : ¬∀x, P x) :
|
||
∃x, ¬P x :=
|
||
@by_contradiction _ D' (assume H1 : ¬∃x, ¬P x,
|
||
have H2 : ∀x, ¬¬P x, from @forall_not_of_not_exists _ _ (take x, decidable_not) H1,
|
||
have H3 : ∀x, P x, from take x, @not_not_elim _ (D x) (H2 x),
|
||
absurd H3 H)
|
||
|
||
theorem iff_true_intro {a : Prop} (H : a) : a ↔ true :=
|
||
iff.intro
|
||
(assume H1 : a, trivial)
|
||
(assume H2 : true, H)
|
||
|
||
theorem iff_false_intro {a : Prop} (H : ¬a) : a ↔ false :=
|
||
iff.intro
|
||
(assume H1 : a, absurd H1 H)
|
||
(assume H2 : false, false.elim H2)
|
||
|
||
theorem ne_self_iff_false {A : Type} (a : A) : (a ≠ a) ↔ false :=
|
||
iff.intro
|
||
(assume H, false.of_ne H)
|
||
(assume H, false.elim H)
|
||
|
||
theorem eq_self_iff_true {A : Type} (a : A) : (a = a) ↔ true :=
|
||
iff_true_intro rfl
|
||
|
||
theorem heq_self_iff_true {A : Type} (a : A) : (a == a) ↔ true :=
|
||
iff_true_intro (heq.refl a)
|
||
|
||
theorem iff_not_self (a : Prop) : (a ↔ ¬a) ↔ false :=
|
||
iff.intro
|
||
(assume H,
|
||
have H' : ¬a, from assume Ha, (H ▸ Ha) Ha,
|
||
H' (H⁻¹ ▸ H'))
|
||
(assume H, false.elim H)
|
||
|
||
theorem true_iff_false : (true ↔ false) ↔ false :=
|
||
not_true_iff_false ▸ (iff_not_self true)
|
||
|
||
theorem false_iff_true : (false ↔ true) ↔ false :=
|
||
not_false_iff_true ▸ (iff_not_self false)
|
||
|
||
theorem iff_true_iff (a : Prop) : (a ↔ true) ↔ a :=
|
||
iff.intro (assume H, of_iff_true H) (assume H, iff_true_intro H)
|
||
|
||
theorem iff_false_iff_not (a : Prop) : (a ↔ false) ↔ ¬a :=
|
||
iff.intro (assume H, not_of_iff_false H) (assume H, iff_false_intro H)
|