lean2/library/logic/axioms/prop_complete.lean
Leonardo de Moura 368f9d347e refactor(frontends/lean): approach used to parse tactics
The previous approach was too fragile

TODO: we should add separate parsing tables for tactics
2015-03-05 18:11:21 -08:00

67 lines
2.2 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.axioms.classical
Author: Leonardo de Moura
-/
import logic.connectives logic.quantifiers logic.cast algebra.relation
open eq.ops
axiom prop_complete (a : Prop) : a = true a = false
definition eq_true_or_eq_false := prop_complete
theorem cases_true_false (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_true_false 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 (of_eq_true Ht))
(assume Hf : a = false, or.inr (not_of_eq_false Hf))
-- this supercedes by_cases in decidable
definition by_cases {p q : Prop} (Hpq : p → q) (Hnpq : ¬p → q) : q :=
or.elim (em p) (assume Hp, Hpq Hp) (assume Hnp, Hnpq Hnp)
-- this supercedes by_contradiction in decidable
theorem by_contradiction {p : Prop} (H : ¬p → false) : p :=
by_cases
(assume H1 : p, H1)
(assume H1 : ¬p, false.rec _ (H H1))
theorem eq_false_or_eq_true (a : Prop) : a = false a = true :=
cases_true_false (λ 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 (of_eq_true Hat)))))
(assume Haf, or.elim (prop_complete b)
(assume Hbt, false.elim (Haf ▸ (Hba (of_eq_true Hbt))))
(assume Hbf, Haf ⬝ Hbf⁻¹))
theorem eq.of_iff {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, eq.of_iff H)
(assume H, iff.of_eq H)
open relation
theorem iff_congruence [instance] (P : Prop → Prop) : is_congruence iff iff P :=
is_congruence.mk
(take (a b : Prop),
assume H : a ↔ b,
show P a ↔ P b, from iff.of_eq (eq.of_iff H ▸ eq.refl (P a)))