EDIT: I found it! I had forgotten about a coercion. Please ignore this :)
I am learning ssreflect and am stuck on how to proceed here. My proof state is the following:
n, n0 : nat
============================
n = n0 -> n == n0
At first, I tried move/eqP, because I thought that would "apply" eqP to n=n0, where "apply" means "get n==n0 out of the reflection given by eqP". However, this attempt produced:
Illegal application (Non-functional construction):
The expression "eqP ?i" of type "?x = ?y"
cannot be applied to the term
"?y0" : "?T0"
I'm confused on what y0 and T0 are supposed to be. I also tried
intros H. eapply (introT eqP) in H.
which produced the error
Unable to apply lemma of type "?x = ?y -> ?x == ?y"
on hypothesis of type "n = n0".
I tried to pass in explicit arguments n0 and n to eqP, just to see if it would work, with
pose proof (eqP n n0).
but this gave an error of
In environment
n, n0 : nat
H : n = n0
The term "n" has type "nat"
while it is expected to have type
"is_true (?x == ?y)".
So, it seems like eqP both wants and doesn't want explicit instantiations for ?x and ?y. I would really appreciate some conceptual explanation as to why move/eqP isn't behaving how I think it should, and what is actually going on with the types of eqP and (introT eqP).
If it is relevant, I am importing
From mathcomp Require Import ssrnat ssreflect ssrfun ssrbool eqtype.
from ssreflect.
Thank you.
Silly mistake! I had a coercion that I forgot about; my actual proof state was Nat n = Nat n0 -> n ==n0.