apply ltac to subexpression of a goal

Question

Here is a short example of what I am trying to do.

Let's say I have a relation

Inductive divisible: nat -> nat -> Type := 
| one : forall n, divisible n 1.
..etc...

I have also the following ltac Ltac simplify := autorewrite with blah

I would like to define a ltac which does simplify to only the first term in a 'divisible' goal. Something like

Ltac simplify_fst :=
  match goal with |- (divisible ?N ?M) =>
autorewrite with subst1 in N
  end.

When I try out the above in the following,

Lemma silly: forall n m, divisible (n + m) 1.
  intros. simplify_fst.

I get a

Error:
Ltac call to "simplify_fst" failed.
Ltac variable N is bound to n + m which cannot be
coerced to a variable.

Can applying ltacs (even simple ones involving only autounfold and autorewrite) be restricted to a subexpression of the goal?

Thank you.

Answer 1

In your case, remember may be useful:

Ltac simplify_fst :=
  match goal with |- (divisible ?N ?M) =>
    let x := fresh "x" in
    let Hx := fresh "Hx" in
    remember N as x eqn:Hx;
    autorewrite with subst1 in Hx;
    subst x
  end.