Merge pull request #2130 from jdchristensen/matrix-universes

Matrix: use strip_reflections to avoid extra universe variables
HoTT · Nov 7, 2024 · 5722dc1 · 5722dc1
2 parents fdd64b5 + 3862664
commit 5722dc1
Showing 1 changed file with 8 additions and 6 deletions.
diff --git a/theories/Algebra/Rings/Matrix.v b/theories/Algebra/Rings/Matrix.v
@@ -5,6 +5,7 @@ Require Import Algebra.Rings.Ring Algebra.Rings.Module Algebra.Rings.CRing
   Algebra.Rings.KroneckerDelta Algebra.Rings.Vector.
 Require Import abstract_algebra.
 Require Import WildCat.Core WildCat.Paths.
+Require Import Modalities.ReflectiveSubuniverse.
 
 Set Universe Minimization ToSet.
 
@@ -692,12 +693,13 @@ Proof.
 Defined.
 
 (** The sum of two upper triangular matrices is upper triangular. *)
-Global Instance upper_triangular_plus {R : Ring@{i}} {n : nat} (M N : Matrix R n n)
+Global Instance upper_triangular_plus@{i} {R : Ring@{i}} {n : nat} (M N : Matrix R n n)
   {H1 : IsUpperTriangular M} {H2 : IsUpperTriangular N}
   : IsUpperTriangular (matrix_plus M N).
 Proof.
   unfold IsUpperTriangular.
-  strip_truncations; apply tr.
+  (* We use [strip_reflections] rather than [strip_truncations] here and below because it generates fewer universe variables in some versions of Coq. *)
+  strip_reflections; apply tr.
   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).
@@ -718,12 +720,12 @@ Proof.
 Defined.
 
 (** The negation of an upper triangular matrix is upper triangular. *)
-Global Instance upper_triangular_negate {R : Ring@{i}} {n : nat} (M : Matrix R n n)
+Global Instance upper_triangular_negate@{i} {R : Ring@{i}} {n : nat} (M : Matrix R n n)
   {H : IsUpperTriangular M}
   : IsUpperTriangular (matrix_negate M).
 Proof.
   unfold IsUpperTriangular.
-  strip_truncations; apply tr.
+  strip_reflections; apply tr.
   intros i j Hi Hj lt_i_j.
   rewrite entry_Build_Matrix.
   rewrite <- rng_negate_zero; f_ap.
@@ -741,12 +743,12 @@ Proof.
 Defined.
 
 (** The product of two upper triangular matrices is upper triangular. *)
-Global Instance upper_triangular_mult {R : Ring@{i}} {n : nat}
+Global Instance upper_triangular_mult@{i} {R : Ring@{i}} {n : nat}
   (M N : Matrix R n n) {H1 : IsUpperTriangular M} {H2 : IsUpperTriangular N}
   : IsUpperTriangular (matrix_mult M N).
 Proof.
   unfold IsUpperTriangular.
-  strip_truncations; apply tr.
+  strip_reflections; apply tr.
   intros i j Hi Hj lt_i_j.
   rewrite entry_Build_Matrix.
   apply ab_sum_zero.