Adapt w.r.t coq/coq#18164 (#130)

This prepares the removal of some files which are deprecated in 8.16.

src/Conversion_tactics.v

@@ -408,7 +408,6 @@ Module N_convert_mod := convert N_convert_type.
 Ltac N_convert := N_convert_mod.convert.
 
 (* Instanciation for the type [nat] *)
-Require Import NPeano.
 Module nat_convert_type <: convert_type.
 
 Definition T : Type := nat.

src/SMT_terms.v

@@ -865,13 +865,13 @@ Module Atom.
     intros [ | | | | | s1 n1 | s1 | s1 | s1 | s1 | s1 ] [ | | | | |s2 n2 | s2 | s2 | s2 | s2 | s2 ];simpl; try constructor;trivial; try discriminate.
     - apply iff_reflect. case_eq (Nat.eqb n1 n2).
       + case_eq ((s1 =? s2)%N).
-        * rewrite N.eqb_eq, beq_nat_true_iff.
+        * rewrite N.eqb_eq, Nat.eqb_eq.
           intros -> ->. split; reflexivity.
-        * rewrite N.eqb_neq, beq_nat_true_iff.
+        * rewrite N.eqb_neq, Nat.eqb_eq.
           intros H1 ->; split; try discriminate.
           intro H. inversion H. elim H1. auto.
       + split; auto.
-        * rewrite beq_nat_false_iff in H. intros. contradict H0.
+        * rewrite Nat.eqb_neq in H. intros. contradict H0.
           intro H'. apply H. inversion H'. reflexivity.
         *  intros. contradict H0. easy.
     - apply iff_reflect. rewrite N.eqb_eq. split; intro H.

src/bva/BVList.v

@@ -10,7 +10,7 @@
 (**************************************************************************)
 
 
-Require Import List Bool NArith Psatz Uint63 Nnat ZArith.
+Require Import List Bool NArith Psatz Uint63 Nnat ZArith PeanoNat.
 Require Import Misc.
 Require Import ProofIrrelevance.
 Import ListNotations.
@@ -2376,7 +2376,7 @@ Qed.
     intros. unfold bv_zextn, zextend, size in *.
     rewrite <- N2Nat.id. apply f_equal. 
     specialize (@length_extend a (nat_of_N i) false). intros.
-    rewrite H0. rewrite plus_distr. rewrite plus_comm.
+    rewrite H0. rewrite plus_distr. rewrite Nat.add_comm.
     apply f_equal.
     apply (f_equal (N.to_nat)) in H.
     now rewrite Nat2N.id in H.
@@ -2393,7 +2393,7 @@ Qed.
     lia.
     intros.
     specialize (@length_extend a (nat_of_N i) b). intros.
-    subst. rewrite plus_distr. rewrite plus_comm.
+    subst. rewrite plus_distr. rewrite Nat.add_comm.
     rewrite Nat2N.id.
     now rewrite <- H1.
   Qed.

src/lia/Lia.v

@@ -542,7 +542,7 @@ Section certif.
       destruct (Atom.reflect_eqb h a);subst.
       intros Heq1;inversion Heq1;clear Heq1;subst;lia.
       intros Heq1;apply IHlvm in Heq1;trivial.
-      apply lt_trans with (1:= Heq1);lia.
+      apply Nat.lt_trans with (1:= Heq1);lia.
     Qed.
 
     Lemma build_pexpr_atom_aux_correct_z :
@@ -603,7 +603,7 @@ Section certif.
        assert (W2:=nat_of_P_pos (Pos.pred pvm)).
        lia.
        rewrite Plt_lt.
-       apply lt_trans with (1:= W1);lia.
+       apply Nat.lt_trans with (1:= W1);lia.
      rewrite H3;simpl;apply IHlvm;trivial.
      intros _ Heq;inversion Heq;clear Heq;subst;unfold wf_vmap;
        simpl;intros (Hwf1, Hwf2);repeat split;simpl.
