move normalize_and_simpl_goal to the beginning of unprepared_solve_goal

theories/lang/lang.v

@@ -627,6 +627,10 @@ Lemma ly_align_log_ly_align_le_iff ly1 ly2:
   (ly_align_log ly1 ≤ ly_align_log ly2 ↔ ly_align ly1 ≤ ly_align ly2)%nat.
 Proof. rewrite /ly_align. apply: Nat.pow_le_mono_r_iff. lia. Qed.
 
+Lemma ly_size_ly_with_align m n :
+  ly_size (ly_with_align m n) = m.
+Proof. done. Qed.
+
 Lemma ly_align_ly_with_align m n :
   ly_align (ly_with_align m n) = keep_factor2 n 1.
 Proof. rewrite /ly_with_align/keep_factor2/factor2. by destruct (factor2' n). Qed.

theories/typing/automation/normalize.v

@@ -29,7 +29,7 @@ Hint Rewrite @bool_decide_eq_x_x_true @if_bool_decide_eq_branches : refinedc_rew
 Hint Rewrite keep_factor2_is_power_of_two keep_factor2_min_eq using can_solve_tac : refinedc_rewrite.
 Hint Rewrite keep_factor2_min_1 keep_factor2_twice : refinedc_rewrite.
 Hint Rewrite ly_align_ly_with_align ly_align_ly_offset ly_align_ly_set_size : refinedc_rewrite.
-Hint Rewrite ly_size_ly_set_size : refinedc_rewrite.
+Hint Rewrite ly_size_ly_set_size ly_size_ly_with_align : refinedc_rewrite.
 
 Local Definition lookup_insert_gmap A K `{Countable K} := lookup_insert (M := gmap K) (A := A).
 Hint Rewrite lookup_insert_gmap : refinedc_rewrite.

theories/typing/automation/solvers.v

@@ -176,9 +176,9 @@ Ltac unfold_common_defs :=
 
 (** * [solve_goal] without cleaning of the context  *)
 Ltac unprepared_solve_goal :=
+  normalize_and_simpl_goal;
   try rewrite -> unfold_int_elem_of_it in *;
   unfold_common_defs; simpl in *;
-  normalize_and_simpl_goal;
   rewrite /ly_size/ly_align_log //=; enrich_context;
   repeat case_bool_decide => //; repeat case_decide => //; repeat case_match => //;
   refined_solver lia.