Stream: Coq users

Topic: Writing a tactic that takes "ident or term number"?


view this post on Zulip Ralf Jung (Oct 14 2023 at 07:29):

Many Coq tactics such as destruct and inversion can be used as inversion N to invert the Nth term on the goal. How can I write a wrapper around them that does the same? e.g. I want to write a wrapper around inversion that does some extra things like subst, but still supports both inversion H and inversion 1.

view this post on Zulip Ralf Jung (Oct 14 2023 at 07:30):

(I'd be okay implementing such a tactic in Ltac2, but it is fundamentally required that the tactic can be called directly from Ltac1)

view this post on Zulip Ralf Jung (Oct 14 2023 at 08:13):

I found the int_or_var tactic notation argument class, but it says that's the same as for do, so it's probably not the ident|natural that I want here

view this post on Zulip Ralf Jung (Oct 16 2023 at 13:26):

filed a feature request: https://github.com/coq/coq/issues/18167

view this post on Zulip Ike Mulder (Oct 16 2023 at 14:32):

At least for ident | natural, overloading the tactic seems to work?

Tactic Notation "my_inversion" int_or_var(n) := idtac "got int";  inversion n.
Tactic Notation "my_inversion" ident(c) := idtac "got ident"; inversion c.

Lemma test (A B C D : Prop) : A /\ B -> B /\ C -> C /\ D -> C.
Proof.
  my_inversion 3. Undo 1.
  intros H1 H2. my_inversion H1.
  Fail my_inversion True.
Abort.

view this post on Zulip Ralf Jung (Oct 22 2023 at 16:21):

that seems to work, thanks!

view this post on Zulip Ralf Jung (Oct 22 2023 at 16:23):

However, now I have the next problem... the point of the tactic is to clear the term being inverted. inversion 1 introduces a new term under some fresh name which we hence should clear. but I don't think there is a way to tell Coq which name to use?
Currently it seems like we have to completely re-implement the logic for "invert the n-th term", but maybe there is some clever way to reuse the logic from the core tactics?

view this post on Zulip Pierre Courtieu (Oct 24 2023 at 08:45):

Ralf Jung said:

However, now I have the next problem... the point of the tactic is to clear the term being inverted. inversion 1 introduces a new term under some fresh name which we hence should clear. but I don't think there is a way to tell Coq which name to use?
Currently it seems like we have to completely re-implement the logic for "invert the n-th term", but maybe there is some clever way to reuse the logic from the core tactics?

You can try to use or take ideas from my library LibHyps. There is a tactical "tac1; { tac2 }" that applies tac1 and then tac2 to "new" hyps i.e. hyps having names that wern't there before tac1 was applied).

view this post on Zulip Pierre Courtieu (Oct 24 2023 at 15:38):

Here is a solution with LibHyps. Several points:

Require Import LibHyps.LibHyps.
Tactic Notation "my_inversion" ident(c) := idtac "got ident"; inversion c.

(* Apply tac ont he first hypothesis of the list l. *)
Ltac onFirstHyp tac l :=
  match l with
    @DCons  _ ?H _ => inversion H;clear H
  | _ => idtac "vide"
  end.
Tactic Notation "my_inversion" int_or_var(n) :=
  idtac "got int";
  (* tactical ;{!< tac } applies on the list of new hyps in order
     "newest first", so the the first hyp is actually the last introduced. *)
  intros until n; {!< onFirstHyp ltac:(fun h => (inversion h; clear h))}.

view this post on Zulip Pierre Courtieu (Oct 24 2023 at 15:41):

Well actually this also works without LibHyps:

  intros until n;
  (match goal with
     H: _ |- _ => (inversion H; clear H)
   end).

view this post on Zulip Ralf Jung (Oct 27 2023 at 17:41):

intros until is new to me, Im going to check that out, thanks!

view this post on Zulip Ralf Jung (Oct 27 2023 at 17:43):

oh wait, the actual magic is match goal here. this relies on hypothesis match order, doesn't it?

view this post on Zulip Ralf Jung (Oct 27 2023 at 17:44):

is that guaranteed? I can't see it in https://coq.inria.fr/refman/proof-engine/ltac.html#coq:tacn.match-goal

view this post on Zulip Ralf Jung (Oct 27 2023 at 17:45):

ah it is

Hypothesis matching for match_hyps normally begins by matching them from left to right, to hypotheses, last to first.

view this post on Zulip Ralf Jung (Oct 27 2023 at 18:15):

@Pierre Courtieu that seems to work, thanks a lot :)


Last updated: Jun 13 2024 at 21:01 UTC