Skip to content

Adapt to Coq#19611 #2127

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Closed
Tragicus wants to merge 2 commits into from
Closed

Adapt to Coq#19611 #2127

Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
213ef4a
fix Algebra/Rings/Matrix.v
Tragicus Sep 30, 2024
13cbce4
Rings/Matrix: revert some universe annotations
jdchristensen Oct 31, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
17 changes: 14 additions & 3 deletions theories/Algebra/Rings/Matrix.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -697,7 +697,11 @@ Global Instance upper_triangular_plus {R : Ring@{i}} {n : nat} (M N : Matrix R n
: IsUpperTriangular (matrix_plus M N).
Proof.
unfold IsUpperTriangular.
strip_truncations; apply tr.
revert_opaque H1.
refine (@Trunc_ind _ _ _ (fun _ => istrunc_truncation _ _) _).
intro H1.
revert_opaque H2; refine (Trunc_ind@{i i} _ _); intro H2.
apply tr.
Comment on lines +700 to +704
Copy link
Collaborator

@jdchristensen jdchristensen Oct 30, 2024

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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.

Copy link
Collaborator

@jdchristensen jdchristensen Oct 31, 2024

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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.

Copy link
Collaborator

@jdchristensen jdchristensen Oct 31, 2024

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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?

Copy link
Contributor

@JasonGross JasonGross Oct 31, 2024 •
edited
Loading

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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})

Copy link
Collaborator

@SkySkimmer SkySkimmer Oct 31, 2024

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I don't think using Unsafe would make the proof particularly cleaner.

Copy link
Collaborator

@jdchristensen jdchristensen Oct 31, 2024 •
edited
Loading

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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?

intros i j Hi Hj lt_i_j.
specialize (H1 i j Hi Hj lt_i_j).
specialize (H2 i j Hi Hj lt_i_j).
Expand All @@ -723,7 +727,10 @@ Global Instance upper_triangular_negate {R : Ring@{i}} {n : nat} (M : Matrix R n
: IsUpperTriangular (matrix_negate M).
Proof.
unfold IsUpperTriangular.
strip_truncations; apply tr.
revert_opaque H.
refine (@Trunc_ind@{i i} _ _ _ (fun _ => istrunc_truncation _ _) _).
intro H.
apply tr.
intros i j Hi Hj lt_i_j.
rewrite entry_Build_Matrix.
rewrite <- rng_negate_zero; f_ap.
Expand All @@ -746,7 +753,11 @@ Global Instance upper_triangular_mult {R : Ring@{i}} {n : nat}
: IsUpperTriangular (matrix_mult M N).
Proof.
unfold IsUpperTriangular.
strip_truncations; apply tr.
revert_opaque H1.
refine (@Trunc_ind _ _ _ (fun _ => istrunc_truncation _ _) _).
intro H1.
revert_opaque H2; refine (Trunc_ind@{i i} _ _); intro H2.
apply tr.
intros i j Hi Hj lt_i_j.
rewrite entry_Build_Matrix.
apply ab_sum_zero.
Expand Down