From d5e8449a71a05d166f4b2e801442066a8434aa84 Mon Sep 17 00:00:00 2001
From: Michael Sammler <noreply@sammler.me>
Date: Wed, 27 Jul 2022 13:37:42 +0200
Subject: [PATCH] Add join_length
---
theories/list_numbers.v | 4 ++++
1 file changed, 4 insertions(+)
diff --git a/theories/list_numbers.v b/theories/list_numbers.v
index 758f3660..94d3843f 100644
--- a/theories/list_numbers.v
+++ b/theories/list_numbers.v
@@ -226,6 +226,10 @@ Section mjoin.
Implicit Types l k : list A.
Implicit Types ls : list (list A).
+ Lemma join_length ls:
+ length (mjoin ls) = sum_list (length <$> ls).
+ Proof. induction ls; [done|]; csimpl. rewrite app_length. lia. Qed.
+
Lemma join_lookup_Some ls i x :
mjoin ls !! i = Some x ↔ ∃ j l i', ls !! j = Some l ∧ l !! i' = Some x
∧ i = sum_list (length <$> take j ls) + i'.
--
GitLab