Hi club,
Can I currently (stdlib-0.88.0) prove the following?
lemma mod_mult: forall x a b.
0 <= x ->
0 < a ->
0 < b ->
mod (mod x (a * b)) a = mod x a
It looks like I would need an axiom about `div x (a * b)` and/or `mod x (a
* b)`.
If the lemma is true, how can I work around this issue? (I can't make it an
axiom because `mod_mult does not contain any local abstract symbol`.)
[If you want some background about when this might come up in program
proof, consider a proof of the base64 encoding function. For performance
reasons, the implementation might use a cyclic array of size 256 (4 cycles
of size 64) instead of a normal array of size 64 for the symbol lookup. You
end up proving that `mod (mod x 256) 64 = mod x 64`.]
Thanks,
Julien
_______________________________________________
Why3-club mailing list
Why3-club@lists.gforge.inria.fr
https://lists.gforge.inria.fr/mailman/listinfo/why3-club
