Adapt to coq/coq#18164 (#103)

Bedrock/Word.v

@@ -2,7 +2,6 @@ Require Export Fiat.Common.Coq__8_4__8_5__Compat.
 (** Fixed precision machine words *)
 
 Require Import Coq.Arith.Arith
-        Coq.Arith.Div2
         Coq.NArith.NArith
         Coq.Bool.Bool
         Coq.ZArith.ZArith.

src/ADTRefinement/FixedPoint.v

@@ -1,6 +1,8 @@
 Require Export Fiat.Common.Coq__8_4__8_5__Compat.
 Require Import Fiat.ADT Fiat.ADTNotation.
 Require Export Fiat.Computation.FixComp.
+Require Import Coq.ZArith.ZArith.
+Require Import Coq.Arith.PeanoNat.
 
 Import LeastFixedPointFun.
 
@@ -113,9 +115,8 @@ Lemma length_wf' : forall A len l,
 Proof.
   induction len; simpl; intros;
     constructor; intros.
-  contradiction (NPeano.Nat.nlt_0_r _ H).
+  contradiction (Nat.nlt_0_r _ H).
   apply IHlen.
-  Require Import Coq.ZArith.ZArith.
   omega.
 Qed.
 

src/CertifiedExtraction/Extraction/External/Lists.v

@@ -5,7 +5,7 @@ Require Export Bedrock.Platform.Facade.examples.QsADTs.
 Lemma CompileEmpty_helper {A}:
   forall (lst : list A) (w : W),
     Programming.propToWord (lst = @nil A) w ->
-    ret (bool2w (EqNat.beq_nat (Datatypes.length lst) 0)) ↝ w.
+    ret (bool2w (Nat.eqb (Datatypes.length lst) 0)) ↝ w.
 Proof.
   unfold Programming.propToWord, IF_then_else in *.
   destruct lst; simpl in *; destruct 1; repeat cleanup; try discriminate; fiat_t.
@@ -15,7 +15,7 @@ Hint Resolve CompileEmpty_helper : call_helpers_db.
 
 Lemma ListEmpty_helper :
   forall {A} (seq: list A),
-    (EqNat.beq_nat (Datatypes.length seq) 0) = match seq with
+    (Nat.eqb (Datatypes.length seq) 0) = match seq with
                                                | nil => true
                                                | _ :: _ => false
                                                end.

src/CertifiedExtraction/Extraction/QueryStructures/CallRules/TupleList.v

@@ -123,7 +123,7 @@ Module ADTListCompilation
       GLabelMap.MapsTo fpointer (Axiomatic Empty) env ->
       {{ tenv }}
         Call vtest fpointer (vlst :: nil)
-      {{ [[`vtest ->> (bool2w (EqNat.beq_nat (Datatypes.length lst) 0)) as _]] :: (DropName vtest tenv) }} ∪ {{ ext }} // env.
+      {{ [[`vtest ->> (bool2w (Nat.eqb (Datatypes.length lst) 0)) as _]] :: (DropName vtest tenv) }} ∪ {{ ext }} // env.
   Proof.
     repeat (SameValues_Facade_t_step || facade_cleanup_call || LiftPropertyToTelescope_t || PreconditionSet_t || injections).
 
@@ -144,7 +144,7 @@ Module ADTListCompilation
       GLabelMap.MapsTo fpointer (Axiomatic Empty) env ->
       {{ tenv }}
         Call vtest fpointer (vlst :: nil)
-      {{ [[`vtest ->> (bool2w (EqNat.beq_nat (Datatypes.length (rev lst)) 0)) as _]] :: tenv }} ∪ {{ ext }} // env.
+      {{ [[`vtest ->> (bool2w (Nat.eqb (Datatypes.length (rev lst)) 0)) as _]] :: tenv }} ∪ {{ ext }} // env.
   Proof.
     intros.
     setoid_rewrite rev_length.

src/CertifiedExtraction/Extraction/QueryStructures/QueryStructures.v

