Adapt to rocq-prover/stdlib#251

Author: proux01

LiveVerif/src/LiveVerif/LiveProgramLogic.v

@@ -101,11 +101,11 @@ Inductive stepping: Type :=.
 Definition ready{P: Prop} := P.
 
 (* heapletwise- and word-aware lia, successor of ZnWords *)
-Ltac hwlia := zify_hyps; puri_simpli_zify_hyps true; zify_goal; xlia zchecker.
+Ltac hwlia := zify_hyps; puri_simpli_zify_hyps true; zify_goal; mp_lia zchecker.
 
-Ltac2 Set bottom_up_simpl_sidecond_hook := fun _ => ltac1:(zify_goal; xlia zchecker).
+Ltac2 Set bottom_up_simpl_sidecond_hook := fun _ => ltac1:(zify_goal; mp_lia zchecker).
 
-Ltac word_lia_hook_for_split_merge ::= zify_goal; xlia zchecker.
+Ltac word_lia_hook_for_split_merge ::= zify_goal; mp_lia zchecker.
 
 Ltac intros_until_trace :=
   repeat lazymatch goal with
@@ -856,7 +856,7 @@ Ltac conclusion_shape_based_step logger :=
   | |- bool_expr_branches _ _ _ _ =>
       logger ltac:(fun _ => idtac "Splitting bool_expr_branches");
       eapply BoolSpec_expr_branches;
-      [ first [ eapply contradictory_branch; zify_goal; xlia zchecker
+      [ first [ eapply contradictory_branch; zify_goal; mp_lia zchecker
               | intro ] .. | ]
   | |- then_branch_marker ?G =>
       logger ltac:(fun _ => idtac "Starting `then` branch");
@@ -1005,7 +1005,7 @@ Ltac sidecond_step logger := first
         end;
         logger ltac:(fun _ => idtac "eexists")
       | (* tried first because it also solves some goals of shape (_ = _) and (_ /\ _) *)
-        zify_goal; xlia zchecker;
+        zify_goal; mp_lia zchecker;
         logger ltac:(fun _ => idtac "zify_goal; xlia zchecker")
       | safe_implication_step;
         logger ltac:(fun _ => idtac "safe_implication_step")
@@ -1187,7 +1187,7 @@ Ltac predicates_safe_to_cancel hypPred conclPred :=
       | array ?elem ?n2 ?vs2 => lazymatch hypPred with
                                 | array elem ?n1 ?vs1 =>
                                     assert_succeeds (idtac; assert (n1 = n2)
-                                                       by (zify_goal; xlia zchecker));
+                                                       by (zify_goal; mp_lia zchecker));
                                     tryif is_evar vs2 then unify vs1 vs2 else idtac
                                 end
       | sepapps nil => lazymatch hypPred with
@@ -1215,7 +1215,7 @@ Ltac is_safe_to_cancel hypClause goalClause :=
       | ?pred2 ?addr2 =>
           first [ constr_eq addr1 addr2
                 | assert_succeeds (idtac; assert (addr1 = addr2)
-                                     by (zify_goal; xlia zchecker)) ];
+                                     by (zify_goal; mp_lia zchecker)) ];
           predicates_safe_to_cancel pred1 pred2
       end
   end.

LiveVerif/src/LiveVerifExamples/Tests/SampleSideconds.v

@@ -7,9 +7,9 @@ Ltac standalone_solver_step :=
       (* from step_hook in tree_set: *)
       | lazymatch goal with
         | |- ?A \/ ?B =>
-            tryif (assert_succeeds (assert (~ A) by (zify_hyps; zify_goal; xlia zchecker)))
+            tryif (assert_succeeds (assert (~ A) by (zify_hyps; zify_goal; mp_lia zchecker)))
             then right else
-            tryif (assert_succeeds (assert (~ B) by (zify_hyps; zify_goal; xlia zchecker)))
+            tryif (assert_succeeds (assert (~ B) by (zify_hyps; zify_goal; mp_lia zchecker)))
             then left else fail
         end
       | solve [auto 4 with nocore safe_core]

LiveVerif/src/LiveVerifExamples/mini_stagefright.v

@@ -8,9 +8,9 @@ Load LiveVerif.
 Ltac step_hook ::=
   lazymatch goal with
   | |- ?A \/ ?B =>
-      tryif (assert_succeeds (assert (~ A) by (zify_goal; xlia zchecker)))
+      tryif (assert_succeeds (assert (~ A) by (zify_goal; mp_lia zchecker)))
       then right else
