multiset

Stream: general

[Kevin Buzzard]

@Ellen Arlt and I are putting multiset.lean through its paces.

Q1) This is perhaps a question about general lean/mathlib conventions disguised as a question about multisets. We have been working with multisets of size 0 and 1 and proving basic API lemmas. Initially I was using ∅ to denote the empty multiset (this is defined in mathlib, it's not my definition). I was surprised to find that multiset.card (∅ : multiset α) = 0 was not a simp lemma (its proof is rfl but it can still be a simp lemma, right?) so I went to data.multiset to decide where to add it. And there I found that multiset.card (0 : multiset α) = 0 was a simp lemma:

import data.multiset

variable {α : Type}

example  : (0 : multiset α) = (∅ : multiset α) := rfl

example : multiset.card (0 : multiset α) = 0 := by simp

example : multiset.card (∅ : multiset α) = 0 := by simp -- fails

Is this an example of the "pecking order" CS thing? Does it say "yes, ∅ and 0 are the same multiset, but if you need to refer to this multiset then mathlib asks that you use 0"? If I'm right, how is one supposed to figure this sort of thing out? The hard way, like I did?

Q2) multiset.strong_induction_on gives me a way of defining functions on multisets. But I am having trouble proving anything at all about such functions. I think I need some sensible eliminators for multiset.strong_induction_on, ideally the one that says that the function defined by multiset.strong_induction_on can be computed on a multiset if I can tell you its values on all proper subsets of the multiset. No doubt this eliminator is "there already" in some form -- but I don't know how to get to it.

[Mario Carneiro]

This is a "pecking order" thing. I was remiss in not including a simp lemma (∅ : multiset α) = 0 but it would have conveyed this intent well

[Mario Carneiro]

Alternatively, in hindsight perhaps it would have been better to make ∅ the primary one, since multisets have "set" in the name (as opposed to calling them free_abelian_group where 0 would be more natural)

[Sebastian Ullrich]

Just idle speculation, I suppose in a future unbundled class hierarchy we would rather have an instance is_zero ∅ (multiset a) instead of has_zero (multiset a)?

[Sebastian Ullrich]

So that there is no (0 : multiset α)

[Mario Carneiro]

I suppose that depends on whether we want to use 0 as notation

[Mario Carneiro]

like I said, it makes sense if you want to use multiset as a free group generator

[Kevin Buzzard]

A related question is what I should be using for {c} = c :: 0 = c :: ∅. Who is top of the tree here?

[Mario Carneiro]

c::0 is used exclusively for singleton on multiset

[Mario Carneiro]

For Q2, you can use this theorem:

theorem strong_induction_eq {p : multiset α → Sort*}
  (s : multiset α) (H) : @strong_induction_on _ p s H =
    H s (λ t h, @strong_induction_on _ p t H) :=
by rw [strong_induction_on]

but the built in equation is also usable, as I did in the proof here

[Kevin Buzzard]

c :: 0 -- Yes, I had spotted this. So I should always use this notation? I noticed in practice that if one sticks to the notation which is top of the tree, then random stuff just "worked better", e.g. I had a split_ifs nightmare scenario when all of a sudden I had four goals; I traced this back to "sometimes using 0 and sometimes emptyset" and when I started being consistent (initially with the wrong choice!) things got better.

[Mario Carneiro]

yes, that's the name of the game

[Mario Carneiro]

These conventions are debatable, but the most important thing is to be consistent about them

[Kevin Buzzard]

As for built in equations for arbitrary definitions, I only noticed that they existed about 20 minutes ago ;-) Thanks @Simon Hudon !

[Mario Carneiro]

the built in equations are much more important for wf definitions, since they are often not by rfl

[Mario Carneiro]

(they are by rfl in theory, but this is where lean breaks from the theory so it proves them automatically instead)

[Kevin Buzzard]

Conventions: I guess the second most important thing is to convey the conventions to your users. I am beginning to realise that these subtleties can actually be read off relatively easily by just reading the source. Presumably sometimes there is a genuine CS reason for choosing one over the other and sometimes it's just a fairly arbitrary choice.

[Kevin Buzzard]

I currently spend three days a week surrounded by about 10 students most of whom know no Lean at all, and I am still amazed by how much their completely basic questions can teach me.

[Patrick Massot]

Does it give more momentum to your book writing effort?

[Kevin Buzzard]

lemma v_empty : value_aux 0 0 = 0 :=
begin
  unfold value_aux, -- strong_induction hell
  rw strong_induction_eq, -- goal now one page long
  rw strong_induction_eq, -- goal now two pages long
  dsimp, -- goal now one line long and doesn't mention induction
  ...

[Kevin Buzzard]

:-)

[Kevin Buzzard]

No -- in fact I spend all my time trying to answer their questions :-) What gives me momentum is that I give one Lean talk per week, and figuring out what to talk about seems to be the same as figuring out what I need to write about next. I am a terrible writer :-/ I am far too verbose. I need a good editor.

