Zulip Chat Archive

Stream: general

Topic: induction on two multisets

Kevin Buzzard (Jul 11 2018 at 07:25):

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 (Jul 11 2018 at 07:27):

You can do this by a nested induction using that function

Kevin Buzzard (Jul 11 2018 at 07:27):

So I tried this

Kevin Buzzard (Jul 11 2018 at 07:29):

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 (Jul 11 2018 at 07:29):

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

Mario Carneiro (Jul 11 2018 at 07:30):

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

Kevin Buzzard (Jul 11 2018 at 07:30):

To define f C L I need more

Kevin Buzzard (Jul 11 2018 at 07:30):

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

Mario Carneiro (Jul 11 2018 at 07:31):

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 (Jul 11 2018 at 07:31):

OK I'll take it from here.

Kevin Buzzard (Jul 11 2018 at 07:31):

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 (Jul 11 2018 at 07:31):

it is two inductions

Mario Carneiro (Jul 11 2018 at 07:31):

one inside the other

Kevin Buzzard (Jul 11 2018 at 07:31):

Right.

Kevin Buzzard (Jul 11 2018 at 07:32):

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

Kevin Buzzard (Jul 11 2018 at 07:32):

We only do induction on nat in maths.

Mario Carneiro (Jul 11 2018 at 07:32):

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

Kevin Buzzard (Jul 11 2018 at 07:32):

This I know.

Kevin Buzzard (Jul 11 2018 at 07:32):

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

Mario Carneiro (Jul 11 2018 at 07:33):

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

Mario Carneiro (Jul 11 2018 at 07:34):

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 (Jul 11 2018 at 07:35):

I didn't even know that namespace existed!

Mario Carneiro (Jul 11 2018 at 07:35):

That's what powers the using_well_founded equation compiler stuff

Kevin Buzzard (Jul 11 2018 at 07:35):

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

Kevin Buzzard (Jul 11 2018 at 07:35):

i.e. indirectly

Mario Carneiro (Jul 11 2018 at 07:35):

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

Mario Carneiro (Jul 11 2018 at 07:36):

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

Andrew Ashworth (Jul 11 2018 at 14:25):

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

Andrew Ashworth (Jul 11 2018 at 14:27):

Probably I need to get with the times :)

Last updated: Dec 20 2023 at 11:08 UTC