I'm trying to write a Ltac tactic to apply an induction principle that I wrote and I'm using `match`

and `context`

to infer the motive. Let's illustrate it with the following example:

```
Example foo m n : m + n = n + m.
Proof.
revert m.
match goal with
| |- context g [n] =>
refine (induction_ltof1 (fun x => context g [x]) _ n) (* Error: The reference context was not found in the current environment. *)
end.
```

`(fun x => context g [x])`

is not accepted by Coq as a valid motive because it interprets context as a reference to some definition instead of a keyword in Ltac. I can try to move it to a local definitions but I get more errors:

```
match goal with
| |- context g [n] =>
let x := fresh "x" in
let P := context g [x] in (* Error: variable x should be bound to a term. *)
refine (induction_ltof1 (fun x => P) _ n)
end.
```

What am I missing?

Instead of `(fun x => context g [x])`

, try `(fun x => ltac:(let v := context g [x] in exact v))`

, to prevent some confusion between tactics and terms.

That works, thanks!

Last updated: Feb 06 2023 at 12:04 UTC