-      tryif (assert_succeeds (assert (~ B) by (zify_goal; xlia zchecker)))
+      tryif (assert_succeeds (assert (~ B) by (zify_goal; mp_lia zchecker)))
       then left else fail
   end.
 

LiveVerif/src/LiveVerifExamples/nt_uint8_string.v

@@ -90,14 +90,14 @@ Derive strCmp SuchThat (fun_correct! strCmp) As strCmp_ok.
   [ | once (typeclasses eauto with purify) ];
   specialize (A \[p2' ^- p2_pre]); cbv beta in A;
   bottom_up_simpl_in_hyp A;
-  specialize (A ltac:(zify_hyps; zify_goal; xlia zchecker)).
+  specialize (A ltac:(zify_hyps; zify_goal; mp_lia zchecker)).
 
   let A := constr:(#array) in
   eapply purify_array_ith_elem in A;
   [ | once (typeclasses eauto with purify) ];
   specialize (A \[p1' ^- p1_pre]); cbv beta in A;
   bottom_up_simpl_in_hyp A;
-  specialize (A ltac:(zify_hyps; zify_goal; xlia zchecker)).
+  specialize (A ltac:(zify_hyps; zify_goal; mp_lia zchecker)).
 
   destr (\[p1' ^- p1_pre] =? len s1);
   destr (\[p2' ^- p2_pre] =? len s2);
@@ -162,7 +162,7 @@ Derive Strcmp SuchThat (fun_correct! Strcmp) As Strcmp_ok.
     repeat match goal with
            | H: with_mem _ (array _ _ _ _) |- _ =>
                eapply array1_to_elem' in H;
-               [ new_mem_hyp H | zify_goal; xlia zchecker ]
+               [ new_mem_hyp H | zify_goal; mp_lia zchecker ]
            end.
     bsimpl_in_hyps.
     steps.

LiveVerif/src/LiveVerifExamples/tree_set.v

@@ -163,7 +163,7 @@ Ltac step_hook ::=
   | H: _ |= bst' _ _ ?p, E: ?p = /[0] |- _ =>
       assert_fails (has_evar H); eapply (invert_bst'_null E) in H
   | H: _ |= bst' _ _ ?p, E: \[?p] = 0 |- _ =>
-      eapply invert_bst'_null in H; [ | zify_goal; xlia zchecker ]
+      eapply invert_bst'_null in H; [ | zify_goal; mp_lia zchecker ]
   | H: _ |= bst' _ _ ?p, N: ?p <> /[0] |- _ =>
       assert_fails (has_evar H); eapply (invert_bst'_nonnull N) in H
   | H: ?addr <> /[0] |- context[bst' ?sk_evar _ ?addr] =>
@@ -187,16 +187,16 @@ Ltac step_hook ::=
       end
   | H: ?res = ?c1 /\ _ \/ ?res = ?c2 /\ _
     |- ?res = ?c1 /\ _ \/ ?res = ?c2 /\ _ =>
-      assert_succeeds (idtac; assert (c1 <> c2) by (zify_goal; xlia zchecker));
+      assert_succeeds (idtac; assert (c1 <> c2) by (zify_goal; mp_lia zchecker));
       destruct H; [left|right]
   | |- ?A \/ ?B =>
-      tryif (assert_succeeds (assert (~ A) by (zify_goal; xlia zchecker)))
+      tryif (assert_succeeds (assert (~ A) by (zify_goal; mp_lia zchecker)))
       then right else
-      tryif (assert_succeeds (assert (~ B) by (zify_goal; xlia zchecker)))
+      tryif (assert_succeeds (assert (~ B) by (zify_goal; mp_lia zchecker)))
       then left else fail
   | H1: ?x <= ?y, H2: ?y <= ?x, C: ?s ?x |- ?s ?y =>
-      (replace y with x by xlia zchecker); exact C
-  | H: _ \/ _ |- _ => decompose [and or] H; clear H; try (exfalso; xlia zchecker); []
+      (replace y with x by mp_lia zchecker); exact C
+  | H: _ \/ _ |- _ => decompose [and or] H; clear H; try (exfalso; mp_lia zchecker); []
   | |- _ => solve [auto 3 with nocore safe_core]
   end.
 

bedrock2/src/bedrock2/PurifyHeapletwise.v

@@ -16,7 +16,7 @@ Ltac split_and_try_exact :=
   end.
 
 Ltac fail_if_too_trivial t :=
-  assert_fails (idtac; assert t by (split_and_try_exact; xlia zchecker)).
+  assert_fails (idtac; assert t by (split_and_try_exact; mp_lia zchecker)).
 
 Ltac puri_simpli_zify_hyp fastMode h t :=
   let pure := purified_hyp h t in
@@ -55,7 +55,7 @@ Inductive derivability_test_marker: Prop := mk_derivability_test_marker.
 Ltac clear_pure_hyp_if_derivable h tp :=
   tryif ident_starts_with __pure_ h then
     try (clear h; assert_succeeds (idtac; assert tp by
-      (split_and_try_exact; zify_goal; xlia zchecker)))
+      (split_and_try_exact; zify_goal; mp_lia zchecker)))
   else idtac.
 
 Ltac clear_upto_marker marker :=

bedrock2/src/bedrock2/SepLib.v

@@ -410,6 +410,6 @@ Require Import bedrock2.unzify.
 
 #[export] Hint Resolve array_nil_is_emp : is_emp.
 #[export] Hint Extern 1 (is_emp (array ?elem ?n ?xs ?a) _) =>
-  eapply (array_0_is_emp elem n xs a ltac:(zify_goal; xlia zchecker)) : is_emp.
+  eapply (array_0_is_emp elem n xs a ltac:(zify_goal; mp_lia zchecker)) : is_emp.
 #[export] Hint Extern 1 (is_emp (array ?elem ?n ? ?a) _) =>
-  eapply (anyval_array_0_is_emp elem n a ltac:(zify_goal; xlia zchecker)) : is_emp.
+  eapply (anyval_array_0_is_emp elem n a ltac:(zify_goal; mp_lia zchecker)) : is_emp.

bedrock2/src/bedrock2/bottom_up_simpl_ltac1.v

@@ -241,7 +241,7 @@ Ltac debug_sidecond :=
   end;
   time "Zify.zify" Zify.zify;
   refine (@xlia _ _);
-  time "xlia zchecker" xlia zchecker.
+  time "xlia zchecker" mp_lia zchecker.
 
 Ltac bottom_up_simpl_sidecond_hook := lia. (* OR xlia zchecker if already zified *)
 

bedrock2/src/bedrock2/to_from_anybytes.v

@@ -447,7 +447,7 @@ Create HintDb fillable.
 : fillable.
 
 #[export] Hint Extern 1 (fillable (array ?elem ?n) _) =>
-  eapply array_fillable; [ xlia zchecker | eauto with fillable ]
+  eapply array_fillable; [ mp_lia zchecker | eauto with fillable ]
 : fillable.
 
 #[export] Hint Extern 20 (contiguous ?p ?n) =>

bedrock2/src/bedrock2/unzify.v

@@ -787,7 +787,7 @@ Ltac clear_if_dup h :=
 
 Ltac do_clear_Z_hyp_if_derivable h :=
   let tp := type of h in
-  try (clear h; assert_succeeds (idtac; assert tp by xlia zchecker)).
+  try (clear h; assert_succeeds (idtac; assert tp by mp_lia zchecker)).
 
 Ltac don't_clear_Z_hyp_if_derivable h := idtac.
 
@@ -845,7 +845,7 @@ Require Import bedrock2.WordNotations. Local Open Scope word_scope.
 Section Tests.
   Local Set Ltac Backtrace.
 
-  Ltac rzify_lia := zify_hyps; zify_goal; xlia zchecker.
+  Ltac rzify_lia := zify_hyps; zify_goal; mp_lia zchecker.
 
   Goal forall (x y: Z), 0 <= x < y -> y < 2 ^ 32 -> x mod 2 ^ 32 < y mod 2 ^ 32.
   Proof. intros. rzify_lia. Succeed Qed. Abort.
@@ -867,7 +867,7 @@ Section Tests.
 
   Goal forall (a b: word),
       word.signed (a ^+ b) = word.signed (b ^+ a).
-  Proof. intros. zify_goal. xlia zchecker. Succeed Qed. Abort.
+  Proof. intros. zify_goal. mp_lia zchecker. Succeed Qed. Abort.
 
   Goal forall (a b c: word),
       word.signed (a ^+ b ^- c) = word.signed (word.opp c ^+ b ^+ a).
@@ -1052,7 +1052,7 @@ Section Tests.
       \[w] = \[if c then /[in1] else /[in2]] ->
       \[w] < 20.
   Proof.
-    intros. zify_hyps. zify_goal. Fail xlia zchecker.
+    intros. zify_hyps. zify_goal. Fail mp_lia zchecker.
   Abort.
 
   Goal forall (left0 right : word) (xs : list word),