The Coq mailing list

[Gaëtan Gilbert <gaetan.gilbert AT skyskimmer.net>]

probably one side uses a primitive projection and the other uses the 
compatibility constant
or both sides use the primitive projection but one is considered 
"unfolded" and the other isn't


Gaëtan Gilbert

On 15/11/2019 23:05, Dan Christensen wrote:
> 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?