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: Dec 20 2023 at 11:08 UTC