The Coq mailing list

[Jason Gross <jasongross9 AT gmail.com>]

If the question you want to ask is "is there any fixpoint which, after reduction via the structural argument, then matches on my variable?", I'd suggest you take a different approach: rather than asking "is this variable matched on?" you can instead ask "please find all matched on variables and case/induct on them".  You'll have to jump through a couple of hoops to avoid infinite loops, but I think this approach is much more feasible than trying to determine, at introduction time, if later computation will lead to this variable being matched on.

On Tue, Jun 2, 2020, 21:01 Jason Gross <jasongross9 AT gmail.com> wrote:

You can search the goal for

context [match x with _ => _ end]

This will tell you if it's the discriminee of a match.  Note that fixpoints won't reduce unless you destruct their structural argument, so it actually doesn't matter whether or not the fixpoint body matches on the argument you care about, it only matters whether the argument occurs in the structural location.

On Tue, Jun 2, 2020, 20:39 Eddy Westbrook <westbrook AT galois.com> wrote:

Jason,

Interesting. The context[?f] pattern combined with is_fix_at_head f is going to apply is_fix_at_head to every subterm of the goal, right? I guess I could also write a tactic that manually crawls the subterms to see if any of them is a fix term applied to the argument I care about.

Is there any way to tell if the fix is destructing a specific argument? What I’m actually try to determine in my tactic (apologies if it wasn’t clear earlier) is whether, in the current goal foorall x, P x, the variable x is destructed by pattern-matching or a fix (containing a pattern-match) somewhere in P. Then, when I intro x, I can also destruct x. Does that make sense?

Thanks to everyone for the help so far, btw.

-Eddy

On Jun 1, 2020, at 2:47 PM, Jason Gross <jasongross9 AT gmail.com> wrote:

You can also write something like:

Ltac is_fix_at_head x :=
  lazymatch x with
  | ?f _ => is_fix_at_head f
  | _ => is_fix x
  end.
Goal forall x y, x + y = y + x.
  unfold "+".
  intros.
  match goal with
  | [ |- context[?f] ] => is_fix_at_head f; idtac f
  end.

and then your tactic looks like:

Ltac head x :=
  lazymatch x with
  | ?f _ => head f
  | _ => x
  end.
Ltac which_arg_struct f :=
  lazymatch f with
    (* python -c 'print("\n".join("  | fix F %s {struct %s} := _ => constr:(%d%%nat)" % (" ".join("x%d" % i for i in range(n)), "x%d" % m, m) for n in range(4) for m in range(n)))' *)
  | fix F x0 {struct x0} := _ => constr:(0%nat)
  | fix F x0 x1 {struct x0} := _ => constr:(0%nat)
  | fix F x0 x1 {struct x1} := _ => constr:(1%nat)
  | fix F x0 x1 x2 {struct x0} := _ => constr:(0%nat)
  | fix F x0 x1 x2 {struct x1} := _ => constr:(1%nat)
  | fix F x0 x1 x2 {struct x2} := _ => constr:(2%nat)
  | ?f => fail 0 "We only support up to 3-argument fix, not" f
  end.
Ltac on_nth_arg_cps f n tac K :=
  lazymatch f with
  | ?f ?x => on_nth_arg_cps
               f n tac
               ltac:(fun n => lazymatch n with
                              | 0 => tac x
                              | S ?n => K n
                              end)
  | _ => K n
  end.
Ltac nth_arg f n :=
  on_nth_arg_cps f n ltac:(fun x => x) ltac:(fun n => lazymatch goal with _ => fail 0 "Not enough arguments; needed" n "extra arguments for" f end).
Ltac on_struct_arg fx tac :=
  let f := head fx in
  is_fix f;
  let n := which_arg_struct f in
  let arg := nth_arg fx n in
  tac arg.
Ltac destruct_struct_arg x := on_struct_arg x ltac:(fun x => destruct x).
Ltac induction_struct_arg x := on_struct_arg x ltac:(fun x => induction x).

Goal forall x y, x + y = y + x.
  unfold "+".
  intros.
  match goal with

  | [ |- context[?f] ] => induction_struct_arg f
  end.

On Mon, Jun 1, 2020 at 5:24 PM Jason Gross <jasongross9 AT gmail.com> wrote:

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