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.
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).
Wow that's great, thanks for the pointer @Rodolphe Lepigre !
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: Sep 23 2023 at 07:01 UTC