Stream: math-comp users

Topic: Debugging auto


view this post on Zulip Patrick Nicodemus (May 01 2023 at 14:21):

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".

view this post on Zulip Patrick Nicodemus (May 01 2023 at 14:25):

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.

view this post on Zulip Patrick Nicodemus (May 01 2023 at 14:28):

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.

view this post on Zulip Gaëtan Gilbert (May 01 2023 at 14:37):

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

view this post on Zulip Patrick Nicodemus (May 01 2023 at 14:39):

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"

view this post on Zulip Patrick Nicodemus (May 01 2023 at 14:40):

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?

view this post on Zulip Gaëtan Gilbert (May 01 2023 at 14:48):

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)

view this post on Zulip Paolo Giarrusso (May 01 2023 at 14:53):

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

view this post on Zulip Gaëtan Gilbert (May 01 2023 at 14:59):

I believe they are used for both


Last updated: Jul 25 2024 at 15:02 UTC