lean solver

Stream: general

[John Rowan]

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]

Why would that work?

[Patrick Massot]

Do you mean pow_succ instead of add_succ?

[John Rowan]

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]

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

[John Rowan]

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

[Patrick Massot]

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

[John Rowan]

so youre saying that this is not possible

[Patrick Massot]

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

[Patrick Massot]

Do you have the maths library mathlib at hand?

[John Rowan]

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

[Patrick Massot]

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

[John Rowan]

im using vscode

[John Rowan]

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]

Did you install everything?

[John Rowan]

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]

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]

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]

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]

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]

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

[Patrick Massot]

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

[Patrick Massot]

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]

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]

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]

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]

In order to get nat.pow_pos you need to import data.nat.basic

[Patrick Massot]

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

[John Rowan]

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]

Did you use the update-mathlib script to make sure you're acting nicely to your computer by having a compiled mathlib?

[John Rowan]

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

[Patrick Massot]

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]

What OS are you using?

[John Rowan]

windows

[Patrick Massot]

sigh...

[Patrick Massot]

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]

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]

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

[Scott Morrison]

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]

(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]

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

[Scott Morrison]

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]

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

[Patrick Massot]

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]

@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]

Agreed, gt_iff_lt and ge_iff_le should become simp lemmas.

[Floris van Doorn]

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]

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]

There are two instances of has_coe nat int. The one which we use everywhere is int.has_coeinstead 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]

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]

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]

it is a faster function for the VM

[Scott Morrison]

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]

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