I am having a strange case where this works
match goal with H: of_slot_data d ≡ ps |- _ => rename H into H1 end.
but when I try to wrap this code into a tactic, it fails
Tactic Notation "myrename" uconstr(pat) "into" ident(Hnew) := lazymatch goal with| H : pat |- _ => rename H into Hnew end.
constr, all to no avail. I think what happens is that when I call my own tactic, Coq infers the term to be
@equiv (cmra_car per_slot) (ofe_equiv (cmra_ofeO per_slot)) (of_slot_data d) ps
which does not match the hypothesis any more. However, when I write a
match inline in the proof script it works, possibly because it defers inferring the hole (the type of the equivalence).
is there any way to actually abstract over the pattern of a
open_constr seems not listed at https://coq.inria.fr/refman/user-extensions/syntax-extensions.html#coq:cmd.Tactic-Notation)
I can't contribute anything to the problem, and likely this is unrelated, but it should be
into Hnew, not
into Hew in your
oh, so maybe I was mislead by that typo during my experiments
but we have
rename select pat into name in std++ and that one also fails, so it's not just me being silly^^
yeah it still fails the same way after fixing that
Set Ltac Debug shows that it does not even enter the match arm; it's the
lazymatch that breaks
I think you're hitting the famous pattern_of_constr piece of code.
yeah, I think I might
and it's entirely unnecessary, all I really need is
Tactic Notation "mytac" pattern(foo)
Any updates on this? I end up using this which is not ideal
Tactic Notation "rename_by_type" constr(t) "into" ident(Hname) := match goal with | H : context [t] |- _ => rename H into Hname end.
I was about to ask this exactly same question but the search lead me to here, I was trying this
(* this works *) Tactic Notation "when" uconstr(x) "do" tactic(t) := match goal with | |- context[x] => t | _ => idtac end. (* this not *) Tactic Notation "apply_by_type" uconstr(t) := match goal with | H' : t |- _ => apply H' end. Variable a : Set. Variable P : a -> Prop. Variable Q : Prop. Axiom PQ : forall x, P x -> Q. Goal forall x, (P x) -> Q. intros ?. when (P _ -> _) do (apply PQ). Qed. Goal forall x, P x -> P x. intros ? ?. (* this fails *) Fail apply_by_type (P x). (* but this works *) match goal with | H : P _ |- _ => apply H end. Qed.
@Daniel Hilst Selli for a slight improvement see here https://gitlab.mpi-sws.org/iris/stdpp/-/blob/master/stdpp/tactics.v#L651
That still has the bug that Ralf described, but in somewhat advanced scenarios; that tactic mostly works
thanks @Paolo Giarrusso
BTW this file is a perl of ltac, lots of rich examples
Last updated: Jan 28 2023 at 05:02 UTC