From 1881ad0aefc4da63aa824bbe202d4790e94778d3 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 13 Jul 2015 10:18:12 -0400 Subject: [PATCH] feat(library/logic/weak_fan): add weak_fan theorem --- library/logic/weak_fan.lean | 118 ++++++++++++++++++++++++++++++++++++ 1 file changed, 118 insertions(+) create mode 100644 library/logic/weak_fan.lean diff --git a/library/logic/weak_fan.lean b/library/logic/weak_fan.lean new file mode 100644 index 000000000..e6b2b0ba8 --- /dev/null +++ b/library/logic/weak_fan.lean @@ -0,0 +1,118 @@ +/- +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 add.cancel_right 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