01104cc81e
This adds a number of lemmas for simplification of `Bool` and `Prop` terms. It pulls lemmas from Mathlib and adds additional lemmas where confluence or consistency suggested they are needed. It has been tested against Mathlib using some automated test infrastructure. That testing module is not yet included in this PR, but will be included as part of this. Note. There are currently some comments saying the origin of the simp rule. These will be removed prior to merging, but are added to clarify where the rule came from during review. --------- Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
170 lines
7.2 KiB
Text
170 lines
7.2 KiB
Text
/-
|
||
Copyright (c) 2020 Microsoft Corporation. All rights reserved.
|
||
Released under Apache 2.0 license as described in the file LICENSE.
|
||
Authors: Leonardo de Moura, Mario Carneiro
|
||
-/
|
||
prelude
|
||
import Init.PropLemmas
|
||
|
||
universe u v
|
||
|
||
/-! # Classical reasoning support -/
|
||
|
||
namespace Classical
|
||
|
||
noncomputable def indefiniteDescription {α : Sort u} (p : α → Prop) (h : ∃ x, p x) : {x // p x} :=
|
||
choice <| let ⟨x, px⟩ := h; ⟨⟨x, px⟩⟩
|
||
|
||
noncomputable def choose {α : Sort u} {p : α → Prop} (h : ∃ x, p x) : α :=
|
||
(indefiniteDescription p h).val
|
||
|
||
theorem choose_spec {α : Sort u} {p : α → Prop} (h : ∃ x, p x) : p (choose h) :=
|
||
(indefiniteDescription p h).property
|
||
|
||
/-- **Diaconescu's theorem**: excluded middle from choice, Function extensionality and propositional extensionality. -/
|
||
theorem em (p : Prop) : p ∨ ¬p :=
|
||
let U (x : Prop) : Prop := x = True ∨ p
|
||
let V (x : Prop) : Prop := x = False ∨ p
|
||
have exU : ∃ x, U x := ⟨True, Or.inl rfl⟩
|
||
have exV : ∃ x, V x := ⟨False, Or.inl rfl⟩
|
||
let u : Prop := choose exU
|
||
let v : Prop := choose exV
|
||
have u_def : U u := choose_spec exU
|
||
have v_def : V v := choose_spec exV
|
||
have not_uv_or_p : u ≠ v ∨ p :=
|
||
match u_def, v_def with
|
||
| Or.inr h, _ => Or.inr h
|
||
| _, Or.inr h => Or.inr h
|
||
| Or.inl hut, Or.inl hvf =>
|
||
have hne : u ≠ v := by simp [hvf, hut, true_ne_false]
|
||
Or.inl hne
|
||
have p_implies_uv : p → u = v :=
|
||
fun hp =>
|
||
have hpred : U = V :=
|
||
funext fun x =>
|
||
have hl : (x = True ∨ p) → (x = False ∨ p) :=
|
||
fun _ => Or.inr hp
|
||
have hr : (x = False ∨ p) → (x = True ∨ p) :=
|
||
fun _ => Or.inr hp
|
||
show (x = True ∨ p) = (x = False ∨ p) from
|
||
propext (Iff.intro hl hr)
|
||
have h₀ : ∀ exU exV, @choose _ U exU = @choose _ V exV := by
|
||
rw [hpred]; intros; rfl
|
||
show u = v from h₀ _ _
|
||
match not_uv_or_p with
|
||
| Or.inl hne => Or.inr (mt p_implies_uv hne)
|
||
| Or.inr h => Or.inl h
|
||
|
||
theorem exists_true_of_nonempty {α : Sort u} : Nonempty α → ∃ _ : α, True
|
||
| ⟨x⟩ => ⟨x, trivial⟩
|
||
|
||
noncomputable def inhabited_of_nonempty {α : Sort u} (h : Nonempty α) : Inhabited α :=
|
||
⟨choice h⟩
|
||
|
||
noncomputable def inhabited_of_exists {α : Sort u} {p : α → Prop} (h : ∃ x, p x) : Inhabited α :=
|
||
inhabited_of_nonempty (Exists.elim h (fun w _ => ⟨w⟩))
|
||
|
||
/-- All propositions are `Decidable`. -/
|
||
noncomputable scoped instance (priority := low) propDecidable (a : Prop) : Decidable a :=
|
||
choice <| match em a with
|
||
| Or.inl h => ⟨isTrue h⟩
|
||
| Or.inr h => ⟨isFalse h⟩
|
||
|
||
noncomputable def decidableInhabited (a : Prop) : Inhabited (Decidable a) where
|
||
default := inferInstance
|
||
|
||
noncomputable def typeDecidableEq (α : Sort u) : DecidableEq α :=
|
||
fun _ _ => inferInstance
|
||
|
||
noncomputable def typeDecidable (α : Sort u) : PSum α (α → False) :=
|
||
match (propDecidable (Nonempty α)) with
|
||
| (isTrue hp) => PSum.inl (@default _ (inhabited_of_nonempty hp))
|
||
| (isFalse hn) => PSum.inr (fun a => absurd (Nonempty.intro a) hn)
|
||
|
||
noncomputable def strongIndefiniteDescription {α : Sort u} (p : α → Prop) (h : Nonempty α) : {x : α // (∃ y : α, p y) → p x} :=
|
||
@dite _ (∃ x : α, p x) (propDecidable _)
|
||
(fun (hp : ∃ x : α, p x) =>
|
||
show {x : α // (∃ y : α, p y) → p x} from
|
||
let xp := indefiniteDescription _ hp;
|
||
⟨xp.val, fun _ => xp.property⟩)
|
||
(fun hp => ⟨choice h, fun h => absurd h hp⟩)
|
||
|
||
/-- the Hilbert epsilon Function -/
|
||
noncomputable def epsilon {α : Sort u} [h : Nonempty α] (p : α → Prop) : α :=
|
||
(strongIndefiniteDescription p h).val
|
||
|
||
theorem epsilon_spec_aux {α : Sort u} (h : Nonempty α) (p : α → Prop) : (∃ y, p y) → p (@epsilon α h p) :=
|
||
(strongIndefiniteDescription p h).property
|
||
|
||
theorem epsilon_spec {α : Sort u} {p : α → Prop} (hex : ∃ y, p y) : p (@epsilon α (nonempty_of_exists hex) p) :=
|
||
epsilon_spec_aux (nonempty_of_exists hex) p hex
|
||
|
||
theorem epsilon_singleton {α : Sort u} (x : α) : @epsilon α ⟨x⟩ (fun y => y = x) = x :=
|
||
@epsilon_spec α (fun y => y = x) ⟨x, rfl⟩
|
||
|
||
/-- the axiom of choice -/
|
||
theorem axiomOfChoice {α : Sort u} {β : α → Sort v} {r : ∀ x, β x → Prop} (h : ∀ x, ∃ y, r x y) : ∃ (f : ∀ x, β x), ∀ x, r x (f x) :=
|
||
⟨_, fun x => choose_spec (h x)⟩
|
||
|
||
theorem skolem {α : Sort u} {b : α → Sort v} {p : ∀ x, b x → Prop} : (∀ x, ∃ y, p x y) ↔ ∃ (f : ∀ x, b x), ∀ x, p x (f x) :=
|
||
⟨axiomOfChoice, fun ⟨f, hw⟩ (x) => ⟨f x, hw x⟩⟩
|
||
|
||
theorem propComplete (a : Prop) : a = True ∨ a = False :=
|
||
match em a with
|
||
| Or.inl ha => Or.inl (eq_true ha)
|
||
| Or.inr hn => Or.inr (eq_false hn)
|
||
|
||
-- this supercedes byCases in Decidable
|
||
theorem byCases {p q : Prop} (hpq : p → q) (hnpq : ¬p → q) : q :=
|
||
Decidable.byCases (dec := propDecidable _) hpq hnpq
|
||
|
||
-- this supercedes byContradiction in Decidable
|
||
theorem byContradiction {p : Prop} (h : ¬p → False) : p :=
|
||
Decidable.byContradiction (dec := propDecidable _) h
|
||
|
||
/-- The Double Negation Theorem: `¬¬P` is equivalent to `P`.
|
||
The left-to-right direction, double negation elimination (DNE),
|
||
is classically true but not constructively. -/
|
||
@[simp] theorem not_not : ¬¬a ↔ a := Decidable.not_not
|
||
|
||
@[simp low] theorem not_forall {p : α → Prop} : (¬∀ x, p x) ↔ ∃ x, ¬p x := Decidable.not_forall
|
||
|
||
theorem not_forall_not {p : α → Prop} : (¬∀ x, ¬p x) ↔ ∃ x, p x := Decidable.not_forall_not
|
||
theorem not_exists_not {p : α → Prop} : (¬∃ x, ¬p x) ↔ ∀ x, p x := Decidable.not_exists_not
|
||
|
||
theorem forall_or_exists_not (P : α → Prop) : (∀ a, P a) ∨ ∃ a, ¬ P a := by
|
||
rw [← not_forall]; exact em _
|
||
theorem exists_or_forall_not (P : α → Prop) : (∃ a, P a) ∨ ∀ a, ¬ P a := by
|
||
rw [← not_exists]; exact em _
|
||
|
||
theorem or_iff_not_imp_left : a ∨ b ↔ (¬a → b) := Decidable.or_iff_not_imp_left
|
||
theorem or_iff_not_imp_right : a ∨ b ↔ (¬b → a) := Decidable.or_iff_not_imp_right
|
||
|
||
theorem not_imp_iff_and_not : ¬(a → b) ↔ a ∧ ¬b := Decidable.not_imp_iff_and_not
|
||
|
||
theorem not_and_iff_or_not_not : ¬(a ∧ b) ↔ ¬a ∨ ¬b := Decidable.not_and_iff_or_not_not
|
||
|
||
theorem not_iff : ¬(a ↔ b) ↔ (¬a ↔ b) := Decidable.not_iff
|
||
|
||
@[simp] theorem imp_iff_left_iff : (b ↔ a → b) ↔ a ∨ b := Decidable.imp_iff_left_iff
|
||
@[simp] theorem imp_iff_right_iff : (a → b ↔ b) ↔ a ∨ b := Decidable.imp_iff_right_iff
|
||
|
||
@[simp] theorem and_or_imp : a ∧ b ∨ (a → c) ↔ a → b ∨ c := Decidable.and_or_imp
|
||
|
||
@[simp] theorem not_imp : ¬(a → b) ↔ a ∧ ¬b := Decidable.not_imp_iff_and_not
|
||
|
||
@[simp] theorem imp_and_neg_imp_iff (p q : Prop) : (p → q) ∧ (¬p → q) ↔ q :=
|
||
Iff.intro (fun (a : _ ∧ _) => (Classical.em p).rec a.left a.right)
|
||
(fun a => And.intro (fun _ => a) (fun _ => a))
|
||
|
||
end Classical
|
||
|
||
/- Export for Mathlib compat. -/
|
||
export Classical (imp_iff_right_iff imp_and_neg_imp_iff and_or_imp not_imp)
|
||
|
||
/-- Extract an element from a existential statement, using `Classical.choose`. -/
|
||
-- This enables projection notation.
|
||
@[reducible] noncomputable def Exists.choose {p : α → Prop} (P : ∃ a, p a) : α := Classical.choose P
|
||
|
||
/-- Show that an element extracted from `P : ∃ a, p a` using `P.choose` satisfies `p`. -/
|
||
theorem Exists.choose_spec {p : α → Prop} (P : ∃ a, p a) : p P.choose := Classical.choose_spec P
|