Lessness (Aug 06 2021 at 10:06): Lessness (Aug 06 2021 at 10:06):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.
Thank you!
Michael Soegtrop (Aug 06 2021 at 12:12):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.
Notification Bot (Aug 06 2021 at 13:29):Lessness has marked this topic as resolved.
Last updated: Oct 03 2023 at 21:01 UTC