Zulip Chat Archive

Stream: new members

Topic: tactic for doing calculation with mod


view this post on Zulip Patrick Lutz (Jun 21 2020 at 21:43):

Is there a tactic (or some other way I guess) to take care of calculations in modular arithmetic? E.g. something that would easily prove the following

import data.nat.basic

example (a b c : ) (ha : a % 5 = 1) (hb : b % 5 = 3)
    (hc : c % 5 = 4) : (a^2 + (b + 2*c)^3) % 5 = 2 := sorry

Right now I can prove this with a series of rewrites and then a call to ring, but it seems too involved. Is there a better way?

view this post on Zulip Chris Hughes (Jun 21 2020 at 21:47):

I would avoid the use of % and use the type zmod for most things like this.

view this post on Zulip Jalex Stark (Jun 21 2020 at 21:48):

import tactic

import data.nat.basic
import data.zmod.basic

example (a b c : zmod 5) (ha : a = 1) (hb : b = 3)
  (hc : c = 4) : (a^2 + (b + 2*c)^3) = 2 :=
begin
  rw [ha, hb, hc], ring,
end

Last updated: May 11 2021 at 12:15 UTC