make version 4.0 not detected

[DanGrayson]

@JasonGross it would be great if you would fix the detection of the version number of make here in HoTT/coq, too! Then my coq-builder script would suddenly start working when it clones from here and tries to compile. Other users would appreciate it, too, I'm sure.

I'm referring to your patch at https://github.com/HoTT/coq/blob/trunk/configure#L340

[JasonGross]

I would, but I don't have permission to push to this repo. We'll have to ask @mattam82 to merge #96. I'm not sure how much longer it'll matter, though, because Matthieu tells me he's hoping to push polyproj to trunk very soon now, and as soon as the HoTT library (mainly, categories) compiles with polyproj (and very little diff), I'll push a commit to HoTT/HoTT switching over to that version (with a log of the timing changes).

[DanGrayson]

Thanks for the pull request. Closing the issue ...

[DanGrayson]

How close are you to getting HoTT to compile with polyproj? I tried it with Foundations a few months ago and it was buggy.

[JasonGross]

Matthieu thinks we're pretty close, I think we're less close. There's a list of issues here which I haven't updated recently; I'll probably go through them and close the ones that have been fixed in the next week or two (unless you want to do so for me!) Currently, I think the most pressing issue is that polyproj seems to have lost universe subtyping for inductives; I can't really check most of categories because of that. There is also this bug in trunk, which breaks some unification that used to work.

[mattam82]

Hi,

The issue with inductives was an overlook in previous versions, as
universe instances of inductives were not compared when they should be. In
the new version, they are compared for equality (conservativity depends on
it). Doing it in a more clever way would require to know if universe
levels are used in an equi- or co- or contra-variant position only inside
the definition, which I can't decide easily. However, one could define
eta-expansion-like constants which would allow coercing between
two different instances of the inductive and inferring what the
requierments on universes should be. E.g. you could use that to lower the
level of a funext instance according to your proof Jason.

Most of HoTT proper goes through right now, it's only the categories part
that has failures afaict. I'm working on that right now.

On Monday, April 7, 2014, Jason Gross [email protected] wrote:

Matthieu thinks we're pretty close, I think we're less close. There's a
list of issues herehttps://github.com/HoTT/coq/search?q=%28polyproj%29&ref=cmdform&state=open&type=Issueswhich I haven't updated recently; I'll probably go through them and close
the ones that have been fixed in the next week or two (unless you want to
do so for me!) Currently, I think the most pressing issue is that polyproj
seems to have lost universe subtyping for inductiveshttps://github.com//issues/93#issuecomment-39254993;
I can't really check most of categories because of that. There is also this
bug in trunk https://coq.inria.fr/bugs/show_bug.cgi?id=3269, which
breaks some unification that used to work.

Reply to this email directly or view it on GitHubhttps://github.com//issues/95#issuecomment-39688727
.

[DanGrayson]

Thanks, Matthieu! Perhaps when it works with HoTT we can take a look at Foundations, too, jointly.

[JasonGross]

The proof will go through with your suggestion, but will require the use of isequiv_adjointify or terrible munging of equalities. The problem (with the proof of the adjoint law) is that some of our types are under lambdas, and so you can't actually use the old proof to prove the eta expanded one unless you happen to have an extra instance functional extensionality to get things started. It would be trivial if we have judgmental weak eta conversion for inductive types, such as

∀ A (x y : A) (p : x = y),
    p ≡
      match p in (_ = y0) return (x = y0) with
        | eq_refl ⇒ eq_refl
      end

But there's no chance that's going to get in by 8.5, right? It would need a typed judgmental equality and all that?

It seems like this would be a nice feature to have (maybe it would work nicely with suggestions I've heard for annotating constants with positive/negative uses so that you could have fancier inductive types?), though I imagine it won't make it to 8.5.

[mattam82]

On 7 avr. 2014, at 19:36, Jason Gross [email protected] wrote:

The proof will go through with your suggestion, but will require the use of isequiv_adjointify or terrible munging of equalities. The problem (with the proof of the adjoint law) is that some of our types are under lambdas, and so you can't actually use the old proof to prove the eta expanded one unless you happen to have an extra instance functional extensionality to get things started. It would be trivial if we have judgmental weak eta conversion for inductive types, such as

∀ A (x y : A) (p : x = y),

p ≡

match p in (_ = y0) return (x = y0) with

| eq_refl ⇒ eq_refl

end
But there's no chance that's going to get in by 8.5, right? It would need a typed judgmental equality and all that?

That’s an interesting question. From a first look, it could be added without typed equality, as the match on the right is (relatively) easily recognizable. I’m just worried about the issue with disjunctions. Adding eta for sums is not easy AFAIR.

It seems like this would be a nice feature to have (maybe it would work nicely with suggestions I've heard for annotating constants with positive/negative uses so that you could have fancier inductive types?), though I imagine it won't make it to 8.5.

Are you thinking of annotating type predicate binders to know about positivity/strict positivity in the syntax?

— Matthieu

[mattam82]

Sure! Today I finished fixing the bugs I found in the test-suite of Coq. I’ll commit my code to
Coq trunk next, as it doesn’t use universe polymorphism so bugs there are not too important for releasing an
α version. After that I’ll come back to HoTT/HoTT and Foundations and push my fixes in the trunk.
— Matthieu

On 7 avr. 2014, at 13:08, Daniel R. Grayson [email protected] wrote:

Thanks, Matthieu! Perhaps when it works with HoTT we can take a look at Foundations, too, jointly.

—
Reply to this email directly or view it on GitHub.

[JasonGross]

I’m just worried about the issue with disjunctions. Adding eta for sums is not easy AFAIR.

I'm not asking for the standard eta rule for inductives; this is a weak form of eta which is (I think) syntactic. The rule for sums is

∀ A B (p : A + B),
    p ≡
      match p in (_ + _) return (A + B) with
        | inl x ⇒ inl x
        | inr y ⇒ inr y
      end

and for unit is

∀ (p : unit),
    p ≡
      match p in (unit) return (unit) with
        | tt ⇒ tt
      end

(note that this doesn't give that all units are judgmentally tt, and so isn't as strong as eta.)

Are you thinking of annotating type predicate binders to know about positivity/strict positivity in the syntax?

Yes, I think so. I think I got the idea from @gmalecha, so he'd know more about the details.

[JasonGross]

Here's another judgmental equality I've been thinking of, which I'm curious how hard it would be to add:

For any types T and U whose head is the same inductive type I, say T ≡ I params1 indices1 and U = I params2 indices2, and if both of the following terms typecheck:

∀ x : T, match x in (I _ indices) return (I params1 indices) with
               | c1 _ args1 ⇒ @c1 params1 args1
               | c2 _ args2 ⇒ @c2 params1 args2
               ...
             end

∀ x : U, match x in (I _ indices) return (I params2 indices) with
               | c1 args1 ⇒ @c1 params2 args1
               | c2 args2 ⇒ @c2 params2 args2
               ...
             end

then have T ≡ U. If I understand correctly, this would be sufficient to derive universe subtyping for inductive types.

[JasonGross]

’ll commit my code to Coq trunk next, as it doesn’t use universe polymorphism so bugs there are not too important for releasing an α version.

Great!