Require Import VST.floyd.proofauto. Theorem T (n: Z) (H: 0 <= n <= 1000): Vint (Int.divu (Int.repr (n * (n + 1))) (Int.repr 2)) = Vint (Int.repr (n * (n + 1) / 2)). Proof. Admitted.
I guess the main missing piece for you is "unfold Int.divu". The rest is relatively straight forward:
Require Import VST.floyd.proofauto. Require Import Lia. Theorem T (n: Z) (H: 0 <= n <= 1000): Vint (Int.divu (Int.repr (n * (n + 1))) (Int.repr 2)) = Vint (Int.repr (n * (n + 1) / 2)). Proof. intros. unfold Int.divu. change (Int.unsigned (Int.repr 2)) with 2. rewrite Int.unsigned_repr. 1: reflexivity. change Int.max_unsigned with 4294967295. replace (n * (n + 1)) with (n*n + n) by ring. pose proof Z.square_le_mono_nonneg n 1000. lia. Qed.
I automate such numerics with Coq interval and/or Coq gappa, but the wrapper tactics get fairly involved cause of the Z to R and back conversion. But as long as it doesn't get much more complicated, posing some info about the non linear part and using lia to figure out the details works quite well.
Lessness has marked this topic as resolved.
Last updated: Oct 03 2023 at 21:01 UTC