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: Oct 13 2024 at 01:02 UTC