add zero (as per #157)

1 files changed, 14 insertions, 0 deletions

diff --git a/src/Arithmetic/Saturated.v b/src/Arithmetic/Saturated.v
index f4f17dcee..ea44d6c3d 100644
--- a/src/Arithmetic/Saturated.v
+++ b/src/Arithmetic/Saturated.v
@@ -599,6 +599,8 @@ Section API.
 
   Definition length : T -> nat := @length Z.
 
+  Definition zero (n:nat) : T := to_list _ (B.Positional.zeros n).
+  
   Definition divmod (p : T) : T * Z :=
     (List.tl p, List.hd 0 p).
 
@@ -620,6 +622,18 @@ Section API.
     Definition eval (p : T) : Z :=
       B.Positional.eval weight (Tuple.from_list (Datatypes.length p) p (eq_refl _)).
 
+    Lemma eval_zero n : eval (zero n) = 0.
+    Proof.
+      cbv [eval zero]. rewrite <-from_list_default_eq with (d:=0).
+      erewrite length_to_list, from_list_default_eq, from_list_to_list.
+      autorewrite with push_basesystem_eval.
+      reflexivity.
+      Unshelve. distr_length.
+    Qed.
+
+    Lemma length_zero n : length (zero n) = n.
+    Proof. cbv [eval zero]. apply length_to_list. Qed.
+
     Lemma eval_add_nz p q :
       max (Datatypes.length p) (Datatypes.length q) <> 0%nat ->
       eval (fst (add p q)) = eval p + eval q - snd (add p q) * weight (Datatypes.length (fst (add p q))).