This was useless.

Lebesgue/nat_compl.v

@@ -80,66 +80,6 @@ Qed.
 End Even_compl.
 
 
-Section Select_in_predicate.
-
-(*
-Lemma classic_P : forall P (n : nat), P n \/ ~ P n.
-Proof.
-intros; apply classic.
-Qed.
-
-Fixpoint select (P : nat -> Prop) : Stream nat :=
-  match (LPO P (classic_P P)) with
-  | inleft H =>
-    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)) /\
-    (forall p, P p -> exists n, n < S N /\ p = phi n).
-
-Definition useful_seq : (nat -> nat) -> Prop :=
-  fun phi =>
-    (forall n, P (phi n)) /\
-    (forall p, P p -> exists n, p = phi n).
-
-(* When we don't need an injective function fhi. *)
-Lemma keep_useful :
-  exists (phi : nat -> nat) (optN : option nat),
-    match optN with
-    | Some N => useful_finite phi N
-    | None => useful_seq phi
-    end.
-Proof.
-destruct (LPO (fun N => P N /\ forall n, N < n -> ~ P n)) as [[N HN] | H].
-intros; apply classic.
-(* *)
-
-
-Admitted.
-
-Definition get_useful :
-    forall {T : Type},
-      (nat -> T) -> T -> (nat -> nat) -> option nat -> nat -> T :=
-  fun T f f0 phi optN n =>
-    match optN with
-    | Some N => match (lt_dec n (S N)) with
-      | left _ => f (phi n)
-      | right _ => f0
-      end
-    | None => f (phi n)
-    end.
-
-End Select_in_predicate.
-
-
 Section Mult_compl.
 
 (** Complements on the multiplication on natural numbers. **)

Lebesgue/stream_compl.v

-(**
-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.