From 5e8b1a896435d8f7a4942edb392e9cfe61bceafa Mon Sep 17 00:00:00 2001
From: Reynald Affeldt <reynald.affeldt@aist.go.jp>
Date: Mon, 5 Sep 2022 09:10:00 +0900
Subject: [PATCH] deprecated warnings for Rstruct's bigmax

---
 theories/Rstruct.v | 22 ++++++++++++++++++++++
 1 file changed, 22 insertions(+)

diff --git a/theories/Rstruct.v b/theories/Rstruct.v
index 0a7d9c6a0..18941ddfe 100644
--- a/theories/Rstruct.v
+++ b/theories/Rstruct.v
@@ -503,15 +503,19 @@ Section bigmaxr.
 Context {R : realDomainType}.
 
 (* bigop pour le max pour des listes non vides ? *)
+#[deprecated(note="To be removed. Use topology.v's bigmax/min lemmas instead.")]
 Definition bigmaxr (r : R) s := \big[Num.max/head r s]_(i <- s) i.
 
+#[deprecated(note="To be removed. Use topology.v's bigmax/min lemmas instead.")]
 Lemma bigmaxr_nil (x0 : R) : bigmaxr x0 [::] = x0.
 Proof. by rewrite /bigmaxr /= big_nil. Qed.
 
+#[deprecated(note="To be removed. Use topology.v's bigmax/min lemmas instead.")]
 Lemma bigmaxr_un (x0 x : R) : bigmaxr x0 [:: x] = x.
 Proof. by rewrite /bigmaxr /= big_cons big_nil maxxx. Qed.
 
 (* previous definition *)
