## 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
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 ints 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 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 (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

#### 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