diff options
author | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-06-02 21:42:14 +0000 |
---|---|---|
committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-06-02 21:42:14 +0000 |
commit | fe008055f8adc7acd6af1483a8e7fef98d27e267 (patch) | |
tree | d484eb859c9210babdd9408fa46c21ca671ebd2d /theories/Logic | |
parent | d51d98682fcff981a1e6b95574c25fc7edf97b3f (diff) |
A constructive proof of Fan theorem where paths are represented by predicates.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16557 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories/Logic')
-rw-r--r-- | theories/Logic/Fan.v | 107 | ||||
-rw-r--r-- | theories/Logic/vo.itarget | 1 |
2 files changed, 108 insertions, 0 deletions
diff --git a/theories/Logic/Fan.v b/theories/Logic/Fan.v new file mode 100644 index 000000000..27b2d64fb --- /dev/null +++ b/theories/Logic/Fan.v @@ -0,0 +1,107 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(** A constructive proof of 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 + [[Simpson99]]. + + [[Simpson99]] Stephen G. Simpson. Subsystems of second order + arithmetic, Cambridge University Press, 1999 *) + + + +Require Import List. +Import ListNotations. + +(** [inductively_barred P l] means that P eventually holds above l *) + +Inductive inductively_barred P : list bool -> Prop := +| now l : P l -> inductively_barred P l +| propagate l : + inductively_barred P (true::l) -> + inductively_barred P (false::l) -> + inductively_barred P l. + +(** [approx X l] says that l is a boolean representation of a prefix of X *) + +Fixpoint approx X (l:list bool) := + match l with + | [] => True + | b::l => approx X l /\ (if b then X (length l) else ~ X (length l)) + end. + +(** [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 := + forall (X:nat -> Prop), exists 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 true>false), or the path true::true::... if P + happens to be inductively_barred *) + +Fixpoint Y P (l:list bool) := + match l with + | [] => True + | b::l => + Y P l /\ + if b then inductively_barred P (false::l) else ~ inductively_barred P (false::l) + end. + +Lemma Y_unique : forall P l1 l2, length l1 = length l2 -> Y P l1 -> Y P l2 -> l1 = l2. +Proof. +induction l1, l2. +- trivial. +- discriminate. +- discriminate. +- intros H (HY1,H1) (HY2,H2). + injection H as H. + pose proof (IHl1 l2 H HY1 HY2). clear HY1 HY2 H IHl1. + subst l1. + f_equal. + destruct a, b; firstorder. +Qed. + +(** X is the translation of Y as a predicate *) + +Definition X P n := exists l, length l = n /\ Y P (true::l). + +Lemma Y_approx : forall P l, approx (X P) l -> Y P l. +Proof. +induction l. +- trivial. +- intros (H,Hb). split. + + auto. + + unfold X in Hb. + destruct a. + * destruct Hb as (l',(Hl',(HYl',HY))). + rewrite <- (Y_unique P l' l Hl'); auto. + * firstorder. +Qed. + +Theorem FanTheorem : forall P, barred P -> inductively_barred P []. +Proof. +intros P Hbar. +destruct (Hbar (X P)) as (l,(Hd,HP)). +assert (inductively_barred P l) by (apply (now P l), HP). +clear Hbar HP. +induction l. +- assumption. +- destruct Hd as (Hd,HX). + apply (IHl Hd). clear IHl. + destruct a; unfold X in HX; simpl in HX. + + apply propagate. + * apply H. + * destruct HX as (l',(Hl,(HY,Ht))); firstorder. + apply Y_approx in Hd. rewrite <- (Y_unique P l' l Hl); trivial. + + destruct HX. exists l. split; auto using Y_approx. +Qed. diff --git a/theories/Logic/vo.itarget b/theories/Logic/vo.itarget index 460468977..ababd75e0 100644 --- a/theories/Logic/vo.itarget +++ b/theories/Logic/vo.itarget @@ -18,6 +18,7 @@ Epsilon.vo Eqdep_dec.vo EqdepFacts.vo Eqdep.vo +Fan.vo FunctionalExtensionality.vo Hurkens.vo IndefiniteDescription.vo |