From 1aec445120f9a8ba0f7bb8d0862e6b7c54c55fac Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Thu, 25 Sep 2014 00:16:24 +0200
Subject: [PATCH] Soundness of constant expression evaluation.

---
 theories/list.v | 8 ++++++++
 1 file changed, 8 insertions(+)

diff --git a/theories/list.v b/theories/list.v
index df5938b8..d7ead777 100644
--- a/theories/list.v
+++ b/theories/list.v
@@ -752,6 +752,14 @@ Proof.
   intros l1 l2 Hl.
   by rewrite <-(reverse_involutive l1), <-(reverse_involutive l2), Hl.
 Qed.
+Lemma sum_list_with_app (f : A → nat) l k :
+  sum_list_with f (l ++ k) = sum_list_with f l + sum_list_with f k.
+Proof. induction l; simpl; lia. Qed.
+Lemma sum_list_with_reverse (f : A → nat) l :
+  sum_list_with f (reverse l) = sum_list_with f l.
+Proof.
+  induction l; simpl; rewrite ?reverse_cons, ?sum_list_with_app; simpl; lia.
+Qed.
 
 (** ** Properties of the [last] function *)
 Lemma last_snoc x l : last (l ++ [x]) = Some x.
-- 
GitLab