# Zulip Chat Archive

## Stream: general

### Topic: lean solver

#### John Rowan (Aug 26 2019 at 14:55):

hello I am trying to solve an induction problem but I am getting an error message

theorem test_ind (n : nat) : (3^n -1) % 2 = 0 :=

nat.rec_on n rfl (λ n ih, by simp only [add_succ, ih])

error:

simplify tactic failed to simplify

can someone tell me what I am doing wrong and how to fix it

#### Patrick Massot (Aug 26 2019 at 14:58):

Why would that work?

#### Patrick Massot (Aug 26 2019 at 14:59):

Do you mean `pow_succ`

instead of `add_succ`

?

#### John Rowan (Aug 26 2019 at 15:00):

I am completely new to lean and I am trying to prove that (3^n-1) is divisible by 2 for all natural numbers and I am not really sure of the syntax to write

#### John Rowan (Aug 26 2019 at 15:02):

there is a red line under the keyword simp and I am getting the error simplify tactic failed to simplify

#### John Rowan (Aug 26 2019 at 15:03):

i tried pow_succ and now it is saying tactic failed, there are unsolved goals

#### Patrick Massot (Aug 26 2019 at 15:04):

I'm afraid you are overoptimistic about what can be proven automatically here

#### John Rowan (Aug 26 2019 at 15:05):

so youre saying that this is not possible

#### Patrick Massot (Aug 26 2019 at 15:06):

It's possible, but you'll have to help Lean a bit

#### Patrick Massot (Aug 26 2019 at 15:07):

Do you have the maths library mathlib at hand?

#### John Rowan (Aug 26 2019 at 15:07):

i don't think so, i am totally new to lean

#### Patrick Massot (Aug 26 2019 at 15:08):

You should have a look at the installation instructions at https://github.com/leanprover-community/mathlib/blob/master/README.md

#### John Rowan (Aug 26 2019 at 15:08):

im using vscode

#### John Rowan (Aug 26 2019 at 15:17):

ok i think that it is working because i can #eval things, but how do i go about solving this proof with mathlib?

#### Patrick Massot (Aug 26 2019 at 15:17):

Did you install everything?

#### John Rowan (Aug 26 2019 at 15:18):

i didn't do anything, i just read through the installation page and it said run #eval 1+1 and it should be working and it worked

#### Patrick Massot (Aug 26 2019 at 15:20):

Each OS specific install page ends with a link to https://github.com/leanprover-community/mathlib/blob/master/docs/install/project.md which is OS-independent. Did you make sure that also works?

#### Johan Commelin (Aug 26 2019 at 15:21):

theorem test_ind (n : nat) : (3^n - 1) % 2 = 0 := begin apply nat.mod_eq_zero_of_dvd, induction n with n ih, { simp }, rw [nat.pow_succ], rw show 3^n * 3 - 1 = 3^n - 1 + 3^n * 2, { rw [add_comm, ← nat.add_sub_assoc], { refl }, { apply nat.pow_pos, exact dec_trivial } }, apply dvd_add ih, apply dvd_mul_left end

#### Johan Commelin (Aug 26 2019 at 15:21):

The first thing I do is get rid of the ugly `%`

... I don't know how to deal with it :stuck_out_tongue_wink:

#### John Rowan (Aug 26 2019 at 15:28):

this only problem now is that there is a red squiggly line under apply here { apply nat.pow_pos, exact dec_trivial } but there is no error message

#### John Rowan (Aug 26 2019 at 15:28):

actually there is an error because of it, unknown identifier 'nat.pow_pos'

#### Patrick Massot (Aug 26 2019 at 15:29):

That lemma is probably from mathlib that you don't want to install...

#### Patrick Massot (Aug 26 2019 at 15:48):

Am I missing somewhere to look for

lemma nat.add_mod (x y n : ℕ) : ((x % n) + (y % n)) % n = (x + y) % n := modeq_add (mod_modeq x n) (mod_modeq y n)

#### Patrick Massot (Aug 26 2019 at 15:48):

I can't find it in mathlib. Of course the proof is very short, but the statement is pretty natural for people who, unlike Johan and I, like `%`

#### John Rowan (Aug 26 2019 at 15:52):

i definetly just installed the mathlib and i am still getting an error at apply unknown identifier 'nat.pow_pos' do i have to import something?

#### Patrick Massot (Aug 26 2019 at 15:54):

Anyway, I had a break from Huber rings and wrote:

import tactic.ring import data.nat.modeq open nat.modeq lemma nat.add_mod (x y n : ℕ) : ((x % n) + (y % n)) % n = (x + y) % n := modeq_add (mod_modeq x n) (mod_modeq y n) theorem test_ind (n : nat) : (3^n -1) % 2 = 0 := nat.rec_on n rfl $ λ n ih, calc (3^(n+1) - 1) % 2 = (2*3^n + 3^n - 1) % 2 : by { rw nat.pow_succ, ring } ... = (2*3^n + (3^n - 1)) % 2 : by rw nat.add_sub_assoc (nat.pow_pos _ _) ; norm_num ... = ((2*3^n % 2) + ((3^n - 1) % 2)) % 2 : by rw nat.add_mod ... = 0 : by simp [ih]

