Ltac question: `tryif` returning `constr` · Coq users

Hi all,
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.

Michael Soegtrop (Mar 01 2021 at 14:47):

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.

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

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.

YoungJu Song (Mar 04 2021 at 10:03):

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.

YoungJu Song (Mar 04 2021 at 10:30):

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.

Michael Soegtrop (Mar 04 2021 at 12:46):

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.

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.

Jason Gross (Mar 04 2021 at 13:03):

The Tactic Notation solution doesn't work because Tactic Notations are not allowed to return constrs. All Tactic Notations effectively implicitly have an idtac; prepended.

Michael Soegtrop (Mar 05 2021 at 09:53):

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.

Pierre-Marie Pédrot (Mar 05 2021 at 11:48):

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

Stream: Coq users

Topic: Ltac question: `tryif` returning `constr`