From 44d92feab8a85ee9f929a50805dc38bdaf442d52 Mon Sep 17 00:00:00 2001 From: Manuel Barbosa Date: Sun, 26 Oct 2025 09:39:45 +0000 Subject: [PATCH] start improving the stability of smt in DynMatrix --- theories/algebra/DynMatrix.eca | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) diff --git a/theories/algebra/DynMatrix.eca b/theories/algebra/DynMatrix.eca index 8338e3170..00ada3d61 100644 --- a/theories/algebra/DynMatrix.eca +++ b/theories/algebra/DynMatrix.eca @@ -1664,10 +1664,12 @@ lemma catmr_subm m n: 0 <= n < cols m => proof. move => n_bound; rewrite eq_matrixP /=. split => [| i j bound]. -- smt(rows_catmr cols_catmr size_subm). +- split;2:smt(cols_catmr size_subm). + by have /# := rows_catmr (subm m 0 (rows m) 0 n) (subm m 0 (rows m) n (cols m)). rewrite get_catmr // cols_subm /=. case (j < n) => j_bound. -- rewrite get_subm /=; first 2 smt(size_catmr size_subm). +- rewrite get_subm /=; 2: smt(size_catmr size_subm). + + by have /# := size_catmr (subm m 0 (rows m) 0 n) (subm m 0 (rows m) n (cols m)). rewrite (getm0E (subm _ _ _ _ _)). + smt(size_catmr size_subm). by rewrite addr0.