easy zmod proof

Stream: new members

[Kenji Nakagawa]

Is there a decent way to prove something about something mod n where you have a proof that if k is true, then k+n is also true, and then just bashing the small cases?
Currently I have this (here the proof of modfact1 is irrelevant except for maybe proving modfact2):

import tactic.basic
import data.zmod.basic

lemma modfact1 (n : ℕ): ((2^(3+n)) : zmod 7).val = (2^n : zmod 7).val :=
begin
  have h2 : (2^3 : zmod 7) = 1 := by refl,
  have h4 : (2^(3+n) : zmod 7).val = (2^3*2^n : zmod 7).val := congr_arg zmod.val (pow_add 2 3 n),
  rwa [h2,one_mul] at h4,
end

lemma modfact2 (n : ℕ)  :  (2^n : zmod 7) = 2 ^ (n : zmod 3).val :=
begin
  sorry,
end

[Yakov Pechersky]

Not very familiar with zmod. But here are two options.

import tactic.basic
import tactic.fin_cases
import data.zmod.basic

lemma modfact2 (n : ℕ)  :  (2^n : zmod 7) = 2 ^ (n : zmod 3).val :=
begin
  set n' := (n : zmod 3) with hn,
  fin_cases n',
  { sorry }, -- 0 case
  { sorry }, -- 1 case
  { sorry }, -- 2 case
end

lemma modfact2' (n : ℕ)  :  (2^n : zmod 7) = 2 ^ (n : zmod 3).val :=
begin
  rcases n with _|_|_|n,
  refl,
  refl,
  refl,
  sorry -- 3+ case
end

[Yakov Pechersky]

You'll probably want to restate modfact1 to be in n + 3 form instead.

[Johan Commelin]

dec_trivial should be able to handle the n < 7 case

[Johan Commelin]

Note that .val is an implementation issue that should be avoided.

[Johan Commelin]

If you want to stay in the nats, maybe 2 ^ n % 7 is what you want.

[Johan Commelin]

@Kenji Nakagawa

lemma modfact2' : ∀ (n : ℕ), n < 7 → (2^n : zmod 7) = 2 ^ (n : zmod 3).val :=
begin
  dec_trivial,
end

[Johan Commelin]

@Kenji Nakagawa

lemma modfact2' : ∀ (n : ℕ), n < 6 → (2^n : zmod 7) = 2 ^ (n : zmod 3).val :=
begin
  dec_trivial,
end

@[simp] lemma zmod.pow_bit0 (n : ℕ) [fact (bit1 n).prime] (k : zmod (bit1 n)) (hk : k ≠ 0) :
  k ^ (bit0 n) = 1 :=
zmod.pow_card_sub_one_eq_one hk

lemma modfact2 (n : ℕ) : (2^n : zmod 7) = 2 ^ (n : zmod 3).val :=
begin
  haveI : fact (nat.prime 7) := by { delta fact, norm_num },
  have h2 : (2 : zmod 7) ≠ 0 := dec_trivial,
  rw ← nat.mod_add_div n 6,
  -- now run `squeeze_simp [h2, pow_add, pow_mul]`
  simp only [h2, pow_add, pow_mul, bit0_zero, one_pow, add_zero, mul_one, zmod.cast_self,
    zmod.pow_bit0, nat.cast_bit0, zero_mul, ne.def, nat.cast_add, not_false_iff, nat.cast_mul],
  apply modfact2',
  apply nat.mod_lt,
  norm_num,
end

[Johan Commelin]

I think that zmod.pow_bit0 should be part of mathlib

[Johan Commelin]

@Mario Carneiro Do you think it makes sense to teach the primality prover of norm_num about fact?

[Kevin Lacker]

this fin_cases is neat. can I somehow use that on a variable n if I just know something like n < 10? (for nats)

[Bryan Gin-ge Chen]

@Kevin Lacker tactic#interval_cases might work better for that use case.

[Kevin Lacker]

ooh interesting

[Kevin Lacker]

just as a sanity check, roughly how many goals should I expect Lean to handle at once. tens? hundreds? thousands? more? less?

[Johan Commelin]

Hmm, I would say < 10. But I don't really know

[Johan Commelin]

Of course it depends immensely on what kind of goals you are talking about

[Kevin Lacker]

i basically have a simple expression of natural numbers, and i want to check that it is nonzero for n = 0 ... 1000

[Kevin Lacker]

but it pegs at 100% cpu whenever i just try to expand this out into 1000 goals

[Kevin Lacker]

well, the compiler can't even really handle 1000 of these proofs each on their own line in a file. so it's probably not going to work to do it via a tactic either....

[Johan Commelin]

@Kevin Lacker please paste some code (and start a new thread :wink:)

[Mario Carneiro]

Johan Commelin said:

Mario Carneiro Do you think it makes sense to teach the primality prover of norm_num about fact?

I think it makes more sense to have a fact.mk

[Mario Carneiro]

the API behind fact is pretty absent

[Johan Commelin]

I mean, it would be nice if it could see through fact, instead of needing to write delta fact; norm_num when prove fact (nat.prime 7)

[Mario Carneiro]

It just uses simp. Should that be a simp lemma?

[Mario Carneiro]

I guess if fact.mk was a simp lemma this would solve the problem

[Johan Commelin]

I guess that would cause other problems. You almost never want to simp fact away.

[Johan Commelin]

Can you do norm_num [extra, simp, lemmas]?

[Mario Carneiro]

Then don't simp a hypothesis

[Mario Carneiro]

yes you can

[Mario Carneiro]

I think if fact.mk, that is p -> fact p was a simp lemma, then it still wouldn't simplify fact away unless it could prove the contents

[Mario Carneiro]

but unless you can find a way to do this with simp I don't think it should go into norm_num. But delta fact is a really ugly way to do it

[Mario Carneiro]

If fact was a one argument structure then you could write <by norm_num>

[Johan Commelin]

Sure, but then you cannot write hp.pos or hp.one_lt etc, for hp : fact p.prime

[Johan Commelin]

  haveI : fact (nat.prime 7) := by norm_num [fact],

[Johan Commelin]

This works (-;

[Mario Carneiro]

you could write hp.1.pos :shrug: