The Coq mailing list

[Samuel Gruetter <gruetter AT mit.edu>]

On Fri, 2019-11-15 at 23:13 +0100, Gaëtan Gilbert wrote:
> 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

If that's indeed the source of the problem, you're in trouble Dan :(
In bedrock2, we had to disable primitive projections because of this, but
that comes at a cost...



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