lean2/library/logic/quantifiers.lean

126 lines
4.4 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.
Authors: Leonardo de Moura, Jeremy Avigad
Universal and existential quantifiers. See also init.logic.
-/
import .connectives
open inhabited nonempty
theorem not_forall_not_of_exists {A : Type} {p : A → Prop} (H : ∃x, p x) : ¬∀x, ¬p x :=
assume H1 : ∀x, ¬p x,
obtain (w : A) (Hw : p w), from H,
absurd Hw (H1 w)
theorem not_exists_not_of_forall {A : Type} {p : A → Prop} (H2 : ∀x, p x) : ¬∃x, ¬p x :=
assume H1 : ∃x, ¬p x,
obtain (w : A) (Hw : ¬p w), from H1,
absurd (H2 w) Hw
theorem forall_congr {A : Type} {φ ψ : A → Prop} (H : ∀x, φ x ↔ ψ x) : (∀x, φ x) ↔ (∀x, ψ x) :=
iff.intro
(assume Hl, take x, iff.elim_left (H x) (Hl x))
(assume Hr, take x, iff.elim_right (H x) (Hr x))
theorem exists_congr {A : Type} {φ ψ : A → Prop} (H : ∀x, φ x ↔ ψ x) : (∃x, φ x) ↔ (∃x, ψ x) :=
iff.intro
(assume Hex, obtain w Pw, from Hex,
exists.intro w (iff.elim_left (H w) Pw))
(assume Hex, obtain w Qw, from Hex,
exists.intro w (iff.elim_right (H w) Qw))
theorem forall_true_iff_true (A : Type) : (∀x : A, true) ↔ true :=
iff.intro (assume H, trivial) (assume H, take x, trivial)
theorem forall_p_iff_p (A : Type) [H : inhabited A] (p : Prop) : (∀x : A, p) ↔ p :=
iff.intro (assume Hl, inhabited.destruct H (take x, Hl x)) (assume Hr, take x, Hr)
theorem exists_p_iff_p (A : Type) [H : inhabited A] (p : Prop) : (∃x : A, p) ↔ p :=
iff.intro
(assume Hl, obtain a Hp, from Hl, Hp)
(assume Hr, inhabited.destruct H (take a, exists.intro a Hr))
theorem forall_and_distribute {A : Type} (φ ψ : A → Prop) :
(∀x, φ x ∧ ψ x) ↔ (∀x, φ x) ∧ (∀x, ψ x) :=
iff.intro
(assume H, and.intro (take x, and.elim_left (H x)) (take x, and.elim_right (H x)))
(assume H, take x, and.intro (and.elim_left H x) (and.elim_right H x))
theorem exists_or_distribute {A : Type} (φ ψ : A → Prop) :
(∃x, φ x ψ x) ↔ (∃x, φ x) (∃x, ψ x) :=
iff.intro
(assume H, obtain (w : A) (Hw : φ w ψ w), from H,
or.elim Hw
(assume Hw1 : φ w, or.inl (exists.intro w Hw1))
(assume Hw2 : ψ w, or.inr (exists.intro w Hw2)))
(assume H, or.elim H
(assume H1, obtain (w : A) (Hw : φ w), from H1,
exists.intro w (or.inl Hw))
(assume H2, obtain (w : A) (Hw : ψ w), from H2,
exists.intro w (or.inr Hw)))
theorem nonempty_of_exists {A : Type} {P : A → Prop} (H : ∃x, P x) : nonempty A :=
obtain w Hw, from H, nonempty.intro w
section
open decidable eq.ops
variables {A : Type} (P : A → Prop) (a : A) [H : decidable (P a)]
include H
definition decidable_forall_eq [instance] : decidable (∀ x, x = a → P x) :=
decidable.rec_on H
(λ pa, inl (λ x heq, eq.rec_on (eq.rec_on heq rfl) pa))
(λ npa, inr (λ h, absurd (h a rfl) npa))
definition decidable_exists_eq [instance] : decidable (∃ x, x = a ∧ P x) :=
decidable.rec_on H
(λ pa, inl (exists.intro a (and.intro rfl pa)))
(λ npa, inr (λ h,
obtain (w : A) (Hw : w = a ∧ P w), from h,
absurd (and.rec_on Hw (λ h₁ h₂, h₁ ▸ h₂)) npa))
end
/- exists_unique -/
definition exists_unique {A : Type} (p : A → Prop) :=
∃x, p x ∧ ∀y, p y → y = x
notation `∃!` binders `,` r:(scoped P, exists_unique P) := r
theorem exists_unique.intro {A : Type} {p : A → Prop} (w : A) (H1 : p w) (H2 : ∀y, p y → y = w) :
∃!x, p x :=
exists.intro w (and.intro H1 H2)
theorem exists_unique.elim {A : Type} {p : A → Prop} {b : Prop}
(H2 : ∃!x, p x) (H1 : ∀x, p x → (∀y, p y → y = x) → b) : b :=
obtain w Hw, from H2,
H1 w (and.elim_left Hw) (and.elim_right Hw)
/- congruences -/
section
variables {A : Type} {p₁ p₂ : A → Prop} (H : ∀x, p₁ x ↔ p₂ x)
theorem congr_forall : (∀x, p₁ x) ↔ (∀x, p₂ x) :=
iff.intro
(assume H', take x, iff.mp (H x) (H' x))
(assume H', take x, iff.mp' (H x) (H' x))
theorem congr_exists : (∃x, p₁ x) ↔ (∃x, p₂ x) :=
iff.intro
(assume H', exists.elim H' (λ x H₁, exists.intro x (iff.mp (H x) H₁)))
(assume H', exists.elim H' (λ x H₁, exists.intro x (iff.mp' (H x) H₁)))
include H
theorem congr_exists_unique : (∃!x, p₁ x) ↔ (∃!x, p₂ x) :=
begin
apply congr_exists,
intro x,
apply congr_and (H x),
apply congr_forall,
intro y,
apply congr_imp (H y) !iff.rfl
end
end