Adapt to Coq#19611 #2127
Adapt to Coq#19611 #2127
Conversation
|
These changes aren't pretty. Can you explain why the changes in coq/coq#19611 make them necessary? It's also surprising to me that so much needs to change in this one file, but nothing else in the entire library needs to change. |
|
I am afraid I will have a hard time answering, since I have no idea how coq deals with universes and my changes only touch the unification algorithm. I am also surprised, but since there already are annotations I was not too worried. I am available if anyone can help me understand what happens. |
| revert_opaque H1. | ||
| refine (@Trunc_ind _ _ _ (fun _ => istrunc_truncation _ _) _). | ||
| intro H1. | ||
| revert_opaque H2; refine (Trunc_ind@{i i} _ _); intro H2. | ||
| apply tr. |
There was a problem hiding this comment.
Ah, I figured out what is special about these uses of strip_truncations. The goal is non-dependent, so Coq isn't able to guess which truncation to apply to the domain. If we replace them with strip_reflections (adding Require Import Modalities.ReflectiveSubuniverse. to the top of the file), then those three lines are the only changes that need making.
Even better would be for strip_truncations to first try Trunc_rec, the non-dependent eliminator. I'll see if I can do this, but it won't be right away. @Alizter , if you have a chance, feel free to take a look.
There was a problem hiding this comment.
Hmm, no, that explanation is not correct. The same universe issue happens whether you use Trunc_ind or Trunc_rec, but things work out ok with either O_ind or O_rec. Somehow the cumulativity of our truncations is causing Coq to generate a free universe variable. That kind of thing has happened to us here and there with other lemmas involving cumulative inductives, but I can't figure out why the update to Coq is causing it to happen just in this file when we use strip_truncations, but not everywhere else that uses that tactic. E.g. Rings/Ideal.v uses it a lot, without issues.
If any Coq developers have any insight into this, it would be very helpful.
There was a problem hiding this comment.
Is there a way in Ltac to find out the universe arguments in a term t? E.g. something like unify t identifier@{?u} that would instantiate a "universe evar u" that we could use later?
There was a problem hiding this comment.
For things like this you should use Ltac2's Constr.Unsafe.kind: the Constant (constant, instance) constructor has the name of the constant and the universe instance. I'm not sure if there are useful operations on instances (cc @SkySkimmer ?), though, other than exact reuse? I guess you can define instance extension and whatnot in Gallina (Definition extend@{i j} : dummy@{i} -> dummy@{j})
There was a problem hiding this comment.
I don't think using Unsafe would make the proof particularly cleaner.
There was a problem hiding this comment.
I would like the strip_truncations tactic to operate on a goal of the form Trunc@{u} X -> Y using Trunc_ind@{u _}. The way it works now, it seems to use Trunc_ind@{v _} (probably with a <= constraint on v), which is valid since Trunc is cumulative, but which generates an unwanted universe variable. (In some cases, Coq later identifies this universe variable with u, but in Matrix.v, it seems to be leaving it free, which is causing problems.) So if some trick can be done in one place to make strip_truncations work this way, it would make proofs cleaner. Unfortunately, I don't understand @JasonGross 's comment well enough to try this.
Alternatively, can a universe variable be passed into a tactic? E.g. could we have strip_truncations@{i j} or strip_truncations i j which tells it which universe variables to use?
coq/coq#19611 changes the behavior of the unification algorithm.