Hi,

I am currently trying to write a coq plugin where I need to define some pattern matching construct programmatically, and I am struggling a little with the API. The pattern matchings I want to build concern identity types and should be overall pretty simple

As a first example to get started, I have defined the following construct in coq:

```
Definition composition (A : Type) (x : A) (y : A) (f : x = y) : x = y :=
match f with
| eq_refl => eq_refl
end.
```

And to be sure that I have all the information at hand, I printed using `Set Printing All`

. Here is what coq prints:

```
composition =
fun (A : Type) (x y : A) (f : @eq A x y) =>
match f in (eq _ a) return (@eq A x a) with
| eq_refl => @eq_refl A x
end
: forall (A : Type) (x y : A) (_ : @eq A x y), @eq A x y
```

I tried to redefine this same construct programmatically (attempt below), but I am not able to do it and I can't debug it by myself. The reason is that I always hit the error: "Instance and signature do not match". I hit this error even when trying to print the term, so I cannot print the term to compare with my desired term and see where I went wrong. I seem to understand that this error is related to the resolution of `let ... in`

constructs, which indicates that I haven't done what I wanted, since I don't think I am using any.

attempt of definition:

```
let mkComposition env sigma _ =
let sigma, base_type = Evarutil.new_Type sigma in
let sigma, eq_type = c_Q env sigma in
let sigma, refl = c_R env sigma in
let
(eq_ind,universe),_ = Inductiveops.find_inductive env sigma eq_type
in
let f = Names.Id.of_string "f" in
let fbind = {binder_name = Names.Name.mk_name f; binder_relevance = Relevant} in
let ret = EConstr.mkApp (eq_type, [| EConstr.mkRel 4; EConstr.mkRel 3; EConstr.mkRel 2 |]) in
let _ = Feedback.msg_debug (str "return_type" ++ Printer.pr_econstr_env env sigma ret) in
let case_info = Inductiveops.make_case_info env eq_ind Relevant RegularStyle in
let constructors = [| refl |] in
let case_return = [| fbind |], ret in
let case_invert = Constr.NoInvert in
let case_branches = [| ([| fbind |], refl) |] in
let constructor = refl in
let pcase = (case_info,
universe,
constructors,
case_return,
case_invert,
constructor,
case_branches) in
let body = EConstr.mkCase pcase in
sigma,
EConstr.mkLambda(
nameR (Names.Id.of_string "A"),
base_type,
EConstr.mkLambda(
nameR (Names.Id.of_string "x"),
EConstr.mkRel 1,
EConstr.mkLambda(
nameR (Names.Id.of_string "y"),
EConstr.mkRel 2,
EConstr.mkLambda(
nameR (Names.Id.of_string "f"),
EConstr.mkApp (eq_type, [| EConstr.mkRel 3;
EConstr.mkRel 2;
EConstr.mkRel 1 |]),
body
))))
```

I am pretty sure there are many things that I am not doing right, but one that's jumping out to me is the variable `a`

in the construct printed by coq. I cannot figure our what this variable represents and how I should reproduce this programmatically. One thing that could also help would be to print the term completely from coq (i.e. print the ast), but I haven't found a way to do this.

Any help for debugging this would be very helpful

what are you trying to do with `fbind`

? I think whatever misunderstanding you have is related

also read https://github.com/coq/coq/blob/d9914f815bbae15e4824ba7cf04607e875d9c127/kernel/constr.mli#L273-L283

Probably, my understanding was that the `match`

construct is binding a variable (in this case `f`

because I am matching on it) and thus requires a binder, which ends up in the `pcase_return`

and in the `pcase_branches`

. Thank you for the pointer, I had found another description in the comments, but this one seems a bit clearer

```
match f in (eq _ a) return (@eq A x a) with
| eq_refl => @eq_refl A x
end
```

does not bind `f`

it binds `a`

and (implicitly, in the not printed `as`

) `_`

in the return term `@eq A x a`

```
let pcase = (case_info,
universe,
constructors,
case_return,
case_invert,
constructor,
case_branches) in
```

`constructors`

is incorrect, that should be the parameters you are matching at (`A`

and `x`

, I'll let you translate to debruijn)

```
let case_return = [| fbind |], ret in
```

the return clause doesn't bind `f`

, it binds `a`

and `_`

```
let case_branches = [| ([| fbind |], refl) |] in
```

the branch binds nothing

Thank you very much, it makes a lot more sense now

Last updated: Oct 13 2024 at 01:02 UTC