The Coq mailing list

[Dan Christensen <jdc AT uwo.ca>]

It's constr_eq that is failing on the two terms that only differ in the
name of a bound variable.  If I use the change tactic to rename the
bound variable x to anything else, everything works.  I'll work on
trying to find a simpler reproducible example.

So, except for this probable bug in Coq, the syntactic_unify approach is
working very well for my use cases.

Dan

On Nov 14, 2019, Dan Christensen 
<jdc AT uwo.ca>
 wrote:

> On Nov 14, 2019, Dan Christensen 
> <jdc AT uwo.ca>
>  wrote:
>
>> On Nov 13, 2019, Samuel Gruetter 
>> <gruetter AT mit.edu>
>>  wrote:
>>
>>> https://github.com/mit-plv/coqutil/blob/master/src/coqutil/Tactics/syntactic_unify.v
>>
>> I tried the syntactic_unify tactic from there, and it worked better
>> than the set method in some simple situations.  But unfortunately
>> syntactic_unify failed to unify some terms that look easy to unify.
>
> I adding some idtac printing to _syntactic_unify, add see that in a
> recursive call it gets passed the two terms
>
>   (fun x : X => @smin X Y (x, @point Y (ispointed_type Y)))
>   (fun a : X => @smin X Y (a, @point Y (ispointed_type Y)))
>
> and fails to unify them in the last clause.  But I can't reproduce this
> in isolation.  Whenever I try to trim things down, the problem goes away.
>
> Here they are with universes:
>
> (fun x : X => @smin@{smash.10422 smash.10423} X Y (x, @point@{smash.10423} 
> Y (ispointed_type@{smash.10423} Y)))
> (fun a : X => @smin@{smash.10422 smash.10423} X Y (a, @point@{smash.10423} 
> Y (ispointed_type@{smash.10423} Y)))
>
> Is there some information idtac wouldn't show that could still prevent
> unification?
>
> On Nov 14, 2019, Jason Gross 
> <jasongross9 AT gmail.com>
>  wrote:
>
>> If the built-in unify fails on those terms, that sounds like a bug in
>> Coq worth reporting. If you want to extract a stand-alone example, you
>> can use my bug minimizer:
>> https://github.com/JasonGross/coq-tools/blob/master/README.md#coq-bug-minimizer
>
> That is a really amazing program!  But it still left a pretty
> complicated development, so I think I'll need to experiment more before
> filing a bug report.
>
> Dan