Tweak proofs.

theories/list_numbers.v

@@ -291,6 +291,9 @@ Section Z_little_endian.
   Local Open Scope Z_scope.
   Implicit Types m n z : Z.
 
+  Lemma Z_to_little_endian_0 n z : Z_to_little_endian 0 n z = [].
+  Proof. done. Qed.
+
   Lemma Z_to_little_endian_succ m n z :
     0 ≤ m →
     Z_to_little_endian (Z.succ m) n z
@@ -376,18 +379,17 @@ Section Z_little_endian.
   Qed.
 
   Lemma Z_to_little_endian_lookup_Some m n z (i : nat) x :
-    0 ≤ m →
-    0 ≤ n →
+    0 ≤ m → 0 ≤ n →
     Z_to_little_endian m n z !! i = Some x ↔
     Z.of_nat i < m ∧ x = Z.land (z ≫ (Z.of_nat i * n)) (Z.ones n).
   Proof.
-    revert z m. induction i as [|i IH]; intros z m Hm Hn; rewrite <-(Z.succ_pred m) at 1.
-    all: destruct (decide (m = 0)); subst; simpl; [ naive_solver lia|].
-    all: rewrite Z_to_little_endian_succ; simpl; [|lia].
-    { rewrite Z.shiftr_0_r. naive_solver lia. }
-    rewrite IH, ?Z.shiftr_shiftr; [|nia..].
-    assert ((n + Z.of_nat i * n) = (Z.of_nat (S i) * n)) as -> by lia.
-    naive_solver lia.
+    revert z i. induction m as [|m ? IH|] using (Z_succ_pred_induction 0);
+      intros z i ??; [..|lia].
+    { destruct i; simpl; naive_solver lia. }
+    rewrite Z_to_little_endian_succ by lia. destruct i as [|i]; simpl.
+    { naive_solver lia. }
+    rewrite IH, Z.shiftr_shiftr by lia.
+    naive_solver auto with f_equal lia.
   Qed.
 
   Lemma little_endian_to_Z_spec n bs i b :
@@ -396,26 +398,20 @@ Section Z_little_endian.
     bs !! Z.to_nat (i `div` n) = Some b →
     Z.testbit (little_endian_to_Z n bs) i = Z.testbit b (i `mod` n).
   Proof.
-    intros Hi Hn. rewrite Z2Nat_inj_div; [|lia..].
-    (* TODO: remove this once lia can solve this automatically on
-    all supported Coq versions. *)
-    assert (Z.to_nat n ≠ 0%nat). { intros ?%(Z2Nat.inj _ 0); lia. }
-    revert i Hi.
-    induction bs as [|b' bs IH]; intros i ?; [done|]; simpl.
-    intros [[? Hb]?]%Forall_cons. intros [[Hx ?]|[? Hbs]]%lookup_cons_Some; subst.
-    - apply Nat.div_small_iff in Hx; [|lia]. apply Z2Nat.inj_lt in Hx; [|lia..].
-      rewrite Z.lor_spec, Z.shiftl_spec, Z.mod_small, (Z.testbit_neg_r _ (i - n)); [|lia..].
-      by rewrite orb_false_r.
-    - rewrite Z.lor_spec, Z.shiftl_spec by lia.
-      assert (Z.to_nat n <= Z.to_nat i)%nat as Hle. { apply Nat.div_str_pos_iff; lia. }
-      assert (n ≤ i). { apply Z2Nat.inj_le; lia. }
-      revert Hbs.
-      assert (Z.to_nat i `div` Z.to_nat n - 1 = Z.to_nat (i - n) `div` Z.to_nat n)%nat as ->. {
-        apply Nat2Z.inj. rewrite !Z2Nat.inj_sub, !Nat2Z_inj_div, !Nat2Z.inj_sub, !Nat2Z_inj_div; [|lia..].
-        rewrite <-(Z.add_opp_r (Z.of_nat _)), Z.opp_eq_mul_m1, Z.mul_comm, Z.div_add; [|lia]. lia.
-      }
-      intros ->%IH; [|lia|done]. rewrite <-Zminus_mod_idemp_r, Z_mod_same_full, Z.sub_0_r.
-      assert (Z.testbit b' i = false) as ->; [|done].
-      eapply Z_bounded_iff_bits_nonneg; [| |done|]; lia.
+    intros Hi Hn Hbs. revert i Hi.
+    induction Hbs as [|b' bs [??] ? IH]; intros i ? Hlookup; simplify_eq/=.
+    destruct (decide (i < n)).
+    - rewrite Z.div_small in Hlookup by lia. simplify_eq/=.
+      rewrite Z.lor_spec, Z.shiftl_spec, Z.mod_small by lia.
+      by rewrite (Z.testbit_neg_r _ (i - n)), orb_false_r by lia.
+    - assert (Z.to_nat (i `div` n) = S (Z.to_nat ((i - n) `div` n))) as Hdiv.
+      { rewrite <-Z2Nat.inj_succ by (apply Z.div_pos; lia).
+        rewrite <-Z.add_1_r, <-Z.div_add by lia.
+        do 2 f_equal. lia. }
+      rewrite Hdiv in Hlookup; simplify_eq/=.
+      rewrite Z.lor_spec, Z.shiftl_spec, IH by auto with lia.
+      assert (Z.testbit b' i = false) as ->.
+      { apply (Z_bounded_iff_bits_nonneg n); lia. }
+      by rewrite <-Zminus_mod_idemp_r, Z_mod_same_full, Z.sub_0_r.
   Qed.
 End Z_little_endian.