The Coq mailing list

[Jonathan <jonikelee AT gmail.com>]

On 07/24/2014 12:51 PM, Jason Gross wrote:
> They are useful because I can use tactics to solve them interactively.  If
> the interesting bit is the first subgoal, and the constraint is something
> that should be solvable by some general tactic that isn't good enough to
> fill in evars, then you can first construct your term, and then later prove
> the laws.  For example, this means that I can construct a category
> interactively, rather than having to first construct the objects,
> morphisms, composition, and identity, all in one go, and then only getting
> to prove the laws interactively.
>
> -Jason

OK - it's getting clearer, I think.   Normally - before this special 
refine behavior - what one would do to change the current goal into a 
more preferred one would be to assert the preferred one.  The assert 
then would give you a witness (hypothesis) in the second subgoal that 
you could use.  However, the witness provided by assert is completely 
generic - untied to any you produced to solve the first subgoal - and so 
can't be used to solve arbitrary constraints that only specific 
instances could solve.

With refine, whatever witness you provide to solve the first subgoal is 
identically the one introduced in the second subgoal.  So, one could 
then construct the category in the first subgoal along with some 
specific element, and use that element as the witness to the first 
subgoal, and get it to solve the second as well.  With assert, you lose 
that ability.  But, you have to be very careful to keep track of the 
constraints imposed by that second subgoal, unless they're trivially 
solvable as you say (but if they're too trivial, then assert would have 
worked just as well!) - although with evar backtracking, things might be 
a bit easier.

But, this is still confusing in certain ways.  If I was going to solve 
such an exists goal by constructing a new category and using a specific 
element in it, I would do so before destructuring the exists goal, so 
that the category and all of its elements appear in both subgoals (when 
I eventually do the eexists).

However, I guess the criticism here is that this is the all-to-common 
(for me, at least) case of needing to fill in an existential when it's 
too late to do so (getting the "Instance is not well-typed in the 
environment of" error) - and instead (hopefully) knowing in advance what 
to do to set up for a successful instantiation.  Reminds me of the old 
joke (often used to explain one-pass vs. two-pass algorithms) about 
giving directions to someone taking a bus: when the bus reaches the 
museum, your stop was the previous one.

If so - great - I appreciate any and all ways to get around the evil 
"Instance is not well-typed in the environment of" error.  Although I do 
suspect that Coq's decisions on when an instance is well-typed are 
overly conservative, and not always uniform.  For example, I have seen 
cases when using instantiate to fill in an evar with a particular 
instance produces the error, but using unify instead with the same evar 
and instance (in the very same goal) works.

-- Jonathan