# Zulip Chat Archive

## Stream: new members

### Topic: how to use simp

#### Jason Gross (Oct 30 2019 at 06:30):

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 (Oct 30 2019 at 06:50):

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 (Oct 30 2019 at 07:34):

Use `norm_num`

for goals like this

#### Mario Carneiro (Oct 30 2019 at 07:35):

`norm_num`

does arithmetic with numerals; `simp`

doesn't understand numerals and their normal forms

#### Mario Carneiro (Oct 30 2019 at 07:37):

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 (Oct 30 2019 at 07:38):

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

#### Kenny Lau (Oct 30 2019 at 13:25):

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

#### Kevin Buzzard (Oct 30 2019 at 15:00):

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 (Oct 30 2019 at 15:22):

`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 (Oct 30 2019 at 16:48):

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 (Oct 30 2019 at 16:48):

But doing this on top of `tidy`

will just be a few lines.

#### Scott Morrison (Oct 30 2019 at 16:49):

(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 (Oct 30 2019 at 17:16):

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 (Oct 30 2019 at 17:20):

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 (Oct 30 2019 at 17:21):

`norm_num`

is a mathlib tactic. Try `import tactic.norm_num`

at the top of your file.

#### Jason Gross (Oct 30 2019 at 17:26):

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 `int`

s which are numerals, and I need to reduce/rewrite/compute the test so that the `if`

statement goes away.

#### Rob Lewis (Oct 30 2019 at 17:26):

(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 (Oct 30 2019 at 17:35):

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

#### Scott Morrison (Oct 30 2019 at 17:37):

(This slowness also prompted me to wonder if I could parallelise `suggest`

. Keeley says "maybe".)

#### Jason Gross (Oct 30 2019 at 19:19):

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 (Oct 30 2019 at 19:20):

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 (Oct 30 2019 at 19:21):

Do you know if you've got compiled `olean`

files for mathlib?

#### Scott Morrison (Oct 30 2019 at 19:21):

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 (Oct 30 2019 at 19:22):

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 (Oct 30 2019 at 19:27):

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

#### Jason Gross (Oct 30 2019 at 19:28):

I don't seem to have olean files, but am trying `leanpkg build`

now (it seems to be compiling mathlib)

#### Jason Gross (Oct 30 2019 at 19:28):

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 (Oct 30 2019 at 19:29):

(And I'm using emacs, not vscode)

#### Jason Gross (Oct 30 2019 at 19:29):

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

#### Jason Gross (Oct 30 2019 at 19:30):

Is there a way to tell `norm_num`

to not unfold some things?

#### Kevin Buzzard (Oct 30 2019 at 19:37):

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 (Oct 30 2019 at 19:41):

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 (Oct 30 2019 at 19:43):

Start with `split_ifs`

?

#### Floris van Doorn (Oct 30 2019 at 19:45):

You can probably do something like `rw [if_pos], norm_num`

(unless you also have other `if`

expressions)

#### Jason Gross (Oct 30 2019 at 19:47):

`split_ifs`

gives me multiple goals; each decidable equality computes to either true or false. I have multiple `if`

s, 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 (Oct 30 2019 at 19:49):

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 (Oct 30 2019 at 19:50):

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 (Oct 30 2019 at 19:50):

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

#### Jason Gross (Oct 30 2019 at 20:05):

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 (Oct 30 2019 at 20:13):

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 (Oct 30 2019 at 20:15):

I don't think the `simp`

attributes you had on the instances will work, will they?

#### Jason Gross (Oct 30 2019 at 20:19):

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 (Oct 30 2019 at 20:19):

(re `simp`

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

#### Jason Gross (Oct 30 2019 at 21:19):

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 (Oct 30 2019 at 21:22):

Hm, and apparently `import tactic.norm_num`

is enough to make `simp [(+)]`

loop

#### Jason Gross (Oct 30 2019 at 21:25):

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

#### Mario Carneiro (Oct 30 2019 at 22:57):

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 (Oct 30 2019 at 23:04):

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

#### Mario Carneiro (Oct 30 2019 at 23:04):

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

#### Mario Carneiro (Oct 30 2019 at 23:05):

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 (Oct 30 2019 at 23:06):

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 (Oct 30 2019 at 23:32):

@Mario Carneiro re `algebra.group_power`

: Thanks!

#### Mario Carneiro (Oct 30 2019 at 23:33):

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

#### Jason Gross (Oct 30 2019 at 23:43):

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

#### Floris van Doorn (Oct 30 2019 at 23:48):

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 (Oct 30 2019 at 23:48):

are those integers?

#### Floris van Doorn (Oct 30 2019 at 23:49):

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 (Oct 30 2019 at 23:50):

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 (Oct 30 2019 at 23:51):

"`norm_num`

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

Last updated: May 14 2021 at 00:42 UTC