lean2/library/logic/axioms/classical.lean
Leonardo de Moura 6632a50015 refactor(library): add namespaces 'or', 'and' and 'iff'
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-09-04 21:25:21 -07:00

56 lines
1.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
-- logic.axioms.classical
-- ======================
import logic.core.quantifiers logic.core.cast struc.relation
open eq_ops
axiom prop_complete (a : Prop) : a = true a = false
theorem cases (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 cases_on (a : Prop) {P : Prop → Prop} (H1 : P true) (H2 : P false) : P a :=
cases P H1 H2 a
-- this supercedes the em in decidable
theorem em (a : Prop) : a ¬a :=
or.elim (prop_complete a)
(assume Ht : a = true, or.inl (eq_true_elim Ht))
(assume Hf : a = false, or.inr (eq_false_elim Hf))
theorem prop_complete_swapped (a : Prop) : a = false a = true :=
cases (λ x, x = false x = true)
(or.inr rfl)
(or.inl rfl)
a
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 (Hbf ▸ (Hab (eq_true_elim Hat)))))
(assume Haf, or.elim (prop_complete b)
(assume Hbt, false_elim (Haf ▸ (Hba (eq_true_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)
open relation
theorem iff_congruence [instance] (P : Prop → Prop) : congruence iff iff P :=
congruence.mk
(take (a b : Prop),
assume H : a ↔ b,
show P a ↔ P b, from eq_to_iff (iff_to_eq H ▸ eq.refl (P a)))