Stream: Coq users

Topic: Match goal's patterns and notations

Kenji Maillard (Apr 14 2021 at 12:53):

In ssreflect-style proving, one is usually quite explicit about variables names.
However, from times to times it is useful to refer to hypothesis in the context by a pattern on their type rather than the name itself (for instance after using inversion where you lose control over the names).
I tried to introduce some notations hacking around Ltac's match goals with mixed success:

From Coq Require Import ssreflect.

Variable (foo : nat -> Type).

Goal foo 3 -> foo 5 -> True.
  intros.
  (* Goal revert elements from the context based on a pattern here `foo _` *)
  move: ltac:(lazymatch goal with | [H : foo _ |- _ ] => exact H end).
  (* I would like to introduce a notation ⦑ pattern ⦒ standing for the previous construction, e.g. *)
  (* move: ⦑ foo _ ⦒. *)
Abort.


(* A failed tentative *)
Tactic Notation "⦑" cpattern(p) "⦒" := (lazymatch goal with | [H : p |- _ ] => exact H end).

Goal foo 3 -> foo 5 -> True.
  intros.
  Fail move: ltac:(⦑ (foo _) ⦒).
Abort.

(* Another slightly random tentative *)
Notation "⦑ p ⦒" := (ltac:(match goal with | [H : p |- _ ] => exact H end)).

Goal foo 3 -> foo 5 -> True.
  intros.
  (* happens to work with fully explicit terms *)
  move: ⦑ foo 3 ⦒.
  (* but fails with open terms *)
  Fail move: ⦑ foo _ ⦒.
Abort.

Are there ways to make this kind of hack work ? (maybe by assigning to the pattern p in the notations the right "category")
I also considered using Ltac2, but didn't see how I could build a single pattern to pass to match_goals functions.

Rodolphe Lepigre (Apr 14 2021 at 12:59):

The std++ library defines a revert select tactic that does just that (https://gitlab.mpi-sws.org/iris/stdpp/-/blob/master/theories/tactics.v#L545).

Kenji Maillard (Apr 14 2021 at 13:05):

Wow that's great, thanks for the pointer @Rodolphe Lepigre !

Théo Winterhalter (Apr 14 2021 at 13:05):

It's a bit frustrating because

let h := match goal with h : foo _ |- _ => h end in
move: h.

works, but I couldn't find a way to make that into a tactic.

Last updated: Oct 13 2024 at 01:02 UTC