Stream: Ltac2

Topic: Query the strategy of a symbol in Ltac2

Michael Soegtrop (Sep 12 2022 at 09:55):

I wonder if there is a way to query the strategy (opaque, transparent, in between) of a symbol in Ltac2.

Pierre-Marie Pédrot (Sep 14 2022 at 08:29):

Not that I know of.

Enrico Tassi (Sep 14 2022 at 14:18):

You can do that in elpi, and call an elpi tactic via ltac1 (horrible, but ...)
https://github.com/LPCIC/coq-elpi/blob/e4bf0b0b3e092b16c89b4e49d64523902fe24d13/coq-builtin.elpi#L1396

Enrico Tassi (Sep 14 2022 at 14:19):

If you tell me the "API" you want I can easily write a few lines for you. Given the bridge, the output has to be a term I guess

Enrico Tassi (Sep 14 2022 at 14:20):

Alternatively, you cal look at the OCAML code implementing these APIs, and take inspiration to write ltac2 bindings

Enrico Tassi (Sep 14 2022 at 14:21):

https://github.com/LPCIC/coq-elpi/blob/e4bf0b0b3e092b16c89b4e49d64523902fe24d13/src/coq_elpi_builtins.ml#L3151-L3179

Michael Soegtrop (Sep 14 2022 at 14:31):

@Enrico Tassi : thanks! Essentially in Ltac2 I have a constr which is a reference or a reference (one can convert between the two, so I don't care) and want an Ltac2 integer, but a constr with a Gallina Z or positive is fine (I have conversion functions for these).

Michael Soegtrop (Sep 14 2022 at 14:36):

@Enrico Tassi : actually looking at this post (https://coq.zulipchat.com/#narrow/stream/237977-Coq-users/topic/Custom.20reduction/near/298778993) I might be more interested in the "original opaqueness", that is if a symbols was defined with Qed or not.

Enrico Tassi (Sep 14 2022 at 19:21):

I'm a bit in a hurry, here a draft:

From elpi Require Import elpi.

Elpi Tactic is_qed_opaque.
Elpi Accumulate lp:{{

pred is-opaque i:gref, o:term.
is-opaque (indt _)  {{ true }}.
is-opaque (indc _)  {{ true }}.
is-opaque (const C) {{ true }} :- coq.env.const C none _, !.
is-opaque (const _) {{ false }}.

solve (goal _ _ _ _ [trm T] as G) GLS :-
  coq.term->gref T GR,
  is-opaque GR B,
  refine B G GLS.

}}.
Elpi Typecheck.

Tactic Notation "is-opaque" uconstr(c) := elpi is_qed_opaque ltac_term:(c).

Lemma x : unit. Proof. exact tt. Qed.
Lemma y : unit. Proof. exact tt. Defined.

Goal True.
pose (b1 := (ltac:(is-opaque nat))).
pose (b2 := (ltac:(is-opaque S))).
pose (b3 := (ltac:(is-opaque x))).
pose (b4 := (ltac:(is-opaque y))).

pose (b5 := (ltac:(is-opaque 37))).
pose (b6 := (ltac:(is-opaque plus))).
Abort.

Last updated: Sep 15 2024 at 13:02 UTC