refactor(library/logic): move identities from classical to identities
This commit is contained in:
Jeremy Avigad
Leonardo de Moura
parent
231039ad26
commit
6ffd719c1a
9 changed files with 150 additions and 146 deletions
|
|
@ -2,61 +2,42 @@
|
|||
-- 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
|
||||
|
||||
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 :=
|
||||
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 case_on (a : Prop) {P : Prop → Prop} (H1 : P true) (H2 : P false) : P a :=
|
||||
case P H1 H2 a
|
||||
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 (eqt_elim Ht))
|
||||
(assume Hf : a = false, or_inr (eqf_elim Hf))
|
||||
(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 :=
|
||||
case (λ x, x = false ∨ x = true)
|
||||
cases (λ 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 trivial (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 Hbf, false_elim (a = b) (Hbf ▸ (Hab (eq_true_elim Hat)))))
|
||||
(assume Haf, or_elim (prop_complete b)
|
||||
(assume Hbt, false_elim (a = b) (Haf ▸ (Hba (eqt_elim Hbt))))
|
||||
(assume Hbt, false_elim (a = b) (Haf ▸ (Hba (eq_true_elim Hbt))))
|
||||
(assume Hbf, Haf ⬝ Hbf⁻¹))
|
||||
|
||||
theorem iff_to_eq {a b : Prop} (H : a ↔ b) : a = b :=
|
||||
|
|
@ -67,106 +48,6 @@ 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 (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 (a b : Prop) : (¬(a ∧ b)) = (¬a ∨ ¬b) :=
|
||||
propext
|
||||
(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_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 (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
|
||||
|
|
|
|||
|
|
@ -1,8 +1,9 @@
|
|||
----------------------------------------------------------------------------------------------------
|
||||
-- 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.prop_decidable
|
||||
-- ===========================
|
||||
|
||||
import logic.axioms.classical logic.axioms.hilbert logic.classes.decidable
|
||||
using decidable inhabited nonempty
|
||||
|
|
|
|||
|
|
@ -45,7 +45,7 @@ theorem hrefl {A : Type} (a : A) : a == a :=
|
|||
eq_to_heq (refl a)
|
||||
|
||||
theorem heqt_elim {a : Prop} (H : a == true) : a :=
|
||||
eqt_elim (heq_to_eq H)
|
||||
eq_true_elim (heq_to_eq H)
|
||||
|
||||
opaque_hint (hiding cast)
|
||||
|
||||
|
|
|
|||
|
|
@ -137,6 +137,12 @@ iff_intro
|
|||
calc_refl iff_refl
|
||||
calc_trans iff_trans
|
||||
|
||||
theorem iff_true_elim {a : Prop} (H : a ↔ true) : a :=
|
||||
iff_mp (iff_symm H) trivial
|
||||
|
||||
theorem iff_false_elim {a : Prop} (H : a ↔ false) : ¬a :=
|
||||
assume Ha : a, iff_mp H Ha
|
||||
|
||||
theorem eq_to_iff {a b : Prop} (H : a = b) : a ↔ b :=
|
||||
iff_intro (λ Ha, subst H Ha) (λ Hb, subst (symm H) Hb)
|
||||
|
||||
|
|
|
|||
|
|
@ -85,10 +85,10 @@ H1 ▸ H2
|
|||
theorem eqmpr {a b : Prop} (H1 : a = b) (H2 : b) : a :=
|
||||
H1⁻¹ ▸ H2
|
||||
|
||||
theorem eqt_elim {a : Prop} (H : a = true) : a :=
|
||||
theorem eq_true_elim {a : Prop} (H : a = true) : a :=
|
||||
H⁻¹ ▸ trivial
|
||||
|
||||
theorem eqf_elim {a : Prop} (H : a = false) : ¬a :=
|
||||
theorem eq_false_elim {a : Prop} (H : a = false) : ¬a :=
|
||||
assume Ha : a, H ▸ Ha
|
||||
|
||||
theorem imp_trans {a b c : Prop} (H1 : a → b) (H2 : b → c) : a → c :=
|
||||
|
|
|
|||
|
|
@ -1,6 +1,6 @@
|
|||
-- Copyright (c) 2014 Microsoft Corporation. All rights reserved.
|
||||
-- Released under Apache 2.0 license as described in the file LICENSE.
|
||||
-- Authors: Jeremy Avigad
|
||||
-- Authors: Jeremy Avigad, Leonardo de Moura
|
||||
|
||||
-- logic.connectives.identities
|
||||
-- ============================
|
||||
|
|
@ -8,9 +8,9 @@
|
|||
-- Useful logical identities. In the absence of propositional extensionality, some of the
|
||||
-- calculations use the type class support provided by logic.connectives.instances
|
||||
|
||||
import logic.core.instances
|
||||
import logic.core.instances logic.classes.decidable logic.core.quantifiers logic.core.cast
|
||||
|
||||
using relation
|
||||
using relation decidable relation.iff_ops
|
||||
|
||||
theorem or_right_comm (a b c : Prop) : (a ∨ b) ∨ c ↔ (a ∨ c) ∨ b :=
|
||||
calc
|
||||
|
|
@ -35,3 +35,116 @@ 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 : (¬true) ↔ false :=
|
||||
iff_intro (assume H, H trivial) (false_elim _)
|
||||
|
||||
theorem not_false : (¬false) ↔ true :=
|
||||
iff_intro (assume H, trivial) (assume H H', H')
|
||||
|
||||
theorem not_or {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 {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_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),
|
||||
resolve_right H (not_not_iff⁻¹ ▸ Ha))
|
||||
|
||||
theorem not_implies {a b : Prop} {Da : decidable a} {Db : decidable b} : (¬(a → b)) ↔ (a ∧ ¬b) :=
|
||||
calc (¬(a → b)) ↔ (¬(¬a ∨ b)) : {imp_or}
|
||||
... ↔ (¬¬a ∧ ¬b) : not_or
|
||||
... ↔ (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_implies_left (mt H Hna),
|
||||
absurd (not_not_elim Hnna) Hna)
|
||||
|
||||
theorem not_exists_forall {A : Type} {P : A → Prop} {D : ∀x, decidable (P x)}
|
||||
(H : ¬∃x, P x) : ∀x, ¬P x :=
|
||||
-- TODO: when type class instances can use quantifiers, we can use write em
|
||||
take x, or_elim (@em _ (D x))
|
||||
(assume Hp : P x, absurd (exists_intro x Hp) H)
|
||||
(assume Hn : ¬P x, Hn)
|
||||
|
||||
theorem not_forall_exists {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 @not_exists_forall _ _ (take x, not_decidable (D x)) 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 a H2)
|
||||
|
||||
theorem a_neq_a {A : Type} (a : A) : (a ≠ a) ↔ false :=
|
||||
iff_intro
|
||||
(assume H, a_neq_a_elim H)
|
||||
(assume H, false_elim (a ≠ a) H)
|
||||
|
||||
theorem eq_id {A : Type} (a : A) : (a = a) ↔ true :=
|
||||
iff_true_intro (refl a)
|
||||
|
||||
theorem heq_id {A : Type} (a : A) : (a == a) ↔ true :=
|
||||
iff_true_intro (hrefl a)
|
||||
|
||||
theorem a_iff_not_a (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 (a ↔ ¬a) H)
|
||||
|
||||
theorem true_eq_false : (true ↔ false) ↔ false :=
|
||||
not_true ▸ (a_iff_not_a true)
|
||||
|
||||
theorem false_eq_true : (false ↔ true) ↔ false :=
|
||||
not_false ▸ (a_iff_not_a false)
|
||||
|
||||
theorem a_eq_true (a : Prop) : (a ↔ true) ↔ a :=
|
||||
iff_intro (assume H, iff_true_elim H) (assume H, iff_true_intro H)
|
||||
|
||||
theorem a_eq_false (a : Prop) : (a ↔ false) ↔ ¬a :=
|
||||
iff_intro (assume H, iff_false_elim H) (assume H, iff_false_intro H)
|
||||
|
|
|
|||
|
|
@ -1,10 +1,11 @@
|
|||
----------------------------------------------------------------------------------------------------
|
||||
-- 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.axioms.classical
|
||||
import logic.axioms.classical logic.axioms.prop_decidable logic.classes.decidable
|
||||
import logic.core.identities
|
||||
|
||||
using decidable
|
||||
|
||||
-- Well-founded relation definition
|
||||
-- We are essentially saying that a relation R is well-founded
|
||||
|
|
@ -16,7 +17,9 @@ definition wf {A : Type} (R : A → A → Prop) : Prop :=
|
|||
theorem wf_induction {A : Type} {R : A → A → Prop} {P : A → Prop} (Hwf : wf R) (iH : ∀x, (∀y, R y x → P y) → P x)
|
||||
: ∀x, P x :=
|
||||
by_contradiction (assume N : ¬∀x, P x,
|
||||
obtain (w : A) (Hw : ¬P w), from not_forall_exists N,
|
||||
-- TODO: when type classes can handle quantifiers, we will not need to give the implicit
|
||||
-- arguments to not_forall_exists
|
||||
obtain (w : A) (Hw : ¬P w), from @not_forall_exists _ _ (take x, _) _ N,
|
||||
-- The main "trick" is to define Q x as ¬P x.
|
||||
-- Since R is well-founded, there must be a R-minimal element r s.t. Q r (which is ¬P r)
|
||||
let Q x := ¬P x in
|
||||
|
|
|
|||
|
|
@ -19,10 +19,10 @@ definition is_zero (x : nat)
|
|||
:= nat_rec true (λ n r, false) x
|
||||
|
||||
theorem is_zero_zero : is_zero zero
|
||||
:= eqt_elim (refl _)
|
||||
:= eq_true_elim (refl _)
|
||||
|
||||
theorem not_is_zero_succ (x : nat) : ¬ is_zero (succ x)
|
||||
:= eqf_elim (refl _)
|
||||
:= eq_false_elim (refl _)
|
||||
|
||||
theorem dichotomy (m : nat) : m = zero ∨ (∃ n, m = succ n)
|
||||
:= nat_rec
|
||||
|
|
|
|||
|
|
@ -9,7 +9,7 @@ definition is_nil {A : Type} (l : list A) : Prop
|
|||
:= list_rec true (fun h t r, false) l
|
||||
|
||||
theorem is_nil_nil (A : Type) : is_nil (@nil A)
|
||||
:= eqt_elim (refl true)
|
||||
:= eq_true_elim (refl true)
|
||||
|
||||
theorem cons_ne_nil {A : Type} (a : A) (l : list A) : ¬ cons a l = nil
|
||||
:= not_intro (assume H : cons a l = nil,
|
||||
|
|
|
|||
Loading…
Reference in a new issue