[Kevin Buzzard]

The main function (value_aux) that I'm dealing with here is defined using two applications of multiset.strong_induction_on. The above lemma evaluates it on the empty set. To evaluate it on a singleton my code looks like

lemma v_one_chain (c : ℕ) : value_aux (c :: 0) 0 = c :=
begin
  unfold value_aux,
  rw strong_induction_eq,
  rw strong_induction_eq,
  simp,
  rw strong_induction_eq,
  simp,
  rw strong_induction_eq,
  simp,
  -- sanity prevails

I am just over the moon that I can actually do things now, although I'm not entirely sure I like my simp style and the intermediate goals are huge.

[Patrick Massot]

Do you know if simp always does the same thing here?

[Sean Leather]

set_option trace.simplify.rewrite true is your friend.

[Patrick Massot]

If it happens to do always the same thing you can either write a new lemma or a specialized tactic

[Kevin Buzzard]

I love the way that at 9:02am (UK time) I was completely stuck and now at 10:06am I have made huge progress in both my understanding of Lean and of the dots and boxes API. @Sean Leather and @Patrick Massot I'm sure you're right -- I should figure out exactly what simp is doing. But I am now too busy excitedly proving all the trivial lemmas that Ellen wanted :-)

[Mario Carneiro]

You want to write an equation lemma for value_aux, similar to strong_induction_eq

[Kevin Buzzard]

How do I write an equation lemma? Is that just a useful lemma, possibly tagged simp, and called something like value_aux.equation_37?

[Mario Carneiro]

Nothing special, you don't get to write equation lemmas like lean does

[Mario Carneiro]

you just give it a regular name and refer to it directly

[Mario Carneiro]

I would probably call it value_aux_eq

[Sean Leather]

As I understand it, an equation lemma would be what you get (or want) naturally for each constructor of an inductive data type. The equation lemma spells out the equation to reduce/simplify the constructor application. Of course, your type doesn't have to be inductive, nor does it need to have more than one constructor, for you to have an equation lemma. It's really just a name for a particular kind of equality.

[Mario Carneiro]

Well, more precisely, you get an equation lemma for each branch of a definition. If it's a straight definition X = Y then you get just one equation, but if it is defined by cases or induction on an inductive type then you get an equation for each constructor, as you say

[Sean Leather]

Right, forgot about about that.

[Kevin Buzzard]

So I had real trouble emulating simp and removing it from the middle of my proofs -- I think it was even rewriting things like lam (h : a \in c :: 0) to lam (h : a = c) and my conv-fu wasn't strong enough. Chris convinced me to try rolling my own inductive definition -- he said it was so that my equation lemmas would be nicer, but I was motivated because I'd never done this sort of thing before. But I'm using induction twice: I am defining a function value : multiset nat -> multiset nat -> nat with the idea being that if I input C and L then I should be able to assume I can evaluate value at C.erase c L and C L.erase l with c in C and l in L. I should say that Chris' docs in the mathlib docs dir were invaluable.

So I got it working, but here's the epilogue: I think the equation compiler might be performing a dangerous simp which I have no way of stopping. @Mario Carneiro am I right? (this was the theory Chris and I came up with). Here's something which doesn't work:

import data.multiset

definition multiset.N_min : multiset ℕ → ℕ := sorry

