Merge pull request #40 from coq-community/fix-deprec

palmskog · web-flow · commit 861e53b8fc4c · 2023-10-15T20:15:11.000+02:00
fix arith deprecations
diff --git a/theories/DKA_Construction.v b/theories/DKA_Construction.v
@@ -249,7 +249,7 @@ Module Algebraic.
     rewrite mx_point_blocks11 by trivial.
     setoid_rewrite mx_point_blocks01 at 2; trivial.
     cbn.
-    rewrite 2minus_diag.
+    rewrite 2 Nat.sub_diag.
     set (U := mx_point 1 n 0 i (1: regex)).
     set (V := mx_point n 1 f 0 (1: regex)).
     set (Y := mx_point n 1 s 0 (a: regex)).
@@ -522,9 +522,10 @@ Module Correctness.
   Proof.
     intros i j n A Hi Hj [Hd He]. split; auto.
     intros s a t Hst. apply delta_add_var in Hst as [Hst|[-> [-> ->]]]; split; auto; simpl.
-     specialize (Hd _ _ _ Hst). destruct A. simpl. num_simpl. eapply lt_le_trans. apply Hd. apply Max.le_max_r.
+     specialize (Hd _ _ _ Hst). destruct A. simpl. num_simpl. eapply Nat.lt_le_trans.
+     apply Hd. apply Nat.le_max_r.
      specialize (Hd _ _ _ Hst). intuition.
-     destruct A. simpl. num_simpl. apply Max.le_max_l.
+     destruct A. simpl. num_simpl. apply Nat.le_max_l.
      destruct A. simpl. auto.
   Qed.
   #[local] Hint Resolve bounded_incr bounded_add_one bounded_add_var : core.
@@ -581,7 +582,7 @@ Module Correctness.
   Qed.
 
   Lemma leb_S: forall n, leb (S n) xH = false.
-  Proof. intros. case le_spec; intro H; trivial. num_simpl. elim (lt_n_O _ H). Qed.
+  Proof. intros. case le_spec; intro H; trivial. num_simpl. elim (Nat.nlt_0_r _ H). Qed.
   Hint Rewrite leb_S : bool_simpl.
 
   Lemma labelling_add_var : forall n A i j s t c, 
@@ -602,7 +603,7 @@ Module Correctness.
   Lemma psurj A: A = mk (size A) (epsilonmap A) (deltamap A) (max_label A).
   Proof. destruct A. reflexivity. Qed.
 
-  Opaque Max.max.
+  Opaque Nat.max.
   Lemma commute_add_var: forall n i f A, 
     bounded A -> belong i A -> belong f A ->
     Algebraic.add_var (nat_of_state i) (nat_of_state f) n (preNFA_to_preMAUT A)
@@ -612,14 +613,14 @@ Module Correctness.
     rewrite <- plus_assoc. apply plus_compat; trivial.
     fold (add_var i f n (mk (size A) (epsilonmap A) (deltamap A) (max_label A))).
     rewrite labelling_add_var.
-    rewrite (@labelling_crop (Max.max (Datatypes.S (nat_of_num n)) (max_label A))); auto with arith.
+    rewrite (@labelling_crop (Nat.max (Datatypes.S (nat_of_num n)) (max_label A))); auto with arith.
     setoid_rewrite eqb_eq_nat_bool. setoid_rewrite id_nat.
     unfold labelling. num_simpl.
     nat_analyse; simpl; fold_regex; try semiring_reflexivity. 
     num_analyse; simpl; fold_regex; try semiring_reflexivity. 
-    elim n0. clear. num_simpl. apply Max.le_max_l. 
+    elim n0. clear. num_simpl. apply Nat.le_max_l.
   Qed.
-  Transparent Max.max.
+  Transparent Nat.max.
 
   Lemma not_true_eq_false: forall b, ~ b = true -> b = false.
   Proof. intros [ ]; tauto. Qed.
