Stream: Coq users

Topic: ✔ How to prove this? Any hints?


view this post on Zulip 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!

view this post on Zulip 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.

view this post on Zulip Notification Bot (Aug 06 2021 at 13:29):

Lessness has marked this topic as resolved.


Last updated: Mar 28 2024 at 14:01 UTC