From 0be32827ddefd227b78d2edff1117b36edaedb20 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Fran=C3=A7ois=20Cl=C3=A9ment?= <francois.clement@inria.fr>
Date: Mon, 21 Mar 2022 19:57:12 +0100
Subject: [PATCH] WIP: playing with streams...

---
 Lebesgue/nat_compl.v    |  16 ++++---
 Lebesgue/stream_compl.v | 101 ++++++++++++++++++++++++++++++++++++++++
 2 files changed, 111 insertions(+), 6 deletions(-)
 create mode 100644 Lebesgue/stream_compl.v

diff --git a/Lebesgue/nat_compl.v b/Lebesgue/nat_compl.v
index 7a07faaa..4926d600 100644
--- a/Lebesgue/nat_compl.v
+++ b/Lebesgue/nat_compl.v
@@ -16,6 +16,7 @@ COPYING file for more details.
 
 From Coq Require Import Classical.
 From Coq Require Import Arith Nat Lia.
+(*From Coq Require Import Streams.*)
 From Coquelicot Require Import Coquelicot.
 
 
@@ -81,22 +82,24 @@ End Even_compl.
 
 Section Select_in_predicate.
 
-Variable P : nat -> Prop. (* Predicate on natural numbers. *)
-
 (*
 Lemma classic_P : forall P (n : nat), P n \/ ~ P n.
 Proof.
 intros; apply classic.
 Qed.
 
-Fixpoint select (P : nat -> Prop) (n : nat) : nat :=
+Fixpoint select (P : nat -> Prop) : Stream nat :=
   match (LPO P (classic_P P)) with
   | inleft H =>
-    let N := proj1_sig H in N
+    let N := proj1_sig H in
+    let P n := match eq_dec n N with | left _ => False | right _ => P n end in
+    Cons N (select P)
   | inright H => 0
   end.
 *)
 
+Variable P : nat -> Prop. (* Predicate on natural numbers. *)
+
 Definition useful_finite : (nat -> nat) -> nat -> Prop :=
   fun phi N =>
     (forall n, n < S N -> P (phi n)) /\
@@ -107,7 +110,7 @@ Definition useful_seq : (nat -> nat) -> Prop :=
     (forall n, P (phi n)) /\
     (forall p, P p -> exists n, p = phi n).
 
-(* When we don't need an injecive function fhi *)
+(* When we don't need an injective function fhi. *)
 Lemma keep_useful :
   exists (phi : nat -> nat) (optN : option nat),
     match optN with
@@ -115,10 +118,11 @@ Lemma keep_useful :
     | None => useful_seq phi
     end.
 Proof.
-destruct (LPO (fun N => forall n, N < n -> ~ P n)) as [[N HN] | H].
+destruct (LPO (fun N => P N /\ forall n, N < n -> ~ P n)) as [[N HN] | H].
 intros; apply classic.
 (* *)
 
+
 Admitted.
 
 Definition get_useful :
diff --git a/Lebesgue/stream_compl.v b/Lebesgue/stream_compl.v
new file mode 100644
index 00000000..e1305ee3
--- /dev/null
+++ b/Lebesgue/stream_compl.v
@@ -0,0 +1,101 @@
+(**
+This file is part of the Elfic library
+
+Copyright (C) Boldo, Clément, Faissole, Martin, Mayero
+
+This library is free software; you can redistribute it and/or
+modify it under the terms of the GNU Lesser General Public
+License as published by the Free Software Foundation; either
+version 3 of the License, or (at your option) any later version.
+
+This library is distributed in the hope that it will be useful,
+but WITHOUT ANY WARRANTY; without even the implied warranty of
+MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
+COPYING file for more details.
+*)
+
+(*From Coq Require Import ClassicalDescription.*)
+From Coq Require Import Arith Lia.
+From Coq Require Import List Streams.
+
+Require Import list_compl.
+
+
+Open Scope list_scope.
+
+
+Section Stream_nat.
+
+CoFixpoint from (n : nat) : Stream nat := Cons n (from (S n)).
+
+Lemma from_hd : forall n, hd (from n) = n.
+Proof.
+easy.
+Qed.
+
+Lemma from_tl : forall n, tl (from n) = from (S n).
+Proof.
+easy.
+Qed.
+
+Lemma from_Str_nth_tl :
+  forall n m, Str_nth_tl m (from n) = from (n + m).
+Proof.
+intros n m; induction m; unfold Str_nth in *; simpl; try (f_equal; lia).
+rewrite <- from_tl, <- tl_nth_tl.
+rewrite IHm, from_tl; f_equal; lia.
+Qed.
+
+Lemma from_correct : forall n m, Str_nth m (from n) = n + m.
+Proof.
+intros; unfold Str_nth; rewrite from_Str_nth_tl; easy.
+Qed.
+
+Definition nats : Stream nat := from 0.
+
+Lemma nats_correct : forall n, Str_nth n nats = n.
+Proof.
+apply from_correct.
+Qed.
+
+End Stream_nat.
+
+
+Section Stream_fun.
+
+Context {A : Type}.
+
+Definition of_fun : (nat -> A) -> Stream A := fun f => map f nats.
+Definition to_fun : Stream A -> nat -> A := fun s n => Str_nth n s.
+
+Lemma of_fun_correct : forall f n, Str_nth n (of_fun f) = f n.
+Proof.
+intros f n; unfold of_fun; rewrite Str_nth_map, nats_correct; easy.
+Qed.
+
+End Stream_fun.
+
+
+Section Stream_select_finite.
+
+Variable P : nat -> Prop.
+
+Variable N : nat.
+Hypothesis HP_finite : P N /\ forall n, N < n -> ~ P n.
+
+Definition select_finite : list nat := select P (seq 0 (S N)).
+
+End Stream_select_finite.
+
+
+Section Stream_select_infinite.
+
+Variable P : nat -> Prop.
+
+Hypothesis HP_infinite : forall N, exists n, N < n /\ P n.
+
+Definition select_infinite : Stream nat.
+Proof.
+Admitted.
+
+End Stream_select_infinite.
-- 
GitLab