diff options
Diffstat (limited to 'mathcomp/algebra')
| -rw-r--r-- | mathcomp/algebra/matrix.v | 28 | ||||
| -rw-r--r-- | mathcomp/algebra/ssrint.v | 30 | ||||
| -rw-r--r-- | mathcomp/algebra/ssrnum.v | 5 |
3 files changed, 34 insertions, 29 deletions
diff --git a/mathcomp/algebra/matrix.v b/mathcomp/algebra/matrix.v index 21730c3..a2b874a 100644 --- a/mathcomp/algebra/matrix.v +++ b/mathcomp/algebra/matrix.v @@ -148,19 +148,19 @@ Local Open Scope ring_scope. Reserved Notation "''M_' n" (at level 8, n at level 2, format "''M_' n"). Reserved Notation "''rV_' n" (at level 8, n at level 2, format "''rV_' n"). Reserved Notation "''cV_' n" (at level 8, n at level 2, format "''cV_' n"). -Reserved Notation "''M_' ( n )" (at level 8, only parsing). +Reserved Notation "''M_' ( n )" (at level 8). (* only parsing *) Reserved Notation "''M_' ( m , n )" (at level 8, format "''M_' ( m , n )"). -Reserved Notation "''M[' R ]_ n" (at level 8, n at level 2, only parsing). -Reserved Notation "''rV[' R ]_ n" (at level 8, n at level 2, only parsing). -Reserved Notation "''cV[' R ]_ n" (at level 8, n at level 2, only parsing). -Reserved Notation "''M[' R ]_ ( n )" (at level 8, only parsing). -Reserved Notation "''M[' R ]_ ( m , n )" (at level 8, only parsing). +Reserved Notation "''M[' R ]_ n" (at level 8, n at level 2). (* only parsing *) +Reserved Notation "''rV[' R ]_ n" (at level 8, n at level 2). (* only parsing *) +Reserved Notation "''cV[' R ]_ n" (at level 8, n at level 2). (* only parsing *) +Reserved Notation "''M[' R ]_ ( n )" (at level 8). (* only parsing *) +Reserved Notation "''M[' R ]_ ( m , n )" (at level 8). (* only parsing *) Reserved Notation "\matrix_ i E" (at level 36, E at level 36, i at level 2, format "\matrix_ i E"). Reserved Notation "\matrix_ ( i < n ) E" - (at level 36, E at level 36, i, n at level 50, only parsing). + (at level 36, E at level 36, i, n at level 50). (* only parsing *) Reserved Notation "\matrix_ ( i , j ) E" (at level 36, E at level 36, i, j at level 50, format "\matrix_ ( i , j ) E"). @@ -168,19 +168,19 @@ Reserved Notation "\matrix[ k ]_ ( i , j ) E" (at level 36, E at level 36, i, j at level 50, format "\matrix[ k ]_ ( i , j ) E"). Reserved Notation "\matrix_ ( i < m , j < n ) E" - (at level 36, E at level 36, i, m, j, n at level 50, only parsing). + (at level 36, E at level 36, i, m, j, n at level 50). (* only parsing *) Reserved Notation "\matrix_ ( i , j < n ) E" - (at level 36, E at level 36, i, j, n at level 50, only parsing). + (at level 36, E at level 36, i, j, n at level 50). (* only parsing *) Reserved Notation "\row_ j E" (at level 36, E at level 36, j at level 2, format "\row_ j E"). Reserved Notation "\row_ ( j < n ) E" - (at level 36, E at level 36, j, n at level 50, only parsing). + (at level 36, E at level 36, j, n at level 50). (* only parsing *) Reserved Notation "\col_ j E" (at level 36, E at level 36, j at level 2, format "\col_ j E"). Reserved Notation "\col_ ( j < n ) E" - (at level 36, E at level 36, j, n at level 50, only parsing). + (at level 36, E at level 36, j, n at level 50). (* only parsing *) Reserved Notation "x %:M" (at level 8, format "x %:M"). Reserved Notation "A *m B" (at level 40, left associativity, format "A *m B"). @@ -248,8 +248,8 @@ Notation "''cV_' n" := 'M_(n, 1) : type_scope. Notation "''M_' n" := 'M_(n, n) : type_scope. Notation "''M_' ( n )" := 'M_n (only parsing) : type_scope. -Notation "\matrix[ k ]_ ( i , j ) E" := (matrix_of_fun k (fun i j => E)) - (at level 36, E at level 36, i, j at level 50): ring_scope. +Notation "\matrix[ k ]_ ( i , j ) E" := (matrix_of_fun k (fun i j => E)) : + ring_scope. Notation "\matrix_ ( i < m , j < n ) E" := (@matrix_of_fun _ m n matrix_key (fun i j => E)) (only parsing) : ring_scope. @@ -1579,7 +1579,7 @@ Qed. Lemma mul_delta_mx_cond m n p (j1 j2 : 'I_n) (i1 : 'I_m) (k2 : 'I_p) : delta_mx i1 j1 *m delta_mx j2 k2 = delta_mx i1 k2 *+ (j1 == j2). Proof. -apply/matrixP=> i k; rewrite !mxE (bigD1 j1) //=. +apply/matrixP => i k; rewrite !mxE (bigD1 j1) //=. rewrite mulmxnE !mxE !eqxx andbT -natrM -mulrnA !mulnb !andbA andbAC. by rewrite big1 ?addr0 // => j; rewrite !mxE andbC -natrM; move/negPf->. Qed. diff --git a/mathcomp/algebra/ssrint.v b/mathcomp/algebra/ssrint.v index 3903609..f54a957 100644 --- a/mathcomp/algebra/ssrint.v +++ b/mathcomp/algebra/ssrint.v @@ -40,6 +40,16 @@ Set Implicit Arguments. Unset Strict Implicit. Unset Printing Implicit Defensive. +Reserved Notation "n %:Z" (at level 2, left associativity, format "n %:Z"). +Reserved Notation "n = m :> 'in' 't'" + (at level 70, m at next level, format "n = m :> 'in' 't'"). +Reserved Notation "n == m :> 'in' 't'" + (at level 70, m at next level, format "n == m :> 'in' 't'"). +Reserved Notation "n != m :> 'in' 't'" + (at level 70, m at next level, format "n != m :> 'in' 't'"). +Reserved Notation "n <> m :> 'in' 't'" + (at level 70, m at next level, format "n <> m :> 'in' 't'"). + Import Order.TTheory GRing.Theory Num.Theory. Delimit Scope int_scope with Z. Local Open Scope int_scope. @@ -50,19 +60,13 @@ Variant int : Set := Posz of nat | Negz of nat. (* the Coq module system. *) (* Coercion Posz : nat >-> int. *) -Notation "n %:Z" := (Posz n) - (at level 2, left associativity, format "n %:Z", only parsing) : int_scope. -Notation "n %:Z" := (Posz n) - (at level 2, left associativity, format "n %:Z", only parsing) : ring_scope. - -Notation "n = m :> 'in' 't'" := (Posz n = Posz m) - (at level 70, m at next level, format "n = m :> 'in' 't'") : ring_scope. -Notation "n == m :> 'in' 't'" := (Posz n == Posz m) - (at level 70, m at next level, format "n == m :> 'in' 't'") : ring_scope. -Notation "n != m :> 'in' 't'" := (Posz n != Posz m) - (at level 70, m at next level, format "n != m :> 'in' 't'") : ring_scope. -Notation "n <> m :> 'in' 't'" := (Posz n <> Posz m) - (at level 70, m at next level, format "n <> m :> 'in' 't'") : ring_scope. +Notation "n %:Z" := (Posz n) (only parsing) : int_scope. +Notation "n %:Z" := (Posz n) (only parsing) : ring_scope. + +Notation "n = m :> 'in' 't'" := (Posz n = Posz m) : ring_scope. +Notation "n == m :> 'in' 't'" := (Posz n == Posz m) : ring_scope. +Notation "n != m :> 'in' 't'" := (Posz n != Posz m) : ring_scope. +Notation "n <> m :> 'in' 't'" := (Posz n <> Posz m) : ring_scope. Definition natsum_of_int (m : int) : nat + nat := match m with Posz p => inl _ p | Negz n => inr _ n end. diff --git a/mathcomp/algebra/ssrnum.v b/mathcomp/algebra/ssrnum.v index 3bae08e..6198b44 100644 --- a/mathcomp/algebra/ssrnum.v +++ b/mathcomp/algebra/ssrnum.v @@ -1579,7 +1579,7 @@ Arguments ler01 {R}. Arguments ltr01 {R}. Arguments normr_idP {R x}. Arguments normr0P {R V v}. -Hint Resolve @ler01 @ltr01 ltr0Sn ler0n : core. +Hint Resolve ler01 ltr01 ltr0Sn ler0n : core. Hint Extern 0 (is_true (0 <= norm _)) => exact: normr_ge0 : core. Section NumDomainOperationTheory. @@ -3821,7 +3821,8 @@ Notation "[ 'arg' 'max_' ( i > i0 ) F ]" := [arg max_(i > i0 | true) F] Variable R : realDomainType. Implicit Types x y z t : R. -Hint Resolve (@num_real R) : core. +Let numR_real := @num_real R. +Hint Resolve numR_real : core. Lemma sgr_cp0 x : ((sg x == 1) = (0 < x)) * |