Of course this is not really the dream proof. Good automation should take as input only the hint to prove `(3^(n+1) - 1) % 2 = ((2*3^n % 2) + ((3^n - 1) % 2)) % 2`

, prove it automatically, and then take the hint `simp [ih]`

. I'm pretty sure there are proof assistants which can already do that, but this still is a weak point of Lean.

#### Patrick Massot (Aug 26 2019 at 15:56):

In order to get `nat.pow_pos`

you need to import `data.nat.basic`

#### Patrick Massot (Aug 26 2019 at 15:57):

(in my snippet this is imported by transitivity from `data.nat.modeq`

)

#### John Rowan (Aug 26 2019 at 16:01):

ahh thanks both of your code snippets work on my lean now, ill just have to study them a while, try to get the hang of lean and mathlib

#### Patrick Massot (Aug 26 2019 at 16:02):

Did you use the `update-mathlib`

script to make sure you're acting nicely to your computer by having a compiled mathlib?

#### John Rowan (Aug 26 2019 at 16:02):

i tried to do that and i got the command not found error in bash

#### Patrick Massot (Aug 26 2019 at 16:04):

I should also say that the playground you chose (easy property of natural numbers) is actually a tricky one. That's because computer are picky about inclusions of sets of numbers. They make it much harder to ignore the fact that `ℕ`

isn't actually contained in `ℤ`

. Playing with more abstract objects is actually less frustrating

#### Patrick Massot (Aug 26 2019 at 16:04):

What OS are you using?

#### John Rowan (Aug 26 2019 at 16:06):

windows

#### Patrick Massot (Aug 26 2019 at 16:09):

sigh...

#### Patrick Massot (Aug 26 2019 at 16:10):

Maybe you can find some help in the conversation at https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/How.20to.20use.20VSCode.20Extension.3F

#### Jeremy Avigad (Aug 26 2019 at 19:59):

For the record, here a nicer proof:

import data.nat.parity tactic.norm_num theorem test_ind (n : nat) : (3^n -1) % 2 = 0 := have 3^n ≥ 1, by { apply nat.succ_le_of_lt, apply nat.pow_pos, norm_num }, by { rw [←nat.even_iff], simp * with parity_simps }

The `rw`

command changes the goal to `even (3^n-1)`

. The simplifier should have been able to show `3^n ≥ 1`

, in which case it would have been an easy one-liner. (The sticking point is that it can't show `3 > 0`

.) In fact, `parity_simps`

should include `←nat.even_iff`

, so the proof *should* have been `simp with parity_simps`

.

#### Scott Morrison (Aug 27 2019 at 00:21):

Can we use this as an opportunity to make `simp with parity_simps`

work?

#### Scott Morrison (Aug 27 2019 at 00:23):

I’m not near a copy of Lean yet, but does `@[simp] lemma foo (n k : nat) : (n+1)^k \ge 1 \iff true := sorry`

handle the first `have`

?

#### Scott Morrison (Aug 27 2019 at 00:54):

(Found a copy of Lean) It does work. We should definitely add it. It is so much nicer if crap like this could be solved with `simp with parity_simps`

. And indeed even nicer if `simp`

, or a friend, could look at the goal and realize for itself that it should clearly be using `parity_simps`

.

#### Scott Morrison (Aug 27 2019 at 00:56):

Does someone want to do this? We’d need:

#### Scott Morrison (Aug 27 2019 at 00:59):

1. Prove the lemma `foo`

I wrote above, give it a name, and a home in `data.nat.basic`

.

2. In `data.nat.parity`

, add a lemma which is just the reverse of the existing nat.even_iff, and mark it as @[parity_simps].

3. Add an example somewhere `example (n : nat) : (3^n - 1) % 2 = 0 := by simp with parity_simps`

to verify it works.

4. Make your first PR to mathlib. :-)

#### Scott Morrison (Aug 27 2019 at 01:00):

@John Rowan , @Ainsley Pahljina, @Eamon Barrett?

#### Patrick Massot (Aug 27 2019 at 09:43):

This is all very cute, but would fail with more complicated examples, or the same kind of result with `% 3`

instead of `%2`

. I think we must keep in mind the larger goal of making calculations more convenient, especially with natural numbers. We really need more tactics to escape nat subtraction hell. Note that

example (n : ℕ) : (3^(n+1) - 1 : ℤ) = 2*3^n + (3^n - 1) := by ring

works. So we only need a tactic to turn the nat version into that version, with side conditions like `1 <= 3^n`

(and tactics discharging as many such goals as possible). I know Floris has some preliminary work in the direction. This would allow writing the exact same proof we would write on paper.

