Alternative choices of induction theorem

[mn200]

Being able to write things like Induct_on `FINITE` is nice, but it'd be even nicer if one had a way of occasionally specifying different theorems from the default. (This is particularly relevant for inductions involving RTC and TC, for example.) I think a syntax like

Induct_on `RTC` using sometheorem >> next_tactic

should be possible. The using infix would be tighter than >> and would modify tactics to first add the provided theorem to the assumption list with some sort of special label. Tactics that were "using-aware" would then have to check the assumption list. One issue with this approach is polymorphic theorems: putting these onto the assumption list pretty well removes the polymorphism. One could imagine horrible hacks with references, or storing theorem names instead of actual theorems...

[mn200]

I think the syntax here should use a string argument, and that the string should then be encoded into the “using assumption”. (One might imagine changing the type of tactics to manipulate some sort of proof contexts instead of our traditional goals, but that's a pretty invasive change.)

[konrad-slind]

Looks like you are describing two things. I don't quite seeing the "using" infix helping with alternate inductions, since if you already have the induction theorem to hand, then ho_match_mp_tac will do the trick. (Of course, there is the preparatory stuff that Induct_on performs, which could be broken out into something more widely usable.) It would be nice to have an ML function that would return all the relevant inductions from some kind of designation (type or predicate, or even string fragment ala DB.find).

On Sun, Nov 18, 2018 at 5:17 AM Michael Norrish notifications@github.com wrote:

I think the syntax here should use a string argument, and that the string should then be encoded into the “using assumption”. (One might imagine changing the type of tactics to manipulate some sort of proof contexts instead of our traditional goals, but that's a pretty invasive change.)

— You are receiving this because you are subscribed to this thread. Reply to this email directly, view it on GitHub https://github.com/HOL-Theorem-Prover/HOL/issues/547#issuecomment-439685010, or mute the thread https://github.com/notifications/unsubscribe-auth/ABDgD-7YJkTVoWeVcEmyUTECUYY_UskIks5uwUGxgaJpZM4UhqqA .

[mn200]

As you say, ho_match_mp_tac doesn't do all that Induct_on does. And in fact, I want Induct_on to do still more. For example, when working with FINITE_INDUCT, have it cope with a goal that looks like

!s t. FINITE s /\ t SUBSET s ==> FINITE t

This requires isolating the FINITE s and moving the !t inwards, so it's not really appropriate for a primitive like ho_match_mp_tac.

When you then also want to have Induct_on to be able to work with different theorems, what's to do? I don't want to give Induct_on a new argument (breaking existing applications), so a general mechanism for temporarily stashing theorem arguments in the assumption list seems workable. This might be something that other tools might use (Cases_on, for example).

[konrad-slind]

As you mentioned, I don't see how stashing things on the assumptions will help apply polymorphic ind. thms.

On Mon, Nov 19, 2018 at 7:03 PM Michael Norrish notifications@github.com wrote:

As you say, ho_match_mp_tac doesn't do all that Induct_on does. And in fact, I want Induct_on to do still more. For example, when working with FINITE_INDUCT, have it cope with a goal that looks like

!s t. FINITE s /\ t SUBSET s ==> FINITE t

This requires isolating the FINITE s and moving the !t inwards, so it's not really appropriate for a primitive like ho_match_mp_tac.

When you then also want to have Induct_on to be able to work with different theorems, what's to do? I don't want to give Induct_on a new argument (breaking existing applications), so a general mechanism for temporarily stashing theorem arguments in the assumption list seems workable. This might be something that other tools might use (Cases_on, for example).

— You are receiving this because you commented. Reply to this email directly, view it on GitHub https://github.com/HOL-Theorem-Prover/HOL/issues/547#issuecomment-440098293, or mute the thread https://github.com/notifications/unsubscribe-auth/ABDgD1m0l1lFU-ZOvbNonNI8zp5_-BSeks5uw1T8gaJpZM4UhqqA .

[mn200]

You stash the name of the theorem, encoded as variable (using, K T name say).

[konrad-slind]

Ah I see!

On Wed, Nov 21, 2018 at 7:38 PM Michael Norrish notifications@github.com wrote:

You stash the name of the theorem, encoded as variable (using, K T name say).

— You are receiving this because you commented. Reply to this email directly, view it on GitHub https://github.com/HOL-Theorem-Prover/HOL/issues/547#issuecomment-440885631, or mute the thread https://github.com/notifications/unsubscribe-auth/ABDgD_FUz5xzgLyzwXE6_HgTCygNlPIYks5uxgAhgaJpZM4UhqqA .

[mn200]

Work on this has been happening in 436637988 and e99f87f3816.

[mn200]

Needs documenting, but I think this is basically done.