Hello everyone,

Today I was inspired by this comment of @herbelin to try and embed a programming language that supports pattern matching of product types in Coq using the PHOAS method. And of course, this needs to come with some reasonable notations.

So, I’m starting with a simple PHOAS encoding of lambda calculus with products types, that can be pattern matched in `Lam`

:

```
From Ltac2 Require Import Ltac2.
Section term.
Variable X : Type.
Inductive prod_pattern := leaf | ppair (l r : prod_pattern).
Fixpoint p2p p : Type :=
match p with
| leaf => X
| ppair l r => p2p l * p2p r
end.
Inductive term : Type :=
| Var (x : X)
| App (x y : term)
| Prod (x y : term)
| Lam p (f : p2p p -> term).
```

Now I want to create some notations for this, such as `[λ (a, (b, c)), a b]`

. This notation should elaborate to `Lam (ppair leaf (ppair leaf leaf)) (fun '(a, (b, c)) => a b)`

. This is a bit of a problem though, because the `(a , (b, c))`

part of the notation needs to generate both `ppair leaf (ppair leaf leaf)`

and the real Coq pattern `'(a, (b, c))`

. This is problematic, because `pattern`

s need to be applicative in Coq, and cannot be computed within the notation. I came up with a solution using Ltac that converts a nested products to `prod_pattern`

:

```
Ltac to_pattern x :=
match x with
| (?x , ?y) => let a := to_pattern x in
let b := to_pattern y in
constr:(ppair a b)
| _ => constr:(leaf)
end.
Notation "[ 'λ' pat , k ]" :=
(Lam ltac:(let r := to_pattern pat in exact r) (fun pat => k))
(at level 0, pat pattern, only parsing).
```

Crazily, this actually almost works! The only problem is that when the `ltac`

part gets evaluated, the system tries to resolve the `binder`

s in the pattern, and errors out:

`Definition test := [λ (a, (b, c)) , App (Var a) (Var b)]. (* The variable a was not found in the current environment. *)`

This can be solved by introducing some bogus variables:

```
Section test.
Variable a b c d e f : X.
Definition test := [λ (a, (b, c)) , App (Var a) (Var b)].
End test.
Print test. (* test = Lam (ppair leaf (ppair leaf leaf)) (fun '(a, (b, _)) => App (Var a) (Var b)) : term *)
```

I tried if Ltac2 may be better suited for this problem because it appears to be working on preterms, but something as simple as the following already errors out:

```
Notation "[[ 'λ' pat , k ]]" :=
(Lam ltac2:(exact leaf) (fun pat => k))
(at level 0, pat pattern, only parsing).
Check [[λ a, Var a]]. (* Missing notation term for variable k, probably an ill-typed expression *)
```

Does anybody have a better solution for this problem?