#### Jeremy Avigad (Aug 27 2019 at 13:55):

@Scott Morrison I didn't think of the `n+1`

trick. That is a good solution. It will let the simpilfier solve some trivial <= goals.

There is another annoyance with the <= / >= notation:

@[simp] lemma foo (n k : nat) : (n+1)^k ≥ 1 ↔ true := sorry example (n : nat) : 3^n ≥ 1 := by simp -- fails example (n : nat) : 1 ≤ 3^n := by simp

We should probably have the simplifier replace >= by <=. Also, the simplifier doesn't need the "iff true" part.

@[simp] lemma bar (m n : nat) : m ≥ n ↔ n ≤ m := iff.rfl @[simp] lemma foo (n k : nat) : 1 ≤ (n+1)^k := by { apply nat.succ_le_of_lt, apply nat.pow_pos, apply nat.succ_pos } example (n : nat) : 3^n ≥ 1 := by simp example (n : nat) : 1 ≤ 3^n := by simp

Also, we should probably have the corresponding theorems for the version of `pow`

in `algebra.group_power`

.

@Patrick Massot The point is well taken. We need better support for calculation on `nat`

.

#### Floris van Doorn (Aug 27 2019 at 15:44):

Agreed, `gt_iff_lt`

and `ge_iff_le`

should become simp lemmas.

#### Floris van Doorn (Aug 27 2019 at 16:09):

Patrick Massot referred to some preliminary code I wrote for this. The idea (that Patrick had) is to move the problem to `int`

and then use `ring`

. The code is below. I use a limited list of simp lemmas to push all casts inside the expression. Does `norm_cast`

provide a tactic/simp-set to do this? I tried to make a simp set from the `move_cast`

cache, or from all `move_cast`

instances, and neither really moves all casts inside.

#### Floris van Doorn (Aug 27 2019 at 16:09):

import tactic.ring import data.nat.modeq section local attribute [instance, priority 0] int.has_coe local attribute [instance, priority 99] nat.cast_coe theorem int.nat_cast_mod {m n : ℕ} : ((m % n : ℕ) : ℤ) = (m : ℤ) % n := by simp end lemma int.add_mod (x y n : ℤ) : ((x % n) + (y % n)) % n = (x + y) % n := sorry open tactic interactive meta def my_simp_list : tactic (list simp_arg_type) := [`nat.cast_bit0, `nat.cast_bit1, `nat.cast_add, `nat.cast_one, `nat.cast_mul, `nat.cast_pow, `int.nat_cast_mod, `nat.cast_zero].mmap $ λ n, simp_arg_type.expr <$> pexpr.of_expr <$> mk_const n meta def move_to_int : tactic unit := do apply `(@nat.cast_injective ℤ _ _), repeat (my_simp_list >>= λ l, interactive.simp none tt l [] (loc.ns [none]) >> repeat (mk_const `nat.cast_sub >>= rewrite_target)) theorem test_ind (n : nat) : (3^n -1) % 2 = 0 := begin move_to_int, induction n with n ih, { simp }, { exact calc ((3:ℤ)^(n+1) - 1) % 2 = ((2*3^n % 2) + ((3^n - 1) % 2)) % 2 : by { simp only [int.add_mod], ring } ... = (0:ℤ) : by simp [-sub_eq_add_neg, ih] }, apply nat.succ_le_of_lt, apply nat.pow_pos, norm_num end

#### Floris van Doorn (Aug 27 2019 at 16:11):

There are two instances of `has_coe nat int`

. The one which we use everywhere is `int.has_coe`

instead of the more general `nat.cast_coe`

. Is the reason for this for performance? Because otherwise it would be nicer to always use the general coercion (now we have to prove all coercion-lemmas twice).

#### Mario Carneiro (Aug 27 2019 at 20:24):

Two reasons: (1) It's faster: it is O(1) where the general cast is exponential; (2) it is forced on us by core - `int.has_coe`

is declared in core and you get it whenever you write the `\u`

without additional adornment. Thinking about it now, we should be able to solve this with a priority setting.

#### Floris van Doorn (Aug 28 2019 at 14:38):

Yes, I was thinking about a priority setting (and reordering `nat_cast_eq_coe_nat`

). When you say it is faster, do you mean computation in the VM or type-class inference search? If it's computation in the VM then we should keep the status quo. Proving all lemmas twice isn't that bad.

#### Mario Carneiro (Aug 28 2019 at 17:25):

it is a faster function for the VM

#### Scott Morrison (Sep 09 2019 at 04:21):

We should probably have the simplifier replace >= by <=.

@Jeremy Avigad, I just made #1418, which does this. I think it will open the way to making `simp`

much stronger at inequalities.

#### Jeremy Avigad (Sep 09 2019 at 14:49):

Thanks for doing that. I think it is the right way to go. I'll merge in a day or two if nobody objects.

Last updated: May 17 2021 at 21:12 UTC