lean2/library/data/examples/depchoice.lean

84 lines
3 KiB
Text
Raw Normal View History

/-
Copyright (c) 2015 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Module: data.examples.depchoice
Author: Leonardo de Moura
-/
import data.encodable
open nat encodable
/-
In mathematics, the axiom of dependent choice is a weak form of the axiom of choice that is
sufficient to develop most of real analysis. See http://en.wikipedia.org/wiki/Axiom_of_dependent_choice.
We can state it as follows:
-/
definition dependent_choice {A : Type} (R : A → A → Prop) :=
(∀ a : A, ∃ b : A, R a b) → (∀ a : A, ∃ f : nat → A, f 0 = a ∧ ∀ n, R (f n) (f (n+1)))
/-
If A is an encodable type, and R is a decidable relation, we can prove (dependent_choice R) using the
constructive choice function "choose"
-/
section depchoice
parameters {A : Type} {R : A → A → Prop}
parameters [encA : encodable A] [decR : decidable_rel R]
include encA decR
local infix `~` := R
private definition f_aux (a : A) (H : ∀ a, ∃ b, a ~ b) : nat → A
| 0 := a
| (n+1) := choose (H (f_aux n))
theorem dependent_choice_of_encodable_of_decidable : dependent_choice R :=
assume H : ∀ a, ∃ b, a ~ b,
take a : A,
let f : nat → A := f_aux a H in
have f_zero : f 0 = a, from rfl,
have R_seq : ∀ n, f n ~ f (n+1), from
take n, show f n ~ choose (H (f n)), from !choose_spec,
exists.intro f (and.intro f_zero R_seq)
/-
The following slightly stronger version can be proved, where we also "return" the constructed function f.
We just have to use Σ instead of ∃, and use Σ-constructor instead of exists.intro.
Recall that ⟨f, H⟩ is notation for (sigma.mk f H)
-/
theorem stronger_dependent_choice_of_encodable_of_decidable
: (∀ a, ∃ b, R a b) → (∀ a, Σ f, f 0 = a ∧ ∀ n, f n ~ f (n+1)) :=
assume H : ∀ a, ∃ b, a ~ b,
take a : A,
let f : nat → A := f_aux a H in
have f_zero : f 0 = a, from rfl,
have R_seq : ∀ n, f n ~ f (n+1), from
take n, show f n ~ choose (H (f n)), from !choose_spec,
⟨f, and.intro f_zero R_seq⟩
end depchoice
/-
If we encode dependent_choice using Σ instead of ∃.
Then, we can prove this version without using any extra hypothesis (e.g., A is encodable or R is decidable).
The function f can be constructed directly from the hypothesis: ∀ a : A, Σ b : A, R a b
because Σ "carries" the witness 'b'. That is, we don't have to search for anything using "choose".
-/
open sigma.ops
section sigma_depchoice
parameters {A : Type} {R : A → A → Prop}
local infix `~` := R
private definition f_aux (a : A) (H : ∀ a, Σ b, a ~ b) : nat → A
| 0 := a
| (n+1) := (H (f_aux n)).1
theorem sigma_dependent_choice : (∀ a, Σ b, R a b) → (∀ a, Σ f, f 0 = a ∧ ∀ n, f n ~ f (n+1)) :=
assume H : ∀ a, Σ b, a ~ b,
take a : A,
let f : nat → A := f_aux a H in
have f_zero : f 0 = a, from rfl,
have R_seq : ∀ n, f n ~ f (n+1), from take n, (H (f n)).2,
⟨f, and.intro f_zero R_seq⟩
end sigma_depchoice