# Zulip Chat Archive

## 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,
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 (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.

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

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

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

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],
```

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

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