failing to unfold an inductive definition

Stream: general

[Scott Morrison]

I'm trying to prove

import data.list.basic

variable (α : Type)
variable [decidable_eq α]

open list

@[simp] theorem count_bag_inter {a : α} :
  ∀ {l₁ l₂ : list α}, count a (l₁.bag_inter l₂) = min (count a l₁) (count a l₂)
| []        l₂ := by simp
| l₁        [] := by simp
| (h :: l₁) l₂ :=
begin
  dsimp [list.bag_inter], -- succeeds but does nothing?
  sorry
end

but can't seem to get access to the interesting inductive case of the definition of list.bag_inter. What am I meant to be doing here?

[Scott Morrison]

For reference, list.bag_inter is defined as

protected def bag_inter {α} [decidable_eq α] : list α → list α → list α
| []      _   := []
| _       []  := []
| (a::l₁) l₂  := if a ∈ l₂ then a :: bag_inter l₁ (l₂.erase a) else bag_inter l₁ l₂

in core.

[Kevin Buzzard]

What do I import to get count?

[Kevin Buzzard]

Oh -- maybe I have to open something? List?

[Kevin Buzzard]

I can't get your code to run :-(

[Scott Morrison]

Sorry, MWE almost there.

[Scott Morrison]

Okay, I've updated the code above to include imports and variables.

[Kevin Buzzard]

#print prefix list.bag_inter reminds us that Lean still does the nil/cons case split on l2 in the a::l1 case when defining bag_inter

[Kevin Buzzard]

begin
  cases l₂, simp,
  dsimp [list.bag_inter], -- now does something
  sorry
end

[Kevin Buzzard]

[PS I'm sorry, I'm so rubbish if I can't get the code to run. I know lots of people can do this sort of question in their heads but I can't. I was missing the decidable equality]

[Scott Morrison]

ah, cool. Thanks! I didn't know about #print prefix.

[Kevin Buzzard]

dsimp [list.bag_inter] I think attempts to simplify using the equation lemmas for list.bag_inter. I used to think it was just magic, but Lean does not do magic. To see the equation lemmas I always use #print prefix.

[Kevin Buzzard]

And when you start looking at equation lemmas you learn random stuff like "even though you defined your function using three cases, Lean internally compiled it up as four cases"