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.
It's not easy to find: Ttactics.TT.tintro
should be the right thing
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.
I fail to see why you need lift_fMAB
, if lift
is parametric in the type (and can therefore work with ?A -> ?B
)
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
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.
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.
ah I see. but then, where you want to use tintro
?
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.
feel free to make an example and we'll look into it
@Beta Ziliani, @Janno : I created a small playground to explain the typed intro issue:
(https://gist.github.com/MSoegtropIMC/36b860c8709b7602847ae929074a4d43)
The questions I have:
I created tactics with a M (A->B) and a M A -> M B type. Both work but when I mrun a tactic created from the latter, demoted goals end up on the shelve while in the first case they are immediate goals. I guess this has to do with how I do the demote - maybe I need a different combinator?
In both cases I would like to have a variable introduced in a type safe way, but I can't figure out how.
Am I doing this in a sensible way?
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.
But I suppose that only affects the first version
I am still going through the file and trying to understand the definitions.
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.
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).
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!
@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?
@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?
P.S.: I updated the GIST with my playground - now everything works as expected.
(https://gist.github.com/MSoegtropIMC/36b860c8709b7602847ae929074a4d43)
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.
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?
yes, exactly
Do you want to do a PR and we'll continue there?
Last updated: Feb 06 2023 at 05:03 UTC