The Coq mailing list

[Dan Christensen <jdc AT uwo.ca>]

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