Stop relying on replace by automatic assumption-based solving

bedrock2/src/bedrock2/SepLogAddrArith.v

@@ -99,7 +99,7 @@ Ltac sepclause_eq OK :=
                       let addrR := addr rhs in
                       assert_fails (has_evar addrL);
                       assert_fails (has_evar addrR);
-                      replace addrL with addrR by solve_word_eq OK;
+                      replace addrL with addrR by first[assumption | symmetry;assumption | solve_word_eq OK];
                       (reflexivity || fail 10000 lhs "and" rhs "have the same address"
                       "according to addr, but can't be matched")
   end.

compiler/src/compiler/FlatToRiscvFunctions.v

@@ -521,7 +521,7 @@ Section Proofs.
                argnames = List.firstn arg_count (reg_class.all reg_class.arg)) as AC. {
       exists (List.length argnames). ssplit. 2: congruence.
       replace argnames with
-          (List.firstn (Datatypes.length argnames) (reg_class.all reg_class.arg)) by assumption.
+          (List.firstn (Datatypes.length argnames) (reg_class.all reg_class.arg)) by (symmetry;assumption).
       rewrite List.firstn_length.
       change (Datatypes.length (reg_class.all reg_class.arg)) with 8%nat.
       clear. blia.
@@ -840,7 +840,7 @@ Section Proofs.
         blia.
       }
       replace retnames with
-          (List.firstn (Datatypes.length retnames) (reg_class.all reg_class.arg)) by assumption.
+          (List.firstn (Datatypes.length retnames) (reg_class.all reg_class.arg)) by (symmetry;assumption).
       rewrite List.firstn_length.
       change (Datatypes.length (reg_class.all reg_class.arg)) with 8%nat.
       clear. blia.

compiler/src/compiler/LowerPipeline.v

@@ -709,7 +709,7 @@ Section LowerPipeline.
           { rewrite Nat2Z.inj_mul, Z2Nat.id by blia.
             replace (Z.of_nat (Datatypes.length stack_trash))
               with (word.unsigned (word.sub stack_pastend stack_start) / bytes_per_word)
-              by assumption.
+              by (symmetry;assumption).
             rewrite <- Z_div_exact_2; try trivial.
             eapply Z.lt_gt; assumption. }
           intros w.
@@ -728,7 +728,7 @@ Section LowerPipeline.
             end.
             replace (Z.of_nat (Datatypes.length stack_trash))
               with (word.unsigned (word.sub stack_pastend stack_start) / bytes_per_word)
-              by assumption.
+              by (symmetry;assumption).
             rewrite <- Z_div_exact_2. 3: assumption.
             2: eapply Z.lt_gt; assumption.
             rewrite word.of_Z_unsigned.

compiler/src/compiler/MMIO.v

@@ -228,7 +228,7 @@ Section MMIO1.
     1: replace x with (word.sub y (word.of_Z 3)) in * by (subst y; solve_word_eq word_ok).
     2: replace x with (word.sub y (word.of_Z 2)) in * by (subst y; solve_word_eq word_ok).
     3: replace x with (word.sub y (word.of_Z 1)) in * by (subst y; solve_word_eq word_ok).
-    4: replace x with y in * by assumption.
+    4: replace x with y in * by (symmetry;assumption).
     all: clear C;
       rewrite ?word.unsigned_sub, ?word.unsigned_of_Z in H, H1;
       unfold word.wrap in *;