From 859f5d20a443f42a42f77cb7ea646222328c746d Mon Sep 17 00:00:00 2001
From: Thibault Dardinier <t.dardinier@gmail.com>
Date: Mon, 10 Jul 2023 11:45:30 -0700
Subject: [PATCH] Simple lemma about appending permutations

---
 ulib/FStar.Seq.Properties.fst  | 6 ++++++
 ulib/FStar.Seq.Properties.fsti | 5 +++++
 2 files changed, 11 insertions(+)

diff --git a/ulib/FStar.Seq.Properties.fst b/ulib/FStar.Seq.Properties.fst
index 589ef8290fc..3a7e6b5c6d7 100644
--- a/ulib/FStar.Seq.Properties.fst
+++ b/ulib/FStar.Seq.Properties.fst
@@ -189,6 +189,12 @@ let lemma_swap_permutes_aux #_ s i j x =
   end
 #pop-options  
 
+let append_permutations #a s1 s2 s1' s2' =
+  (
+    lemma_append_count s1 s2;
+    lemma_append_count s1' s2'
+  )
+
 let lemma_swap_permutes #a s i j
   = FStar.Classical.forall_intro
                     #a
diff --git a/ulib/FStar.Seq.Properties.fsti b/ulib/FStar.Seq.Properties.fsti
index 1c67ecf8b6a..3734681e829 100644
--- a/ulib/FStar.Seq.Properties.fsti
+++ b/ulib/FStar.Seq.Properties.fsti
@@ -196,6 +196,11 @@ val lemma_swap_permutes_aux: #a:eqtype -> s:seq a -> i:nat{i<length s} -> j:nat{
 
 type permutation (a:eqtype) (s1:seq a) (s2:seq a) =
        (forall i. count i s1 = count i s2)
+
+val append_permutations: #a:eqtype -> s1:seq a -> s2:seq a -> s1':seq a -> s2':seq a -> Lemma
+    (requires permutation a s1 s1' /\ permutation a s2 s2')
+    (ensures permutation a (append s1 s2) (append s1' s2'))
+
 val lemma_swap_permutes (#a:eqtype) (s:seq a) (i:nat{i<length s}) (j:nat{i <= j && j<length s})
   : Lemma (permutation a s (swap s i j))