@@ -927,7 +928,7 @@ Lemma build_max_label: forall a i e f A, i < max_label A -> i < max_label (build
 Proof.
   induction a; intros i e f A Hi; rewrite (psurj A); simpl; auto.
    rewrite max_label_add_one. auto.
-   num_simpl. eauto 2 using Max.le_max_r with arith.
+   num_simpl. eauto 2 using Nat.le_max_r with arith.
 Qed.
 
 Lemma collect_max_label: 
@@ -941,7 +942,7 @@ Proof.
    eapply IHa2 in Hi as [Hi|Hi]. left. apply build_max_label, Hi. auto. 
    rewrite max_label_add_one. auto. 
    revert Hi. NumSetProps.set_iff. intuition.
-   subst. left. destruct A; simpl. num_simpl. eauto using Max.le_max_l with arith.
+   subst. left. destruct A; simpl. num_simpl. eauto using Nat.le_max_l with arith.
 Qed.
 
 Lemma max_label_collect: 
@@ -958,7 +959,7 @@ Proof.
    eapply IHa2 in Hi as [[j ? ?]|Hi]. left. exists j; auto using collect_incr_2. right. assumption. 
    eapply IHa in Hi as [Hi|Hi]; auto.
    revert Hi. rewrite max_label_add_one, max_label_incr. auto. 
-   revert Hi. rewrite max_label_add_var. num_simpl. apply Max.max_case; auto.
+   revert Hi. rewrite max_label_add_var. num_simpl. apply Nat.max_case; auto.
    intro Hi. left. exists (nat_of_num p). auto with arith. num_simpl. auto with set.
 Qed.
 
@@ -981,8 +982,9 @@ Proof.
 
   clear. intros a b H. apply inf_leq. intros c Hc.
   apply max_label_collect in Hc as [[d ? Hd]|?]. 
-   rewrite H in Hd. eapply collect_max_label in Hd as [Hd|?].
-    eapply le_lt_trans. eassumption. unfold statesetelt_of_nat in Hd. rewrite id_nat in Hd. eassumption.
-    NumSetProps.setdec.
-    simpl in *. compute in H0. lia_false.
+  rewrite H in Hd. eapply collect_max_label in Hd as [Hd|?].
+  eapply Nat.le_lt_trans. eassumption. unfold statesetelt_of_nat in Hd.
+  rewrite id_nat in Hd. eassumption.
+  NumSetProps.setdec.
+  simpl in *. compute in H0. lia_false.
 Qed.
diff --git a/theories/DKA_DFA_Equiv.v b/theories/DKA_DFA_Equiv.v
@@ -389,11 +389,11 @@ Section correctness.
        constructor.
         intros l Hl. apply Htar. rewrite <- add_lists_S. apply Htar''. assumption. 
         apply (ci_sameclass Htar'').
-        transitivity tar''. apply Htar''. apply Htar.   
-        apply le_trans with (measure tar''). apply Htar. apply Htar''.
+        transitivity tar''. apply Htar''. apply Htar.
+        apply Nat.le_trans with (measure tar''). apply Htar. apply Htar''.
        apply Htar.
       apply Htar'', Hxy.
-      eapply le_lt_trans. apply Htar''. apply Hsize. 
+      eapply Nat.le_lt_trans. apply Htar''. apply Hsize. 
 
     clear IHn. intro Hr.
     destruct (IH _ Hr) as [IH1 IH2]; clear Hr IH. 
@@ -405,8 +405,8 @@ Section correctness.
      apply IH1. apply diag_ok; ti_auto. 
 
      transitivity (DS.union tarjan x y). apply DSUtils.le_union. apply IH1.
-     apply le_trans with (measure (DS.union tarjan x y)). 
-     apply IH1. apply (measure_union_strict (size:=size)) in Hn; auto using lt_le_weak; num_lia.
+     apply Nat.le_trans with (measure (DS.union tarjan x y)). 
+     apply IH1. apply (measure_union_strict (size:=size)) in Hn; auto using Nat.lt_le_incl; num_lia.
      apply IH1. apply in_union.
   Qed.
 
diff --git a/theories/DKA_DFA_Language.v b/theories/DKA_DFA_Language.v
@@ -99,12 +99,12 @@ Proof.
   - compute. firstorder.
     lia.
   - intros j. simpl. unfold lang_union. rewrite IHn. clear IHn. intuition. 
-    exists O; auto with arith. rewrite plus_comm. assumption.
+    exists O; auto with arith. rewrite Nat.add_comm. assumption.
     destruct H0 as [k ? ?]. exists (Datatypes.S k); auto with arith. rewrite <- plus_n_Sm. assumption.
     destruct H as [[|k] ? ?].
-    + left. rewrite plus_comm in H0. assumption.
+    + left. rewrite Nat.add_comm in H0. assumption.
     + right. exists k; auto with arith. rewrite <- plus_n_Sm in H0. assumption.
-Qed.   
+Qed.
 
 Lemma mx_leq_pointwise `{SL: SemiLattice}: forall n m A (M N: MX_ A n m), 
   M <== N <-> forall i j, i<n -> j<m -> !M i j <== !N i j.
diff --git a/theories/DKA_Merge.v b/theories/DKA_Merge.v
@@ -53,26 +53,24 @@ Definition compare_DFAs T (equiv: DFA.t -> state -> state -> option T) A B :=
 
 Lemma below_max_pi0: forall n m m', below n m -> below (pi0 n) (max (pi0 m) (pi1 m')).
 Proof.
-  intros. rewrite lt_nat_spec, max_spec. eapply lt_le_trans. 2: apply Max.le_max_l. 
+  intros. rewrite lt_nat_spec, max_spec. eapply Nat.lt_le_trans. 2: apply Nat.le_max_l.
   rewrite <- lt_nat_spec. apply lt_pi0. assumption.
 Qed.
 
 Lemma below_max_pi1: forall n m m', below n m' -> below (pi1 n) (max (pi0 m) (pi1 m')).
 Proof.
-  intros. rewrite lt_nat_spec, max_spec. eapply lt_le_trans. 2: apply Max.le_max_r. 
+  intros. rewrite lt_nat_spec, max_spec. eapply Nat.lt_le_trans. 2: apply Nat.le_max_r.
   rewrite <- lt_nat_spec. apply lt_pi1. assumption.
 Qed.
 
- 
-
 Lemma merge_bounded: forall A B, bounded A -> bounded B -> bounded (merge_DFAs A B).
 Proof.
   intros A B HA HB. constructor.
   intros a i. simpl. case_eq (pimatch i); intros p Hp.
    apply below_max_pi0. apply (bounded_delta HA). 
    apply below_max_pi1. apply (bounded_delta HB). 
-   rewrite lt_nat_spec. apply le_lt_trans with (nat_of_state (pi0 (delta A 0 0))).
-    apply le_O_n. rewrite <- lt_nat_spec. rapply below_max_pi0. apply (bounded_delta HA). 
+   rewrite lt_nat_spec. apply Nat.le_lt_trans with (nat_of_state (pi0 (delta A 0 0))).
+    apply Nat.le_0_l. rewrite <- lt_nat_spec. rapply below_max_pi0. apply (bounded_delta HA).
   unfold finaux, merge_DFAs.
   apply NumSetProps.Props.fold_rec_nodep. apply NumSetProps.Props.fold_rec_nodep.
    intro i. NumSetProps.setdec.
diff --git a/theories/Model_MinPlus.v b/theories/Model_MinPlus.v
@@ -85,14 +85,15 @@ Section protect.
   Instance mp_ConverseSemiRing: ConverseIdemSemiRing mp_Graph.
   Proof.
     constructor; simpl; eauto with typeclass_instances. 
-     destruct x; trivial. destruct y; trivial. destruct z; trivial. simpl. rewrite Plus.plus_assoc. reflexivity. 
+     destruct x; trivial. destruct y; trivial. destruct z; trivial. simpl.
+     rewrite Nat.add_assoc. reflexivity. 
      destruct x; reflexivity. 
-     destruct x; trivial. destruct y; trivial. simpl. rewrite plus_comm. reflexivity. 
+     destruct x; trivial. destruct y; trivial. simpl. rewrite Nat.add_comm. reflexivity. 
      destruct y; reflexivity.
      destruct x; trivial. destruct y; trivial. simpl. rewrite min_comm. reflexivity. 
      destruct y; reflexivity.
      destruct x; trivial. destruct y; trivial; destruct z; trivial. simpl. 
-     rewrite Min.plus_min_distr_r. reflexivity. 
+     rewrite Nat.add_min_distr_r. reflexivity. 
   Qed.
   
   Definition mp_IdemSemiRing: IdemSemiRing mp_Graph := Converse.CISR_ISR.  
diff --git a/theories/Monoid.v b/theories/Monoid.v
@@ -286,7 +286,7 @@ Section Props1.
     intros until n.
     rewrite <- (iter_once a) at 4.
     rewrite <- iter_split.
-    rewrite plus_comm.
+    rewrite Nat.add_comm.
     reflexivity.
   Qed.
   
diff --git a/theories/MxGraph.v b/theories/MxGraph.v
@@ -85,12 +85,12 @@ Ltac destruct_blocks :=
 Ltac mx_intros i j Hi Hj :=
   apply mx_equal'; intros i j Hi Hj;
   match type of Hi with
-    | i < 0%nat => elim (lt_n_O _ Hi)
+    | i < 0%nat => elim (Nat.nlt_0_r _ Hi)
     | i < 1%nat => destruct i; [clear Hi | elim (lt_n_1 Hi)]
     | _ => idtac
   end;
   match type of Hj with
-    | j < 0%nat => elim (lt_n_O _ Hj)
+    | j < 0%nat => elim (Nat.nlt_0_r _ Hj)
     | j < 1%nat => destruct j; [clear Hj | elim (lt_n_1 Hj)]
     | _ => idtac
   end.
diff --git a/theories/MxSemiRing.v b/theories/MxSemiRing.v
@@ -202,35 +202,35 @@ Section Props2.
   Proof.
     simpl. intros. destruct_blocks.
   
-    rewrite (plus_comm m), sum_cut. 
+    rewrite (Nat.add_comm m), sum_cut. 
     apply plus_compat.
     apply sum_compat; intros. 
     destruct_blocks. reflexivity. lia_false.
-    rewrite (plus_comm m), sum_shift. 
+    rewrite (Nat.add_comm m), sum_shift. 
     apply sum_compat; intros.
     destruct_blocks. reflexivity.
 
-    rewrite (plus_comm m), sum_cut. 
+    rewrite (Nat.add_comm m), sum_cut. 
     apply plus_compat.
     apply sum_compat; intros. 
     destruct_blocks. reflexivity. lia_false.
-    rewrite (plus_comm m), sum_shift. 
+    rewrite (Nat.add_comm m), sum_shift. 
     apply sum_compat; intros.
     destruct_blocks. reflexivity.
 
-    rewrite (plus_comm m), sum_cut. 
+    rewrite (Nat.add_comm m), sum_cut. 
     apply plus_compat.
     apply sum_compat; intros. 
     destruct_blocks. reflexivity. lia_false.
-    rewrite (plus_comm m), sum_shift. 
+    rewrite (Nat.add_comm m), sum_shift. 
     apply sum_compat; intros.
     destruct_blocks. reflexivity.
 
-    rewrite (plus_comm m), sum_cut. 
+    rewrite (Nat.add_comm m), sum_cut. 
     apply plus_compat.
     apply sum_compat; intros. 
     destruct_blocks. reflexivity. lia_false.
-    rewrite (plus_comm m), sum_shift. 
+    rewrite (Nat.add_comm m), sum_shift. 
     apply sum_compat; intros.
     destruct_blocks. reflexivity.
   Qed.
diff --git a/theories/Numbers.v b/theories/Numbers.v
@@ -82,7 +82,7 @@ Module Type NUM.
 
   (* specification of operations and predicates, w.r.t. nat *)
   Axiom S_nat_spec : forall n, nat_of_num (S n) = Datatypes.S (nat_of_num n).
-  Axiom max_spec : forall n m, nat_of_num (max n m) = Max.max (nat_of_num n) (nat_of_num m).
+  Axiom max_spec : forall n m, nat_of_num (max n m) = Nat.max (nat_of_num n) (nat_of_num m).
   Axiom le_nat_spec : forall n m, n <= m <-> (nat_of_num n <= nat_of_num m)%nat.
   Axiom lt_nat_spec : forall n m, n <  m <-> (nat_of_num n <  nat_of_num m)%nat.
 
@@ -136,12 +136,12 @@ Module NumUtils (N : NUM).
   Proof.
     constructor.
     intros x; unfold Pos.le. rewrite le_nat_spec. auto with arith.
-    intros x y z Hxy Hyz. rewrite le_nat_spec in *. apply (le_trans _ (nat_of_num y)); auto. 
+    intros x y z Hxy Hyz. rewrite le_nat_spec in *. apply (Nat.le_trans _ (nat_of_num y)); auto. 
   Qed.
 
   #[global] Instance lt_transitive: Transitive lt.
   Proof.
-    intros x y z Hxy Hyz. rewrite lt_nat_spec in *. apply (lt_trans _ (nat_of_num y)); auto. 
+    intros x y z Hxy Hyz. rewrite lt_nat_spec in *. apply (Nat.lt_trans _ (nat_of_num y)); auto. 
   Qed.
 
   Lemma num_peano_rec : 
@@ -431,12 +431,12 @@ Module Positive <: NUM.
     lia.
   Qed.
 
-  Lemma max_spec : forall n m, nat_of_num (max n m) = Max.max (nat_of_num n) (nat_of_num m).
+  Lemma max_spec : forall n m, nat_of_num (max n m) = Nat.max (nat_of_num n) (nat_of_num m).
   Proof.
     intros n m. unfold max, Pos.max. fold (compare n m). destruct (compare_spec n m).
-     rewrite Max.max_r; trivial. apply lt_le_weak. rewrite <- lt_nat_spec. assumption.
-     subst. rewrite Max.max_r; trivial. 
-     rewrite Max.max_l; trivial. apply lt_le_weak. rewrite <- lt_nat_spec. assumption.
+     rewrite Nat.max_r; trivial. apply Nat.lt_le_incl. rewrite <- lt_nat_spec. assumption.
+     subst. rewrite Nat.max_r; trivial. 
+     rewrite Nat.max_l; trivial. apply Nat.lt_le_incl. rewrite <- lt_nat_spec. assumption.
   Qed.
 
 
diff --git a/theories/SemiLattice.v b/theories/SemiLattice.v
@@ -183,7 +183,7 @@ Section FSumDef.
     sum i (S k) f == sum i k f + f (i+k)%nat.
   Proof. 
     revert i; induction k; intro i.
-    simpl. rewrite plus_0_r; apply plus_com.
+    simpl. rewrite Nat.add_0_r; apply plus_com.
     change (sum i (S (S k)) f) with (f i + sum (S i) (S k) f).
     rewrite IHk, plus_assoc. simpl. auto with compat.
   Qed.
diff --git a/theories/SemiRing.v b/theories/SemiRing.v
@@ -317,7 +317,7 @@ endtests*)
         (plus (VLSet_to_X b) (dot (VLst_to_X a) y))
         (VLSet_to_X (norm_aux' n b a y)))%nat.
     Proof.
-      induction n; split; intros; try elim (lt_n_O _ H); 
+      induction n; split; intros; try elim (Nat.nlt_0_r _ H); 
         destruct IHn as [IHnorm_aux IHnorm_aux'].
   
       (* norm_aux *)
