From 909e127ec64bf98904882f43a35e3023ee124be7 Mon Sep 17 00:00:00 2001 From: Avi Shinnar Date: Sun, 28 Apr 2024 00:21:08 -0400 Subject: [PATCH] Prove icoef_maxnorm_triang Signed-off-by: Avi Shinnar --- coq/FHE/arith.v | 18 ++++++++++++++++-- 1 file changed, 16 insertions(+), 2 deletions(-) diff --git a/coq/FHE/arith.v b/coq/FHE/arith.v index 0a416203..50db5860 100644 --- a/coq/FHE/arith.v +++ b/coq/FHE/arith.v @@ -2692,8 +2692,22 @@ Lemma icoef_maxnorm_triang (a b : {poly int}) : icoef_maxnorm (a + b) <= icoef_maxnorm a + icoef_maxnorm b. Proof. rewrite /icoef_maxnorm. - - Admitted. + apply/bigmax_leqP => i _. + eapply leq_trans; first by rewrite coefD; apply absz_triang. + apply leq_add. + - case: (boolP (i < size a)); intros. + + eapply leq_trans; cycle 1. + apply leq_bigmax_seq; rewrite ?mem_index_enum //. + by apply (@leq_trans `|a`_(Ordinal p)|). + + rewrite nth_default //. + by rewrite leqNgt i0. + - case: (boolP (i < size b)); intros. + + eapply leq_trans; cycle 1. + apply leq_bigmax_seq; rewrite ?mem_index_enum //. + by apply (@leq_trans `|b`_(Ordinal p)|). + + rewrite nth_default //. + by rewrite leqNgt i0. +Qed. Lemma icoef_maxnorm_neg (a : {poly int}) : icoef_maxnorm (-a) = icoef_maxnorm a.