lean2/library/logic/identities.lean

151 lines
5.3 KiB
Text
Raw Blame History

This file contains ambiguous Unicode characters

This file contains Unicode characters that might be confused with other characters. If you think that this is intentional, you can safely ignore this warning. Use the Escape button to reveal them.

/-
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, not.decidable) 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)