Ralf Jung (Oct 14 2023 at 07:29): 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.
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)
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
Ralf Jung (Oct 16 2023 at 13:26):filed a feature request: https://github.com/coq/coq/issues/18167
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.
that seems to work, thanks!
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?
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 1introduces 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).
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))}.
Well actually this also works without LibHyps:
intros until n;
(match goal with
H: _ |- _ => (inversion H; clear H)
end).
intros until is new to me, Im going to check that out, thanks!
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?
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
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.
Ralf Jung (Oct 27 2023 at 18:15):@Pierre Courtieu that seems to work, thanks a lot :)
Last updated: Oct 13 2024 at 01:02 UTC