Simplifying pattern matches

Stream: new members

[Plam]

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]

@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]

Hm. I thought using simp only would avoid those lemmas being used. Is that not the case?

[Wojciech Nawrocki]

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]

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]

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]

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

[Kevin Buzzard]

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]

I think I would recommend rolling your own nat.

[Plam]

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]

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]

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

[Kevin Buzzard]

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

#print prefix hidden.exp

Insert that after your definition of exp.

[Kevin Buzzard]

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

[Kevin Buzzard]

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]

Oh no I'm wrong

[Kevin Buzzard]

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

set_option pp.all true
#print prefix hidden.exp

[Kevin Buzzard]

hidden.exp.equations._eqn_2 is using your add.

[Kevin Buzzard]

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]

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]

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

[Plam]

Oh, cool! Lemme have a look

[Kevin Buzzard]

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]

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]

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]

I think.

[Plam]

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]

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]

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]

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]

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]

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]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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]

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]

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]

1 is indeed succ zero