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.
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.