Stream: Coq users

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


view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip Simon Hudon (Jun 08 2021 at 15:52):

That works, thanks!

view this post on Zulip gallais (May 02 2024 at 08:30):

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 bstill left on the RHS of the equality!).
Is there any way to abstract over all occurrences of the variable?

view this post on Zulip gallais (May 02 2024 at 16:19):

FTR, the trick was to use pattern (from HTNW on SO)


Last updated: Jun 23 2024 at 23:01 UTC