The Coq mailing list

[Jason Gross <jasongross9 AT gmail.com>]

Note that the following works in Coq 8.11:

Goal forall x y, x + y = y + x.
  unfold "+".
  intros.
  lazymatch goal with
  | [ |- context[fix f (a : ?A) (b : ?B) {struct a} : ?C := _] ] => idtac
  end.
  lazymatch goal with
  | [ |- context[fix f a b {struct a} := _] ] => idtac
  end.
  lazymatch goal with
  | [ |- context[fix f a b {struct a} := match a with _ => _ end] ] => idtac
  end.
  lazymatch goal with
  | [ |- context[fix f a b {struct a} := match a with O => @?O_case a b | S n => _ end] ] => idtac
  end.
  lazymatch goal with
  | [ |- context[fix f a b {struct a} := match a with O => @?O_case f a b | S n => @?S_case f a b n end] ] => idtac
  end.

Note that the struct annotation is mandatory, and so you need separate cases for different numbers of arguments and different recursive arguments.

On Mon, Jun 1, 2020 at 3:44 PM Gregory Malecha <gregory AT bedrocksystems.com> wrote:

It is late, but you can do this in template-coq simply by quoting the term and writing a function to check what you want. It wouldn't be truly gorgeous, but it doesn't require anything that is unsafe. Note that what template-coq gives you is a Gallina inductive type that reifies a Gallina term, so inspecting a term is *literally* just Coq pattern matching. That said, this is definitely not unification, so if you want "definitionally equal to" rather than "syntactically equal to you are currently out of luck with template-coq.

On Mon, May 18, 2020 at 5:40 AM Pierre-Marie Pédrot <pierre-marie.pedrot AT inria.fr> wrote:

Hi,

On 16/05/2020 03:17, Eddy Westbrook wrote:
> Is there any way to pattern-match on a fix + match term like (fix foo
> (x1:A1) … := match xi with … ) in a term? I am trying to write some
> tactics to determine if a particular argument is being destructed in
> a term, in order to apply the destruct or induction tactic on it, but
> it seems that Ltac at least won’t let me search for fix terms…?

if you're using Coq >= 8.11, it is possible to do this in Ltac2, albeit
in a way deemed "unsafe". Once done, you can also wrap the resulting
Ltac2 tactic into a proper Ltac1 tactic, so that it is transparent for
the end-user. Look at the Ltac2.Constr.Unsafe module for more details.

PMP

--

Gregory Malecha

Mail: gregory AT bedrocksystems.com

BedRock

Systems Inc
UNBREAKABLE FOUNDATION FOR

FORMALLY SECURED COMPUTING