The Coq mailing list

[Dan Christensen <jdc AT uwo.ca>]

I have attached a trimmed file that shows what might be a bug
in constr_eq.  It's still 67 lines long and relies on the HoTT
library (tested with version b20bb57373928 from Oct 30).

With this trimmed version, it's no longer true that renaming
the bound variable makes the problem go away, so it's not as
air tight a bug report as I wanted, but the file is much smaller.

Any comments before I try submitting a bug report?

Dan

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

> 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:
>
>> 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?

Attachment: smash_bug_min1.v
Description: Binary data