Merge #394

394: Adapt to coq/coq#18164 r=Janno a=Villetaneuse

We want to remove deprecated Arith files.

Co-authored-by: Pierre Rousselin <rousselin@math.univ-paris13.fr>

examples/basics_tutorial.v

@@ -47,12 +47,12 @@ Import M.notations.
 (** In addition, we import a couple of modules from the standard
 library that we are going to use in some examples. *)
 
-Require Import Arith.Arith Arith.Div2.
+Require Import Arith.Arith.
 Require Import Lists.List.
 Require Import Strings.String.
 
 Set Implicit Arguments.
-Notation "x == y" := (beq_nat x y) (at level 60).
+Notation "x == y" := (Nat.eqb x y) (at level 60).
 
 (** We start by showing the standard _unit_ and _bind_ operators,
 which in our language are called [ret] (for return) and [bind]. The
@@ -204,7 +204,7 @@ Definition collatz :=
       if n == 1 then
         ret nil
       else if is_even n then
-        f (div2 n)
+        f (Nat.div2 n)
       else
         f (3 * n + 1)
     in
@@ -668,12 +668,11 @@ Program Definition eq_nats  :=
       ret _
     end.
 Next Obligation.
-  symmetry.
-  apply beq_nat_refl.
+  apply Nat.eqb_refl.
 Qed.
 Next Obligation.
-  rewrite beq_nat_true_iff.
-  apply plus_comm.
+  rewrite Nat.eqb_eq.
+  apply Nat.add_comm.
 Qed.
 (** Notice how we use the [[H]] notation after the right arrow in the
 pattern. The name [H] will be instantiated with a proof of equality of

tests/ConstrSelector.v

@@ -44,7 +44,7 @@ Definition total_map (A:Type) := id -> A.
 
 Definition beq_id id1 id2 :=
   match id1,id2 with
-    | Id n1, Id n2 => beq_nat n1 n2
+    | Id n1, Id n2 => Nat.eqb n1 n2
   end.
 
 Definition t_update {A:Type} (m : total_map A)
@@ -82,7 +82,7 @@ Fixpoint beval (st : state) (b : bexp) : bool :=
   match b with
   | BTrue       => true
   | BFalse      => false
-  | BEq a1 a2   => beq_nat (aeval st a1) (aeval st a2)
+  | BEq a1 a2   => Nat.eqb (aeval st a1) (aeval st a2)
   | BLe a1 a2   => leb (aeval st a1) (aeval st a2)
   | BNot b1     => negb (beval st b1)
   | BAnd b1 b2  => andb (beval st b1) (beval st b2)

tests/comptactics.v

@@ -29,35 +29,35 @@ Abort.
 
 Require Import Arith.
 
-Example exif (x : nat) : if beq_nat (S x) 1 then x = 0 : Type else True.
+Example exif (x : nat) : if Nat.eqb (S x) 1 then x = 0 : Type else True.
 MProof.
-variabilize (beq_nat (S x) (S 0)) as t.
-assert (B:t = beq_nat (S x) 1).
+variabilize (Nat.eqb (S x) (S 0)) as t.
+assert (B:t = Nat.eqb (S x) 1).
 reflexivity.
 Abort.
 
 Definition sillyfun (n : nat) : bool :=
-  if beq_nat n 3 then false
-  else if beq_nat n 5 then false
+  if Nat.eqb n 3 then false
+  else if Nat.eqb n 5 then false
   else false.
 
 Theorem sillyfun_false : forall (n : nat),
   (sillyfun n = false) : Type.
 MProof.
   intros n. unfold sillyfun.
-  variabilize (beq_nat n 3) as t3.
+  variabilize (Nat.eqb n 3) as t3.
   destruct t3.
   simpl. reflexivity.
   simpl.
-  variabilize (beq_nat _ _) as t5.
+  variabilize (Nat.eqb _ _) as t5.
   destruct t5 &> reflexivity.
 Qed.
 
 
 
 Definition sillyfun1 (n : nat) : bool :=
-  if beq_nat n 3 then true
-  else if beq_nat n 5 then true
+  if Nat.eqb n 3 then true
+  else if Nat.eqb n 5 then true
   else false.
 
 Fixpoint evenb (n:nat) : bool :=
@@ -74,7 +74,7 @@ Theorem sillyfun1_odd : forall (n : nat),
      oddb n = true) : Type .
 MProof.
   intros n. unfold sillyfun1.
-  variabilize (beq_nat n 3) as t.
+  variabilize (Nat.eqb n 3) as t.
   assert (Heqe3 : t = (n =? 3)%nat) |1> reflexivity.
   move_back Heqe3.
   destruct t &> intro Heqe3.

tests/declare.v

@@ -79,18 +79,22 @@ Compute ltac:(mrun alrdecl).
 
 Print NAT4. (* definitions before the failing one are declared. *)
 
+(* NOTE: We give a unidirectional version of Nat.succ_le_mono for compatibility. *)
+Lemma succ_le_mono_lr (n m : nat) : n <= m -> S n <= S m.
+Proof. now apply ->PeanoNat.Nat.succ_le_mono. Qed.
+
 (* we should check that the terms are closed w.r.t. section variables *)
 (* JANNO: for now we just raise an catchable exception. *)
 Fail Compute fun x y =>
           ltac:(mrun (
                     mtry
-                      M.declare dok_Definition "lenS" true (Le.le_n_S x y);; M.ret tt
+                      M.declare dok_Definition "lenS" true (succ_le_mono_lr x y);; M.ret tt
                       with | UnboundVar => M.failwith "This must fail" | _ => M.ret tt end
                )).
 
 (* This used to fail because of weird universe issues. *)
-Compute ltac:(mrun (c <- M.declare dok_Definition "blu" true (Le.le_n_S); M.print_term c)).
-Definition decl_blu := (c <- M.declare dok_Definition "blu" true (Le.le_n_S); M.print_term c).
+Compute ltac:(mrun (c <- M.declare dok_Definition "blu" true (succ_le_mono_lr); M.print_term c)).
+Definition decl_blu := (c <- M.declare dok_Definition "blu" true (succ_le_mono_lr); M.print_term c).
 (* This now fails because the previous failure no longer exists and [blu] is declared. *)
 Fail Compute ltac:(mrun decl_blu).
 

tests/destruct_eq.v

@@ -1,16 +1,16 @@
 From Mtac2 Require Import Mtac2 CompoundTactics.
 From Coq.Arith Require Import Arith.
 
-Example beq_nat_ex : forall n, if beq_nat n 3 then True else True.
+Example beq_nat_ex : forall n, if (Nat.eqb n 3) then True else True.
 MProof.
   intros n.
-  CT.destruct_eq (beq_nat _ _).
+  CT.destruct_eq (Nat.eqb _ _).
   - simpl. intro H. T.exact I.
   - simpl. intro H. T.exact I.
 Qed.
 
-Example beq_nat_ex_comp : forall n, if beq_nat n 3 then True else True.
+Example beq_nat_ex_comp : forall n, if (Nat.eqb n 3) then True else True.
 MProof.
   intros n.
-  CT.destruct_eq (beq_nat _ _) &> simpl &> intros &> T.exact I.
+  CT.destruct_eq (Nat.eqb _ _) &> simpl &> intros &> T.exact I.
 Qed.

tests/hugo.v

@@ -11,12 +11,16 @@ Require Import Lia.
 
 Lemma lt_0_S n : 0 < S n. Proof. lia. Qed.
 
+(* NOTE: unidirectional version of Nat.succ_lt_mono for compatibility. *)
+Lemma succ_lt_mono_lr (n m : nat) : n < m -> S n < S m.
+Proof. now intros H; apply ->PeanoNat.Nat.succ_lt_mono. Qed.
+
 Fixpoint prove_leq n m : M (n < m) :=
   match n, m with
   | 0, S _ => M.ret (lt_0_S _)
   | S n', S m' =>
     H <- prove_leq n' m';
-    M.ret (Lt.lt_n_S _ _ H)
+    M.ret (succ_lt_mono_lr _ _ H)
   | _, _ => M.failwith "n not < m"
   end.
 

tests/mctacticstests.v

@@ -268,14 +268,14 @@ Qed.
 Example apply_tactic (a b : nat) : a > b -> S a > S b.
 MProof.
   intro H.
-  apply Gt.gt_n_S.
+  apply (proj1 (PeanoNat.Nat.succ_lt_mono b a)).
   assumption.
 Qed.
 
 Example apply_tactic_fail (a b : nat) : a > b -> S a > b.
 MProof.
   intro H.
-  Fail apply Gt.gt_n_S.
+  Fail apply (proj1 (PeanoNat.Nat.succ_lt_mono b a)).
 Abort.
 
 Goal forall b1 b2 b3 : bool, andb b1 (andb b2 b3) = andb b1 (andb b2 b3).