## 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 04 2023 at 21:01 UTC