def value_aux' : multiset ℕ → multiset ℕ → ℕ
| C L := multiset.N_min (multiset.pmap
      (λ a (h : a ∈ C),
--        have multiset.card (C.erase a) < multiset.card C,
--          from multiset.card_lt_of_lt (multiset.erase_lt.2 h),
        have multiset.card (C.erase a) + multiset.card L < multiset.card C + multiset.card L,
          from add_lt_add_right (multiset.card_lt_of_lt (multiset.erase_lt.2 h)) _,
        a - 2 + int.nat_abs (2 - value_aux' (C.erase a) L))
        C (λ _,id) + multiset.pmap
      (λ a (h : a ∈ L),
--        have multiset.card (L.erase a) < multiset.card L,
--          from multiset.card_lt_of_lt (multiset.erase_lt.2 h),
        have multiset.card C + multiset.card (multiset.erase L a) < multiset.card C + multiset.card L,
          from add_lt_add_left (multiset.card_lt_of_lt (multiset.erase_lt.2 h)) _,
        a - 4 +int.nat_abs (4 - value_aux' C (L.erase a)))
        L (λ _,id))
using_well_founded {rel_tac := λ _ _, `[exact ⟨_, measure_wf
  (λ CL, multiset.card CL.fst + multiset.card CL.snd)⟩]}

This is mostly noise -- the key thing to see is that I am taking as input two multisets, I am defining value_aux on the pair C L by a function which involves evaluating it on pairs C' L and C L' with C'<C and L'<L resp. The tactic I tell Lean to use to prove well-foundedness is, I think, the function sending C L to card C + card L (there's a psigma type involved, hopefully I got it right). The not-commented-out haves insert precisely what Lean needs to see a proof of, if I've understood things correctly. However the code above does not compile -- the equation compiler complains:

The nested exception contains the failure state for the decreasing tactic.
nested exception message:
failed
state:
value_aux' : (Σ' (a : multiset ℕ), multiset ℕ) → ℕ,
C L : multiset ℕ,
a : ℕ,
h : a ∈ C,
this : multiset.card (multiset.erase C a) + multiset.card L < multiset.card C + multiset.card L
⊢ multiset.card (multiset.erase C a) < multiset.card C

Now that looks strange to me, because if I've understood correctly, this is precisely what the equation compiler wanted to see a proof of. Chris conjectures that simp got applied before assumption. If I comment out the have/from pairs and replace with the commented-out ones, the code compiles fine (and my equation lemmas don't mention multiset.rec :-) ). Chris points out that if the behaviour of simp changes in the future, then my code breaks in a really obscure way and there's little I can do about it. Have we understood what's going on correctly?

[Chris Hughes]

Here's a method that avoids the simplifier

def value_aux' (N_min : multiset ℕ → ℕ) : multiset ℕ → multiset ℕ → ℕ
| C L := N_min (multiset.pmap
      (λ a (h : a ∈ C),
--        have multiset.card (C.erase a) < multiset.card C,
--          from multiset.card_lt_of_lt (multiset.erase_lt.2 h),
        have multiset.card (C.erase a) + multiset.card L < multiset.card C + multiset.card L,
          from add_lt_add_right (multiset.card_lt_of_lt (multiset.erase_lt.2 h)) _,
        a - 2 + int.nat_abs (2 - value_aux' (C.erase a) L))
        C (λ _,id) + multiset.pmap
      (λ a (h : a ∈ L),
--        have multiset.card (L.erase a) < multiset.card L,
--          from multiset.card_lt_of_lt (multiset.erase_lt.2 h),
        have multiset.card C + multiset.card (multiset.erase L a) < multiset.card C + multiset.card L,
          from add_lt_add_left (multiset.card_lt_of_lt (multiset.erase_lt.2 h)) _,
        a - 4 +int.nat_abs (4 - value_aux' C (L.erase a)))
        L (λ _,id))
using_well_founded {dec_tac := tactic.assumption, rel_tac := λ _ _, `[exact ⟨_, measure_wf
  (λ CL, multiset.card CL.fst + multiset.card CL.snd)⟩]}

[Chris Hughes]

I changed the dec_tac at the bottom

[Mario Carneiro]

Yes, the standard fix when the default dec_tac is being stupid is to replace it with tactic.assumption like chris did

[Mario Carneiro]

Actually the default dec_tac doesn't use simp, it is a custom tactic that does a few heuristic rules to do with nat.lt

[Mario Carneiro]

it is default_dec_tac in well_founded_tactics.lean

[Mario Carneiro]

But I'm confused what the issue was that caused you to move away from the original version

[Kevin Buzzard]

Short answer: I wanted to get rid of the dangerous simps and this approach ("start again") would have the advantage that it (a) might solve this and (b) would also teach me something (slightly complicated use of equation compiler).

Long technical answer: Your original fix was fine modulo these dangerous simps. I was just talking to Chris about it and he said "why did you even use multiset.strong_induction_on when you could use the equation compiler?" and because I couldn't get rid of my dangerous simp and because I'd never used using_well_founded before I thought I'd give it a go to teach myself something (which turns out to be pretty easy to understand modulo the lam _ _, [exact` bit, which I'm leaving as a black box). Chris pointed out that one only had to use the equation compiler once, whereas I was using strong induction twice, so I felt that rewriting this was somehow going in the right direction.

An example (two examples) of the dangerous simp in my original code looks like this: note that this is with value_aux, the version of my function which uses strong induction twice per application (as opposed to value_aux' above).

lemma v_one_chain (c : ℕ) (h : c ≥ 3) : value_aux (c :: 0) 0 = c :=
begin
  unfold value_aux,
  rw strong_induction_eq,
  rw strong_induction_eq,
  simp,
  rw strong_induction_eq,
  rw strong_induction_eq,
  simp,
  show 2 + (c - 2) = c, -- irritating-to-Patrick goal (c is a nat)
  rw add_comm,refine nat.sub_add_cancel _,
  exact le_trans (show 2 ≤ 3, by exact dec_trivial) h,
end

This uses Mario's eliminator for strong_induction_on and compiles fine. The issue of course is with the simps in the middle. Replacing the first simp with dsimp breaks the code. Before the first simp is applied, the goal is https://gist.github.com/kbuzzard/d9f70ae02b5861bbce0f8d958e16619a and after it's applied, the goal becomes (the still quite long) https://gist.github.com/kbuzzard/07495e93ed94b3d4e5bfd4015a52914f . These goals are too big for my liking and the direct approach seemed like it would be likely to make them smaller. There are strong_induction_ons around in these goals but the rewrites won't work without the first simp. Sean suggested set_option trace.simplify.rewrite true and the output of that on the first dangerous simp is https://gist.github.com/kbuzzard/1a01ad2bc29aad1c257452c4d2d894d5 . I am certainly not a world expert in trace outputs, but I was interpreting the first line 0. [simplify.rewrite] [multiset.mem_singleton]: a ∈ c :: 0 ==> a = c of that trace output as meaning "first we replace that mem term with an eq term" but as far as I could see the only occurrences of a ∈ c :: 0 were in terms like (λ (a : ℕ) (h : a ∈ c :: 0), ... and I could not do that rewrite with my bare hands (maybe I am just lame at conv but OTOH rewriting the type of a term is probably a dangerous business). In short, I couldn't remove the dangerous simp so I thought I'd try another approach.

[Kevin Buzzard]

Actually the default dec_tac doesn't use simp, it is a custom tactic that does a few heuristic rules to do with nat.lt

PS that's good to know. Thanks. @Chris Hughes it wasn't using simp after all. PPS I think https://nat.lt is in Lithuanian.

[Mario Carneiro]

I think you may not have understood my suggestion to write an equation lemma

[Mario Carneiro]

Here is a version of value_aux' that uses strong_induction_on for its definition (presumably this looks like your original definition, although you didn't show it here):

def value_aux (N_min : multiset ℕ → ℕ) (C : multiset ℕ) : multiset ℕ → ℕ :=
multiset.strong_induction_on C $ λ C IH₁ L,
multiset.strong_induction_on L $ λ L IH₂,
N_min (
  multiset.pmap
    (λ a (h : a ∈ C),
      a - 2 + int.nat_abs (2 - IH₁ (C.erase a) (multiset.erase_lt.2 h) L))
    C (λ _, id) +
  multiset.pmap
    (λ a (h : a ∈ L),
      a - 4 + int.nat_abs (4 - IH₂ (L.erase a) (multiset.erase_lt.2 h)))
    L (λ _,id))

[Kevin Buzzard]

[equation lemma] For sure that is true. Probably my question immediately after your comment indicated this. Sometimes I do stuff to learn more

[Kevin Buzzard]

Yes, it looks pretty much like that

[Kevin Buzzard]

except I used C2 instead of C and L2 instead of L because I am scared of free and bound variables having the same name

[Mario Carneiro]

This is the equation lemma corresponding to that definition

theorem value_aux_eq (N_min : multiset ℕ → ℕ) (C L : multiset ℕ) :
  value_aux N_min C L = N_min (
    multiset.pmap
      (λ a (h : a ∈ C),
        a - 2 + int.nat_abs (2 - value_aux N_min (C.erase a) L))
      C (λ _, id) +
    multiset.pmap
      (λ a (h : a ∈ L),
        a - 4 + int.nat_abs (4 - value_aux N_min C (L.erase a)))
      L (λ _,id)) := sorry

[Kevin Buzzard]

I don't understand your application of the "equation lemma" function.

[Mario Carneiro]

(Actually, you can simplify the pmap away the way it's been written here, since h is no longer used)

[Kevin Buzzard]

Is there an equation lemma corresponding to every definition?

[Kevin Buzzard]

What is "the equation lemma corresponding to nat"?

[Kevin Buzzard]

or "the equation lemma corresponding to quotient.sound" etc etc.

[Mario Carneiro]

Informally, an "equation lemma" says that a definition is what it was defined to be

[Mario Carneiro]

nat and quotient.sound don't have equation lemmas because they are constants, not defs

[Kevin Buzzard]

real?

[Kevin Buzzard]

def f : nat -> nat := lam x, x + 3?

[Mario Carneiro]

It has an equation lemma, although you would rarely use it

[Mario Carneiro]

that definitely does

[Kevin Buzzard]

it's something like "forall x , f x = x + 3"?

[Mario Carneiro]

yes

[Kevin Buzzard]

Maybe I don't understand the _point_ then.

[Kevin Buzzard]

Is it tagged as a simp lemma?

[Kevin Buzzard]

Who is using these equation lemmas?

[Mario Carneiro]

sometimes it's a simp lemma

[Kevin Buzzard]

?!

[Kevin Buzzard]

Who makes the decision?

[Mario Carneiro]

it gets used whenever you "unfold the definition"

[Kevin Buzzard]

Aah!

[Kevin Buzzard]

When I use unfold, sometimes it says that simp failed

[Mario Carneiro]

some definitions are marked @[simp] meaning that their equation lemmas are simp lemmas

[Kevin Buzzard]

You can tag a definition with simp? I am not sure I ever internalised that

[Mario Carneiro]

like list.append

@[simp] protected def append : list α → list α → list α
| []       l := l
| (h :: s) t := h :: (append s t)

[Mario Carneiro]

This marks this definition's two (!) equation lemmas as simp lemmas

[Kevin Buzzard]

I can see all the equation lemmas with #print prefix list.append perhaps

[Mario Carneiro]

yes

[Kevin Buzzard]

So I must confess that I've never really understood the output of that sort of command.

[Kevin Buzzard]

We have _main, _main._meta_aux etc

[Kevin Buzzard]

it's quite intimidating

[Mario Carneiro]

But sometimes lean doesn't generate equation lemmas the way you would like them, so you have to write your own, and that's my point

[Kevin Buzzard]

I am still missing a big issue

[Kevin Buzzard]

OK so I wrote my function

[Kevin Buzzard]

and the equation lemmas are all wrong

[Kevin Buzzard]

so I need to write another one.

[Mario Carneiro]

For example, here's another way to write list.append

def list.append' {α} (l₁ l₂ : list α) : list α :=
list.rec_on l₁ l₂ (λ a l₁ IH, a :: IH)

[Kevin Buzzard]

OK so I wrote one: "theorem X : f x = g x -- this is the equation lemma I want"

[Kevin Buzzard]

that's a lemma

[Kevin Buzzard]

Is it an equation lemma?

[Mario Carneiro]

the equation lemmas are not what we would like

#print prefix list.append'
-- list.append' : Π {α : Type u_1}, list α → list α → list α
-- list.append'.equations._eqn_1 : ∀ {α : Type u_1} (l₁ l₂ : list α),
--   list.append' l₁ l₂ = list.rec_on l₁ l₂ (λ (a : α) (l₁ IH : list α), a :: IH)

[Kevin Buzzard]

why not?

[Kevin Buzzard]

What's wrong with them?

[Kevin Buzzard]

I don't understand several things

[Kevin Buzzard]

"equation lemmas are used in unfold"

[Kevin Buzzard]

"sometimes they're simp lemmas"

[Mario Carneiro]

While it is true that append is equal to that rec_on mess, that's not what I want to see

[Kevin Buzzard]

"they're generated automatically"

[Kevin Buzzard]

that's about all I know

[Kevin Buzzard]

about equation lemmas

[Kevin Buzzard]

I am missing some fundamental point about why they exist and why they're important

[Kevin Buzzard]

"if you write a definition, Lean generates a bunch of lemmas with obscure names"

[Mario Carneiro]

what I want to see are the things that the definition is trying to say, namely list.append [] l = l and list.append (a::l) l' = a :: list.append l l'

[Mario Carneiro]

This is really important for controlling the complexity of statements

[Kevin Buzzard]

"if you write the definition differently, you might get different lemmas, and Mario can see that this might cause problems but Kevin still has no understanding of when equation lemmas are used so doesn't care what these auto-generated lemmas are"

[Mario Carneiro]

if every time you used nat.add it unfolded to its definition it would be utterly unreadable

[Kevin Buzzard]

it can't unfold

[Kevin Buzzard]

oh wit

[Kevin Buzzard]

oh wait

[Kevin Buzzard]

is nat.add one of these things whose definition is not what I think it is?

[Kevin Buzzard]

Is it not 0 -> x, succ y -> succ (x+y)?

[Mario Carneiro]

really making progress in this proof:

example (x : ℕ) : 0 + x = 0 :=
begin
  dsimp only [(+)], delta nat.add,
-- ⊢ nat.brec_on x
--       (λ (a : ℕ) (_F : nat.below (λ (a : ℕ), ℕ → ℕ) a) (a_1 : ℕ),
--          (λ (a a_1 : ℕ) (_F : nat.below (λ (a : ℕ), ℕ → ℕ) a_1),
--             nat.cases_on a_1 (λ (_F : nat.below (λ (a : ℕ), ℕ → ℕ) 0), id_rhs ℕ a)
--               (λ (a_1 : ℕ) (_F : nat.below (λ (a : ℕ), ℕ → ℕ) (nat.succ a_1)),
--                  id_rhs ℕ (nat.succ ((_F.fst).fst a)))
--               _F)
--            a_1
--            a
--            _F)
--       0 =
--     0
end

[Kevin Buzzard]

I'm already lost, apparently it's nat.add._main

[Kevin Buzzard]

that does not look good

[Mario Carneiro]

If simp did this Leo would be fired by now

[Kevin Buzzard]

The problem has occurred because nat.add is for some reason defined in a stupid way

[Kevin Buzzard]

I fixed this up in my blog IIRC

[Mario Carneiro]

no, the problem has occurred because I unfolded the definition without folding it back up again

[Kevin Buzzard]

Does the equation compiler create that monstrosity?

[Mario Carneiro]

Even if I defined nat.add the simple way, it would still not be pretty to look at

[Kevin Buzzard]

oh holy moley

[Mario Carneiro]

I want to see 0 + x not nat.rec bla bla

[Kevin Buzzard]

nat.add is defined sensibly in core.lean

[Kevin Buzzard]

what has the equation compiler done??

[Mario Carneiro]

The equation lemmas say things like x + succ y = succ (x + y)

[Kevin Buzzard]

namespace nat
  protected def add : nat → nat → nat
  | a  zero     := a
  | a  (succ b) := succ (add a b)

[Kevin Buzzard]

That got turned into the monstrosity

[Mario Carneiro]

this is true by rfl, but the really important thing is that the RHS does not have nat.rec in it

[Mario Carneiro]

or nat.brec_on or its cousins

[Kevin Buzzard]

Right -- Chris was stressing the importance of getting away from multiset.rec

[Kevin Buzzard]

which I had in my initial equation lemmas for the value function

[Mario Carneiro]

In fact, you could say that's the main purpose of equation lemmas, to hide recursors

[Kevin Buzzard]

actually it's even worse, my equation lemmas for value have strong induction in

[Kevin Buzzard]

value_aux.equations._eqn_1 : ∀ (C : multiset ℕ),
  value_aux C =
    multiset.strong_induction_on C
      (λ (C2 : multiset ℕ) (HC : Π (t : multiset ℕ), t < C2 → multiset ℕ → ℕ) (L : multiset ℕ),
         multiset.strong_induction_on L
           (λ (L2 : multiset ℕ) (HL : Π (t : multiset ℕ), t < L2 → ℕ),
              multiset.N_min
                (multiset.pmap
                     (λ (a : ℕ) (h : a ∈ C2), a - 2 + int.nat_abs (2 - ↑(HC (multiset.erase C2 a) _ L2)))
                     C2
                     _ +
                   multiset.pmap
                     (λ (a : ℕ) (h : a ∈ L2), a - 4 + int.nat_abs (4 - ↑(HL (multiset.erase L2 a) _)))
                     L2
                     _)))

[Kevin Buzzard]

Can you tell me a formal definition of which parts of the output of #print prefix value_aux are the equation lemmas?

[Kevin Buzzard]

Is it precisely those which start value_aux.equation...?

[Mario Carneiro]

yes, those are the automatically generated equation lemmas

[Kevin Buzzard]

because I have other things like the stunning observation value_aux._proof_4 : ∀ (L2 : multiset ℕ) (_x : ℕ), _x ∈ L2 → _x ∈ L2

[Kevin Buzzard]

Is that an equation lemma?

[Kevin Buzzard]

I don't know what I'd do without that lemma

[Mario Carneiro]

those are extracting proof terms inside non-proof terms for performance

[Kevin Buzzard]

but not equation lemmas.

[Mario Carneiro]

the extraction code isn't so bright

[Mario Carneiro]

equation lemmas are equations

[Kevin Buzzard]

OK so when I make a new definition, Lean makes some equation lemmas, and we've seen examples where these lemmas are in some sense unusable

[Mario Carneiro]

right

[Kevin Buzzard]

so now all I need to know is

[Kevin Buzzard]

(1) what is actually using them and (2) how to write better ones

[Mario Carneiro]

When you write a definition you should already have in mind what its equation lemmas are

[Mario Carneiro]

In this case, you knew you wanted value_aux to depend on itself at other values

[Kevin Buzzard]

If we go back to nat.add I can see x + succ y = succ (x + y) would be the sort of thing that as an end user I would simply _assume_ was true by rfl, given the definition

[Mario Carneiro]

which is where something like this comes from

theorem value_aux_eq (N_min : multiset ℕ → ℕ) (C L : multiset ℕ) :
  value_aux N_min C L = N_min (
    C.map (λ a, a - 2 + int.nat_abs (2 - value_aux N_min (C.erase a) L)) +
    C.map (λ a, a - 4 + int.nat_abs (4 - value_aux N_min C (L.erase a)))) := sorry

[Kevin Buzzard]

Right -- I feel like I want that theorem to be true by rfl

[Kevin Buzzard]

because in my non-CS mathematical mind that is "exactly how I defined the function"

[Kevin Buzzard]

that theorem is "true by definition"

[Mario Carneiro]

exactly

[Kevin Buzzard]

but funnily enough I don't see it in my list of equation lemmas

[Mario Carneiro]

Half of the work is taking your "definition" and turning it into something lean will accept, and the other half is getting back to the original thing you wanted to call the definition

[Mario Carneiro]

that latter step is the equation lemma

[Kevin Buzzard]

I had never remotely comprehended this.

[Kevin Buzzard]

I thought that "Lean did the second part automatically"

[Mario Carneiro]

it does, for the most part

[Mario Carneiro]

but it's not perfect, it doesn't accept every definitionesque thing mathematicians dream up

[Kevin Buzzard]

OK so let's say I can prove the lemma which I thought should be rfl but which wasn't.

[Kevin Buzzard]

Is it just a case of making sure that lemma is called value_aux.equations._eqn_2?

[Mario Carneiro]

Unfortunately, lean doesn't let you install your own equation lemmas like that

[Kevin Buzzard]

OK so we're back to (1) I don't know how to make a lemma into an equation lemma and (2) I don't know exactly what is using the equation lemmas and when

[Mario Carneiro]

when you right your own equation lemma, it's just a theorem, an equality you can use in rewrite and simp

[Kevin Buzzard]

and rfl

[Kevin Buzzard]

because equation lemmas are true by definition, right? :-)

[Mario Carneiro]

If you prove it by rfl you can also use it in dsimp

[Mario Carneiro]

Sometimes it's rfl sometimes not

[Kevin Buzzard]

If it's not rfl then Lean made a mistake

[Kevin Buzzard]

because the equation lemmas are the things which are true by definition

[Mario Carneiro]

for more elaborate definitional mechanisms, DTT doesn't recognize it as definitional but you can still prove it with some work

[Kevin Buzzard]

OK

[Kevin Buzzard]

so now I proved a lemma, the proof unfortunately wasn't rfl, I want to use it everywhere because in my brain the lemma is "true by definition of the object".

[Kevin Buzzard]

Now what?

[Mario Carneiro]

In particular, I doubt value_aux_eq is true by rfl, particularly when I changed the pmap to map

[Kevin Buzzard]

Yes i can quite believe it's not

[Kevin Buzzard]

not least because value_aux uses multiset.strong_induction_on twice

[Mario Carneiro]

but it is nevertheless "the way we want it to unfold" so we treat it as the equation lemma

[Kevin Buzzard]

"so we treat it as the equation lemma" is the bit I don't get

[Kevin Buzzard]

Are you just saying "prove a lemma and then occasionally rw with it"?

[Mario Carneiro]

It just means we use that theorem when we would otherwise "unfold value_aux"

[Kevin Buzzard]

So

lemma v_one_chain (c : ℕ) (h : c ≥ 3) : value_aux (c :: 0) 0 = c :=
begin
  unfold value_aux,
  rw strong_induction_eq,
  rw strong_induction_eq,
  simp,
  rw strong_induction_eq,
  rw strong_induction_eq,
  simp,
...

is not the right approach?

[Mario Carneiro]

no

[Kevin Buzzard]

even though I have the right equation lemma?

[Kevin Buzzard]

(I assume I do, I think you wrote it)

[Mario Carneiro]

you want to use the equation lemma for value_aux, not the equation lemma for strong_induction_on

[Mario Carneiro]

you will use the latter to prove the former

[Kevin Buzzard]

aah

[Kevin Buzzard]

aah I was thinking "Mario said to use an equation lemma, I don't know what that is, I think Mario wrote it for me, I'll just use that"

[Kevin Buzzard]

So an equation lemma is just a lemma, with no magic properties, it doesn't have to have a weird name like foo._equation_7_main_sunfold

[Mario Carneiro]

no, that's just the usual name for lean's autogenerated equation lemmas

[Kevin Buzzard]

what makes it an equation lemma is that it represents a fact which the end user would like to think was "true by definition"

[Kevin Buzzard]

if they were a wooly thinker, like e.g. a pure mathematician

[Mario Carneiro]

those get some special magic, like being able to write simp [f] instead of simp [f.equations_1]

[Kevin Buzzard]

Yes, I learnt that yesterday

[Kevin Buzzard]

OK so let me step back and try to wrap up

[Kevin Buzzard]

When I write a definition, I might want to consider what the fundamental properties of that definition are -- the things which should be "true by definition"

[Kevin Buzzard]

or "true because it's completely obvious"

[Kevin Buzzard]

and then I might want to look at the subset of the output of #print prefix foo consisting only of things which have the string "equation" in them

[Kevin Buzzard]

and I might want to just check that everything I want to be "true by definition" is there

[Mario Carneiro]

The autogenerated equation lemmas are easy to predict without looking at them like that

[Kevin Buzzard]

and if it's not then I might want to make a note of this, prove the remaining facts, and then spend the rest of my life rewriting with them

[Sean Leather]

@Kevin Buzzard Perhaps “true by the definition you wished it had”? “True because it's obvious” is maybe too generous in what it allows.

[Kevin Buzzard]

The autogenerated equation lemmas are easy to predict without looking at them like that

says someone who has probably looked at the code which generates them

[Mario Carneiro]

for each branch of the definition, each :=, you get a lemma saying your definition applied to those arguments gives the RHS

[Kevin Buzzard]

@Sean Leather that's a better way of phrasing it. My definition of value by "induction on (induction on ...)" was never going to create the lemma I wanted

[Kevin Buzzard]

but on the other hand there was clearly a definition which in some sense I "wished I had written"

[Kevin Buzzard]

and that was precisely the definition I _did_ write yesterday, using the equation compiler

[Kevin Buzzard]

So all this stinks. There are things which should be true by rfl but which I can't prove with rfl

[Mario Carneiro]

One place where you might be surprised is in definitions with wildcards

def X {α} : list α → list α → list α
| [] _ := []
| _ [] := []
| x y := x
#print prefix X
-- X.equations._eqn_1 : ∀ {α : Type u_1}, X list.nil list.nil = list.nil
-- X.equations._eqn_2 : ∀ {α : Type u_1} (hd : α) (tl : list α), X list.nil (hd :: tl) = list.nil
-- X.equations._eqn_3 : ∀ {α : Type u_1} (hd : α) (tl : list α), X (hd :: tl) list.nil = list.nil
-- X.equations._eqn_4 : ∀ {α : Type u_1} (hd : α) (tl : list α) (hd_1 : α) (tl_1 : list α), X (hd :: tl) (hd_1 :: tl_1) = hd :: tl

[Mario Carneiro]

notice that X x y = x is not an equation lemma since it has to do some case splits first

[Kevin Buzzard]

right

[Kevin Buzzard]

that all makes sense to me

[Kevin Buzzard]

that's a lemma, that X x y = x

[Kevin Buzzard]

actually it's perhaps not even true but I see your point whether or not this example is exactly right

[Kevin Buzzard]

So I prove this lemma by cases on x

[Kevin Buzzard]

and then I decree in my head that this is an equation lemma

[Mario Carneiro]

Maybe a better example of an equation lemma for this one is X [] y = [] and X x [] = []

[Mario Carneiro]

Neither of these is true by rfl

[Kevin Buzzard]

yes

[Kevin Buzzard]

both proof by cases

[Kevin Buzzard]

These look like simp lemmas to me

[Mario Carneiro]

They are that too

[Kevin Buzzard]

So an equation lemma seems to me to have no formal definition

[Mario Carneiro]

equation lemmas are often good simp lemmas

[Kevin Buzzard]

it's "something which the user is clearly going to need again and again"

[Kevin Buzzard]

so should probably be proved immediately after the definition

[Mario Carneiro]

but sometimes they would lead to infinite unfolding, like the equation lemma for value_aux

[Kevin Buzzard]

I think nat is well-founded

[Mario Carneiro]

equation lemmas for wf definitions often have that problem

[Mario Carneiro]

gcd x y unfolds forever when given variable x and y

[Kevin Buzzard]

Oh!

[Mario Carneiro]

it doesn't matter that nat is well founded

[Kevin Buzzard]

Oh you're absolutely right!

[Mario Carneiro]

because these are open terms

[Kevin Buzzard]

We're not doing case splits on constructors for multiset or whatever

[Kevin Buzzard]

oh so that lemma is actually quite dangerous!

[Kevin Buzzard]

Shall I make it a simp lemma?

[Mario Carneiro]

yes, you only want to use it with rw or simp {single_pass := tt}

[Kevin Buzzard]

right

[Mario Carneiro]

it should definitely not be a simp lemma

[Kevin Buzzard]

right!

[Kevin Buzzard]

I gave an entire lecture on functions last Monday

[Kevin Buzzard]

I feel like I could give another one now

[Mario Carneiro]

:)

[Kevin Buzzard]

Many thanks as ever Mario.

[Kevin Buzzard]

What's nice about zulip rather than IRL meetings is that now I understand much better I can just read through the thread again with the benefit of hindsight and try to catch extra subtleties.

[Kevin Buzzard]

Half of the work is taking your "definition" and turning it into something lean will accept, and the other half is getting back to the original thing you wanted to call the definition

This is somehow the key point. I have quite a flexible way of thinking about definitions and their basic properties, I guess because mathematicians are trained like that. Some properties of a definition are so completely basic that I think I've got into the habit of simply assuming that they will be (a) true and (b) rfl. For simple functions this might well be the case. For more complex definitions which need some bending to shove into Lean, life might not be so easy. I have a definition by induction on two variables, and Mario's equation lemma is exactly how I am thinking the definition "works". I shove the definition into Lean in perhaps an inelegant way ("Mario wrote multiset.strong_induction_on and I can apply it twice, that'll do") and now I need to be aware of the fact that Lean's understanding of the function is now quite far from my intuitive idea of how it works, and it should now be a top priority to sort this situation out by proving the lemmas which say that the definition behaves the way I expect it to. If I'm writing some API then I might want to consider proving these so-called "equation lemmas" -- this is an informal definition and it seems to mean "the lemmas which an end user might expect to be true by definition, whether or not they are true by rfl" -- immediately after the definition of the function. Some might already be there with exotic names with _s in, and the ones that are not should be written as a matter of priority or other mathematicians will not be able to use the function in the intuitive way which they would like to.