From 3f306a5628f67942bb5cf81fab71b10280ca92b4 Mon Sep 17 00:00:00 2001 From: Lionel Rieg <lionel.rieg@univ-grenoble-alpes.fr> Date: Mon, 28 Aug 2023 15:01:04 +0200 Subject: [PATCH] Some more warnings --- CaseStudies/Convergence/Algorithm_noB.v | 16 +++++++++++--- CaseStudies/Convergence/Impossibility_2G_1B.v | 22 ++++++++++++++----- .../Exploration/ImpossibilityKDividesN.v | 10 ++++++--- CaseStudies/Exploration/Tower.v | 12 +++++++--- Spaces/R.v | 2 +- 5 files changed, 47 insertions(+), 15 deletions(-) diff --git a/CaseStudies/Convergence/Algorithm_noB.v b/CaseStudies/Convergence/Algorithm_noB.v index cdc2905d..a089825f 100644 --- a/CaseStudies/Convergence/Algorithm_noB.v +++ b/CaseStudies/Convergence/Algorithm_noB.v @@ -18,9 +18,19 @@ (**************************************************************************) -Require Import Utf8 Reals SetoidDec Lia SetoidList. -From Pactole Require Import Util.Preliminary Util.Fin Setting Spaces.R2 - Observations.SetObservation Models.Rigid Models.NoByzantine Models.Similarity. +Require Import Utf8. +Require Import Reals. +Require Import SetoidDec. +Require Import Lia. +Require Import SetoidList. +Require Import Pactole.Util.Preliminary. +Require Import Pactole.Util.Fin. +Require Import Pactole.Setting. +Require Import Pactole.Spaces.R2. +Require Import Pactole.Observations.SetObservation. +Require Import Pactole.Models.Rigid. +Require Import Pactole.Models.NoByzantine. +Require Import Pactole.Models.Similarity. Set Implicit Arguments. Close Scope R_scope. Import Datatypes. diff --git a/CaseStudies/Convergence/Impossibility_2G_1B.v b/CaseStudies/Convergence/Impossibility_2G_1B.v index 5ee361a8..ed342e76 100644 --- a/CaseStudies/Convergence/Impossibility_2G_1B.v +++ b/CaseStudies/Convergence/Impossibility_2G_1B.v @@ -18,9 +18,21 @@ (**************************************************************************) -Require Import Utf8 Reals Psatz SetoidDec Arith.Div2 Lia SetoidList. -From Pactole Require Import Util.Preliminary Util.Fin Util.Enum Setting Spaces.R - Observations.MultisetObservation Models.Similarity Models.Rigid. +Require Import Utf8. +Require Import Reals. +Require Import Psatz. +Require Import SetoidDec. +Require Import Arith.Div2. +Require Import Lia. +Require Import SetoidList. +Require Import Pactole.Util.Preliminary. +Require Import Pactole.Util.Fin. +Require Import Pactole.Util.Enum. +Require Import Pactole.Setting. +Require Import Pactole.Spaces.R. +Require Import Pactole.Observations.MultisetObservation. +Require Import Pactole.Models.Similarity. +Require Import Pactole.Models.Rigid. Set Implicit Arguments. Close Scope R_scope. Close Scope VectorSpace_scope. @@ -122,7 +134,7 @@ Proof using n_non_0. assert (Hn0 := n_non_0). rewrite nG_nB, nB_value. destruct n as [| ?]. - lia. -- simpl. rewrite plus_comm. simpl. lia. +- cbn. rewrite Nat.add_comm. cbn. lia. Qed. (* TODO: move to a definition/problem file *) @@ -231,7 +243,7 @@ Lemma glast_right : In glast right. Proof using . rewrite right_spec. simpl. assert (Heven := even_nG). destruct n as [| [| ]]; simpl; auto; []. -apply le_n_S, Nat.div2_decr, le_n_Sn. +apply le_n_S, Nat.div2_decr, Nat.le_succ_diag_r. Qed. Hint Resolve gfirst_left glast_right left_right_exclusive : core. diff --git a/CaseStudies/Exploration/ImpossibilityKDividesN.v b/CaseStudies/Exploration/ImpossibilityKDividesN.v index 9ba8b338..b1bbb07f 100644 --- a/CaseStudies/Exploration/ImpossibilityKDividesN.v +++ b/CaseStudies/Exploration/ImpossibilityKDividesN.v @@ -7,9 +7,13 @@ (* *) (**************************************************************************) -Require Import Utf8 Arith SetoidList. -From Pactole Require Import Util.Stream Models.NoByzantine - Models.RingSSync CaseStudies.Exploration.ExplorationDefs. +Require Import Utf8. +Require Import Arith. +Require Import SetoidList. +Require Import Pactole.Util.Stream. +Require Import Pactole.Models.NoByzantine. +Require Import Pactole.Models.RingSSync. +Require Import Pactole.CaseStudies.Exploration.ExplorationDefs. Set Implicit Arguments. Typeclasses eauto := (bfs). diff --git a/CaseStudies/Exploration/Tower.v b/CaseStudies/Exploration/Tower.v index b3f16321..78a5ad6e 100644 --- a/CaseStudies/Exploration/Tower.v +++ b/CaseStudies/Exploration/Tower.v @@ -16,9 +16,15 @@ *) (**************************************************************************) -Require Import Utf8 SetoidList Arith_base Lia. -From Pactole Require Import Util.Stream Util.Enum Util.Fin Models.NoByzantine - Models.RingSSync CaseStudies.Exploration.ExplorationDefs. +Require Import Utf8. +Require Import List SetoidList. +Require Import Arith_base Lia. +Require Import Pactole.Util.Stream. +Require Import Pactole.Util.Enum. +Require Import Pactole.Util.Fin. +Require Import Pactole.Models.NoByzantine. +Require Import Pactole.Models.RingSSync. +Require Import Pactole.CaseStudies.Exploration.ExplorationDefs. Open Scope list_scope. Set Implicit Arguments. diff --git a/Spaces/R.v b/Spaces/R.v index 80d7c738..3a889734 100644 --- a/Spaces/R.v +++ b/Spaces/R.v @@ -412,7 +412,7 @@ intro sim. destruct (similarity_in_R_case sim) as [Hinc | Hdec]. apply similarity_decreasing; trivial; []. (* TODO Coq 8.17 : does [lra] work again? *) rewrite <- (Rplus_opp_r (zoom sim)), <- Rminus_0_l. - unfold Rminus. apply Rplus_le_compat; try reflexivity; []. apply Rlt_le, zoom_pos. + unfold Rminus. apply Rplus_le_compat; try lra; []. apply Rlt_le, zoom_pos. Qed. (** To conclude that two similarities are equal, it is enough to show that they are equal on two points. *) -- GitLab