Zulip Chat Archive

Stream: general

Topic: lean solver


view this post on Zulip 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

view this post on Zulip Patrick Massot (Aug 26 2019 at 14:58):

Why would that work?

view this post on Zulip Patrick Massot (Aug 26 2019 at 14:59):

Do you mean pow_succ instead of add_succ?

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip John Rowan (Aug 26 2019 at 15:03):

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

view this post on Zulip Patrick Massot (Aug 26 2019 at 15:04):

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

view this post on Zulip John Rowan (Aug 26 2019 at 15:05):

so youre saying that this is not possible

view this post on Zulip Patrick Massot (Aug 26 2019 at 15:06):

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

view this post on Zulip Patrick Massot (Aug 26 2019 at 15:07):

Do you have the maths library mathlib at hand?

view this post on Zulip John Rowan (Aug 26 2019 at 15:07):

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

view this post on Zulip 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

view this post on Zulip John Rowan (Aug 26 2019 at 15:08):

im using vscode

view this post on Zulip 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?

view this post on Zulip Patrick Massot (Aug 26 2019 at 15:17):

Did you install everything?

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip 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:

view this post on Zulip 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

view this post on Zulip John Rowan (Aug 26 2019 at 15:28):

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

view this post on Zulip Patrick Massot (Aug 26 2019 at 15:29):

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

view this post on Zulip 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)

view this post on Zulip 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 %

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip Patrick Massot (Aug 26 2019 at 15:56):

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

view this post on Zulip Patrick Massot (Aug 26 2019 at 15:57):

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

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip John Rowan (Aug 26 2019 at 16:02):

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

view this post on Zulip 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

view this post on Zulip Patrick Massot (Aug 26 2019 at 16:04):

What OS are you using?

view this post on Zulip John Rowan (Aug 26 2019 at 16:06):

windows

view this post on Zulip Patrick Massot (Aug 26 2019 at 16:09):

sigh...

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Scott Morrison (Aug 27 2019 at 00:21):

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

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip Scott Morrison (Aug 27 2019 at 00:56):

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

view this post on Zulip 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. :-)

view this post on Zulip Scott Morrison (Aug 27 2019 at 01:00):

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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Floris van Doorn (Aug 27 2019 at 15:44):

Agreed, gt_iff_lt and ge_iff_le should become simp lemmas.

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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_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).

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Mario Carneiro (Aug 28 2019 at 17:25):

it is a faster function for the VM

view this post on Zulip 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.

view this post on Zulip 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