Stream: Coq users

Topic: Ltac: abstracting over pattern?


view this post on Zulip Ralf Jung (Jun 17 2021 at 09:51):

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.

I tried uconstr, open_constr and 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 match?

view this post on Zulip Ralf Jung (Jun 17 2021 at 09:53):

(btw, open_constr seems not listed at https://coq.inria.fr/refman/user-extensions/syntax-extensions.html#coq:cmd.Tactic-Notation)

view this post on Zulip Yannick Forster (Jun 17 2021 at 10:04):

I can't contribute anything to the problem, and likely this is unrelated, but it should be into Hnew, not into Hew in your myrename

view this post on Zulip Ralf Jung (Jun 17 2021 at 10:22):

oh, so maybe I was mislead by that typo during my experiments

view this post on Zulip Ralf Jung (Jun 17 2021 at 10:23):

but we have rename select pat into name in std++ and that one also fails, so it's not just me being silly^^

view this post on Zulip Ralf Jung (Jun 17 2021 at 10:24):

yeah it still fails the same way after fixing that

view this post on Zulip Ralf Jung (Jun 17 2021 at 10:24):

Set Ltac Debug shows that it does not even enter the match arm; it's the lazymatch that breaks

view this post on Zulip Pierre-Marie Pédrot (Jun 17 2021 at 11:59):

I think you're hitting the famous pattern_of_constr piece of code.

view this post on Zulip Ralf Jung (Jun 17 2021 at 15:15):

yeah, I think I might

view this post on Zulip Ralf Jung (Jun 17 2021 at 15:15):

and it's entirely unnecessary, all I really need is Tactic Notation "mytac" pattern(foo)

view this post on Zulip Daniel Hilst Selli (Sep 01 2022 at 20:39):

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.

view this post on Zulip Paolo Giarrusso (Sep 01 2022 at 21:49):

@Daniel Hilst Selli for a slight improvement see here https://gitlab.mpi-sws.org/iris/stdpp/-/blob/master/stdpp/tactics.v#L651

view this post on Zulip Paolo Giarrusso (Sep 01 2022 at 21:50):

That still has the bug that Ralf described, but in somewhat advanced scenarios; that tactic mostly works

view this post on Zulip Daniel Hilst Selli (Sep 02 2022 at 14:13):

thanks @Paolo Giarrusso

BTW this file is a perl of ltac, lots of rich examples


Last updated: Jan 28 2023 at 05:02 UTC