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!

I ended up reconstructing the same solution (cf. https://old.reddit.com/r/Coq/comments/1ci2jt4/making_coq_more_readable/l27tkhv/) but `context`

only abstracts over the first occurrence (in the example we get `P := fun m : bool => negb (negb m) = b : bool -> Prop`

with a free `b`

still left on the RHS of the equality!).

Is there any way to abstract over all occurrences of the variable?

FTR, the trick was to use `pattern`

(from HTNW on SO)

Last updated: Jun 23 2024 at 23:01 UTC