## Stream: new members

### Topic: easy zmod proof

#### Kenji Nakagawa (Oct 01 2020 at 05:39):

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 (Oct 01 2020 at 05:57):

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 (Oct 01 2020 at 06:05):

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

#### Johan Commelin (Oct 01 2020 at 06:06):

dec_trivial should be able to handle the n < 7 case

#### Johan Commelin (Oct 01 2020 at 06:11):

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

#### Johan Commelin (Oct 01 2020 at 06:11):

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

#### Johan Commelin (Oct 01 2020 at 06:14):

@Kenji Nakagawa

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


#### Johan Commelin (Oct 01 2020 at 06:28):

@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,
-- now run squeeze_simp [h2, pow_add, pow_mul]
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 (Oct 01 2020 at 06:28):

I think that zmod.pow_bit0 should be part of mathlib

#### Johan Commelin (Oct 01 2020 at 06:29):

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

#### Kevin Lacker (Oct 01 2020 at 06:30):

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 (Oct 01 2020 at 06:32):

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

ooh interesting

#### Kevin Lacker (Oct 01 2020 at 06:33):

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

#### Johan Commelin (Oct 01 2020 at 06:39):

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

#### Johan Commelin (Oct 01 2020 at 06:39):

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

#### Kevin Lacker (Oct 01 2020 at 06:44):

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

#### Kevin Lacker (Oct 01 2020 at 06:45):

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

#### Kevin Lacker (Oct 01 2020 at 06:58):

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 (Oct 01 2020 at 06:59):

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

#### Mario Carneiro (Oct 01 2020 at 17:14):

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 (Oct 01 2020 at 17:15):

the API behind fact is pretty absent

#### Johan Commelin (Oct 01 2020 at 17:18):

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 (Oct 01 2020 at 17:38):

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

#### Mario Carneiro (Oct 01 2020 at 17:39):

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

#### Johan Commelin (Oct 01 2020 at 17:40):

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

#### Johan Commelin (Oct 01 2020 at 17:41):

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

#### Mario Carneiro (Oct 01 2020 at 17:41):

Then don't simp a hypothesis

yes you can

#### Mario Carneiro (Oct 01 2020 at 17:42):

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 (Oct 01 2020 at 17:43):

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 (Oct 01 2020 at 17:44):

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

#### Johan Commelin (Oct 01 2020 at 17:48):

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

#### Johan Commelin (Oct 01 2020 at 17:49):

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


This works (-;

#### Mario Carneiro (Oct 01 2020 at 17:49):

you could write hp.1.pos :shrug:

Last updated: Dec 20 2023 at 11:08 UTC