how to use simp

Stream: new members

[Jason Gross]

I have

-- set_option pp.numerals false
example : (3 : ℤ) * (nat.succ 1) = 6 :=
begin
  simp [int.mul,bit0,bit1,has_one.one,int.one,int.add,nat.add,has_add.add,has_mul.mul,int.mul,coe,lift_t,has_lift_t.lift,coe_t,has_coe_t.coe,coe_b,has_coe.coe]
end

I want to simplify the goal until it is 6 = 6 or nat.succ (nat.succ (nat.succ (nat.succ (nat.succ (nat.succ nat.zero)))) = nat.succ (nat.succ (nat.succ (nat.succ (nat.succ (nat.succ nat.zero)))). (I know that I can prove it by reflexivity, but I am using this as a test case for a more complicated goal involving arithmetic expressions that I need to simplify to numerals, where I don't know what the final result is going to be (or where there are too many different possibilities to list out).) If I add either nat.mul or has_zero.zero to this list, then lean times out. How do I finish this simplification?

[Jason Gross]

Also, how do I unfold list.partition._match_1? simp only [list.partition._match_1] seems to just always fail with simplify tactic failed to simplify

[Mario Carneiro]

Use norm_num for goals like this

[Mario Carneiro]

norm_num does arithmetic with numerals; simp doesn't understand numerals and their normal forms

[Mario Carneiro]

Unfolding everything in sight is 99% of the time the wrong thing to do. Lemmas should exist to unfold one definition at a time, and theorems should not have to break through more than two layers of abstraction or so

[Mario Carneiro]

What is the more complex goal you are trying to solve? This looks like an XY problem to me

[Kenny Lau]

can we write a meta-tactic that will use the correct tactic in each situation? :P

[Kevin Buzzard]

It's really hard for an outsider to know the correct tactic. You have some stupid question which involves multiplication by 2 on the naturals and everyone says" Oh, it's Presburger, use omega" or something -- and then you have some other question which involves multiplication too and omega doesn't work and then they say "oh that's not Presburger, but ring will do that one obviously and you say "but the naturals aren't a ring" and they say "yeah but it's shorter than semiring", and then there's another one but neither omega or ring work and it turns out you need linarith. The mathematician proof of all of these is "it's now obvious", and we have difficulty expressing this exasperation in the language of tactics because for you it's several different kinds of obvious.

[Reid Barton]

tidy already basically works like this. We could easily make a differently-configured tidy that just tries norm_num, linarith, ring, omega and shows you what worked (which tidy already knows how to do).

[Scott Morrison]

This is a good idea. It's probably best to call a version of ring that doesn't attempt to rewrite if it fails to close the goal. It may be worth thinking a little about which of these tactics "fail fast", and perhaps improve this.

[Scott Morrison]

But doing this on top of tidy will just be a few lines.

[Scott Morrison]

(On a related note, I have written a few proofs recently leaving the line suggest at the bottom of my begin ... end block as I work, and it can be pretty awesome... "Oh, you're done! That goal too!")

[Kevin Buzzard]

I don't like errors in my code so I often leave sorry at the end of every branch I've not filled in (say I'm in the middle of a big tactic mode proof). Do I just stop using sorry and start using suggest?

[Jason Gross]

I get unknown identifier 'norm_num'(I'm using lean installed from https://github.com/leanprover/lean/releases/download/v3.4.2/lean-3.4.2-linux.tar.gz)

[Kevin Buzzard]

norm_num is a mathlib tactic. Try import tactic.norm_num at the top of your file.

[Jason Gross]

What is the more complex goal you are trying to solve? This looks like an XY problem to me

@Mario Carneiro I'm trying to perf-test lean's tactics for rewriting/partial evaluation on a goal for generating straightline-code for big integer field arithmetic for a fixed prime modulus on a fixed-width platform. In particular, I'm trying to rewrite in this goal until everything except let_in and arithmetic definitions on non-numerals is unfolded, and I will also need to rewrite with this lemma to lift binders so they don't block rewriting/reduction. Additionally, there are a number of places where I'm doing a test on equality of ints which are numerals, and I need to reduce/rewrite/compute the test so that the if statement goes away.

[Rob Lewis]

(On a related note, I have written a few proofs recently leaving the line suggest at the bottom of my begin ... end block as I work, and it can be pretty awesome... "Oh, you're done! That goal too!")

Isn't this super laggy? That's folding over the environment a lot.

[Scott Morrison]

Yes, it's slow, but not as slow as me, so sometimes it has time to say something helpful. :-)

[Scott Morrison]

(This slowness also prompted me to wonder if I could parallelise suggest. Keeley says "maybe".)

[Jason Gross]

I've now installed mathlib, norm_num seems to take forever to finish? (Also, Warning (flycheck): Syntax checker lean-checker reported too many errors (774) and is disabled.)

[Jason Gross]

Also excessive memory consumption detected at 'replace' (potential solution: increase memory consumption threshold) (Edit: or maybe this was left over from a different file)

[Scott Morrison]

Do you know if you've got compiled olean files for mathlib?

[Scott Morrison]

Perhaps can you show us your leanpkg.toml file, and tell us what happens when you run leanpkg build on the command line in the root directory of your project?

[Kevin Buzzard]

Did you install Lean and mathlib and then open a project directory in VS Code with mathlib as a dependency all following the instructions on the mathlib readme?

[Jason Gross]

Ah, it does in fact finish, it just takes 3 minutes to run

[Jason Gross]

I don't seem to have olean files, but am trying leanpkg build now (it seems to be compiling mathlib)

[Jason Gross]

The leanpkg.toml file:

$ leanpkg dump
[package]
name = "fiat-crypto"
version = "0.1"
lean_version = "3.4.2"
path = "src-lean"

[dependencies]
mathlib = {git = "https://github.com/leanprover-community/mathlib.git", rev = "ca9008153aaa6f16c7e2f691231b889dbb05a576"}

[Jason Gross]

(And I'm using emacs, not vscode)

[Jason Gross]

Ah, and now it's much faster, on the order of a couple of seconds

[Jason Gross]

Is there a way to tell norm_num to not unfold some things?

[Kevin Buzzard]

I think norm_num is usually used as a finishing tactic, i.e. you tell it to kill the goal, you don't use it to get half way there. Or do you mean you want it to only work on one goal and it's working on all of them? That happens for some tactics (but I can't remember if norm_num is one of them). Fix with {norm_num} if this is the issue?

[Jason Gross]

No, I want to use something that doesn't finish the goal. Here's a toy example: suppose I have something like if <complicated expression of int> = <other complicated expression of int> then term1 else term2 and I want to reduce this to either term1 or term2, what should I use to reduce the arithmetic on numerals, the decidable equality, and the if-then-else, but leave term1 and term2 mostly untouched (except for where they contain decidable equality / arithmetic as subterms)?

[Kevin Buzzard]

Start with split_ifs?

[Floris van Doorn]

You can probably do something like rw [if_pos], norm_num (unless you also have other if expressions)

[Jason Gross]

split_ifs gives me multiple goals; each decidable equality computes to either true or false. I have multiple ifs, some are true, and others are false. How do I say "rewrite with whichever of if_pos and if_neg can be solved by computing the decidable instance?

[Kevin Buzzard]

can you do split_ifs and then run cases h on the hypotheses h which are false? Or do you want something slicker?

[Jason Gross]

I expect there to be a couple hundred if statements, I don't want a couple thousand goals, especially not if I have to handle them manually...

[Kevin Buzzard]

Oh I see. You need a computer scientist, sorry ;-)

[Jason Gross]

Another question: How do I get norm_num to simplify my new definitions? I noticed there is no int.pow, so I wrote

@[simp]
def int.pow_nat (b : ℤ) (e : ℕ) : ℤ :=
  nat.rec
    1
    (λ _ acc, b * acc)
    e

@[simp]
instance int_has_pow_nat : has_pow int nat := ⟨int.pow_nat⟩

@[simp]
def int.pow (b : ℤ) : ℤ → ℤ
| (int.of_nat n) := b ^ n
| (int.neg_succ_of_nat n) := 0

@[simp]
instance : has_pow int int := ⟨int.pow⟩

but norm_num doesn't simplify it.

[Rob Lewis]

I'll take a look at your earlier questions in a bit and see if I have any hints. For the latest: you can tell norm_num to reduce definitions with square brackets, e.g. norm_num [int.pow]. For your example, that definition of pow_nat will get in the way.

def int.pow_nat (b : ℤ) : ℕ → ℤ
| 0 := 1
| (k+1) := b * int.pow_nat k

instance int_has_pow_nat : has_pow int nat := ⟨int.pow_nat⟩

def int.pow (b : ℤ) : ℤ → ℤ
| (int.of_nat n) := b ^ n
| (int.neg_succ_of_nat n) := 0

instance : has_pow int int := ⟨int.pow⟩

example : (-2 : ℤ)^4 = 16 :=
by norm_num [(^), int.pow, int.pow_nat]

[Rob Lewis]

I don't think the simp attributes you had on the instances will work, will they?

[Jason Gross]

Why is it that norm_num [(^), int.pow, int.pow_nat] works for (-2 : ℤ) ^ 0 but fails to reduce for int.pow (-2 : ℤ) 0?

[Jason Gross]

(re simp on instances: idk, I'm still at the cargo-culting stage in learning lean)

[Jason Gross]

Why is it that neither norm_num nor simp can deal with these definitions?

import tactic.norm_num

def int.pow_nat' (b : ℤ) : ℕ → ℤ
| 0 := 1
| (k+1) := b * int.pow_nat' k

@[simp]
def int.pow_nat_rev (e : ℕ) : ℤ → ℤ
| (int.of_nat b) := int.of_nat (b ^ e)
| (int.neg_succ_of_nat b) := int.pow_nat' (int.neg_succ_of_nat b) e

@[simp]
def int.pow_nat (b : ℤ) (e : ℕ) : ℤ := int.pow_nat_rev e b

example : (int.mod 1 (int.pow_nat 2 16) = 0) :=
begin
  simp [int.mod,int.pow_nat,(^),int.pow_nat_rev]
end
-- 18:1: tactic failed, there are unsolved goals
-- state:
-- ⊢ int.mod 1 (int.pow_nat_rev 16 2) = 0

[Jason Gross]

Hm, and apparently import tactic.norm_num is enough to make simp [(+)] loop

[Jason Gross]

Reported as https://github.com/leanprover-community/mathlib/issues/1637

[Mario Carneiro]

This is a good idea. It's probably best to call a version of ring that doesn't attempt to rewrite if it fails to close the goal.

That would be the ring1 tactic

[Mario Carneiro]

Note that simp can often be made to loop if you have lemmas that disagree about what normal form is

[Mario Carneiro]

you have to not only add a new thing but remove the old one if you want to avoid this

[Mario Carneiro]

I expect that simp [(+)] loops because there is a lemma in the default simp set that re-folds int.add x y to x + y

[Mario Carneiro]

Power on integers is supported in norm_num via monoid.pow. You will have to import algebra.group_power but then you can just write x ^ y where x : Z and y : N

[Jason Gross]

@Mario Carneiro re algebra.group_power: Thanks!

[Mario Carneiro]

I also responded to leanprover-community/lean#76, I don't know if you still want to pursue it

[Jason Gross]

I replied on leanprover-community/lean#76; feel free to do whatever you think makes sense about the issue

[Floris van Doorn]

You might have already figured it out, but the following works:

import algebra.group_power tactic.norm_num

example : 1 % 2 ^ 16 = 0 :=
begin
  norm_num,
end

[Mario Carneiro]

are those integers?

[Floris van Doorn]

Good point, probably not. But the following also reduces to false:

import algebra.group_power tactic.norm_num

example : (1 : ℤ) % 2 ^ 16 = 0 :=
by norm_num

[Kevin Buzzard]

I was looking at "but the following works" and thinking "is that actually _true_ though?" Now I try it I see by "works" Floris means "does not compile" :D

[Floris van Doorn]

"norm_num works", which I think is what the question was. But in my second message I clarified it :)