Stream: Coq users

Topic: `match`, `context` and creating a lambda term in Ltac

Simon Hudon (Jun 08 2021 at 03:30):

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?

Guillaume Melquiond (Jun 08 2021 at 05:17):

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.

Simon Hudon (Jun 08 2021 at 15:52):

That works, thanks!

Last updated: Oct 03 2023 at 02:34 UTC