+#[deprecated(note="To be removed. Use topology.v's bigmax/min lemmas instead.")]
 Lemma bigmaxrE (r : R) s : bigmaxr r s = foldr Num.max (head r s) (behead s).
 Proof.
 rewrite (_ : bigmaxr _ _ = if s isn't h :: t then r else \big[Num.max/h]_(i <- s) i).
@@ -520,6 +524,7 @@ rewrite (_ : bigmaxr _ _ = if s isn't h :: t then r else \big[Num.max/h]_(i <- s
 by case: s => //=; rewrite /bigmaxr big_nil.
 Qed.
 
+#[deprecated(note="To be removed. Use topology.v's bigmax/min lemmas instead.")]
 Lemma bigrmax_dflt (x y : R) s : Num.max x (\big[Num.max/x]_(j <- y :: s) j) =
   Num.max x (\big[Num.max/y]_(i <- y :: s) i).
 Proof.
@@ -528,10 +533,12 @@ by rewrite !big_cons !big_nil maxxx maxCA maxxx maxC.
 by rewrite big_cons maxCA IH maxCA [in RHS]big_cons IH.
 Qed.
 
+#[deprecated(note="To be removed. Use topology.v's bigmax/min lemmas instead.")]
 Lemma bigmaxr_cons (x0 x y : R) lr :
   bigmaxr x0 (x :: y :: lr) = Num.max x (bigmaxr x0 (y :: lr)).
 Proof. by rewrite [y :: lr]lock /bigmaxr /= -lock big_cons bigrmax_dflt. Qed.
 
+#[deprecated(note="To be removed. Use topology.v's bigmax/min lemmas instead.")]
 Lemma bigmaxr_ler (x0 : R) s i :
   (i < size s)%N -> (nth x0 s i) <= (bigmaxr x0 s).
 Proof.
@@ -542,6 +549,7 @@ by rewrite big_cons bigrmax_dflt le_maxr orbC IH.
 Qed.
 
 (* Compatibilité avec l'addition *)
+#[deprecated(note="To be removed. Use topology.v's bigmax/min lemmas instead.")]
 Lemma bigmaxr_addr (x0 : R) lr (x : R) :
   bigmaxr (x0 + x) (map (fun y : R => y + x) lr) = (bigmaxr x0 lr) + x.
 Proof.
@@ -550,6 +558,7 @@ elim: t h => /= [|h' t IH] h; first by rewrite ?(big_cons,big_nil) -addr_maxl.
 by rewrite [in RHS]big_cons bigrmax_dflt addr_maxl -IH big_cons bigrmax_dflt.
 Qed.
 
+#[deprecated(note="To be removed. Use topology.v's bigmax/min lemmas instead.")]
 Lemma bigmaxr_mem (x0 : R) lr : (0 < size lr)%N -> bigmaxr x0 lr \in lr.
 Proof.
 rewrite /bigmaxr; case: lr => // h t _.
@@ -560,6 +569,7 @@ rewrite big_cons bigrmax_dflt inE eq_le; case: lerP => /=.
 Qed.
 
 (* TODO: bigmaxr_morph? *)
+#[deprecated(note="To be removed. Use topology.v's bigmax/min lemmas instead.")]
 Lemma bigmaxr_mulr (A : finType) (s : seq A) (k : R) (x : A -> R) :
   0 <= k -> bigmaxr 0 (map (fun i => k * x i) s) = k * bigmaxr 0 (map x s).
 Proof.
@@ -569,6 +579,7 @@ by rewrite !bigmaxr_un.
 by rewrite bigmaxr_cons {}ih bigmaxr_cons maxr_pmulr.
 Qed.
 
+#[deprecated(note="To be removed. Use topology.v's bigmax/min lemmas instead.")]
 Lemma bigmaxr_index (x0 : R) lr :
   (0 < size lr)%N -> (index (bigmaxr x0 lr) lr < size lr)%N.
 Proof.
@@ -577,6 +588,7 @@ move: (@bigmaxr_mem x0 (h :: t) isT).
 by rewrite ltnS index_mem inE /= eq_sym H.
 Qed.
 
+#[deprecated(note="To be removed. Use topology.v's bigmax/min lemmas instead.")]
 Lemma bigmaxr_lerP (x0 : R) lr (x : R) :
   (0 < size lr)%N ->
   reflect (forall i, (i < size lr)%N -> (nth x0 lr i) <= x) ((bigmaxr x0 lr) <= x).
@@ -586,6 +598,7 @@ move=> lr_size; apply: (iffP idP) => [le_x i i_size | H].
 by move/(nthP x0): (bigmaxr_mem x0 lr_size) => [i i_size <-]; apply: H.
 Qed.
 
+#[deprecated(note="To be removed. Use topology.v's bigmax/min lemmas instead.")]
 Lemma bigmaxr_ltrP (x0 : R) lr (x : R) :
   (0 < size lr)%N ->
   reflect (forall i, (i < size lr)%N -> (nth x0 lr i) < x) ((bigmaxr x0 lr) < x).
@@ -595,6 +608,7 @@ move=> lr_size; apply: (iffP idP) => [lt_x i i_size | H].
 by move/(nthP x0): (bigmaxr_mem x0 lr_size) => [i i_size <-]; apply: H.
 Qed.
 
+#[deprecated(note="To be removed. Use topology.v's bigmax/min lemmas instead.")]
 Lemma bigmaxrP (x0 : R) lr (x : R) :
   (x \in lr /\ forall i, (i < size lr) %N -> (nth x0 lr i) <= x) -> (bigmaxr x0 lr = x).
 Proof.
@@ -614,6 +628,7 @@ apply/negP => /eqP H; apply: neq_i; rewrite -H eq_sym; apply/eqP.
 by apply: index_uniq.
 Qed. *)
 
+#[deprecated(note="To be removed. Use topology.v's bigmax/min lemmas instead.")]
 Lemma bigmaxr_lerif (x0 : R) lr :
   uniq lr -> forall i, (i < size lr)%N ->
      (nth x0 lr i) <= (bigmaxr x0 lr) ?= iff (i == index (bigmaxr x0 lr) lr).
@@ -625,9 +640,11 @@ by apply: bigmaxr_mem; apply: (leq_trans _ i_size).
 Qed.
 
 (* bigop pour le max pour des listes non vides ? *)
+#[deprecated(note="To be removed. Use topology.v's bigmax/min lemmas instead.")]
 Definition bmaxrf n (f : {ffun 'I_n.+1 -> R}) :=
   bigmaxr (f ord0) (codom f).
 
+#[deprecated(note="To be removed. Use topology.v's bigmax/min lemmas instead.")]
 Lemma bmaxrf_ler n (f : {ffun 'I_n.+1 -> R}) i :
   (f i) <= (bmaxrf f).
 Proof.
@@ -637,6 +654,7 @@ suff -> : nth (f ord0) (codom f) i = f i; first by [].
 by rewrite /codom (nth_map ord0) ?size_enum_ord // nth_ord_enum.
 Qed.
 
+#[deprecated(note="To be removed. Use topology.v's bigmax/min lemmas instead.")]
 Lemma bmaxrf_index n (f : {ffun 'I_n.+1 -> R}) :
   (index (bmaxrf f) (codom f) < n.+1)%N.
 Proof.
@@ -646,11 +664,14 @@ rewrite [in X in (_ < X)%N](_ : n.+1 = size (codom f)); last first.
 by apply: bigmaxr_index; rewrite size_codom card_ord.
 Qed.
 
+#[deprecated(note="To be removed. Use topology.v's bigmax/min lemmas instead.")]
 Definition index_bmaxrf n f := Ordinal (@bmaxrf_index n f).
 
+#[deprecated(note="To be removed. Use topology.v's bigmax/min lemmas instead.")]
 Lemma ordnat i n (ord_i : (i < n)%N) : i = Ordinal ord_i :> nat.
 Proof. by []. Qed.
 
+#[deprecated(note="To be removed. Use topology.v's bigmax/min lemmas instead.")]
 Lemma eq_index_bmaxrf n (f : {ffun 'I_n.+1 -> R}) :
   f (index_bmaxrf f) = bmaxrf f.
 Proof.
@@ -661,6 +682,7 @@ move/(nth_index (f ord0)) => <-; rewrite (nth_map ord0).
 by rewrite size_enum_ord; apply: bmaxrf_index.
 Qed.
 
+#[deprecated(note="To be removed. Use topology.v's bigmax/min lemmas instead.")]
 Lemma bmaxrf_lerif n (f : {ffun 'I_n.+1 -> R}) :
   injective f -> forall i,
      (f i) <= (bmaxrf f) ?= iff (i == index_bmaxrf f).