decreasing induction

Stream: general

[Kayla Thomas]

Is there a way to prove that a predicate on lists or sets holds for the empty case by showing that when it holds for n elements it holds for n - 1 elements?

[Pedro Sánchez Terraf]

If it is false for every list/set, then your hypothesis vacuously holds.

[Kayla Thomas]

Hmm. I may have misinterpreted the proof I am trying to formalize.

[Kayla Thomas]

It is the proof of the completeness theorem for propositional logic, in which there is an algorithm to remove one by one each assumption Bn from B1 ... Bn |- P leaving |- P.

[Jireh Loreaux]

Kayla, if you also know that it is true for some fixed list of positive length, then your approach works. There is docs#nat.decreasing_induction.

[Kayla Thomas]

We know that B1 ... Bn |- P holds for some finite list B1...Bn, and can show from that that B1 ... Bn-1 |- P holds, and then B1 ... Bn-2 |- P, etc. We then argue that we can use this to show that |- P holds.

[Kayla Thomas]

Is there a way to use docs#nat.decreasing_induction for lists or finite sets?

[Kayla Thomas]

That is, I see, induction e using r, but I'm not sure how to use it.

[Jireh Loreaux]

You could phrase it in terms of the length of an initial segment of the list and then do the nat version on that variable.

[Kayla Thomas]

Ok. Thank you.