From 9cb238534df6e2932a6775149e64ab05eb89585a Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sun, 13 Jul 2014 01:39:35 +0100 Subject: [PATCH] feat(library/standard): add hilbert's choice operator Signed-off-by: Leonardo de Moura --- library/standard/hilbert.lean | 22 ++++++++++++++++++++++ 1 file changed, 22 insertions(+) create mode 100644 library/standard/hilbert.lean diff --git a/library/standard/hilbert.lean b/library/standard/hilbert.lean new file mode 100644 index 000000000..d9aedbc0e --- /dev/null +++ b/library/standard/hilbert.lean @@ -0,0 +1,22 @@ +-- 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 + +variable epsilon {A : Type} {H : inhabited A} (P : A → Bool) : A +axiom epsilon_ax {A : Type} {P : A → Bool} (Hex : ∃ a, P a) : P (@epsilon A (inhabited_exists Hex) P) + +theorem epsilon_singleton {A : Type} (a : A) : @epsilon A (inhabited_intro a) (λ x, x = a) = a +:= epsilon_ax (exists_intro a (refl a)) + +theorem axiom_of_choice {A : Type} {B : A → Type} {R : Π x, B x → Bool} (H : ∀ x, ∃ y, R x y) : ∃ f, ∀ x, R x (f x) +:= let f [inline] := λ x, @epsilon _ (inhabited_exists (H x)) (λ y, R x y), + H [inline] := take x, epsilon_ax (H x) + in exists_intro f H + +theorem skolem {A : Type} {B : A → Type} {P : Π x, B x → Bool} : (∀ x, ∃ y, P x y) ↔ ∃ f, (∀ x, P x (f x)) +:= iff_intro + (assume H : (∀ x, ∃ y, P x y), axiom_of_choice H) + (assume H : (∃ f, (∀ x, P x (f x))), + take x, obtain (fw : ∀ x, B x) (Hw : ∀ x, P x (fw x)), from H, + exists_intro (fw x) (Hw x))