fix naming

theories/typing/int.v

@@ -197,55 +197,55 @@ Section programs.
       move ? : (bits_per_int it - 1) => k.
       have ? : 0 ≤ k.
       { suff : bits_per_int it > 0 by lia. by apply: bits_per_int_gt_0. }
-      have H : ∀ n, -2^k ≤ n ≤ 2^k - 1 ↔
+      have Hb : ∀ n, -2^k ≤ n ≤ 2^k - 1 ↔
         ∀ l, k ≤ l → Z.testbit n l = bool_decide (n < 0)
         by intros; rewrite -bounded_iff_bits; lia.
-      move => /H H1 /H H2.
-      apply H => l Hl.
-      by rewrite Htestbit Hsign H1 ?H2.
+      move => /Hb Hn1 /Hb Hn2.
+      apply Hb => l Hl.
+      by rewrite Htestbit Hsign Hn1 ?Hn2.
     - rewrite /int_modulus.
       move ? : (bits_per_int it) => k.
       have ? : 0 ≤ k.
       { suff : bits_per_int it > 0 by lia. by apply: bits_per_int_gt_0. }
-      have H : ∀ n, 0 ≤ n → n ≤ 2^k - 1 ↔
+      have Hb : ∀ n, 0 ≤ n → n ≤ 2^k - 1 ↔
         ∀ l, k ≤ l → Z.testbit n l = bool_decide (n < 0)
         by intros; rewrite bool_decide_false -?pos_bounded_iff_bits; lia.
-      move => [Hn1 /H H1] [Hn2 /H H2].
+      move => [Hn1 /Hb HN1] [Hn2 /Hb HN2].
       have Hn := Hnonneg Hn1 Hn2.
       split; first done.
-      apply (H _ Hn) => l Hl.
-      by rewrite Htestbit H1 ?H2.
+      apply (Hb _ Hn) => l Hl.
+      by rewrite Htestbit HN1 ?HN2.
   Qed.
 
   Lemma arith_op_result_in_range (it : int_type) (n1 n2 n : Z) op :
     n1 ∈ it → n2 ∈ it → arith_op_result it n1 n2 op = Some n →
     arith_op_sidecond it n1 n2 n op → n ∈ it.
   Proof.
-    move => H1 H2 Hn Hsc.
+    move => Hn1 Hn2 Hn Hsc.
     destruct op => //=; simpl in Hsc, Hn; destruct_and? => //.
     all: inversion Hn; simplify_eq.
     - apply (bitwise_op_result_in_range Z.land andb) => //.
-      + rewrite Z.land_nonneg; tauto.
-      + repeat case_bool_decide; try rewrite -> Z.land_neg in *; tauto.
+      + rewrite Z.land_nonneg; naive_solver.
+      + repeat case_bool_decide; try rewrite -> Z.land_neg in *; naive_solver.
       + by apply Z.land_spec.
     - apply (bitwise_op_result_in_range Z.lor orb) => //.
       + by rewrite Z.lor_nonneg.
-      + repeat case_bool_decide; try rewrite -> Z.lor_neg in *; tauto.
+      + repeat case_bool_decide; try rewrite -> Z.lor_neg in *; naive_solver.
       + by apply Z.lor_spec.
     - apply (bitwise_op_result_in_range Z.lxor xorb) => //.
       + by rewrite Z.lxor_nonneg.
-      + have H : ∀ n, bool_decide (n < 0) = negb (bool_decide (0 ≤ n)).
+      + have Hn : ∀ n, bool_decide (n < 0) = negb (bool_decide (0 ≤ n)).
         { intros. repeat case_bool_decide => //; lia. }
-        rewrite !H.
-        repeat case_bool_decide; try rewrite -> Z.lxor_nonneg in *; tauto.
+        rewrite !Hn.
+        repeat case_bool_decide; try rewrite -> Z.lxor_nonneg in *; naive_solver.
       + by apply Z.lxor_spec.
     - split.
-      + transitivity 0; [ apply min_int_le_0 | by apply Z.shiftl_nonneg ].
+      + trans 0; [ apply min_int_le_0 | by apply Z.shiftl_nonneg ].
       + done.
     - split.
-      + transitivity 0; [ apply min_int_le_0 | by apply Z.shiftr_nonneg ].
-      + destruct H1.
-        transitivity n1; last done. rewrite Z.shiftr_div_pow2; last by lia.
+      + trans 0; [ apply min_int_le_0 | by apply Z.shiftr_nonneg ].
+      + destruct Hn1.
+        trans n1; last done. rewrite Z.shiftr_div_pow2; last by lia.
         apply Z.div_le_upper_bound. { apply Z.pow_pos_nonneg => //. }
         rewrite -[X in X ≤ _]Z.mul_1_l. apply Z.mul_le_mono_nonneg_r => //.
         rewrite -(Z.pow_0_r 2). apply Z.pow_le_mono_r; lia.
@@ -268,11 +268,11 @@ Section programs.
     - iIntros (σ v') "_ !%". split.
       + destruct op => //.
         all: inversion 1; simplify_eq/=.
-        4,5,9,10: case_bool_decide => //.
+        all: try case_bool_decide => //.
         all: destruct it as [? []]; simplify_eq/= => //.
         all: try by rewrite ->it_in_range_mod in * => //; simplify_eq.
       + move => ->; destruct op => //; econstructor => // => //.
-        4,6,11,13: inversion Hsc; case_bool_decide; tauto.
+        all: try by inversion Hsc; case_bool_decide; naive_solver.
         all: destruct it as [? []]; simplify_eq/= => //.
         all: try by rewrite it_in_range_mod.
     - iIntros "!>". iApply "HΦ"; last done.  by iPureIntro.