Stream: Coq users

Topic: refine in Ltac2


view this post on Zulip Joachim Breitner (Dec 05 2020 at 15:57):

Still learning things about Ltac2 so this may be a pretty naive question, but what is the Ltac2 equivalent of refine ?["foo"], i.e. rename the current goal to some given string?

view this post on Zulip Joachim Breitner (Dec 05 2020 at 16:59):

More Ltac2 questions (or maybe Coq questions?): Is it expected that this changes the number of goals from 1 to 0?

      ltac1:(let n := numgoals in idtac "There are" n "goals");
      assert ($h : True) by exact I;
      ltac1:(let n := numgoals in idtac "There are" n "goals");

It prints:

There are 1 goals
There are 0 goals

so where did my goal go?

view this post on Zulip Fabian Kunze (Dec 05 2020 at 17:01):

Are you sure that in the second case, the "by" clause is only exact I and not exact I;ltac:(...)? (not sure about the precedence)

view this post on Zulip Joachim Breitner (Dec 05 2020 at 17:03):

Ah, interesting! That might explain it. I also just found that

assert ($h := I);

does not have that problem…

view this post on Zulip Joachim Breitner (Dec 05 2020 at 17:04):

Good catch, that was it. Tricky… Thanks! :-)

view this post on Zulip Fabian Kunze (Dec 05 2020 at 17:04):

you could test ...;(refine _ by _);,,,

view this post on Zulip Joachim Breitner (Dec 05 2020 at 17:06):

Right, that’s how I confirmed your theory

view this post on Zulip Paolo Giarrusso (Dec 06 2020 at 01:32):

Or also place parens around (assert by).

view this post on Zulip Paolo Giarrusso (Dec 06 2020 at 01:33):

Any tacticals that take a tactic have this bug, the tracker has an entry for the case of intuition.

view this post on Zulip Paolo Giarrusso (Dec 06 2020 at 01:33):

They should take tactic3 instead.


Last updated: Feb 01 2023 at 11:04 UTC