Zulip Chat Archive

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.

Janno (Sep 07 2020 at 08:44):

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.

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

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.

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.

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)

Michael Soegtrop (Sep 07 2020 at 13:41):

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

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.

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.

Beta Ziliani (Sep 07 2020 at 13:57):

Michael Soegtrop (Sep 07 2020 at 14:01):

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.

Beta Ziliani (Sep 07 2020 at 19:09):

Michael Soegtrop (Sep 11 2020 at 09:51):

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

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.

Janno (Sep 11 2020 at 12:03):

Janno (Sep 11 2020 at 12:04):

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.

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).

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.

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?

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.

Michael Soegtrop (Sep 12 2020 at 12:11):

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.

Michael Soegtrop (Sep 12 2020 at 17:01):

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.

Stream: Mtac2

Topic: chained typed intro

Michael Soegtrop (Sep 07 2020 at 08:03):