# Zulip Chat Archive

## Stream: new members

### Topic: Simplifying pattern matches

#### Plam (Mar 05 2019 at 14:17):

I observe different behaviour in the simplifier that depends on if I use my own `add`

or Lean's native `add`

. I've done my best to make my add match Lean's (found here: https://github.com/leanprover/lean/blob/ceacfa7445953cbc8860ddabc55407430a9ca5c3/library/init/core.lean#L399-L405)

In particular, the simplify tactic fails to simplify with my own `add`

. Here's code using my `add`

:

namespace hidden def add : ℕ → ℕ → ℕ | m 0 := m | m (nat.succ n) := nat.succ (add m n) local infix ` + ` := add local attribute [pattern] add def mult (m : ℕ) : ℕ → ℕ | 0 := 0 | (n + 1) := mult n + m local infix `*` := mult def exp (m : ℕ) : ℕ → ℕ | 0 := 1 | (n + 1) := m * exp n local infix `^` := exp theorem exp_zero_one : ∀ m, m ^ 0 = 1 := by {intros, refl} theorem exp_one_self : ∀ m, m ^ 1 = m | 0 := rfl | (n + 1) := begin simp only [exp] end end hidden

From this I get `simplify tactic failed to simplify`

. Simply removing my definition of `add`

(code below) lets the simplifier advance to `(n + 1)*1 = n + 1`

namespace hidden def mult (m : ℕ) : ℕ → ℕ | 0 := 0 | (n + 1) := mult n + m local infix `*` := mult def exp (m : ℕ) : ℕ → ℕ | 0 := 1 | (n + 1) := m * exp n local infix `^` := exp theorem exp_zero_one : ∀ m, m ^ 0 = 1 := by {intros, refl} theorem exp_one_self : ∀ m, m ^ 1 = m | 0 := rfl | (n + 1) := begin simp only [exp] end end hidden

#### Johan Commelin (Mar 05 2019 at 14:58):

@Plam The simplifier doesn't use magic. It simplifies expressions using lemmas that are tagged with `@[simp]`

in front of them. Since you didn't write any such lemmas for your own `add`

, the simplifier doesn't help you...

#### Plam (Mar 05 2019 at 14:58):

Hm. I thought using `simp only`

would avoid those lemmas being used. Is that not the case?

#### Wojciech Nawrocki (Mar 05 2019 at 15:12):

By default, `simp`

will try to simplify the goal using all available lemmas marked with `@[simp]`

. `simp only [h1, h2, ..]`

will not use any of those, but only the lemmas `h1, h2, ..`

that you provide. However, `exp`

does not seem to be a simplification lemma, as those are usually of the form `complicated_expression = simplified_expression`

(the ordering matters - the left side should be the more complicated one). In your case, `exp`

is the definition of exponentiation and I'm not sure if `simp`

can use that. You could try using `unfold exp`

to expand the definition of `exp`

. *EDIT*: Oh, it seems it can use that, fair enough. Still, you will need to provide more lemmas so that the whole expression can be simplified, as just `exp`

is not enough. Marking some lemmas with `@[simp]`

is the preferred way of doing this.

#### Plam (Mar 05 2019 at 15:21):

Thanks for the guidance! Yep, `exp`

is not enough. What I'm confused about is what I need to add to `add`

to make it behave like the Lean add when simplifying. In particular, changing `exp`

to pattern match on `(nat.succ n) rather than `

(n + 1)` makes the two cases behave the same.

(In both below proofs I am using `simp only`

)

Here is a working proof:

namespace hidden def add : ℕ → ℕ → ℕ | m 0 := m | m (nat.succ n) := nat.succ (add m n) instance : has_add ℕ := ⟨add⟩ attribute [pattern] add def mult (m : ℕ) : ℕ → ℕ | 0 := 0 | (n + 1) := mult n + m local infix `*` := mult def exp (m : ℕ) : ℕ → ℕ | 0 := 1 | (nat.succ n) := m * exp n local infix `^` := exp theorem mult_one : ∀ n, n * 1 = n := sorry theorem exp_one_self : ∀ m, m ^ 1 = m | 0 := rfl | (n + 1) := begin simp only [exp, mult_one] end end hidden

Here is a failed proof:

namespace hidden def add : ℕ → ℕ → ℕ | m 0 := m | m (nat.succ n) := nat.succ (add m n) instance : has_add ℕ := ⟨add⟩ attribute [pattern] add def mult (m : ℕ) : ℕ → ℕ | 0 := 0 | (n + 1) := mult n + m local infix `*` := mult def exp (m : ℕ) : ℕ → ℕ | 0 := 1 | (n +1) := m * exp n local infix `^` := exp theorem mult_one : ∀ n, n * 1 = n := sorry theorem exp_one_self : ∀ m, m ^ 1 = m | 0 := rfl | (n + 1) := begin simp only [exp, mult_one] end end hidden

The only difference is defining the inductive case of `exp`

on `(nat.succ n)`

vs `(n + 1)`

#### Plam (Mar 05 2019 at 15:23):

BTW, on the being able to use `exp`

in the simplifier, I believe this is because of magical trickery on the part of the equation compiler: "The example above shows that [some defining equations] hold definitionally [...].

The equation compiler tries to ensure that this holds whenever possible, as is the case with straightforward structural induction. In other situations, however, reductions hold only propositionally, which is to say, they are equational theorems that must be applied explicitly. The equation compiler generates such theorems internally. They are not meant to be used directly by the user; rather, the simp and rewrite tactics are configured to use them when necessary."

#### Kevin Buzzard (Mar 05 2019 at 17:27):

This is hellish to work with because Lean already has an instance of `has_add nat`

#### Kevin Buzzard (Mar 05 2019 at 17:31):

def mult (m : ℕ) : ℕ → ℕ | 0 := 0 | (n + 1) := mult n + m

I think the `(n + 1)`

is Lean's add, and the `mult n + m`

is your add. This is madness!

#### Kevin Buzzard (Mar 05 2019 at 17:32):

I think I would recommend rolling your own nat.

#### Plam (Mar 05 2019 at 17:34):

OK. Happy to avoid rolling my own nat, but just to check: if there weren't already duplicate definitions floating around, using `pattern`

on add would let me pattern match in that way?

#### Kevin Buzzard (Mar 05 2019 at 17:36):

The equation compiler wants to use Lean's inductive definition of nat. So it wants you to define things for zero and succ. If there weren't duplicate definitions then yes you can use `pattern`

to make the equation compiler look nicer.

#### Kevin Buzzard (Mar 05 2019 at 17:36):

But for your failed proof it's really hard to make any progress

#### Kevin Buzzard (Mar 05 2019 at 17:39):

def exp (m : ℕ) : ℕ → ℕ | 0 := 1 | (n + 1) := m * exp n #print prefix hidden.exp

Insert that after your definition of `exp`

.

#### Kevin Buzzard (Mar 05 2019 at 17:39):

There you can see the secret equations which Lean will use when you write `simp only [exp]`

.

#### Kevin Buzzard (Mar 05 2019 at 17:40):

But `rw hidden.exp.equations._eqn_2`

fails, because it is looking for `exp m (n + 1) = m*exp m n`

where that `+`

is, I believe, Lean's `+`

on nat.

#### Kevin Buzzard (Mar 05 2019 at 17:41):

Oh no I'm wrong

#### Kevin Buzzard (Mar 05 2019 at 17:42):

def exp (m : ℕ) : ℕ → ℕ | 0 := 1 | (n + 1) := m * exp n set_option pp.all true #print prefix hidden.exp

#### Kevin Buzzard (Mar 05 2019 at 17:42):

`hidden.exp.equations._eqn_2`

is using your add.

#### Kevin Buzzard (Mar 05 2019 at 17:45):

theorem exp_one_self : ∀ m, m ^ 1 = m | 0 := rfl | (n + 1) := begin -- goal (n + 1)^1 = n + 1 show hidden.exp (@has_add.add.{0} nat hidden.has_add n (@has_one.one.{0} nat nat.has_one)) (@has_add.add.{0} nat hidden.has_add (@has_zero.zero.{0} nat nat.has_zero) (@has_one.one.{0} nat nat.has_one)) = n + 1, rw hidden.exp.equations._eqn_2 (n + 1) 0, -- progress! sorry end end hidden

#### Plam (Mar 05 2019 at 17:46):

It even doesn't work with lots of renaming:

namespace hidden def my_add : ℕ → ℕ → ℕ | m 0 := m | m (nat.succ n) := nat.succ (my_add m n) precedence `&` : 1 infix `&` := my_add attribute [pattern] my_add def mult (m : ℕ) : ℕ → ℕ | 0 := 0 | (n & 1) := mult n & m local infix `*` := mult def exp (m : ℕ) : ℕ → ℕ | 0 := 1 | (n & 1) := m * exp n local infix `^` := exp theorem mult_one : ∀ n, n * 1 = n := sorry theorem exp_one_self : ∀ m, m ^ 1 = m | 0 := rfl | (n & 1) := begin simp only [exp, mult_one] end end hidden

#### Kevin Buzzard (Mar 05 2019 at 17:46):

I managed to convert the goal into `(n + 1)*(n + 1)^0 = n + 1`

.

#### Plam (Mar 05 2019 at 17:46):

Oh, cool! Lemme have a look

#### Kevin Buzzard (Mar 05 2019 at 17:49):

`instance : has_add ℕ := ⟨add⟩`

. This is not using Lean correctly, really. Lean already has an instance of `has_add nat`

and you've defined a second one. Now you don't really know which one Lean will use. The problem is that nat has a bunch of structure and you are attempting to over-ride parts of that structure, but you have not done it cleverly enough to over-ride Lean's underlying trust that you're using structures and instances sensibly. This might be possible, but you'll probably have to talk to a computer scientist about how to make it work. By far the easiest fix is to roll your own nat, it seems to me.

#### Plam (Mar 05 2019 at 17:51):

Good to know. I hadn't got to the sections on type classes yet -- thought there might be clever ways not to have them be unique in Lean. Still curious why my version above with `&`

doesn't work!

#### Kevin Buzzard (Mar 05 2019 at 17:55):

Your simp fails because this already fails:

theorem exp_one_self : ∀ m, m ^ 1 = m | 0 := rfl | (n & 1) := begin rw hidden.exp.equations._eqn_2 (n&1) 0, end

#### Kevin Buzzard (Mar 05 2019 at 17:57):

I think.

#### Plam (Mar 05 2019 at 18:00):

Hm. Looks like I maybe misunderstood pattern matching -- it's not picking apart the exponent in terms of `&`

like I'd expected. This works:

theorem exp_one_self : ∀ m, m ^ 1 = m | 0 := rfl | (n & 1) := begin have : 1 = (0&1) := rfl, rw this, rw hidden.exp.equations._eqn_2 (n&(0&1)) 0, rw exp, rw mult_one end

#### Kevin Buzzard (Mar 05 2019 at 18:01):

I think that what `simp only [exp]`

does under the hood is that it thinks "OK so I have these two equation lemmas, let's try and get one of them to work. Let's take a look at what we have here". Your equation lemmas tell us what `m^0`

and what `m^(n&1)`

evaluate to. But Lean sees `m^1`

, so it thinks "OK, so what is this 1? OK so I know it's a nat, so it's either 0 or succ of something. Aah, in fact I know what 1 is, it's succ 0, so this is great, hopefully there's an equation lemma mentioning `m^(nat.succ n)`

...aww crap, the user has done something really weird with making `&`

a pattern and I am completely confused. Why didn't he use normal pattern matching with 0 and succ like the equation compiler does by default? I give up"

#### Kevin Buzzard (Mar 05 2019 at 18:02):

The equation compiler knows that nats are built using 0 and succ, but you have managed to persuade the equation compiler to build something using 0 and `&`

, and then its inbuilt algorithms in `simp`

get confused.

#### Kevin Buzzard (Mar 05 2019 at 18:03):

All of this can be fixed if you roll your own nat, because then the equation compiler will be expecting what you will give it by default.

#### Plam (Mar 05 2019 at 18:08):

Doesn't your model predict that if I defined my own nats and then define a my_add and a pattern for them and then defined exp in terms of that pattern, it would still get confused? And if that's true, why doesn't it get confused when I define exp in terms of _normal_ (+), which is, after all, a pattern?

#### Kevin Buzzard (Mar 05 2019 at 18:21):

My understanding is certainly partially confused yes, but I know for sure that if you define your own nat then it works like a dream, because I wrote that blog post I cited earlier, and it's not working for you, and you're definitely doing something unexpected because you have made the equation compiler generate unhelpful lemmas as opposed to helpful ones.

#### Plam (Mar 05 2019 at 18:24):

Gotcha. I guess the lesson is to steer clear of stomping on the builtins. Thanks for the help btw!

#### Kevin Buzzard (Mar 05 2019 at 18:25):

Your patterns managed to get the equation compiler to generate some funky equation lemmas, and that seemed to be your downfall.

#### Kevin Buzzard (Mar 05 2019 at 18:33):

So looking back, at least some of what I'm saying makes some sense. I should say that I have no idea how the equation compiler works and I've never looked at the Lean source code. But when you defined `exp`

using (nat.succ) you get the right equation lemmas:

namespace hidden def add : ℕ → ℕ → ℕ | m 0 := m | m (nat.succ n) := nat.succ (add m n) instance : has_add ℕ := ⟨add⟩ attribute [pattern] add def mult (m : ℕ) : ℕ → ℕ | 0 := 0 | (n + 1) := mult n + m local infix `*` := mult def exp (m : ℕ) : ℕ → ℕ | 0 := 1 | (nat.succ n) := m * exp n #print prefix hidden.exp /- hidden.exp.equations._eqn_1 : ∀ (m : ℕ), exp m 0 = 1 hidden.exp.equations._eqn_2 : ∀ (m n : ℕ), exp m (nat.succ n) = m*exp m n -/ def exp' (m : ℕ) : ℕ → ℕ | 0 := 1 | (n +1) := m * exp' n #print prefix hidden.exp' /- hidden.exp'.equations._eqn_1 : ∀ (m : ℕ), exp' m 0 = 1 hidden.exp'.equations._eqn_2 : ∀ (m n : ℕ), exp' m (n + 1) = m*exp' m n -/ -- and what is that `n + 1` exactly? set_option pp.notation false set_option pp.implicit true #print prefix hidden.exp' /- hidden.exp'.equations._eqn_1 : ∀ (m : nat), @eq nat (exp' m 0) 1 hidden.exp'.equations._eqn_2 : ∀ (m n : nat), @eq nat (exp' m (@has_add.add nat hidden.has_add n 1)) (mult m (exp' m n)) -/ -- it's `hidden.add n 1` end hidden

Using your hidden add as a pattern you can over-ride the choice Lean wants to make, and it seems that the upshot is that you get equation lemmas which the simplifier can't use, for some reason I do not fully understand because I do not really know how the simplifier works other than the fact that I know `simp [exp]`

tries to use the equation lemmas.

#### Plam (Mar 05 2019 at 18:40):

Fiddling with this is in the `&`

case I suspect the issue could be desugaring of numerals. Maybe `1`

gets converted straight to `nat.succ n`

and so never goes through `my_add`

. Not sure though

#### Kevin Buzzard (Mar 05 2019 at 19:23):

set_option pp.numerals false #check 1 -- has_one.one ℕ : ℕ definition X : has_one ℕ := by apply_instance #print X -- nat.has_one #print nat.has_one -- one := nat.succ nat.zero

#### Kevin Buzzard (Mar 05 2019 at 19:41):

1 is indeed succ zero

Last updated: May 17 2021 at 21:12 UTC