@@ -725,9 +725,9 @@ Transparent interp_aux.
      assert (W:= IH' _ _ Hlt2 H0 (refl_equal _) H1);clear IH'.
      decompose [and] W;clear W.
      destruct H5;repeat split;trivial.
-     apply le_trans with (1:= H3);trivial.
+     apply Nat.le_trans with (1:= H3);trivial.
      intros p Hlt;rewrite H2, H7;trivial.
-     apply lt_le_trans with (1:=Hlt);trivial.
+     apply Nat.lt_le_trans with (1:=Hlt);trivial.
      simpl;rewrite H9, andb_true_r.
      apply (bounded_pexpr_le (fst vm0));auto with arith.
      simpl;rewrite H6, H11;simpl.
@@ -744,9 +744,9 @@ Transparent interp_aux.
      assert (W:= IH' _ _ Hlt2 H0 (refl_equal _) H1);clear IH'.
      decompose [and] W;clear W.
      destruct H5;repeat split;trivial.
-     apply le_trans with (1:= H3);trivial.
+     apply Nat.le_trans with (1:= H3);trivial.
      intros p Hlt;rewrite H2, H7;trivial.
-     apply lt_le_trans with (1:=Hlt);trivial.
+     apply Nat.lt_le_trans with (1:=Hlt);trivial.
      simpl;rewrite H9, andb_true_r.
      apply (bounded_pexpr_le (fst vm0));auto with arith.
      simpl;rewrite H6, H11;simpl.
@@ -763,9 +763,9 @@ Transparent interp_aux.
      assert (W:= IH' _ _ Hlt2 H0 (refl_equal _) H1);clear IH'.
      decompose [and] W;clear W.
      destruct H5;repeat split;trivial.
-     apply le_trans with (1:= H3);trivial.
+     apply Nat.le_trans with (1:= H3);trivial.
      intros p Hlt;rewrite H2, H7;trivial.
-     apply lt_le_trans with (1:=Hlt);trivial.
+     apply Nat.lt_le_trans with (1:=Hlt);trivial.
      simpl;rewrite H9, andb_true_r.
      apply (bounded_pexpr_le (fst vm0));auto with arith.
      simpl;rewrite H6, H11;simpl.
@@ -829,9 +829,9 @@ Transparent interp_aux.
      assert (W:= IH' _ _ H0 (refl_equal _) H1);clear IH'.
      decompose [and] W;clear W.
      destruct H5;repeat split;trivial.
-     apply le_trans with (1:= H3);trivial.
+     apply Nat.le_trans with (1:= H3);trivial.
      intros p Hlt;rewrite H2, H7;trivial.
-     apply lt_le_trans with (1:=Hlt);trivial.
+     apply Nat.lt_le_trans with (1:=Hlt);trivial.
      simpl;rewrite H9, andb_true_r.
      apply (bounded_pexpr_le (fst vm0));auto with arith.
      simpl;rewrite H6, H11;simpl.
@@ -849,9 +849,9 @@ Transparent interp_aux.
      assert (W:= IH' _ _ H0 (refl_equal _) H1);clear IH'.
      decompose [and] W;clear W.
      destruct H5;repeat split;trivial.
-     apply le_trans with (1:= H3);trivial.
+     apply Nat.le_trans with (1:= H3);trivial.
      intros p Hlt;rewrite H2, H7;trivial.
-     apply lt_le_trans with (1:=Hlt);trivial.
+     apply Nat.lt_le_trans with (1:=Hlt);trivial.
      simpl;rewrite H9, andb_true_r.
      apply (bounded_pexpr_le (fst vm0));auto with arith.
      simpl;rewrite H6, H11;simpl.
@@ -869,9 +869,9 @@ Transparent interp_aux.
      assert (W:= IH' _ _ H0 (refl_equal _) H1);clear IH'.
      decompose [and] W;clear W.
      destruct H5;repeat split;trivial.
-     apply le_trans with (1:= H3);trivial.
+     apply Nat.le_trans with (1:= H3);trivial.
      intros p Hlt;rewrite H2, H7;trivial.
-     apply lt_le_trans with (1:=Hlt);trivial.
+     apply Nat.lt_le_trans with (1:=Hlt);trivial.
      simpl;rewrite H9, andb_true_r.
      apply (bounded_pexpr_le (fst vm0));auto with arith.
      simpl;rewrite H6, H11;simpl.
@@ -1001,10 +1001,10 @@ Transparent build_z_atom.
       assert (W1:= build_pexpr_correct _ _ _ _ H1 Heq2 H).
       decompose [and] W1;clear W1.
       split;trivial.
-      split;[ apply le_trans with (1:= H4);trivial | ].
+      split;[ apply Nat.le_trans with (1:= H4);trivial | ].
       split.
        intros p Hlt;rewrite H0, H8;trivial.
-       apply lt_le_trans with (1:= Hlt);trivial.
+       apply Nat.lt_le_trans with (1:= Hlt);trivial.
       split.
        unfold bounded_formula;simpl;rewrite H10, andb_true_r.
        apply (bounded_pexpr_le (fst vm0));auto with arith.
@@ -1386,10 +1386,10 @@ Transparent build_z_atom.
       assert (W:= IHcl _ _ _ Heq2 H);decompose [and] W;clear W.
       split;trivial.
       split.
-       apply le_trans with (1:= H1);trivial.
+       apply Nat.le_trans with (1:= H1);trivial.
       split.
         intros p Hlt;rewrite H0, H5;trivial.
-        apply lt_le_trans with (1:= Hlt);trivial.
+        apply Nat.lt_le_trans with (1:= Hlt);trivial.
       split.
        simpl;rewrite H7, andb_true_r.
        apply bounded_bformula_le with (2:= H2);trivial.

src/spl/Syntactic.v

@@ -131,7 +131,7 @@ Section CheckAtom.
       unfold apply_unop; destruct (t_interp t_i t_func t_atom .[ i]) as [A v]; 
       destruct (Typ.cast A Typ.Tpositive) as [k| ]; auto.
 
-      intros n m n1 m2. simpl. unfold is_true. rewrite !andb_true_iff, beq_nat_true_iff, N.eqb_eq. intros [[-> ->] H]. rewrite (check_hatom_correct _ _ H); auto.
+      intros n m n1 m2. simpl. unfold is_true. rewrite !andb_true_iff, Nat.eqb_eq, N.eqb_eq. intros [[-> ->] H]. rewrite (check_hatom_correct _ _ H); auto.
       intros n m. simpl. unfold is_true. rewrite andb_true_iff, N.eqb_eq. intros [-> H]. rewrite (check_hatom_correct _ _ H); auto.
       intros n m. simpl. unfold is_true. rewrite andb_true_iff, N.eqb_eq. intros [-> H]. rewrite (check_hatom_correct _ _ H); auto.
       (* bv_extr *)