Thanks!
With the intermediary step, it works fine with Alt-Ergo 1.30 after split.
What takes most of time (almost all the time) is to see that it should use
Mod_mult.
lemma mod_mult: forall x a b. 0 <= x -> 0 < a -> 0 < b ->
mod (mod x (a * b)) a = mod x a
by mod (mod x (a * b)) a = mod (a * ((- b) * div x (a * b)) + x) a /\
mod (a * ((- b) * div x (a * b)) + x) a = mod x a
On Thu, Oct 19, 2017 at 8:19 AM, Guillaume Melquiond <
guillaume.melqui...@inria.fr> wrote:
> On 18/10/2017 21:56, Julien Cretin wrote:
> > 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)`.
>
> No, you don't need anything else; the two axioms provided by Why3
> (Div_mod and Mod_bound) about div and mod are complete.
>
> That said, getting all the way from these two axioms to the property you
> want to prove might be a bit long. So you should make use of the
> Mod_mult lemma provided by Why3 to cut it short:
>
> mod (mod x (a * b)) a =
> mod (x - a * b * div x (a * b)) a =
> mod x a
>
> Best regards,
>
> Guillaume
> _______________________________________________
> Why3-club mailing list
> Why3-club@lists.gforge.inria.fr
> https://lists.gforge.inria.fr/mailman/listinfo/why3-club
>
_______________________________________________
Why3-club mailing list
Why3-club@lists.gforge.inria.fr
https://lists.gforge.inria.fr/mailman/listinfo/why3-club
