Nicolas Rinaudo (Sep 19 2023 at 07:36): Nicolas Rinaudo (Sep 19 2023 at 07:36):I find myself with the following goal:
([ ], [ ]) = (l1, l2)
Naively, this leads me to the conclusion that l1 = [] and l2 = [], which I'd think the injectivity of type constructors would give me for free.
I also believe that the injection strategy does exactly that - in an equality statement where the same constructor is called in the lhs and the rhs, create term for term equality statements.
Clearly I'm misunderstanding something, because what coq tells me instead is Not a negated primitive equality.
Does anybody know which of my assumptions is incorrect?
Guillaume Melquiond (Sep 19 2023 at 07:38):If this was a hypothesis, then the injectivity of constructors would indeed apply. But if it is the goal, it is just the fundamental property of functions. You can use apply f_equal2.
Nicolas Rinaudo (Sep 19 2023 at 07:40):That's created two subgoals in which I had to prove that [] = l1 and [] = l2, I must be doing something wrong...
Guillaume Melquiond (Sep 19 2023 at 07:41):Yes, that is the point. If you want to prove that the pair l1, l2 is a pair of empty lists, then you need to prove that each of them is an empty list.
Nicolas Rinaudo (Sep 19 2023 at 07:42):Well I should have thought maybe more than 5 seconds before reporting back... thank you!
James Wood (Sep 19 2023 at 17:51):Terminological remark: “injectivity of type constructors” is a thing, but it means something else. I think you meant to say “injectivity of (value) constructors”. Type constructors construct types.
Karl Palmskog (Sep 19 2023 at 17:56):"injectivity of a type's constructors"? Maybe?
Karl Palmskog (Sep 19 2023 at 17:58):there is this gem from Coq'Art book:
An inductive definition actually contains several terms that are types. One of these terms is the type of the type being defined the others are the type of the constructors. Each of these type terms also has a type, and the inductive definition is only well-formed if the type of all these type expressions is the same up to convertibility.
Nicolas Rinaudo (Sep 19 2023 at 20:04):Sorry - I meant to write injectivity of constructors, but I'd been talking of GADTs with a friend before so this is what popped out instead. Thanks for taking the time to explain!
Nicolas Rinaudo (Sep 19 2023 at 20:05):Is the coq'art quote saying "all constructors yield values of a subtype of the inductive type they're defined in" ?
Pierre Castéran (Sep 19 2023 at 20:24):This quote is (we hope!) made a little less abstract with a small example.
(page 381, paragraph "Universe Constraints" of chapter "Foundations of Inductive Types")
Paolo Giarrusso (Sep 19 2023 at 20:50):Nicolas: Coq does not have subtypes in that sense — think Haskell not Scala
Nicolas Rinaudo (Sep 19 2023 at 20:50):isn't that what "the type of these expressions is the same up to convertibility" means though?
Paolo Giarrusso (Sep 19 2023 at 20:56):Convertibility is symmetric, subtyping isn't.
Nicolas Rinaudo (Sep 19 2023 at 20:56):ah. Clear. Thank you.
Paolo Giarrusso (Sep 19 2023 at 20:58):But you are right there is a parallel :-).
Paolo Giarrusso (Sep 19 2023 at 20:59):Also, subtyping does come up but for different and more advanced reasons — universes — but let me not try to explain that properly. (Also, not sure you need to know about that early)
Nicolas Rinaudo (Sep 19 2023 at 21:00):yes, please, don't scare me off too quickly. I'm enjoying myself with a difficulty ramp up that seems reasonable, if you have me look too far ahead, I might just run away :)
Karl Palmskog (Sep 19 2023 at 21:00):universes :melt:
Karl Palmskog (Sep 19 2023 at 21:02):talking about universes to a Coq beginner is like... going into detail about filters in the first lecture of calculus? Maybe?
Paolo Giarrusso (Sep 19 2023 at 21:04):Agreed, agreed — I only mentioned that because "Coq doesn't have subtyping" is a white lie, but the details don't matter here
Stefan Monnier (Sep 19 2023 at 22:28):Agreed, agreed — I only mentioned that because "Coq doesn't have
subtyping" is a white lie, but the details don't matter here
Hopefully this will be fixed eventually by shedding cumulativity :smile:
Karl Palmskog (Sep 20 2023 at 08:52):are there really plans to remove cumulativity? Given that it's viewed as a "very dramatic design choice" I'd expect there would be more noise about it if there were plans.
Pierre-Marie Pédrot (Sep 20 2023 at 08:54):There is a global conspiracy to remove Prop ⊆ Type, but that's about it.
Pierre-Marie Pédrot (Sep 20 2023 at 08:56):(even such a simple change is not obviously going to really happen, so...)
Meven Lennon-Bertrand (Sep 20 2023 at 08:56):In my understanding, cumulativity is very necessary if you want to keep monomorphic universe levels. Non-cumulative universe are only viable if everything everywhere is fully universe-poly, so that the many equality constraints (instead of inequality) you get all over the place do not immediately lead to a collapse between all universes
Meven Lennon-Bertrand (Sep 20 2023 at 08:57):As far as I understand, no cumulativity + univ-poly everywhere is the model adopted by Lean, and it seems to suit them well, btw
Karl Palmskog (Sep 20 2023 at 08:59):in my design choice link, Buzzard says this about Lean's cumulativity design:
Right now it's suboptimal because we have to API ourselves around lack of universe cumulativity and nobody got around to doing it yet.
I guess they may have gotten around now.
Meven Lennon-Bertrand (Sep 20 2023 at 08:59):But given the usual historical accident that virtually every dev in Coq currently uses global universes, and this is not easy to migrate away from because of the current cost of univ-poly in a world with cumulativity, I'm not even sure how the move could happen…
Meven Lennon-Bertrand (Sep 20 2023 at 08:59):Karl Palmskog said:
in my design choice link, Buzzard says this about Lean's cumulativity design:
Right now it's suboptimal because we have to API ourselves around lack of universe cumulativity and nobody got around to doing it yet.
I guess they may have gotten around now.
Ah, maybe I'm wrong then
Karl Palmskog (Sep 20 2023 at 09:02):is there even any "advice" or "design principles" around universes in Coq? What I can find is some advice to not use -type-in-type in the Common criteria for Coq doc, but that's it
Paolo Giarrusso (Sep 20 2023 at 10:28):"don't partially apply template polymorphic inductives", maybe? And it's not even practical...
Paolo Giarrusso (Sep 20 2023 at 10:30):The most realistic strategy, there, is to fork stdlib containers to be universe-polymorphic. We have our own at Bedrock
Karl Palmskog (Sep 20 2023 at 10:41):forking stdlib was discussed at Coq Workshop (also for using SProp and the like). But I think that will not scale very well, at least with the number of forks
Karl Palmskog (Sep 20 2023 at 10:45):There is a global conspiracy to remove Prop ⊆ Type
Who are the members of this cabal? (And what are their motivations?)
Pierre-Marie Pédrot (Sep 20 2023 at 11:21):@Karl Palmskog I think I'm an unwilling member of the cabal, but the people at Nantes are much more initiated.
Pierre-Marie Pédrot (Sep 20 2023 at 11:22):I'm not sure I really understand the motivations, apart maybe for considerations about setoid TT and the like
Pierre-Marie Pédrot (Sep 20 2023 at 11:23):(I think that the unavowable belief is that it should be trivial to switch from Prop to SProp, and Prop ⊆ Type is the major barrier there)
Pierre-Marie Pédrot (Sep 20 2023 at 11:24):in a world where SProp-equality can be rewritten without breaking the theory, SProp and Prop are essentially (FINE PRINT) the same
Pierre-Marie Pédrot (Sep 20 2023 at 11:24):the fine print is obviously Acc-elimination, which holds in Prop but not SProp
Pierre-Marie Pédrot (Sep 20 2023 at 11:25):but (barring impredicativity) if you had an erasable modality, you could just do everything with Acc in Type
Pierre-Marie Pédrot (Sep 20 2023 at 11:25):so yeah, I think the goal is to switch to SProp by crippling Prop or something
Guillaume Melquiond (Sep 20 2023 at 11:57):Unless I am mistaken, Prop ⊆ Type is also a major pain point for extraction, because the extracted type can change dynamically depending on the context (and thus extra care is needed to avoid segfaults).
Paolo Giarrusso (Sep 20 2023 at 12:00):But is this realistic in Coq? The attempts I see to even use SProp today keep running into trouble https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/322
Meven Lennon-Bertrand (Sep 20 2023 at 12:03):Guillaume Melquiond said:
Unless I am mistaken, Prop ⊆ Type is also a major pain point for extraction, because the extracted type can change dynamically depending on the context (and thus extra care is needed to avoid segfaults).
Wed' have to invoke @Yannick Forster for details, but for sure in MetaCoq's extraction there are subtleties with this subtyping… To the point I think it needs to be turned off when we certify things on it?
Yannick Forster (Sep 20 2023 at 12:06):It's a pain point in extraction in the sense that the result of extraction might indeed be plain wrong if the Prop ⊆ Type rule is used to type-check something - indeed as @Guillaume Melquiond says you can run into segfaults. Thus, in MetaCoq the verification of extraction relies on a typed input with Prop ⊆ Type disabled in the type system
Meven Lennon-Bertrand (Sep 20 2023 at 12:08):Do you have a concrete example of something that goes wrong?
Guillaume Melquiond (Sep 20 2023 at 12:14):I think the simplest example is the function snd : (A B:Type) -> A * B -> B. If A and B happens to live in Prop, then so does A * B, which means that an element of that type is no longer a pair but a unit, so there is no second component.
Théo Winterhalter (Sep 20 2023 at 12:16):This one also uses template polymorphism though.
Notification Bot (Sep 20 2023 at 13:14):27 messages were moved from this topic to #Coq users > Removing cumulativity by Karl Palmskog.
Nicolas Rinaudo (Sep 20 2023 at 13:17):Well this wasn't terrifying at all.
Last updated: Oct 13 2024 at 01:02 UTC