norm_num question

Stream: new members

[Michael Stoll]

Why does the following not work?

example : (3 : zmod 8)^2 = 1 := by norm_num

gives

tactic failed, there are unsolved goals
state:
⊢ 9 = 1

If norm_num cannot do it, how can numerical calculations then be done in ℤ/nℤ?

[Mario Carneiro]

norm_fin does this kind of thing but I think it doesn't work on zmod. You can also prove 9 % 8 = 1 % 8 using norm_num and apply a theorem to deduce the zmod fact

[Heather Macbeth]

I think dec_trivial works on this kind of thing.

[Heather Macbeth]

import data.zmod.basic

example : (3 : zmod 8)^2 = 1 := by dec_trivial

[Michael Stoll]

@Heather Macbeth Hm, I think I tried that (perhaps in a slightly more complicated situation).

This also gives

example (a : zmod 17) : a^4 ≠ 2 := by { fin_cases a; dec_trivial }

But I guess that trying the same with (say)

example (a b c : zmod 8) : a^2 + b^2 + c^2 ≠ 7

will be too much for Lean.

[Michael Stoll]

My original question still stands: Is there a (good) reason why this is not part of what norm_num does?

[Yakov Pechersky]

Just because the norm_fin extension hasn't been expanded to support zmod (n + 1). An easy way would be to transfer through the fin (n + 1) \~-+* zmod (n + 1) ring equiv (which is just refl)

[Johan Commelin]

Michael Stoll said:

This also gives

example (a : zmod 17) : a^4 ≠ 2 := by { fin_cases a; dec_trivial }

This should work with dec_trivial! (note the !).

[Michael Stoll]

I was thinking of the 8^3 = 512 cases the naive approach would generate.

[Michael Stoll]

(Previous version had a wrong statement.)
The simpler version:

example (a b : zmod 4) : a^2 + b^2 ≠ 3 := begin fin_cases a; { fin_cases b; dec_trivial, } end

works without the ! and also with it.

[Rob Lewis]

The 512 cases aren't instant, but aren't horribly slow. For the "simpler" version, luckily dec_trivial can only prove true statements :smile:

[Michael Stoll]

I had just realized that and was editing my message...

[Michael Stoll]

On my machine, I get a deterministic timeout from the 512 cases (with dec_trivial!).

[Michael Stoll]

... and also with dec_trivial.

[Rob Lewis]

Are you using fin_cases first? This isn't necessary. Lean knows that universal quantifiers over a finite type are decidable.

example (a b c : zmod 8) : a^2 + b^2 + c^2 ≠ 7 :=
by dec_trivial!

[Michael Stoll]

OK; I didn't know that. In fact, I have no really good idea what dec_trivial[!] is and is not capable of doing.
Still trying to feel my way in...

[Johan Commelin]

The difference between dec_trivial and dec_trivial! is quite small. The version with ! will try to revert some assumptions, but otherwise it's just the same as dec_trivial.

[Johan Commelin]

And dec_trivial tells Lean: hey all definitions involved are computable. You should be able to use them to run a finite algorithm and decide the truth of this claim.

[Johan Commelin]

But the efficiency of that algorithm can of course be horrible, depending on those definitions and the size of the objects involved.

[Michael Stoll]

I expected the following to work, but it doesn't.

lemma l1 (a : zmod 8) : a^2 = 0 ∨ a^2 = 1 ∨ a^2 = 4 := by dec_trivial!

example (a : zmod 8) (h : a^2 = 6) : false :=
begin
  have l := l1 a,
  rw h at l,
  dec_trivial, -- gives error, also with dec_trivial!
end

It does, however, after inserting revert l before dec_trivial. Why does this make a difference?

[Kyle Miller]

Michael Stoll said:

My original question still stands: Is there a (good) reason why this is not part of what norm_num does?

I'm wondering this, too. Is it out of scope for norm_num to be able to reduce zmod numerals?

[Yakov Pechersky]

It can be a norm_num extensions, probably within the extension provided by norm_fin