val lemma_length0_implies_empty (#a:_) (#n:_) (il: interleaving a n{length il = 0})
  : Lemma (ensures (il == empty_interleaving a n))
val lemma_length0_implies_empty (#a:_) (#n:_) (il: interleaving a n{length il = 0})
  : Lemma (ensures (il == empty_interleaving a n))
let lemma_length0_implies_empty (#a #n:_) (il: interleaving a n{length il = 0})
  : Lemma (ensures (il == empty_interleaving a n))
  = S.lemma_empty il
module Zeta.Interleave

open FStar.Classical
open Zeta.SeqIdx

module IF = Zeta.IdxFn

let seq_index = SA.seq_index

let gen_seq (a:eqtype) (n:_) =
  {
    IF.a = elem_src a n;
    IF.phi = (fun _ -> True);
    IF.phi_commutes_with_prefix = (fun _ _ -> ());
  }

(* an element is from src t *)
let from_src #a #n (t: nat) (il: interleaving a n) (i: seq_index il)
  = t = (S.index il i).s

let to_elem #a #n (il: interleaving a n) (i: seq_index il)
  = (S.index il i).e

let i_seq (#a:_) (#n:nat) (il: interleaving a n)
  = IF.map #(gen_seq a n) (to_elem #a #n) il

let index_prop (#a #n:_) (il: interleaving a n) (i: SA.seq_index il)
  : Lemma (ensures ((S.index il i).e = index il i))
  = IF.lemma_map_map #(gen_seq a n) #_ to_elem il i

let seq_i_fm (a:eqtype) n (i:nat)
  : IF.fm_t (gen_seq a n) a
  = IF.FM (from_src #a #n i) (to_elem #a #n)

let s_seq_i (#a:_) (#n:_) (il: interleaving a n) (i:nat{i < n})
  = IF.filter_map (seq_i_fm a n i) il

let s_seq (#a:_) (#n:_) (il: interleaving a n)
  = init n (s_seq_i il)

let per_thread_prefix #a #n il i
  = let ss = s_seq il in
    let il' = prefix il i in
    let ss' = s_seq il' in
    let aux (t:_)
      : Lemma (ensures (S.index ss' t `prefix_of` S.index ss t))
      = IF.lemma_filter_map_prefix (seq_i_fm a n t) il i
    in
    forall_intro aux

let i2s_map (#a:_) (#n:_) (il:interleaving a n) (i:seq_index il)
  = let t = src il i in
    let fm = seq_i_fm a n t in
    let j = IF.filter_map_map fm il i in
    IF.lemma_map_map #(gen_seq a n) (to_elem #a #n) il i;
    (t,j)

let i2s_map_monotonic (#a #n:_) (il: interleaving a n) (i j: SA.seq_index il)
  : Lemma (requires (src il i = src il j))
          (ensures ((i < j ==> snd (i2s_map il i) < snd (i2s_map il j)) /\
                    (j < i ==> snd (i2s_map il j) < snd (i2s_map il i))))
  = let t = src il i in
    let fm = seq_i_fm a n t in
    IF.lemma_filter_map_map_monotonic fm il i j

let s2i_map (#a:_) (#n:_) (il:interleaving a n) (si: sseq_index (s_seq il))
  = let t,j = si in
    let fm = seq_i_fm a n t in
    let i = IF.filter_map_invmap fm il j in
    IF.lemma_map_map #(gen_seq a n) (to_elem #a #n) il i;
    i

let s2i_map_monotonic (#a #n:_) (il: interleaving a n) (i j: sseq_index (s_seq il))
  : Lemma (requires (fst i = fst j))
          (ensures ((snd i < snd j ==> s2i_map il i < s2i_map il j) /\
                    (snd j < snd i ==> s2i_map il j < s2i_map il i)))
  = let t = fst i in
    let fm = seq_i_fm a n t in
    IF.filter_map_invmap_monotonic fm il (snd i) (snd j)

let lemma_i2s_s2i (#a:_) (#n:_) (il:interleaving a n) (i:seq_index il):
  Lemma (ensures (s2i_map il (i2s_map il i) = i))
  = ()

let lemma_index_prefix_property (#a #n:_) (il:interleaving a n) (i:nat{i <= length il}) (j:nat{j < i}):
  Lemma (ensures (index (prefix il i) j = index il j))
  = IF.lemma_map_map #(gen_seq a n) (to_elem #a #n) il j;
    let fm = IF.map_fm #(gen_seq a n) #_ (to_elem #a #n)   in
    IF.filter_map_map_prefix_property fm il j i;
    ()

let lemma_prefix_prefix_property (#a #n:_) (il:interleaving a n) (i:nat{i <= length il}) (j:nat{j <= i}):
  Lemma (ensures (prefix (prefix il i) j == prefix il j))
  = ()

let lemma_iseq_prefix_property (#a:_) (#n:_) (il: interleaving a n) (i:nat{i <= length il})
  : Lemma (ensures (SA.prefix (i_seq il) i = i_seq (prefix il i)))
  = let fm = IF.map_fm #(gen_seq a n) #_ (to_elem #a #n)   in
    IF.lemma_filter_map_prefix fm il i

let lemma_i2s_prefix_property (#a:_) (#n:_) (il:interleaving a n)(i:nat{i <= length il})(j:nat{j < i}):
  Lemma (ensures (i2s_map (prefix il i) j = i2s_map il j))
  = let t = src il j in
    let fm = seq_i_fm a n t in
    IF.filter_map_map_prefix_property fm il j i;
    ()

let lemma_iseq_append1 (#a #n:_) (il': interleaving a n) (x: elem_src a n)
  : Lemma (ensures (let il = SA.append1 il' x in
                    i_seq il = SA.append1 (i_seq il') x.e))
  = let il = SA.append1 il' x in
    let fm = IF.map_fm #(gen_seq a n) #_ (to_elem #a #n)   in
    SA.lemma_prefix1_append il' x;
    IF.lemma_filter_map_snoc fm il
/
Zeta.SSeq.fsti.checked Zeta.SeqIdx.fsti.checked Zeta.SeqAux.fsti.checked Zeta.IdxFn.fsti.checked prims.fst.checked FStar.Seq.fst.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.Classical.Sugar.fsti.checked FStar.Classical.fsti.checked FStar.Calc.fsti.checked
Zeta.Interleave.fst
il: Zeta.Interleave.interleaving a n {FStar.Seq.Base.length il = 0}
  -> FStar.Pervasives.Lemma (ensures il == Zeta.Interleave.empty_interleaving a n)
Prims.eqtype Prims.nat Zeta.Interleave.interleaving Prims.b2t Prims.op_Equality Prims.int FStar.Seq.Base.length Zeta.Interleave.elem_src FStar.Seq.Base.lemma_empty Prims.unit Prims.l_True Prims.squash Prims.eq2 FStar.Seq.Base.seq Prims.l_or Zeta.Interleave.empty_interleaving Prims.Nil FStar.Pervasives.pattern
let lemma_length0_implies_empty (#a #n: _) (il: interleaving a n {length il = 0})
    : Lemma (ensures (il == empty_interleaving a n)) =
  
S.lemma_empty il