@@ -154,7 +154,7 @@ Ltac _compile_length :=
   match_ProgOk
     ltac:(fun prog pre post ext env =>
             match constr:((pre, post)) with
-            | (?pre, Cons ?k (ret (bool2w (EqNat.beq_nat (Datatypes.length (rev ?seq)) 0))) (fun _ => ?pre')) =>
+            | (?pre, Cons ?k (ret (bool2w (Nat.eqb (Datatypes.length (rev ?seq)) 0))) (fun _ => ?pre')) =>
               let vlst := find_fast (wrap (FacadeWrapper := WrapInstance (H := QS_WrapFiatWTupleList)) seq) ext in
               match vlst with
               | Some ?vlst => eapply (WTupleListCompilation.CompileEmpty_spec (idx := 3) (vlst := vlst))

src/Common.v

@@ -1,5 +1,4 @@
 Require Import Coq.Lists.List.
-Require Import Coq.Numbers.Natural.Peano.NPeano.
 Require Import Coq.ZArith.ZArith Coq.Lists.SetoidList.
 Require Export Coq.Setoids.Setoid Coq.Classes.RelationClasses
         Coq.Program.Program Coq.Classes.Morphisms.
@@ -1330,7 +1329,7 @@ Definition path_prod' {A B} {x x' : A} {y y' : B}
 
 Lemma lt_irrefl' {n m} (H : n = m) : ~n < m.
 Proof.
-  subst; apply Lt.lt_irrefl.
+  subst; apply Nat.lt_irrefl.
 Qed.
 
 Lemma or_not_l {A B} (H : A \/ B) (H' : ~A) : B.
@@ -1627,7 +1626,7 @@ Module opt.
   Definition snd {A B} := Eval compute in @snd A B.
   Definition andb := Eval compute in andb.
   Definition orb := Eval compute in orb.
-  Definition beq_nat := Eval compute in EqNat.beq_nat.
+  Definition beq_nat := Eval compute in Nat.eqb.
 
   Module Export Notations.
     Delimit Scope opt_bool_scope with opt_bool.
@@ -1641,7 +1640,7 @@ Module opt2.
   Definition snd {A B} := Eval compute in @snd A B.
   Definition andb := Eval compute in andb.
   Definition orb := Eval compute in orb.
-  Definition beq_nat := Eval compute in EqNat.beq_nat.
+  Definition beq_nat := Eval compute in Nat.eqb.
   Definition leb := Eval compute in Compare_dec.leb.
 
   Module Export Notations.

src/Common/BoundedLookup.v

@@ -141,7 +141,7 @@ Section BoundedIndex.
 
     Fixpoint fin_beq {m n} (p : Fin.t m) (q : Fin.t n) :=
       match p, q with
-      | @Fin.F1 m', @Fin.F1 n' => EqNat.beq_nat m' n'
+      | @Fin.F1 m', @Fin.F1 n' => Nat.eqb m' n'
       | Fin.FS _ _, Fin.F1 _ => false
       | Fin.F1 _, Fin.FS _ _ => false
       | Fin.FS _ p', Fin.FS _ q' => fin_beq p' q'
@@ -153,7 +153,7 @@ Section BoundedIndex.
     Proof.
       intros; pattern n, p, q; eapply Fin.rect2; simpl;
         intuition; try (congruence || discriminate).
-      - symmetry; eapply beq_nat_refl.
+      - eapply Nat.eqb_refl.
       - eauto using Fin.FS_inj.
     Qed.
 

src/Common/Enumerable.v

@@ -20,7 +20,7 @@ Section enum.
 
   Definition enumerate_fun_beq (enumerate : list A) (f g : A -> B)
   : bool
-    := EqNat.beq_nat (List.length (List.filter (fun x => negb (beq (f x) (g x))) enumerate)) 0.
+    := Nat.eqb (List.length (List.filter (fun x => negb (beq (f x) (g x))) enumerate)) 0.
 
   Definition enumerate_fun_bl_in
              (bl : forall x y, beq x y = true -> x = y)
@@ -29,7 +29,7 @@ Section enum.
   Proof.
     unfold enumerate_fun_beq.
     intros H x H'.
-    apply EqNat.beq_nat_true in H.
+    apply Nat.eqb_eq in H.
     apply bl.
     destruct (beq (f x) (g x)) eqn:Heq; [ reflexivity | exfalso ].
     apply Bool.negb_true_iff in Heq.

src/Common/Equality.v

@@ -1,5 +1,6 @@
 Require Import Coq.Lists.List Coq.Lists.SetoidList.
 Require Import Coq.Bool.Bool.
+Require Import Coq.Arith.PeanoNat.
 Require Import Coq.Strings.Ascii.
 Require Import Coq.Strings.String.
 Require Import Coq.Logic.Eqdep_dec.
@@ -379,10 +380,10 @@ Definition internal_prod_dec_lb {A B} eq_A eq_B A_lb B_lb x y
              H
              (surjective_pairing _))).
 
-Global Instance nat_BoolDecR : BoolDecR nat := EqNat.beq_nat.
-Global Instance nat_BoolDec_bl : BoolDec_bl (@eq nat) := @EqNat.beq_nat_true.
+Global Instance nat_BoolDecR : BoolDecR nat := Nat.eqb.
+Global Instance nat_BoolDec_bl : BoolDec_bl (@eq nat) := fun n m => (proj1 (Nat.eqb_eq n m)).
 Global Instance nat_BoolDec_lb : BoolDec_lb (@eq nat) :=
-  fun x y => proj2 (@EqNat.beq_nat_true_iff x y).
+  fun x y => proj2 (@Nat.eqb_eq x y).
 
 Lemma unit_bl {x y} : unit_beq x y = true -> x = y.
 Proof. apply internal_unit_dec_bl. Qed.

src/Common/FixedPoints.v

@@ -62,7 +62,7 @@ Section fixedpoints.
              | _ => omega
              | [ H : forall a, _ -> _ = _ |- _ ] => rewrite H by omega
              | [ H : _ < _ |- _ ] => hnf in H
-             | [ H : S _ <= S _ |- _ ] => apply Le.le_S_n in H
+             | [ H : S _ <= S _ |- _ ] => apply Nat.succ_le_mono in H
              | [ H : sizeof ?x <= ?y, H' : ?y <= sizeof (step ?x) |- _ ]
                => let H'' := fresh in
                   assert (H'' : sizeof (step x) <= sizeof x) by apply step_monotonic;
@@ -95,7 +95,7 @@ Section listpair.
   Lemma step_monotonic lss : sizeof_pair (step lss) <= sizeof_pair lss.
   Proof.
     unfold step, sizeof_pair; simpl;
-      apply Plus.plus_le_compat;
+      apply Nat.add_le_mono;
       apply length_filter.
   Qed.
 

src/Common/Frame.v

@@ -1,7 +1,7 @@
 Require Import
         SetoidClass
-        Coq.Arith.Max
-        Coq.Classes.Morphisms.
+        Coq.Classes.Morphisms
+        Coq.Arith.PeanoNat.
 Require Export Fiat.Common.Coq__8_4__8_5__Compat.
 
 Generalizable All Variables.
@@ -212,7 +212,7 @@ Module PreO.
   Qed.
 
   Definition Nat : t le.
-  Proof. constructor; [ apply Le.le_refl | apply Le.le_trans ].
+  Proof. constructor; [ apply Nat.le_refl | apply Nat.le_trans ].
   Qed.
 
   Definition discrete (A : Type) : t (@Logic.eq A).
@@ -408,7 +408,7 @@ Module PO.
     constructor; intros.
     - apply PreO.Nat.
     - solve_proper.
-    - apply Le.le_antisym; assumption.
+    - apply Nat.le_antisymm; assumption.
   Qed.
 
   Definition discrete (A : Type) : t (@Logic.eq A) Logic.eq.
@@ -585,8 +585,8 @@ Module JoinLat.
   Proof. constructor; intros.
          - apply PO.Nat.
          - solve_proper.
-         - constructor. simpl. apply Max.le_max_l. apply Max.le_max_r.
-           apply Max.max_lub.
+         - constructor. simpl. apply Nat.le_max_l. apply Nat.le_max_r.
+           apply Nat.max_lub.
   Qed.
 
   (** Max for propositions is the propositional OR, i.e., disjunction *)

src/Common/Le.v

@@ -1,6 +1,5 @@
 (** * Common facts about [≤] *)
 Require Export Fiat.Common.Coq__8_4__8_5__Compat.
-Require Import Coq.Arith.Le.
 Require Import Coq.ZArith.ZArith.
 Require Import Coq.Classes.Morphisms.
 Require Import Coq.Program.Basics.
@@ -46,7 +45,7 @@ Proof.
   induction n; simpl; try reflexivity.
   rewrite IHn; clear IHn.
   edestruct le_canonical; [ exfalso | reflexivity ].
-  { eapply le_Sn_n; eassumption. }
+  { eapply Nat.nle_succ_diag_l; eassumption. }
 Qed.
 
 Lemma le_canonical_nS {n m pf} (H : le_canonical n m = left pf)
@@ -103,13 +102,13 @@ Proof. omega. Qed.
 Global Instance le_lt_Proper : Proper (Basics.flip le ==> le ==> impl) lt.
 Proof.
   repeat intro.
-  eapply lt_le_trans; [ | eassumption ].
-  eapply le_lt_trans; eassumption.
+  eapply Nat.lt_le_trans; [ | eassumption ].
+  eapply Nat.le_lt_trans; eassumption.
 Qed.
 
 Global Instance le_lt_Proper' : Proper (le ==> Basics.flip le ==> Basics.flip impl) lt.
 Proof.
   repeat intro.
-  eapply lt_le_trans; [ | eassumption ].
-  eapply le_lt_trans; eassumption.
+  eapply Nat.lt_le_trans; [ | eassumption ].
+  eapply Nat.le_lt_trans; eassumption.
 Qed.

src/Common/List/FlattenList.v

@@ -92,7 +92,7 @@ Section FlattenList.
     - auto with arith.
     - unfold compose;
       rewrite app_length, <- IHseq.
-      rewrite plus_comm, <- plus_assoc; auto with arith.
+      rewrite Nat.add_comm, <- Nat.add_assoc; auto with arith.
   Qed.
 
   Lemma length_flatten :

src/Common/List/ListFacts.v

@@ -351,8 +351,8 @@ Section ListFacts.
     clear IHseq; revert a default; induction seq;
       simpl; intros; auto with arith.
     rewrite <- IHseq.
-    rewrite Plus.plus_comm, <- Plus.plus_assoc; f_equal.
-    rewrite Plus.plus_comm; reflexivity.
+    rewrite Nat.add_comm, <- Nat.add_assoc; f_equal.
+    rewrite Nat.add_comm; reflexivity.
   Qed.
 
   Lemma map_snd {A B C} :
@@ -433,7 +433,7 @@ Section ListFacts.
   Proof.
     induction seq; simpl; intros; eauto with arith.
     rewrite IHseq; f_equal; eauto with arith.
-    repeat rewrite <- Plus.plus_assoc; f_equal; auto with arith.
+    repeat rewrite <- Nat.add_assoc; f_equal; auto with arith.
   Qed.
 
   Lemma length_flat_map :
@@ -603,7 +603,7 @@ Section ListFacts.
     { destruct y; simpl.
       { destruct x; simpl; repeat (f_equal; []); try reflexivity; omega. }
       { rewrite IHls; destruct x; simpl; repeat (f_equal; []); try reflexivity.
-        rewrite NPeano.Nat.add_succ_r; reflexivity. } }
+        rewrite Nat.add_succ_r; reflexivity. } }
   Qed.
 
   Lemma in_map_iffT' {A B}
@@ -639,7 +639,7 @@ Section ListFacts.
         (f : A -> nat) (ls : list A) (y : nat)
     : iffT (In y (map f ls)) { x : A | f x = y /\ In x ls }.
   Proof.
-    apply in_map_iffT, NPeano.Nat.eq_dec.
+    apply in_map_iffT, Nat.eq_dec.
   Defined.
 
   Lemma nth_take_1_drop {A} (ls : list A) n a
@@ -670,7 +670,7 @@ Section ListFacts.
     : drop 1 (drop y ls) = drop (S y) ls.
   Proof.
     rewrite drop_drop.
-    rewrite NPeano.Nat.add_1_r.
+    rewrite Nat.add_1_r.
     reflexivity.
   Qed.
 
@@ -967,15 +967,15 @@ Section ListFacts.
        | [ H : context[option_map _ ?x] |- _ ] => destruct x eqn:?; unfold option_map in H
        | _ => solve [ repeat (esplit || eassumption) ]
        | [ H : context[nth_error (_::_) ?x] |- _ ] => is_var x; destruct x; simpl nth_error in H
-       | [ H : S _ < S _ |- _ ] => apply lt_S_n in H
+       | [ H : S _ < S _ |- _ ] => apply (proj2 (Nat.succ_lt_mono _ _)) in H
        | _ => solve [ eauto with nocore ]
        | [ |- context[if ?b then _ else _] ] => destruct b eqn:?
        | [ H : ?A -> ?B |- _ ] => let H' := fresh in assert (H' : A) by (assumption || omega); specialize (H H'); clear H'
        | [ H : forall n, n < S _ -> _ |- _ ] => pose proof (H 0); specialize (fun n => H (S n))
        | _ => progress simpl in *
        | [ H : forall x, ?f x = ?f ?y -> _ |- _ ] => specialize (H _ eq_refl)
        | [ H : forall x, ?f ?y = ?f x -> _ |- _ ] => specialize (H _ eq_refl)
-       | [ H : forall n, S n < S _ -> _ |- _ ] => specialize (fun n pf => H n (lt_n_S _ _ pf))
+       | [ H : forall n, S n < S _ -> _ |- _ ] => specialize (fun n pf => H n (proj1 (Nat.succ_lt_mono _ _) pf))
        | [ H : nth_error nil ?x = Some _ |- _ ] => is_var x; destruct x
        | [ H : forall m x, nth_error (_::_) m = Some _ -> _ |- _ ] => pose proof (H 0); specialize (fun m => H (S m))
        | [ H : or _ _ |- _ ] => destruct H
@@ -1106,11 +1106,11 @@ Section ListFacts.
     induction ls as [|x xs IHxs].
     { simpl; intros; destruct (n - offset); reflexivity. }
     { simpl; intros.
-      destruct (beq_nat n offset) eqn:H';
-        [ apply beq_nat_true in H'
-        | apply beq_nat_false in H' ];
+      destruct (Nat.eqb n offset) eqn:H';
+        [ apply Nat.eqb_eq in H'
+        | apply Nat.eqb_neq in H' ];
         subst;
-        rewrite ?minus_diag; trivial.
+        rewrite ?Nat.sub_diag; trivial.
       destruct (n - offset) eqn:H''.
       { omega. }
       { rewrite IHxs by omega.
@@ -1997,7 +1997,7 @@ Section ListFacts.
       List.In n ns -> f n <= fold_right (fun n acc => max (f n) acc) 0 ns.
   Proof.
     induction ns; intros; inversion H; subst; simpl;
-      apply NPeano.Nat.max_le_iff; [ left | right ]; auto.
+      apply Nat.max_le_iff; [ left | right ]; auto.
   Qed.
 
   Lemma fold_right_higher_is_higher {A}
@@ -2006,7 +2006,7 @@ Section ListFacts.
       fold_right (fun n acc => max (f n) acc) 0 ns <= x.
   Proof.
     induction ns; simpl; intros; [ apply le_0_n | ].
-    apply NPeano.Nat.max_lub.
+    apply Nat.max_lub.
     apply H; left; auto.
     apply IHns; intros; apply H; right; auto.
   Qed.
@@ -2023,8 +2023,8 @@ Section ListFacts.
   (* if a list is empty, the result of filtering the list with anything will still be empty *)
   Lemma filter_nil_is_nil {A}
     : forall (l : list A) (pred : A -> bool),
-      beq_nat (Datatypes.length l) 0 = true
-      ->  beq_nat (Datatypes.length (filter pred l)) 0 = true.
+      Nat.eqb (Datatypes.length l) 0 = true
+      ->  Nat.eqb (Datatypes.length (filter pred l)) 0 = true.
   Proof.
     induction l; intros; simpl; try inversion H.
     reflexivity.
@@ -2374,7 +2374,7 @@ Section ListFacts.
       = option_map (fun v => (start + idx, v)) (nth_error ls idx).
   Proof.
     revert start idx; induction ls as [|l ls IHls], idx as [|idx]; try reflexivity.
-    { simpl; rewrite NPeano.Nat.add_0_r; reflexivity. }
+    { simpl; rewrite Nat.add_0_r; reflexivity. }
     { simpl; rewrite <- plus_n_Sm, IHls; reflexivity. }
   Qed.
 

src/Common/List/Operations.v

@@ -74,7 +74,7 @@ Module Export List.
   Fixpoint nth'_helper {A} (n : nat) (ls : list A) (default : A) (offset : nat) :=
     match ls with
       | nil => default
-      | x::xs => if EqNat.beq_nat n offset
+      | x::xs => if Nat.eqb n offset
                  then x
                  else nth'_helper n xs default (S offset)
     end.