Stream: Coq users

Topic: ✔ Matching Gallina's `let .. in` with Ltac

Nikola Katić (Aug 02 2022 at 12:52):

Hi all,
Is such thing possible? E.g.

Goal 1 = let n := 1 in n.
match goal with
| [ |- context[let _ in _] ] => idtac "let";
| _ => idtac "nope"
end.

Ltac has its own let construct, I guess that is the problem.
Is there anything like constr: which could be specified in order to get Gallina's let matched?

Kenji Maillard (Aug 02 2022 at 12:59):

You just need to add the := of the let in the pattern, and it works (also remove the trailing ; after "let"):

Goal 1 = let n := 1 in n.
match goal with
| [ |- context[let _ := _ in _] ] => idtac "let"
| _ => idtac "nope"
end.

Nikola Katić (Aug 02 2022 at 13:04):

Thanks @Kenji Maillard! That makes sense :smile:

Nikola Katić (Aug 02 2022 at 13:54):

Is there any reason why this match wouldn't work?

Goal 10 = let n := 1 in (n + 9).
match goal with
| [ |- context[ let X := ?V in ?Z] ] => idtac "let"
| _ => idtac "nope"
end.

But this match works:

Goal 10 = let n := 1 in (n + 9).
match goal with
| [ |- context[ let X := ?V in _] ] => idtac "let"
| _ => idtac "nope"
end.

Kenji Maillard (Aug 02 2022 at 14:03):

The value to be bound by Z depends on X so that might explains why it does not work in the first case.
With 2nd order pattern matching it seems to work fine:

Goal 10 = let n := 1 in (n + 9).
match goal with
| [ |- context[ let X := ?V in @?Z X] ] => idtac "let"
| _ => idtac "nope"
end.

Nikola Katić (Aug 02 2022 at 14:16):

Kenji Maillard said:

The value to be bound by Z depends on X so that might explains why it does not work in the first case.
With 2nd order pattern matching it seems to work fine:

Goal 10 = let n := 1 in (n + 9).
match goal with
| [ |- context[ let X := ?V in @?Z X] ] => idtac "let"
| _ => idtac "nope"
end.

Wow! Will read more about 2nd order capabilities. Thanks again @Kenji Maillard :smile:

Notification Bot (Aug 03 2022 at 07:56):

Nikola Katić has marked this topic as resolved.

Last updated: Oct 13 2024 at 01:02 UTC