From 44f86620d6547d76bfe843c3106003a55748df45 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Fran=C3=A7ois=20Cl=C3=A9ment?= <francois.clement@inria.fr>
Date: Fri, 25 Mar 2022 16:35:22 +0100
Subject: [PATCH] This was useless.
---
Lebesgue/nat_compl.v | 60 ------------------------
Lebesgue/stream_compl.v | 101 ----------------------------------------
2 files changed, 161 deletions(-)
delete mode 100644 Lebesgue/stream_compl.v
diff --git a/Lebesgue/nat_compl.v b/Lebesgue/nat_compl.v
index 4926d600..27722091 100644
--- a/Lebesgue/nat_compl.v
+++ b/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. **)
diff --git a/Lebesgue/stream_compl.v b/Lebesgue/stream_compl.v
deleted file mode 100644
index e1305ee3..00000000
--- a/Lebesgue/stream_compl.v
+++ /dev/null
@@ -1,101 +0,0 @@
-(**
-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