Stream: Ltac2

Topic: Ltac2 `match!` statement questions

DArends (Apr 21 2024 at 09:41):

I have two questions regarding the ltac2 match! statement:

1. Is it possible to insert terms into the match! 'cpattern'. I tried doing it like this,

From Ltac2 Require Import Ltac2 Message.

Goal 3 = 4.
let constr_3 := constr:(3) in
match! goal with
| [|- constr_3 = ?h ] => print (of_constr h)
end.

but this doesn't seem to work. Changing the constr_3 term to $constr_3 results in a Unbound value constr_3 error.
My goal being that I can use the result of a previous match statement in the next match statement.

2. Is it possible to create a match pattern that extracts elements of type x? For instance, if I have a goal containingx and y where x and y are both of type nat, is there any way to create a match pattern that matches the x and y terms? See the following code snippet

From Ltac2 Require Import Ltac2 Message.
Goal 3 = 4.
(* Prints 'contains nat' *)
match! goal with
| [|- context [ nat ] ] => print (of_string "contains nat" )
| [|- _] => print (of_string "does not contain nat" )
end.
Abort.

Goal True.
(* Prints 'does not contain nat' *)
match! goal with
| [|- context [ nat ] ] => print (of_string "contains nat" )
| [|- _] => print (of_string "does not contain nat" )
end.
Abort.

I have tried using context [ ?x:nat ] but this gives a warning Casts are ignored in patterns [cast-in-pattern,automation].

I am using Coq version 8.17.0.

Thanks in advance!

Gaëtan Gilbert (Apr 21 2024 at 10:59):

1. no, see also https://github.com/coq/coq/pull/18856
2. no

Pierre-Marie Pédrot (Apr 21 2024 at 11:24):

Didn't we have a way to include patterns into patterns though? I thought this was merged at some point.

Gaëtan Gilbert (Apr 21 2024 at 11:48):

patterns yes, terms no

Pierre-Marie Pédrot (Apr 21 2024 at 11:54):

But maybe patterns are sufficient, the above example doesn't discriminate enough.

DArends (Apr 24 2024 at 10:41):

Pierre-Marie Pédrot said:

But maybe patterns are sufficient, the above example doesn't discriminate enough.

Thanks for the swift response!

Out of curiosity I tried to search for the 'patterns in patterns', but I am unable to find more information on this. Could you maybe point me in the right direction?

Gaëtan Gilbert (Apr 24 2024 at 10:48):

use pattern:(foo) instead of constr:(foo) and $pattern:x instead of $x

Last updated: Oct 12 2024 at 13:01 UTC