Strange behavior of “match with”, won’t find “_match”

Stream: general

[Mario Weitzer]

I was trying to define a has_add instance for lists without using an auxiliary function and noticed a strange behavior of "match with". First I tried a one-liner in term mode which works fine:

namespace hidden

class has_add (α : Type*) :=
(add : α → α → α)

def add {α : Type*} [has_add α] : α → α → α := has_add.add

notation a ` +' ` b := add a b

instance nat_has_add : has_add nat :=
has_add.mk nat.add

instance list_has_add {α : Type u} [has_add α] : has_add (list α) :=
has_add.mk
(λ l₁, list.rec_on l₁
  (λ l₂, l₂)
  (λ hd₁ tl₁ ih₁,
    λ l₂, list.cases_on l₂
      (hd₁ :: tl₁)
      (λ hd₂ tl₂, (hd₁ +' hd₂) :: (ih₁ tl₂))))

#reduce [1, 2, 3] +' [4, 5, 6] --[5, 7, 9]
#reduce [1, 2, 3] +' [4, 5]    --[5, 7, 3]
#reduce [1, 2] +' [4, 5, 6]    --[5, 7, 6]

Then I tried to do the same thing with patter matching and using an auxiliary function this also works without problems:

def list_add {α : Type u} {hadd : has_add α} : list α → list α → list α
| list.nil list.nil := list.nil
| list.nil (hd₂ :: tl₂) := hd₂ :: tl₂
| (hd₁ :: tl₁) list.nil := hd₁ :: tl₁
| (hd₁ :: tl₁) (hd₂ :: tl₂) := (hd₁ +' hd₂) :: (list_add tl₁ tl₂)

instance list_has_add {α : Type u} [ha : has_add α] : has_add (list α) :=
has_add.mk (@list_add α ha)

However, if I don't want to use an auxiliary function I need to use "match with" (I think) because I need to invoke the constructor of has_add, and here I noticed a strange behavior I can't explain:

instance list_has_add {α : Type u} [has_add α] : has_add (list α) :=
has_add.mk
(λ l₁ l₂, match l₁, l₂ with
| list.nil, list.nil := list.nil
| list.nil, (hd₂ :: tl₂) := hd₂ :: tl₂
| (hd₁ :: tl₁), list.nil := hd₁ :: tl₁
| (hd₁ :: tl₁), (hd₂ :: tl₂) := by exact (hd₁ +' hd₂) :: (_match tl₁ tl₂) --This works
--| (hd₁ :: tl₁), (hd₂ :: tl₂) := (hd₁ +' hd₂) :: (_match tl₁ tl₂) --but this does not (it won't find _match in term mode)
end)

The same holds true if I define the auxiliary function using "match with":

def list_add {α : Type u} {hadd : has_add α} : list α → list α → list α :=
λ l₁ l₂, match l₁, l₂ with
| list.nil, list.nil := list.nil
| list.nil, (hd₂ :: tl₂) := hd₂ :: tl₂
| (hd₁ :: tl₁), list.nil := hd₁ :: tl₁
| (hd₁ :: tl₁), (hd₂ :: tl₂) := by exact (hd₁ +' hd₂) :: (_match tl₁ tl₂) --This works
--| (hd₁ :: tl₁), (hd₂ :: tl₂) := (hd₁ +' hd₂) :: (_match tl₁ tl₂) --but this does not (it won't find _match in term mode)
end

instance list_has_add {α : Type u} [ha : has_add α] : has_add (list α) :=
has_add.mk (@list_add α ha)

Does anybody know why term mode and tactic mode make a difference here? Also, how can I choose a different name for "_match"?

[Kyle Miller]

Match expressions are elaborated by creating an auxiliary definition, which is why you find there is a _match function. Lean 3 doesn't support recursive definitions with expressions. I would suggest creating an auxiliary definition using pattern matching yourself like in your second example.

As to why you can use tactics to see the auxiliary _match, tactic blocks defer their elaboration until later -- either when there's nothing left to do or when something forces all pending tactics to evaluate. Presumably here the block is being deferred to when the auxiliary definition is being defined. I don't think you can rely on this. I haven't checked, but I suspect a well-placed let would break it.

[Mario Weitzer]

I see, thanks!