From 20aaaff61efefeac5985ddf754c3b213536bda27 Mon Sep 17 00:00:00 2001
From: Barry Trager <bmt@us.ibm.com>
Date: Sun, 29 Oct 2023 07:11:27 +0100
Subject: [PATCH] canon_norm_zero_mod_qpoly

---
 coq/FHE/encode.v | 40 +++++++++++++++++++++++++---------------
 1 file changed, 25 insertions(+), 15 deletions(-)

diff --git a/coq/FHE/encode.v b/coq/FHE/encode.v
index 7e640c58..2790af65 100644
--- a/coq/FHE/encode.v
+++ b/coq/FHE/encode.v
@@ -2310,22 +2310,24 @@ Section norms.
     by rewrite canon_norm_inf_C_pow.
   Qed.
 
-  Lemma f_le_big_max n (i : 'I_n) (F : 'I_n -> R) :
-    (F i <= \big[Order.max/0]_(j < n) F j)%O.
-  Proof.
-    Admitted.
-      
-
-  Lemma canon_norm_inf_val n (p : {poly R}) i :
-    (normc ((map_poly RtoC p).[odd_nth_roots n 0 i]) <= canon_norm_inf n p)%O.
+  Lemma canon_norm_inf_val n (p : {poly R}) (i : 'I_(2^n-1).+1) :
+    (normc ((map_poly RtoC p).[odd_nth_roots' n 0 i]) <= canon_norm_inf n p)%O.
   Proof.
     unfold canon_norm_inf, norm_inf.
     simpl.
-    generalize (f_le_big_max (2^n) i (fun i => normc (map_poly RtoC p).[odd_nth_roots n 0 i])); intros.
+    generalize (@bigmaxr_le (2^n-1).+1 (odd_nth_roots' n) 0 (fun c => normc (map_poly RtoC p).[c]) i); intros.
     eapply Order.POrderTheory.le_trans.
-    - apply H.
-    - admit.
-    Admitted.
+    - rewrite /Order.le/=.
+      apply H.
+    - rewrite /Order.le/=.
+      apply /RlebP.
+      right.
+      apply eq_big_seq.
+      intros ??.
+      f_equal.
+      unfold mx_eval.
+      by rewrite !mxE.
+  Qed.
 
   Lemma squeez0 (x : R) :
     (R0 <= x)%O ->
@@ -2342,7 +2344,7 @@ Section norms.
       by replace (R0) with (IZR (Z0)) in H by lra.
   Qed.
 
-  Lemma canon_norm_zer_mod_qpoly n (p : {poly R}) :
+  Lemma canon_norm_zero_mod_qpoly n (p : {poly R}) :
     canon_norm_inf n p = 0 ->
     Pdiv.Ring.rmodp (R:=R_ringType) p ('X^(2 ^ n) + 1%:P) = 0.
   Proof.
@@ -2351,12 +2353,20 @@ Section norms.
     intros.
     unfold root.
     apply /eqP.
-    generalize (canon_norm_inf_val n p i); intros.
+    generalize (canon_norm_inf_val n p); intros.
+    destruct i.
+    assert (m < (2^n-1).+1) by lia.
+    specialize (H0 (Ordinal H1)).
     rewrite H in H0.
     apply ComplexField.Normc.eq0_normc.
     apply squeez0.
     - apply normc_nneg.
-    - by replace (R0) with (IZR (Z0)) by lra.
+    - replace (odd_nth_roots n 0 (Ordinal (n:=2^n) i)) with
+        (odd_nth_roots' n 0 (Ordinal (n:=(2^n-1).+1) H1)).
+      + by replace (R0) with (IZR (Z0)) by lra.
+      + unfold odd_nth_roots'.
+        unfold odd_nth_roots.
+        by rewrite !mxE.
   Qed.
 
 (* following only holds on quotient ring by x^+(2^n) + 1