Michael Soegtrop (Aug 26 2020 at 15:26): Michael Soegtrop (Aug 26 2020 at 15:26):I have difficulties to get the details of using TT.ttac right. E.g. I have the following using the M monad:
Definition EqReflFail : Exception. constructor. Qed.
Definition MTAC_eq_refl {T : Type} {a b : T} : M (a=b) :=
mmatch a=b as eq return M eq with
| [? x] x=x => M.ret (@Coq.Init.Logic.eq_refl T x)
| _ => M.raise EqReflFail
end.
which I hope solves an equation by reflexivity in case this is possible and throws an exception otherwise. I somehow can't figure out how to convert this to using TT.ttac, so that it has the signature:
Definition MTAC_eq_refl {T : Type} {a b : T} : TT.ttac (a=b)
instead
Janno (Aug 26 2020 at 15:29):What about the following?
Definition MTAC_eq_refl {T : Type} {a b : T} : TT.ttac (a=b) :=
mmatch a=b as eq return TT.ttac eq with
| [? x] x=x => TT.apply (@Coq.Init.Logic.eq_refl T x)
| _ => M.raise EqReflFail
end.
Embarrassing - I was sure I tried this but as it looks I had a typo somewhere and couldn't make sense out of the error message.
Janno (Aug 26 2020 at 15:31):Sadly the error messages are always horrible :(
Janno (Aug 26 2020 at 15:32):BTW: To actually run typed tactics we usually wrap them in normal tactics using the match_goal notation in the %TT scope which allows one to use ttacs in the branches of match_goal.
Michael Soegtrop (Aug 26 2020 at 15:33):Yes, I saw that. I need some more experience with what type safety I get then.
Michael Soegtrop (Aug 26 2020 at 15:35):E.g. right now I wonder what is best practice if I know a tactic leaves a goal and I can statically say what this goal would be. Should I demote it as dynamic goal or specify this in the static type? In the latter case, how would I do it? Can I just add a hypothesis to the goal and it would still be able to apply it to the goal without this hypothesis?
Janno (Aug 26 2020 at 15:39):There is no general recommendation here. I tend to expose as many static types as possible but sometimes the type of the subgoal involves binders that one cannot easily refer to in the type of the tactic.
Janno (Aug 26 2020 at 15:39):I don't understand the second part of your question.
Beta Ziliani (Aug 26 2020 at 15:40):Can you provide an example @Michael Soegtrop ?
Michael Soegtrop (Aug 26 2020 at 15:49):Say I have a Mtac2 tactic (return type TT.ttac X) which applies a lemma A->B->X. The premise of type A I can solve with another Mtac2 tactic, but the premise of type B not. Now I can demote it, but then, as far as I understand, this wouldn't show up in the type of the tactic. In such a case, can I use TT.ttac (B->X) as return type, or does this have disadvantages in certain usages of the tactic then? Is there a better type to return than TT.ttac (B->X) or is TT.ttac (B->X) just fine?
Michael Soegtrop (Aug 26 2020 at 15:51):Another best practices thing I wonder about: if my tactic does not produce dynamic goals, should I return M X or should I always stick to TT.ttac X in order to make the use of tactic combinators easier?
Janno (Aug 26 2020 at 16:21):If you can mention the goal in the static type I do not see any downside to that.
Janno (Aug 26 2020 at 16:23):Another best practices thing I wonder about: if my tactic does not produce dynamic goals, should I return
M Xor should I always stick toTT.ttac Xin order to make the use of tactic combinators easier?
I don't think we have enough examples to know what works best. I find myself converting M programs to ttac programs sometimes because I realize I do actually want to be able to spawn new subgoals. But I don't keep count so I can't quite say how often that has happened to me.
Michael Soegtrop (Aug 26 2020 at 16:30):@Janno : thanks - I will stick to ttac then until I find a reason for not doing so.
My first debugging question: I defined a function with return type TT.ttac X where X is some Prop and am in a proof context (started with Proof, not with MProof) where the goal is X. Now I do "mrun my_tactic" and I get an error "Different types", which puzzles me a bit.
Janno (Aug 26 2020 at 16:34):mrun doesn't actually know how to run typed tactics (to avoid making the interpreter more complex). As mentioned above in this thread I recommend the (match_goal with .. end )%TT to get a tactic that calls your ttac.
Janno (Aug 26 2020 at 16:34):That horrible error message is on us though and I'll make an issue to improve that.
Janno (Aug 26 2020 at 16:36):Sorry, my comment above said "mrun doesn't know how to run tactics" but it was meant to say "mrun doesn't know how to run typed tactics".
Michael Soegtrop (Aug 26 2020 at 16:37):I see. So I can use mrun to run tactics returning (M X) but not (ttac X).
Janno (Aug 26 2020 at 16:37):and mrun also runs tactics.
Michael Soegtrop (Aug 26 2020 at 16:43):I got confused by this example in tauto.v:
Module Mtac_V4.
:
Program Definition solve_tauto : forall {P:Prop}, ttac P :=
:
Ltac solve_tauto := mrun solve_tauto.
:
MProof.
r <- solve_tauto; M.ret (mfst r).
Qed.
I saw the tactic definition with mrun for a ttac tactic, but didn't realize it is used in a different way than the other tactic definitions in this file.
Janno (Aug 26 2020 at 17:02):Oh, that Ltac .. line should probably not be in there.
Michael Soegtrop (Aug 26 2020 at 18:04):I am still struggling with properly applying a tactic returning a ttac. What I am doing is:
Definition TestTTac (x : X) (y : Y) : TT.ttac (my_prop x y) := ...
Definition TestTac : tactic :=
(match_goal with
| [[? x y |- my_prop x y ]] => r <- TestTTac x y; M.ret (mfst r)
end
)%TT.
Goal ...
mrun TestTac.
This works but it leaves the dynamic goals on the shelve. Is there a way to apply an Mtac2 tactic function such that the goals end up on the goal stack?
Beta Ziliani (Aug 26 2020 at 18:26):ah, M.ret there is not what you need, I think it's to_T
Beta Ziliani (Aug 26 2020 at 18:26):so it won't forget the goals generated by your tactic
Janno (Aug 26 2020 at 18:59):Wait, this shouldn't even typecheck. I suppose there is coercion somewhere that gets in the way. The branch should just be TestTTac x y.
Michael Soegtrop (Aug 26 2020 at 21:14):Janno said:
Wait, this shouldn't even typecheck. I suppose there is coercion somewhere that gets in the way. The branch should just be
TestTTac x y.
This is inspired by this example: (https://github.com/Mtac2/Mtac2/blob/b89e2770cae592ef9a3bf7a1cd45cec90ddabc34/examples/tauto.v#L191). I have seen a coercion from M to ttac.
Can you give me a few more hints on the recommended way of applying an Mtac2 function with type "ttac X" to a goal of type X?
Janno (Aug 27 2020 at 07:31):The recommended way is (match_goal with | [[ |- X ]] => my_ttac end)%TT. where my_ttac : ttac X.
Michael Soegtrop (Aug 27 2020 at 09:13):The recommended way is
(match_goal with | [[ |- X ]] => my_ttac end)%TT. wheremy_ttac : ttac X.
thanks, this does work as expected!
I have the impression that some parts of the tauto.v example more drag people away from the right path than pushing them to it. Do you think it would help if I review it now as a fresh new user of Mtac2 or do you see from our discussion where the issues are?
I would btw. think that it makes sense to recommend people to first start with the old Mtac1 tutorial (adjusted to work with Mtac2) and then start the Mtac2 (ttac) tutorial with a short comment on the issues of M (with a link to your Mtac2 paper). The combined tutorials should be very effective - with a few minor changes to tauto.v as discussed above.
I put a port of the Mtac1 tutorial here: (https://gist.github.com/MSoegtropIMC/f5fe0426acba807d9bf7c98829a6059d) but with what I learned in the last 24 hours I would rework it again (especially I replaced run with eval, but I guess in many cases it should be replaced with mrun). I can do this rework this weekend. I am sure I will mess up a few things, but I hope this gives you some input and where additional information is required.
One more note: if run is replaced with eval in the old tutorial, the eval remaining in the proof terms looks really scary. I understand that it is safe because the type checker evaluates it to check its type, but it is less obvious that this is safe than when run is used, where you end up with a usual proof term or fail - not with a proof term which contains a functions which is not per se guaranteed to terminate. I would think that this deserves some extra words, especially that Mtac2 - as far as I understand from the papers - does not do any changes to the Coq kernel to achieve what it does.
All in all my first impression of Mtac2 is very good - thanks for the great work!
Janno (Aug 27 2020 at 11:32):I have the impression that some parts of the tauto.v example more drag people away from the right path than pushing them to it. Do you think it would help if I review it now as a fresh new user of Mtac2 or do you see from our discussion where the issues are?
I've seen at least 1 issue (the misleading mrun call with a ttac argument that is never actually used and would fail anyway). I am so far removed from being new to Mtac2 that it is often hard for me to spot how inaccessible the tutorials are. You giving it a thorough review would be very much appreciated.
especially I replaced run with eval, but I guess in many cases it should be replaced with mrun [...]
with a proof term which contains a functions which is not per se guaranteed to terminate
I often forget eval even exists. We need some kind of high-level documentation that tells people what the proper entry points to running tactics are. mrun is indeed the right thing basically always. BTW: eval simply uses a Hint Extern to call mrun during type class search, which then fills in the result of the computation. There really is no trickery here except for the usual thing in Coq where it's hard to figure out what's going on from the outside. And indeed, we do not modify the kernel at all!
I can do this rework this weekend. I am sure I will mess up a few things, but I hope this gives you some input and where additional information is required.
I am more than happy to look over anything you produce and incorporate it into the repository (and whatever other place would be best for documentation). Thank you so much!
All in all my first impression of Mtac2 is very good - thanks for the great work!
I think I can speak for both Beta and me when I say we are happy to hear that!
Beta Ziliani (Aug 27 2020 at 12:22):I did already pushed the tutorial in the master branch, carefully mentioning that eval is best avoided: https://github.com/Mtac2/Mtac2/blob/master/examples/basics_tutorial.v
Beta Ziliani (Aug 27 2020 at 12:23):and yes to everything :-)
Michael Soegtrop (Aug 27 2020 at 12:37):Very well - I will review the combined tutorials with my new user glasses.
Michael Soegtrop (Sep 03 2020 at 12:16):Beta Ziliani said:
I did already pushed the tutorial in the master branch, carefully mentioning that
evalis best avoided: https://github.com/Mtac2/Mtac2/blob/master/examples/basics_tutorial.v
I went through the revised tutorial - very nice. For the moment just one comment: the use of Mtac Do in line 232 is a bit unmotivated.
I am still experimenting with M and ttac, so I am not yet sure what I would write into a tutorial - trying to get the sweet spot between not understanding it and not understanding people who don't understand it.
Michael Soegtrop (Sep 03 2020 at 13:21):@Beta Ziliani
A few more editorial points (besides the one just above):
I would write
(** One problem with [Program] is that it generates big proof terms. *)
Print inlist'.
(* Let's look at the proof terms generated in the obligations and plug
those terms into the holes. *)
Print inlist'_obligation_1.
Print inlist'_obligation_2.
because otherwise people might think you say that the obligations are large.
In
Program
Definition search (P : Prop) :=
mfix1 f (s:list dyn) : M P :=
mmatch s with
| [? (x:P) s'] (Dyn x) :: s' => ret x
| [? d s'] d :: s' => f s'
| _ => raise NotFound
end.
the Program is not required although you just explained why it is required. This looks outdated.
In
Instead, we use two new operators: [nu] and [abs]
abs should be abs_fun.
In the last example, the connection between eval and the operator [H] remains unclear. This section looks interesting, but from the description I really don't understand exactly what [H] does, even on second read. Looking up definitions of [ makes things even more obscure. I think this deserves a few more words.
Except for these minor points, I would say this tutorial is very nice.
Beta Ziliani (Sep 03 2020 at 15:41):Thanks for the comments, Michael! I pushed changes to the tutorial based on them
Michael Soegtrop (Sep 04 2020 at 07:34):@Beta Ziliani :
sorry for nitpicking, but I think some points need more changes:
for Mtac Do there is no explanation whatsoever what this does or is good for. I think you should give a few more examples (besides the definition of the Exception).
for Program Definition you removed the Program, but still explain in the comment above that it is needed. It would be interesting to know if UniCoq now solves the problem you used to solve with Program. If so maybe a word on this would be worthwhile at this point.
the [H] things is still a bit obscure. With your change it becomes clear that [H] has nothing to do with eval (I got this wrong before). But the [H] feature itself is still unclear. For what kind of pattern can it be used? Pairs or something more generic? I think you should leave a few words on why this deserves a special syntax and what would happen if you wouldn't have this special syntax.
One more thought: I think it would be nice if you would replace the auto in the last proof with an extension of tauto which can handle equalities by reflexivity. Which opens the question how one writes extensible code in Mtac2 ... . In Ltac1 the appendix D method is to use tactic notations. They can be reassigned to different tactics and when a notation is used in a tactic it uses the latest definition. This for sure won't work with Mtac2 since it is Gallina, but I wonder how you handle this in your applications of Mtac. One could e.g. pass some kind of Gallina structure with some sort of hint database, possibly as a type class or use modules to provide some context to a Mtac2 tactic - I think of something like ring or field. The best infrastructure for writing extensible tactics is - I would say - found in Coq-Elpi.
Beta Ziliani (Sep 04 2020 at 15:42):Good points!
for Mtac Do there is no explanation whatsoever what this does or is good for. I think you should give a few more examples (besides the definition of the Exception).
Do you think it is best to remove it, or to explain it? I'm unsure at what's best here.
One more thought: [...]
One way to make open-ended tactics is to use typeclasses. Or you can probably also use Coq notations. We can work an example together if you want.
Michael Soegtrop (Sep 04 2020 at 16:06):for Mtac Do there is no explanation whatsoever what this does or is good for. I think you should give a few more examples (besides the definition of the Exception).
Do you think it is best to remove it, or to explain it? I'm unsure at what's best here.
I would put in a small example as alternative to Definition with ! e.g. to evaluate the collatz sequence. It is not terribly elegant that you have to Define + Print. How about:
(** An alternative method to print the result of an Mtac2 computations without creating a definition is: *)
Mtac Do collatz 6 >>= M.print_term.
(** where [a >>= f] is a notation for [M.bind a f] and [M.print_term] is a Mtac2 function to print arbitrary terms *)
I would put this after the Define+Print.
One way to make open-ended tactics is to use typeclasses. Or you can probably also use Coq notations. We can work an example together if you want.
In order to keep the tutorial short - right now it has a very good balance - I would think about putting some hook into the tauto tactic which allows to plug in additional tactics to solve the leaf propositions, like e.g. reflexivity, and use this in the final example. Not sue how one would do this ...
Michael Soegtrop (Sep 04 2020 at 16:11):P.S.: I would prefer a type class or module solution to the extension of tactics. The notation hack used in Ltac1 is really an ugly hack.
Janno (Sep 04 2020 at 16:38):I am also interested in a TC-based approach to extending tactics.
Janno (Sep 04 2020 at 16:39):I don't think the problem is easy to solve. There are several alternative solutions and none of them seem particularly great. The big question mark for me is the problem of integrating TC backtracking with Mtac2 backtracking.
Janno (Sep 04 2020 at 16:41):It seems to me that there are basically two possibilities: either one takes the first TC instance and just uses that. If it fails there is no further TC search. (This model would have TC instances with a field of type M ...)
Alternatively, one simply uses mrun to run Mtac2 code at TC search time. This way one can try multiple TC instances until one succeeds.
Janno (Sep 04 2020 at 16:42):However, neither method allows distinguishing fatal failures from "not applicable" failures and debugging/maintaining these kinds of tactics can get very hard without being able to easily observe that distinction
Michael Soegtrop (Sep 04 2020 at 16:51):Did you consider using the module system? Unlike type classes it would not add a second kind of backtracking or ltac code - it would be in this sense deterministic. Of cause it is not "first class citizen" as type classes are, but I think for really complicated stuff it is more manageable than type classes cause of this determinism and the guidance it gives to the user. Also one can still make it first class for specific instances by registering module generated instances to the type class system. The downside is that these could not be parametric. I am not sure how bad this would be - for ring and field e.g. parametricity was only added very recently.
Paolo Giarrusso (Sep 04 2020 at 18:15):How do modules let you extend stuff?
Paolo Giarrusso (Sep 04 2020 at 18:16):Oh.
Paolo Giarrusso (Sep 04 2020 at 18:16):You want a module that abstracts over the implementation of some function?
Paolo Giarrusso (Sep 04 2020 at 18:19):You could still use normal abstraction or typeclasses for that, without using TC backtracking. No need for second-class abstraction. I'll admit that's true for every use of Coq modules, modulo ergonomics.
Michael Soegtrop (Sep 05 2020 at 09:00):Paolo Giarrusso said:
You want a module that abstracts over the implementation of some function?
That is one way - have an implementation of some Mtac2 program inside of a module functor and plug in bits and pieces via supplying arguments to the functor.
Another way is to give some record with some extensions to the Mtac2 program and use modules to construct such records. In general this can get quite complicated, e.g. might require the development of some theory with a certain structure, which could be defined with a module type.
I agree that for an example in the tutorial it is probably best to have some record type with functions to extend the functionality of an Mtac2 program and literally pass this record when the function is called. How one constructs and supplies such a record - with type classes, modules, canonical structures, Elpi, yet another Mtac2 program, you name it, can be left open.
Last updated: Feb 06 2023 at 05:03 UTC