Hi all;

This may be foolish but I am trying to use math-comp in a different context, not necessarily using ssreflect.

Could anyone please help me to understand why "simple apply" fails here? I would love it if somebody could talk me through what the unification is doing and why it's getting tripped up so I can circumvent this in the future.

```
Require Import ssrfun.
Require Import ssrbool.
Require Import mathcomp.ssreflect.seq.
Require Import mathcomp.ssreflect.ssrnat.
Require Import mathcomp.ssreflect.eqtype.
Require Import mathcomp.ssreflect.fintype.
Require Import mathcomp.ssreflect.tuple.
Require Import mathcomp.ssreflect.finfun.
Definition ffunP_l := fun aT rT f1 f2 => proj1 (@ffunP aT rT f1 f2).
Context (x y : nat).
Context (f : @finfun_of (exp_finIndexType (x))
(fun _ : ordinal x => ordinal y)
(ssreflect.Phant
(forall _ : ordinal x, ordinal y))).
Goal @eq
(@finfun_of (exp_finIndexType x)
(fun _ : ordinal x => ordinal y)
(ssreflect.Phant
(forall _ : ordinal x, ordinal y)))
(@FinfunDef.finfun (exp_finIndexType x)
(fun _ : ordinal x => ordinal y)
(fun x0 : ordinal x =>
@fun_of_fin (exp_finIndexType y)
(fun _ : ordinal y => ordinal y)
(ssreflect.Phant
(forall _ : ordinal y, ordinal y))
(@FinfunDef.finfun (exp_finIndexType y)
(fun _ : ordinal y => ordinal y)
(fun k : ordinal y => k))
(@fun_of_fin (exp_finIndexType x)
(fun _ : ordinal x => ordinal y)
(ssreflect.Phant
(forall _ : ordinal x,
ordinal y)) f x0))) f.
simple apply ffunP_l.
```

Gives

```
Error: Unable to unify "Finite.sort ?M1109" with "'I_x".
```

I notice that `simple apply (ffunP_l _)`

is successful. So if you create the metavariable before passing it to simple apply, it solves it. I guess simple apply doesn't make choices that result in new metavariables being created but it will try to solve existing ones. But I still don't feel like I understand what is happening.

I have a similar problem with ltac's `rewrite`

on this problem as well. `rewrite -> ffunE`

fails, but `rewrite -> (ffunE _)`

succeeds. I don't know how to interpret this.

There are 2 kinds of unification variables in Coq, the "metavariables" `?M1234`

and the "existential variables" ("evars") `?X1234`

(sometimes printed as `?Goal`

or some other name)

`apply`

and `rewrite`

generate metavariables, but holes in terms (such as `_`

or implicit arguments) generate evars

It seems that you found a case where they behave differently

I was not aware of this distinction. Is this the same kind of distinction that is made when people talk about multiple underlying unification algorithms for Coq, i.e. "tactic unification" vs "elaboration unification"

Could we say that metavariables are the unification variables for the tactic unification algorithm and evars are the unification variables for the term elaboration unification algorithm?

it is related as tactic unification is the only one that understands metavariables, but both can unify evars (indeed in your example tactic unification fails with metavariables but succeeds when made to operate on evars)

~~Does that mean that~~ are canonical structures only used for solving evars, not metavars?

I believe they are used for both

Last updated: Jul 25 2024 at 15:02 UTC