Stream: Mtac2

Topic: chained typed intro


view this post on Zulip Michael Soegtrop (Sep 07 2020 at 08:03):

I wonder if there is a tactic which does a typed intro, but which can only be chained with a tactic which produces a goal of matching function type.
There is ├Čntro_base` where I can specify a tactic executed after the intro, but I am looking for something where I know the tactic (and goal type) executed before the intro.

view this post on Zulip Janno (Sep 07 2020 at 08:44):

It's not easy to find: Ttactics.TT.tintro should be the right thing

view this post on Zulip Michael Soegtrop (Sep 07 2020 at 09:24):

Now I have difficulties to get things type checked - I guess I got what I asked for ;-)

What I have is a tactic with type M_do_something (some args) : M (nicer_goal -> some_goal) and I want to intro a few variables from nicer_goal and demote the remaining nicer_goal.

I have a function (which might already exist):

lift_fMAB
     : M (?A -> ?B) -> ttac (?A -> ?B)

and with this I write:

Definition T_do_something : tactic :=
  (match_goal with
   | [[? a b c |- some_goal a b c ]] =>
      lift_fMAB (M_do_something a b c) <**> TT.demote
   end
  )%TT.

How would I add TT.tintro for nicer_goal here?

My style is still influenced a lot by the fact that I feel more comfortable with the M world and do most things there and only convert to TT in the last step. I guess this makes it a bit harder to work nicely with TT tactics. Is there a nicer way to write the above?

Btw.: I can manage to get the tactic do what I want with typed_intro, but then I could write tactics which won't work in the end, that is where the type given to typed_intro does not match the first argument of nicer_goal.

view this post on Zulip Beta Ziliani (Sep 07 2020 at 13:32):

I fail to see why you need lift_fMAB, if lift is parametric in the type (and can therefore work with ?A -> ?B)

view this post on Zulip Michael Soegtrop (Sep 07 2020 at 13:41):

I fail to see why you need lift_fMAB

Ah yes, a relict from experimenting with returning M(A)->M(B) vs. M(A->B). I swapped a lot between these two options and wanted it as similar as possible. I also have a lift_fMAMB {A B : Type} (f : M A -> M B) : ttac A -> ttac B (where normal lift does not work). Actually I have:

Definition lift_fMAB {A B : Type} (f : M (A -> B)) : ttac (A -> B) := lift f

view this post on Zulip Beta Ziliani (Sep 07 2020 at 13:44):

answering your question, you need to know that your goal is of the form nicer_goal -> some_goal. Right now you're matching against some_goal, so it assumes the hypothesis is already in the context.

view this post on Zulip Michael Soegtrop (Sep 07 2020 at 13:51):

While M_do_something a b c solves a goal of form nicer_goal -> some_goal, the tactic lift_fMAB (M_do_something a b c) <**> TT.demote solves a goal of form some_goal. So at the left of the <**> the information about nicer_goal is still there.

If it helps I can create a test example I can share.

view this post on Zulip Beta Ziliani (Sep 07 2020 at 13:57):

ah I see. but then, where you want to use tintro?

view this post on Zulip Michael Soegtrop (Sep 07 2020 at 14:01):

but then, where you want to use tintro?

Well between the main tactic and the demote - I just can't figure out how to get it right, and the error messages require a lot of imagination on how the types will look unified. But I must admit I didn't try that hard - I am mostly working on something else today.

view this post on Zulip Beta Ziliani (Sep 07 2020 at 19:09):

feel free to make an example and we'll look into it

view this post on Zulip Michael Soegtrop (Sep 11 2020 at 09:51):

@Beta Ziliani, @Janno : I created a small playground to explain the typed intro issue:

(https://gist.github.com/MSoegtropIMC/36b860c8709b7602847ae929074a4d43)

The questions I have:

view this post on Zulip Janno (Sep 11 2020 at 12:01):

I think we've pushed you into the wrong direction. Or maybe it's the lack of documentation.. Either way, this here is bound to give you problems:

Definition lift_MAMB {A B : Type} (f : M A -> M B) : ttac A -> ttac B :=
  (fun a : ttac A => lift (f (lower a))).

In particular, lower throws away the dynamic goals, leaving behind dangling, unsolved evars which mrun will always shelve.

view this post on Zulip Janno (Sep 11 2020 at 12:03):

But I suppose that only affects the first version

view this post on Zulip Janno (Sep 11 2020 at 12:04):

I am still going through the file and trying to understand the definitions.

view this post on Zulip Janno (Sep 11 2020 at 12:07):

For the last variant you can introduce a in a type-safe way by removing the call to demote (which throws away static type information of the subgoal) in TT_MAB_APR and write T_MAB_APR this way:

Definition T_MAB_APR : tactic := (match_goal with | [[ |- R]] => TT_MAB_APR <**> tintro (fun a => TT.demote) end)%TT.

view this post on Zulip Janno (Sep 11 2020 at 12:14):

Apart from that I can safely say that anything that goes through M <...> instead of tactic or ttac will end up throwing goals away (unless, of course, <...> contains mlist (goal gs_any), as it does for tactic and ttac and you do the proper work to track all your goals manually).

view this post on Zulip Michael Soegtrop (Sep 11 2020 at 13:16):

In particular, `lower` throws away the dynamic goals, leaving behind dangling, unsolved evars which `mrun` will always shelve.

Yes, this gave me some headaches. I thought that as long as I use lift_MAMB only to convert a tactic living in the M world to a tactic it should be safe since the M world tactic does not produce dynamic goals. But I see now that chaining it with demote leads to the shelving, since it will throw away the demoted goals. I will see how I can improve this. As I said I can write most of my stuff in the M world, but in the end I will have a few remaining goals (of known type) and I want to convert the M world tactic into something I can run with mrun. As far as i can see, I have to demote the remaining goals for this and convert it to a tactic with match_goal, unless the M world tactic solves the goal completely.

It would be very helpful to have a generic function which converts a M world tactic of type (A -> B -> <current goal>) into a tactic one can run with mrun if the current goal is <current goal>

Definition T_MAB_APR : tactic := (match_goal with | [[ |- R]] => TT_MAB_APR <**> tintro (fun a => TT.demote) end)%TT.

Ah yes - trivial once you know it! Thanks!

view this post on Zulip Michael Soegtrop (Sep 12 2020 at 08:46):

@Janno : I get along well with tintro now and I guess I can fix the M A -> M B style tactics, although I now think that the M (A->B) style is better. Thanks for the detailed explanation!

One question: I introduced the function MAB_MBC_MAC and the notation <;> to connect tactics with type M (A->B) and M (B->C). How would you write the tactic MAB_APR without this? Is my usage non idiomatic?

view this post on Zulip Michael Soegtrop (Sep 12 2020 at 10:13):

@Janno : I removed the lower from my lift_MAMB function by passing the dynamic goals from the ttac input through to the ttac output. Since the M based tactic does not add any dynamic goals, I think this should work and at least in simple tests it does. It now reads:

Definition lift_MAMB {A B : Type} (f : M A -> M B) : ttac A -> ttac B :=
  (fun att : ttac A => (att >>= (fun '(m: a; adg) => b <- f (M.ret a) ; M.ret (m: b; adg))))%MC.

Do you foresee any issues with this definition?

view this post on Zulip Michael Soegtrop (Sep 12 2020 at 12:11):

P.S.: I updated the GIST with my playground - now everything works as expected.
(https://gist.github.com/MSoegtropIMC/36b860c8709b7602847ae929074a4d43)

view this post on Zulip Beta Ziliani (Sep 12 2020 at 14:50):

Nitpicking, I'd say I'll change the <;;> notation with <o>, mimicking the o composition operator (. in Haskell, o in math books). And i'd swap the arguments, as you do with the notation. It should be added to the library I think. I don't know about <;>, but probably too.

view this post on Zulip Michael Soegtrop (Sep 12 2020 at 17:01):

I'd say I'll change the <;;> notation with <o>

Fine with me - I thought of it more as a kind of tactic chaining (usually ; or ;;), but thinking of it as function composition is also fine.

And i'd swap the arguments, as you do with the notation

You mean for the function?

view this post on Zulip Beta Ziliani (Sep 21 2020 at 13:35):

yes, exactly

view this post on Zulip Beta Ziliani (Sep 21 2020 at 13:36):

Do you want to do a PR and we'll continue there?


Last updated: Feb 06 2023 at 05:03 UTC