aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
authorGravatar Hugo Herbelin <Hugo.Herbelin@inria.fr>2014-12-01 19:27:17 +0100
committerGravatar Hugo Herbelin <Hugo.Herbelin@inria.fr>2014-12-01 19:48:35 +0100
commit8ef0f5209619c1125474e6fbed9a55ffbd6599a2 (patch)
tree2718ed8bef72eaa17406d63921cea8c48e015536
parent2f61ea2926a72ba3d7b5cb8a1746e34df99838cc (diff)
Added an arithmetical characterization of the hypothesis of WKL.
-rw-r--r--theories/Logic/WKL.v26
1 files changed, 26 insertions, 0 deletions
diff --git a/theories/Logic/WKL.v b/theories/Logic/WKL.v
index 24f1717a7..4706b8749 100644
--- a/theories/Logic/WKL.v
+++ b/theories/Logic/WKL.v
@@ -23,6 +23,8 @@
Require Import WeakFan List.
Import ListNotations.
+Require Import Omega.
+
(** [is_path_from P n l] means that there exists a path of length [n]
from [l] on which [P] does not hold *)
@@ -31,6 +33,30 @@ Inductive is_path_from (P:list bool -> Prop) : nat -> list bool -> Prop :=
| next_left l n : ~ P l -> is_path_from P n (true::l) -> is_path_from P (S n) l
| next_right l n : ~ P l -> is_path_from P n (false::l) -> is_path_from P (S n) l.
+(** We give the characterization of is_path_from in terms of a more common arithmetical formula *)
+
+Proposition is_path_from_characterization P n l :
+ is_path_from P n l <-> exists l', length l' = n /\ forall n', n'<=n -> ~ P (rev (firstn n' l') ++ l).
+Proof.
+intros. split.
+- induction 1 as [|* HP _ (l'&Hl'&HPl')|* HP _ (l'&Hl'&HPl')].
+ + exists []. split. reflexivity. intros n <-/le_n_0_eq. assumption.
+ + exists (true :: l'). split. apply eq_S, Hl'. intros [|] H.
+ * assumption.
+ * simpl. rewrite <- app_assoc. apply HPl', le_S_n, H.
+ + exists (false :: l'). split. apply eq_S, Hl'. intros [|] H.
+ * assumption.
+ * simpl. rewrite <- app_assoc. apply HPl', le_S_n, H.
+- intros (l'& <- &HPl'). induction l' as [|[|]] in l, HPl' |- *.
+ + constructor. apply (HPl' 0). apply le_0_n.
+ + eapply next_left.
+ * apply (HPl' 0), le_0_n.
+ * fold (length l'). apply IHl'. intros n' H/le_n_S. apply HPl' in H. simpl in H. rewrite <- app_assoc in H. assumption.
+ + apply next_right.
+ * apply (HPl' 0), le_0_n.
+ * fold (length l'). apply IHl'. intros n' H/le_n_S. apply HPl' in H. simpl in H. rewrite <- app_assoc in H. assumption.
+Qed.
+
(** [infinite_from P l] means that we can find arbitrary long paths
along which [P] does not hold above [l] *)