diff options
| -rw-r--r-- | doc/stdlib/index-list.html.template | 3 | ||||
| -rw-r--r-- | theories/Logic/Fan.v | 107 | ||||
| -rw-r--r-- | theories/Logic/vo.itarget | 1 |
3 files changed, 110 insertions, 1 deletions
diff --git a/doc/stdlib/index-list.html.template b/doc/stdlib/index-list.html.template index b7a76b94f..9382a0890 100644 --- a/doc/stdlib/index-list.html.template +++ b/doc/stdlib/index-list.html.template @@ -37,7 +37,7 @@ through the <tt>Require Import</tt> command.</p> </dd> <dt> <b>Logic</b>: - Classical logic and dependent equality + Classical logic, dependent equality, extensionality, choice axioms </dt> <dd> theories/Logic/SetIsType.v @@ -69,6 +69,7 @@ through the <tt>Require Import</tt> command.</p> theories/Logic/IndefiniteDescription.v theories/Logic/FunctionalExtensionality.v theories/Logic/ExtensionalityFacts.v + theories/Logic/Fan.v </dd> <dt> <b>Structures</b>: 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 |