From 8e662ade237de57aff878bbbd3e07d2cd911327b Mon Sep 17 00:00:00 2001 From: Oskar Goldhahn Date: Tue, 2 Jun 2026 15:46:04 +0200 Subject: [PATCH] simplify some smt calls --- theories/algebra/DynMatrix.eca | 11 +++++------ 1 file changed, 5 insertions(+), 6 deletions(-) diff --git a/theories/algebra/DynMatrix.eca b/theories/algebra/DynMatrix.eca index 8338e31700..b9050761eb 100644 --- a/theories/algebra/DynMatrix.eca +++ b/theories/algebra/DynMatrix.eca @@ -1663,18 +1663,17 @@ lemma catmr_subm m n: 0 <= n < cols m => (subm m 0 (rows m) 0 n || subm m 0 (rows m) n (cols m)) = m. proof. move => n_bound; rewrite eq_matrixP /=. -split => [| i j bound]. -- smt(rows_catmr cols_catmr size_subm). +rewrite rows_catmr cols_catmr 2!cols_subm 2!rows_subm /= maxzz /=. +split => [/#| i j bound]. rewrite get_catmr // cols_subm /=. case (j < n) => j_bound. -- rewrite get_subm /=; first 2 smt(size_catmr size_subm). - rewrite (getm0E (subm _ _ _ _ _)). +- rewrite get_subm /= 1,2:/# (getm0E (subm _ _ _ _ _)). + smt(size_catmr size_subm). by rewrite addr0. - rewrite getm0E; 1: smt(size_catmr size_subm). rewrite add0r get_subm; [3:smt()]. - + smt(rows_catmr rows_subm). - + smt(cols_catmr cols_subm). + + by elim bound. + + smt(). qed. lemma subm_colmx (m: matrix) l :