From 9c4e02192bbaeb4009c798bd15fac22ce1235e10 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 +++++------ theories/prelude/Logic.ec | 2 +- 2 files changed, 6 insertions(+), 7 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 : diff --git a/theories/prelude/Logic.ec b/theories/prelude/Logic.ec index c4b133b7ff..f5713a09c3 100644 --- a/theories/prelude/Logic.ec +++ b/theories/prelude/Logic.ec @@ -522,7 +522,7 @@ lemma addbACA : interchange (^) (^) by smt(). lemma andb_addl : left_distributive (/\) (^) by smt(). lemma andb_addr : right_distributive (/\) (^) by smt(). lemma addKb : left_loop idfun (^) by smt(). -lemma addbK : right_loop idfun (^) by smt(). +lemma addbK : right_loop idfun (^) by case. lemma addIb : left_injective (^) by smt(). lemma addbI : right_injective (^) by smt().