lean2/library/logic/axioms/classical.lean
Leonardo de Moura a8d58fdd33 refactor(library): mark absurd_elim argument as implicit
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-08-26 18:27:39 -07:00

177 lines
5.8 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.
-- Author: Leonardo de Moura
----------------------------------------------------------------------------------------------------
import logic.connectives.basic logic.connectives.quantifiers logic.connectives.cast struc.relation
using eq_ops
axiom prop_complete (a : Prop) : a = true a = false
theorem case (P : Prop → Prop) (H1 : P true) (H2 : P false) (a : Prop) : P a :=
or_elim (prop_complete a)
(assume Ht : a = true, Ht⁻¹ ▸ H1)
(assume Hf : a = false, Hf⁻¹ ▸ H2)
theorem case_on (a : Prop) {P : Prop → Prop} (H1 : P true) (H2 : P false) : P a :=
case P H1 H2 a
theorem em (a : Prop) : a ¬a :=
or_elim (prop_complete a)
(assume Ht : a = true, or_inl (eqt_elim Ht))
(assume Hf : a = false, or_inr (eqf_elim Hf))
theorem prop_complete_swapped (a : Prop) : a = false a = true :=
case (λ x, x = false x = true)
(or_inr (refl true))
(or_inl (refl false))
a
theorem not_true : (¬true) = false :=
have aux : (¬true) ≠ true, from
assume H : (¬true) = true,
absurd_not_true (H⁻¹ ▸ trivial),
resolve_right (prop_complete (¬true)) aux
theorem not_false : (¬false) = true :=
have aux : (¬false) ≠ false, from
assume H : (¬false) = false,
H ▸ not_false_trivial,
resolve_right (prop_complete_swapped (¬false)) aux
theorem not_not_eq (a : Prop) : (¬¬a) = a :=
case (λ x, (¬¬x) = x)
(calc (¬¬true) = (¬false) : {not_true}
... = true : not_false)
(calc (¬¬false) = (¬true) : {not_false}
... = false : not_true)
a
theorem not_not_elim {a : Prop} (H : ¬¬a) : a :=
(not_not_eq a) ▸ H
theorem propext {a b : Prop} (Hab : a → b) (Hba : b → a) : a = b :=
or_elim (prop_complete a)
(assume Hat, or_elim (prop_complete b)
(assume Hbt, Hat ⬝ Hbt⁻¹)
(assume Hbf, false_elim (a = b) (Hbf ▸ (Hab (eqt_elim Hat)))))
(assume Haf, or_elim (prop_complete b)
(assume Hbt, false_elim (a = b) (Haf ▸ (Hba (eqt_elim Hbt))))
(assume Hbf, Haf ⬝ Hbf⁻¹))
theorem iff_to_eq {a b : Prop} (H : a ↔ b) : a = b :=
iff_elim (assume H1 H2, propext H1 H2) H
theorem iff_eq_eq {a b : Prop} : (a ↔ b) = (a = b) :=
propext
(assume H, iff_to_eq H)
(assume H, eq_to_iff H)
theorem eqt_intro {a : Prop} (H : a) : a = true :=
propext
(assume H1 : a, trivial)
(assume H2 : true, H)
theorem eqf_intro {a : Prop} (H : ¬a) : a = false :=
propext
(assume H1 : a, absurd H1 H)
(assume H2 : false, false_elim a H2)
theorem by_contradiction {a : Prop} (H : ¬a → false) : a :=
or_elim (em a)
(assume H1 : a, H1)
(assume H1 : ¬a, false_elim a (H H1))
theorem a_neq_a {A : Type} (a : A) : (a ≠ a) = false :=
propext
(assume H, a_neq_a_elim H)
(assume H, false_elim (a ≠ a) H)
theorem eq_id {A : Type} (a : A) : (a = a) = true :=
eqt_intro (refl a)
theorem heq_id {A : Type} (a : A) : (a == a) = true :=
eqt_intro (hrefl a)
theorem not_or (a b : Prop) : (¬(a b)) = (¬a ∧ ¬b) :=
propext
(assume H, or_elim (em a)
(assume Ha, absurd_elim (or_inl Ha) H)
(assume Hna, or_elim (em b)
(assume Hb, absurd_elim (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 (a b : Prop) : (¬(a ∧ b)) = (¬a ¬b) :=
propext
(assume H, or_elim (em a)
(assume Ha, or_elim (em b)
(assume Hb, absurd_elim (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_or (a b : Prop) : (a → b) = (¬a b) :=
propext
(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),
resolve_right H ((not_not_eq a)⁻¹ ▸ Ha))
theorem not_implies (a b : Prop) : (¬(a → b)) = (a ∧ ¬b) :=
calc (¬(a → b)) = (¬(¬a b)) : {imp_or a b}
... = (¬¬a ∧ ¬b) : not_or (¬a) b
... = (a ∧ ¬b) : {not_not_eq a}
theorem a_eq_not_a (a : Prop) : (a = ¬a) = false :=
propext
(assume H, or_elim (em a)
(assume Ha, absurd Ha (H ▸ Ha))
(assume Hna, absurd (H⁻¹ ▸ Hna) Hna))
(assume H, false_elim (a = ¬a) H)
theorem true_eq_false : (true = false) = false :=
not_true ▸ (a_eq_not_a true)
theorem false_eq_true : (false = true) = false :=
not_false ▸ (a_eq_not_a false)
theorem a_eq_true (a : Prop) : (a = true) = a :=
propext (assume H, eqt_elim H) (assume H, eqt_intro H)
theorem a_eq_false (a : Prop) : (a = false) = ¬a :=
propext (assume H, eqf_elim H) (assume H, eqf_intro H)
theorem not_exists_forall {A : Type} {P : A → Prop} (H : ¬∃x, P x) : ∀x, ¬P x :=
take x, or_elim (em (P x))
(assume Hp : P x, absurd_elim (exists_intro x Hp) H)
(assume Hn : ¬P x, Hn)
theorem not_forall_exists {A : Type} {P : A → Prop} (H : ¬∀x, P x) : ∃x, ¬P x :=
by_contradiction (assume H1 : ¬∃ x, ¬P x,
have H2 : ∀x, ¬¬P x, from not_exists_forall H1,
have H3 : ∀x, P x, from take x, not_not_elim (H2 x),
absurd H3 H)
theorem peirce (a b : Prop) : ((a → b) → a) → a :=
assume H, by_contradiction (assume Hna : ¬a,
have Hnna : ¬¬a, from not_implies_left (mt H Hna),
absurd (not_not_elim Hnna) Hna)
-- with classical logic, every predicate respects iff
using relation
theorem iff_congr [instance] (P : Prop → Prop) : congr iff iff P :=
congr_mk
(take (a b : Prop),
assume H : a ↔ b,
show P a ↔ P b, from eq_to_iff (subst (iff_to_eq H) (refl (P a))))