Reduce tactic arguments · Elpi users & devs

Stream: Elpi users & devs

Topic: Reduce tactic arguments

Tomaz Gomes (Sep 24 2024 at 12:30):

The syntax seems to work! But I encountered another problem. Consider for instance this predicate:

  replace I O :-
    (copy {{ 2%nat }} {{ 3%nat }}) => copy I O.

We can successfully apply it in the following cases:

Tactic Notation "replace" ident(i) constr(x) :=
  elpi replace_tac ltac_string:(i) ltac_term:(x).

Definition a := 2.

Goal False.
  replace foo 2.
  let a := eval hnf in a in
  replace bar a.
  Abort.

But the following cases don't work:

Definition f : nat -> nat := fun _ => a.

Goal False.
  let f := eval hnf in f in
  replace bar f.
  Abort.

If we fully reduce f first (eval compute in f in ...) then it works, but I would prefer not to use this. Do you have an idea of what is the best strategy to reduce f maybe during the execution of copy in order to be able to do the replace?

Notification Bot (Sep 24 2024 at 12:32):

A message was moved here from #Elpi users & devs > Extending predicate with multiple clauses by Enrico Tassi.

Enrico Tassi (Sep 24 2024 at 12:35):

I don't have the full code, that would help.

I suggest you do not call hnf outside, but rather use any coq.reduction.* APIs provided by Elpi: https://github.com/LPCIC/coq-elpi/blob/31279beb7532a39fa0c0d6405cd92451814e4899/builtin-doc/coq-builtin.elpi#L1503

solve (goal _ _ _ _ [str Id, trm T] as G) GL :-
  coq.reduction.lazy.norm T T1,
  your-code Id T1 G GL.

Last updated: Oct 13 2024 at 01:02 UTC