I would like to branch on tactic success/failure and return different constr in each branch.
For this, I tried below, but it fails. Is there a way to fix it?
Goal False. let tmp := constr:("A") in pose tmp. let tmp := tryif idtac then constr:("A") else constr:("B") in pose tmp. let tmp := tryif fail then constr:("A") else constr:("B") in pose tmp. Abort.
Ltac functions either return a tactic or a value. Afaik Ltac has some heuristics to decide this, which do not always do what you want. If you get a value returning tactic but want a tactic retuning tactic, you can prepend an "idtac; ". I am not aware of a good trick for the other way around, that is when Ltac decides your tactic returns a tactic but you want it to return a value, as in your case above.
One trick I use is to return a refine tactic which produces the value:
Goal False. let tmp := refine 1 in pose ltac:(tmp). let tmp := tryif idtac then refine 1 else refine 2 in pose ltac:(tmp). let tmp := tryif fail then refine 3 else refine 4 in pose ltac:(tmp).
I someone is aware of a better trick, I would also be interested to know it.
Btw.: I mostly switched to Ltac2 and (sometimes Mtac2) cause of this. In Ltac2 it is quite clear if a function returns a tactic or a value.
Thanks a lot for your detailed comment, @Michael Soegtrop .
I like your trick and will try that.
Also, thanks for letting me know about what Ltac2 is capable of. I should consider switching too.
It seems like the trick mentioned there (https://coq.zulipchat.com/#narrow/stream/237977-Coq-users/topic/Ltac.20to.20check.20if.20a.20term.20is.20existential.20or.20not/near/228365548) also helps here. @Michael Soegtrop
To be specific, below code works:
Ltac suceed_or_fail_to_bool TAC := match goal with | |- _ => let _ := match tt with | _ => TAC end in constr:(true) | |- _ => constr:(false) end . Goal False. let tmp := suceed_or_fail_to_bool idtac in pose tmp. let tmp := suceed_or_fail_to_bool fail in pose tmp. Abort.
Neat! One could pass the values selected for success and fail as arguments as in:
Ltac suceed_or_fail_select TAC S F:= match goal with | |- _ => let _ := match tt with | _ => TAC end in S | |- _ => F end. Goal False. let tmp := constr:(1) in pose tmp. let tmp := suceed_or_fail_select idtac constr:(2) constr:(3) in pose tmp. let tmp := suceed_or_fail_select fail constr:(4) constr:(5) in pose tmp.
But I wonder why this doesn't work:
Tactic Notation "if_success" tactic(TAC) "then" constr(S) "else" constr(F) := suceed_or_fail_select TAC S F. Goal False. let tmp := if_success idtac then 2 else 3 in pose tmp.
Tactic Notation solution doesn't work because
Tactic Notations are not allowed to return constrs. All
Tactic Notations effectively implicitly have an
@Jason Gross : thanks for the clarification!
I must say I meanwhile really like Ltac2, also because these things are explicit there. At the beginning this can be a burden, because the heuristics of Ltac frequently do the right thing and one doesn't really need to understand it in too much depths to use it. Ltac2 needs more understanding upfront - and honestly the docs could be improved a bit to make this easier - but it doesn't take that much complexity until Ltac2 is really much easier than Ltac. Mtac2 goes along this path, it is substantially more obscure upfront, but there is a level of complexity where things get easier with it.
@Pierre-Marie Pédrot : one thing I still miss in Ltac2 to make it even more explicit are return type annotations.
I think there is an open wish somewhere. It shouldn't be hard to do but due to campl5 it's always risky to tweak the grammar without triggering unwanted changes of syntax without realizing
Last updated: Feb 04 2023 at 23:02 UTC