Stream: Ltac2

Topic: Using ids with context match

Michael Soegtrop (Mar 18 2021 at 08:05):

@Pierre-Marie Pédrot ; I can't figure out how to use the term id one can give in a context match. Syntactically it works, but whenever I use the id, I get a hard to digest error message:

Require Import Ltac2.Ltac2.
Require Import Ltac2.Message.

Ltac2 works ():=
  lazy_match! goal with
  | [ |- context [S ?n] ] => Message.print (Message.of_constr n)
  end.

Ltac2 doesnt ():=
  lazy_match! goal with
  | [ |- context n [S _] ] => Message.print (Message.of_constr n)
  end.

For the latter I get:

This expression has type
(((Pattern.match_kind * Pattern.t) list * (Pattern.match_kind * pattern)) * (ident array -> Pattern.context array ->
                                                                              constr array -> constr -> unit)) list
but an expression was expected of type
(((Pattern.match_kind * Pattern.t) list * (Pattern.match_kind * Pattern.t)) * (ident array -> Pattern.context array
                                                                                -> constr array -> Pattern.context
                                                                                -> 'a)) list

Am I doing something wrong or is this a bug?

Pierre-Marie Pédrot (Mar 18 2021 at 08:22):

I agree the error message is not very readable. I thought I had already written a patch to make it more palatable, but it seems not.

Pierre-Marie Pédrot (Mar 18 2021 at 08:23):

If you look carefully, the difference between the two types is constr vs. Pattern.context.

Pierre-Marie Pédrot (Mar 18 2021 at 08:23):

The reason is that a matching context is not a term, but a term with a hole.

Pierre-Marie Pédrot (Mar 18 2021 at 08:23):

You have to provide something to fill the context with to get a proper term.

Pierre-Marie Pédrot (Mar 18 2021 at 08:24):

See Pattern.instantiate for that.

Michael Soegtrop (Mar 18 2021 at 13:59):

OK, this works:

Ltac2 somehow ():=
  lazy_match! goal with
  | [ |- context n [S ?n'] ] => Message.print (Message.of_constr (Pattern.instantiate n n'))
  end.

But I don't quite see why it has to be like this - it reduces the usefulness of giving the complete context a name if I have to somehow put it together later anyway - I could just write S n'. When the match is done, it should be clear how to fill in the whole.

Do you have uses cases in mind, where it would make sense to put in something else than the matched sub-term?

Pierre-Marie Pédrot (Mar 18 2021 at 14:19):

It could be a more complex context, though. For instance if you have variable capture and the like.

Michael Soegtrop (Mar 18 2021 at 17:01):

Sorry I still don't get it. In what case could I supply an argument for the holes in the context, Ltac2 couldn't figure out on this own?

Pierre-Marie Pédrot (Mar 18 2021 at 20:32):

I am not sure I see what you are asking for, actually.

Pierre-Marie Pédrot (Mar 18 2021 at 20:33):

In Ltac1 you also have to fill the context with a term to use it. It so happens that there is runtime trickery to cast it on the fly to a term but in general it's an ill-typed term.

Pierre-Marie Pédrot (Mar 18 2021 at 20:36):

e.g. this fails:

Goal 1 = 1.
Proof.
match goal with [ |- context c [S ?n] ] => pose c end.

with variable c should be bound to a term.

Pierre-Marie Pédrot (Mar 18 2021 at 20:36):

The only case where you can use it is idtac c AFAIU

Pierre-Marie Pédrot (Mar 18 2021 at 20:37):

(or explicit instantiation, obviously)

Michael Soegtrop (Mar 19 2021 at 09:25):

Sorry, I mixed this up with the as name in Ltac1 - I didn't realize that the semantics of this is entirely different.

Last updated: Apr 16 2024 at 05:01 UTC