118 lines
4.7 KiB
Text
118 lines
4.7 KiB
Text
/-
|
|
Copyright (c) 2015 Microsoft Corporation. All rights reserved.
|
|
Released under Apache 2.0 license as described in the file LICENSE.
|
|
Author: Leonardo de Moura
|
|
|
|
This file is based on Coq's WeakFan.v file
|
|
|
|
A constructive proof of a non-standard version of the weak Fan Theorem
|
|
in the formulation of which infinite paths are treated as
|
|
predicates. The representation of paths as relations avoid the
|
|
need for classical logic and unique choice. The idea of the proof
|
|
comes from the proof of the weak König's lemma from separation in
|
|
second-order arithmetic:
|
|
|
|
Stephen G. Simpson. Subsystems of second order
|
|
arithmetic, Cambridge University Press, 1999
|
|
-/
|
|
import data.list
|
|
open bool nat list
|
|
|
|
namespace weak_fan
|
|
-- inductively_barred P l means that P eventually holds above l
|
|
inductive inductively_barred (P : list bool → Prop) : list bool → Prop :=
|
|
| base : ∀ l, P l → inductively_barred P l
|
|
| propagate : ∀ l,
|
|
inductively_barred P (tt::l) →
|
|
inductively_barred P (ff::l) →
|
|
inductively_barred P l
|
|
|
|
-- approx X l says that l is a boolean representation of a prefix of X
|
|
definition approx : (nat → Prop) → (list bool) → Prop
|
|
| X [] := true
|
|
| X (b::l) := approx X l ∧ (cond b (X (length l)) (¬ (X (length l))))
|
|
|
|
-- barred P means that for any infinite path represented as a predicate, the property P holds for some prefix of the path
|
|
definition barred P := ∀ X, ∃ l, approx X l ∧ P l
|
|
|
|
/-
|
|
The proof proceeds by building a set Y of finite paths
|
|
approximating either the smallest unbarred infinite path in P, if
|
|
there is one (taking tt > ff), or the path tt::tt::...
|
|
if P happens to be inductively_barred
|
|
-/
|
|
private definition Y : (list bool → Prop) → list bool → Prop
|
|
| P [] := true
|
|
| P (b::l) := Y P l ∧ (cond b (inductively_barred P (ff::l)) (¬(inductively_barred P (ff::l))))
|
|
|
|
private lemma Y_unique : ∀ {P l₁ l₂}, length l₁ = length l₂ → Y P l₁ → Y P l₂ → l₁ = l₂
|
|
| P [] [] h₁ h₂ h₃ := rfl
|
|
| P [] (a₂::l₂) h₁ h₂ h₃ := by contradiction
|
|
| P (a₁::l₁) [] h₁ h₂ h₃ := by contradiction
|
|
| P (a₁::l₁) (a₂::l₂) h₁ h₂ h₃ :=
|
|
have n₁ : length l₁ = length l₂, by rewrite [*length_cons at h₁]; apply nat.add_right_cancel h₁,
|
|
have n₂ : Y P l₁, from and.elim_left h₂,
|
|
have n₃ : Y P l₂, from and.elim_left h₃,
|
|
assert ih : l₁ = l₂, from Y_unique n₁ n₂ n₃,
|
|
begin
|
|
clear Y_unique, subst l₂, congruence,
|
|
show a₁ = a₂,
|
|
begin
|
|
cases a₁,
|
|
{cases a₂, reflexivity, exact absurd (and.elim_right h₃) (and.elim_right h₂)},
|
|
{cases a₂, exact absurd (and.elim_right h₂) (and.elim_right h₃), reflexivity}
|
|
end
|
|
end
|
|
|
|
-- X is the translation of Y as a predicate
|
|
private definition X P n := ∃ l, length l = n ∧ Y P (tt::l)
|
|
|
|
private lemma Y_approx : ∀ {P l}, approx (X P) l → Y P l
|
|
| P [] h := trivial
|
|
| P (a::l) h :=
|
|
begin
|
|
have ypl : Y P l, from Y_approx (and.elim_left h),
|
|
unfold Y, split,
|
|
{exact ypl},
|
|
{cases a,
|
|
{have nxp : ¬X P (length l), begin unfold approx at h, rewrite cond_ff at h, exact and.elim_right h end,
|
|
rewrite cond_ff, intro ib,
|
|
have xp : X P (length l), begin existsi l, split, reflexivity, unfold Y, split, exact ypl, rewrite cond_tt, exact ib end,
|
|
contradiction},
|
|
{rewrite cond_tt,
|
|
have xp : X P (length l), begin unfold approx at h, rewrite cond_tt at h, exact and.elim_right h end,
|
|
obtain l₁ hl yptt, from xp,
|
|
begin
|
|
unfold Y at yptt, rewrite cond_tt at yptt,
|
|
have ypl₁ : Y P l₁, from and.elim_left yptt,
|
|
have ib₁ : inductively_barred P (ff::l₁), from and.elim_right yptt,
|
|
have ll₁ : l₁ = l, from Y_unique hl ypl₁ ypl,
|
|
subst l, exact ib₁
|
|
end}}
|
|
end
|
|
|
|
theorem weak_fan : ∀ {P}, barred P → inductively_barred P [] :=
|
|
λ P Hbar,
|
|
obtain l Hd HP, from Hbar (X P),
|
|
assert ib : inductively_barred P l, from inductively_barred.base l HP,
|
|
begin
|
|
clear Hbar HP,
|
|
induction l with a l ih,
|
|
{exact ib},
|
|
{unfold approx at Hd, cases Hd with Hd HX,
|
|
have ypl : Y P l, from Y_approx Hd,
|
|
cases a,
|
|
{rewrite cond_ff at HX,
|
|
have xpl : X P (length l), begin unfold X, existsi l, split, reflexivity, unfold Y, rewrite cond_tt, split, repeat assumption end,
|
|
exact absurd xpl HX},
|
|
{rewrite cond_tt at HX,
|
|
obtain l₁ hl yptt, from HX,
|
|
begin
|
|
unfold Y at yptt, rewrite cond_tt at yptt,
|
|
have ll₁ : l₁ = l, from Y_unique hl (and.elim_left yptt) ypl,
|
|
subst l₁,
|
|
have ibl : inductively_barred P l, from inductively_barred.propagate l ib (and.elim_right yptt),
|
|
exact ih Hd ibl,
|
|
end}}
|
|
end
|
|
end weak_fan
|