Stream: Coq users

Topic: Ltac: abstracting over pattern?

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?

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)

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

Ralf Jung (Jun 17 2021 at 10:22):

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

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^^

Ralf Jung (Jun 17 2021 at 10:24):

yeah it still fails the same way after fixing that

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

Pierre-Marie Pédrot (Jun 17 2021 at 11:59):

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

Ralf Jung (Jun 17 2021 at 15:15):

yeah, I think I might

Ralf Jung (Jun 17 2021 at 15:15):

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

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.

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

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

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: Oct 13 2024 at 01:02 UTC