induction on two multisets

Stream: general

[Kevin Buzzard]

I am trying to define a function multiset nat -> multiset nat -> nat, by induction. If I have two multisets C and L and if I know the value of the function on all the pairs (C-{x},L)(with x in C) and (C,L-{y}) (with y in L) then I have a formula which will give me the value at (C,L). The formula is not symmetric in C and L. The tool which the API gives me is

multiset.strong_induction_on :
  Π {α : Type u_1} {p : multiset α → Sort u_2} (s : multiset α),
    (Π (s : multiset α), (Π (t : multiset α), t < s → p t) → p s) → p s

but I can't figure out how to use this directly.

[Mario Carneiro]

You can do this by a nested induction using that function

[Kevin Buzzard]

So I tried this

[Kevin Buzzard]

but my interpretation of what you're saying is "define f(C,L) for L constant and C varying, by induction on C" and the problem is that the definition needs both C and L to move. What am I missing?

[Mario Carneiro]

Define f C L for all L and fixed C, by induction on C

[Mario Carneiro]

In the IH we know f (C-{x}) L' for all L' and need to define f C L

[Kevin Buzzard]

To define f C L I need more

[Kevin Buzzard]

I need f C L' for all L' smaller than L

[Mario Carneiro]

we do so by induction on L. Now the induction hypothesis gives us f C (L-{y}) and we must define f C L

[Kevin Buzzard]

OK I'll take it from here.

[Kevin Buzzard]

The reason I asked was that I was not 100% sure that the tools I had were enough. If you're confident that they are then I just need to work harder. Thanks for the tips.

[Mario Carneiro]

it is two inductions

[Mario Carneiro]

one inside the other

[Kevin Buzzard]

Right.

[Kevin Buzzard]

I'm a mathematician. I don't understand induction properly :-)

[Kevin Buzzard]

We only do induction on nat in maths.

[Mario Carneiro]

This can also be viewed as a well founded induction in lex order, first by C then L

[Kevin Buzzard]

This I know.

[Kevin Buzzard]

But the only way I know to do a well-founded induction is on an inductive type.

[Mario Carneiro]

and since (C-{x},L) and (C,L-{y}) are both less in this order, this method should work

[Mario Carneiro]

I guess an alternative to the multiset.strong_induction_on API is just to provide a proof that multiset < is well founded and let you use the tools from the well_founded namespace

[Kevin Buzzard]

I didn't even know that namespace existed!

[Mario Carneiro]

That's what powers the using_well_founded equation compiler stuff

[Kevin Buzzard]

The only time I've used well-founded stuff is when trying to persuade the equation compiler that my definition is sound.

[Kevin Buzzard]

i.e. indirectly

[Mario Carneiro]

Back in the old days we used well_founded.fix when we wanted to write a wf definition

[Mario Carneiro]

and it requires a proof that the relation du jour is well founded

[Andrew Ashworth]

I didn't get the memo that this method was passe

[Andrew Ashworth]

Probably I need to get with the times :)