Stream: Ltac2

Topic: pose proof / issues with ltac2 in assert

Michael Soegtrop (Mar 05 2021 at 14:03):

@Pierre-Marie Pédrot I try to write a function for pose proof. I guess in Ltac2 Std.v the constructor AssertValue (ident, constr) should get an ident option to make this easy, or am I missing something?

This variant does work:

Require Import Ltac2.Ltac2.

Definition type_of {T : Type} (t : T) := T.

Ltac2 type_of (x : constr) := eval cbv beta delta [type_of] in (type_of $x).

Ltac2 pose_proof (proof_term : constr) :=
  let proof_type := type_of proof_term in
  assert ($proof_type) by exact $proof_term.

Goal True.
  pose_proof constr:(I).
  exact H.
Qed.

but I wonder why this one doesn't:

Ltac2 rct(x : constr) := Control.refine (fun () => x).

Ltac2 pose_proof' (proof_term : constr) :=
  assert (ltac2:(rct (type_of proof_term))) by exact $proof_term.

It gives an error The reference rct was not found in the current environment. which I don't understand. It looks like ltac2 doesn't work in the argument of assert.

Pierre-Marie Pédrot (Mar 05 2021 at 17:21):

This is a parsing issue.

Pierre-Marie Pédrot (Mar 05 2021 at 17:22):

assert (ltac2:(foo)) is parsed as if you were willing to assert the hypothesis named ltac2 with type foo.

Pierre-Marie Pédrot (Mar 05 2021 at 17:23):

It's one of the reasons I am not very fond of the current quotation system: it's very fragile from a parsing point of view.

Pierre-Marie Pédrot (Mar 06 2021 at 09:59):

FTR, you can work around this by adding a pair of parentheses around the ltac2:(...) quotations. It will force the parser to consider it as a Gallina term.

Michael Soegtrop (Mar 06 2021 at 14:24):

assert (ltac2:(foo)) is parsed as if you were willing to assert the hypothesis named ltac2 with type foo.

Ah yes, I can see that it is tricky to get the ltac2: parsed as I intended it.

It's one of the reasons I am not very fond of the current quotation system: it's very fragile from a parsing point of view.

Do you have a suggestion for an alternative which would be more robust?

Last updated: Oct 12 2024 at 12:01 UTC