val interleaving_snoc (#a #n:_) (il: interleaving a n{length il > 0})
  : Lemma (ensures (let i = length il - 1 in
                    let ss = s_seq il in
                    let is = i_seq il in
                    let il' = prefix il i in
                    let ss' = s_seq il' in
                    let is' = i_seq il' in
                    let x = index il i in
                    let t = src il i in
                    i2s_map il i = (t,S.length (S.index ss' t)) /\
                    ss' == sseq_prefix ss t /\
                    is' = SA.prefix is i))
val interleaving_snoc (#a #n:_) (il: interleaving a n{length il > 0})
  : Lemma (ensures (let i = length il - 1 in
                    let ss = s_seq il in
                    let is = i_seq il in
                    let il' = prefix il i in
                    let ss' = s_seq il' in
                    let is' = i_seq il' in
                    let x = index il i in
                    let t = src il i in
                    i2s_map il i = (t,S.length (S.index ss' t)) /\
                    ss' == sseq_prefix ss t /\
                    is' = SA.prefix is i))
let interleaving_snoc (#a #n:_) (il: interleaving a n{length il > 0})
  : Lemma (ensures (let i = length il - 1 in
                    let ss = s_seq il in
                    let is = i_seq il in
                    let il' = prefix il i in
                    let ss' = s_seq il' in
                    let is' = i_seq il' in
                    let x = index il i in
                    let t = src il i in
                    i2s_map il i = (t,S.length (S.index ss' t)) /\
                    ss' == sseq_prefix ss t /\
                    is' = SA.prefix is i))
  = let i = length il - 1 in
    let ss = s_seq il in
    let is = i_seq il in
    let t = src il i in
    let il' = prefix il i in
    let ss' = s_seq il' in
    let is' = i_seq il' in

    (* already proven in iseq_prefix_property *)
    assert(is' = SA.prefix is i);

    i2s_map_snoc il;

    let ss'2 = sseq_prefix ss t in
    let aux (tid:_)
      : Lemma (ensures (S.index ss' tid = S.index ss'2 tid))
      = let fm = seq_i_fm a n tid in
        IF.lemma_filter_map_snoc fm il;
        let s' = S.index ss' tid in
        if tid = t then
          lemma_prefix1_append s' (index il i)
    in
    forall_intro aux;
    assert(S.equal ss' ss'2);
    ()
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

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

let lemma_empty_sseq (a:eqtype) (n:_) (i: nat{i < n})
  : Lemma (ensures (let il = empty_interleaving a n in
                    S.index (s_seq il) i = S.empty #a))
  = let il = empty_interleaving a n in
    S.lemma_empty (S.index (s_seq il) i)

#push-options "--fuel 1 --ifuel 1 --query_stats"

let i2s_map_snoc (#a #n:_) (il: interleaving a n{length il > 0})
  : Lemma (ensures (let i = length il - 1 in
                    let t = src il i in
                    let ss = s_seq il in
                    let s = S.index ss t in
                    let sl = S.length s in
                    i2s_map il i = (t, sl - 1)))
  = let i = length il - 1 in
    let t = src il i in
    let ss = s_seq il in
    let s = S.index ss t in
    let sl = S.length s in

    let _,j = i2s_map il i in
    assert(sl > 0);
    if j < sl - 1 then
      let i' = s2i_map il (t,sl - 1) in
      s2i_map_monotonic il (t,j) (t,sl-1)
/
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
      (let i = FStar.Seq.Base.length il - 1 in
        let ss = Zeta.Interleave.s_seq il in
        let is = Zeta.Interleave.i_seq il in
        let il' = Zeta.Interleave.prefix il i in
        let ss' = Zeta.Interleave.s_seq il' in
        let is' = Zeta.Interleave.i_seq il' in
        let x = Zeta.Interleave.index il i in
        let t = Zeta.Interleave.src il i in
        Zeta.Interleave.i2s_map il i = (t, FStar.Seq.Base.length (FStar.Seq.Base.index ss' t)) /\
        ss' == Zeta.SSeq.sseq_prefix ss t /\ is' = Zeta.SeqAux.prefix is i))
Prims.eqtype Prims.nat Zeta.Interleave.interleaving Prims.b2t Prims.op_GreaterThan FStar.Seq.Base.length Zeta.Interleave.elem_src Prims.unit Prims._assert FStar.Seq.Base.equal FStar.Seq.Base.seq FStar.Classical.forall_intro Prims.l_and Prims.op_LessThan Prims.op_Equality FStar.Seq.Base.index Prims.l_True Prims.squash Prims.Nil FStar.Pervasives.pattern Prims.l_or Zeta.SeqAux.lemma_prefix1_append Zeta.Interleave.index Prims.bool Zeta.IdxFn.lemma_filter_map_snoc Zeta.Interleave.gen_seq Zeta.IdxFn.fm_t Zeta.Interleave.seq_i_fm Zeta.SSeq.sseq_prefix Zeta.Interleave.i2s_map_snoc Zeta.SeqAux.prefix Zeta.Interleave.i_seq Zeta.SSeq.sseq Zeta.Interleave.s_seq Zeta.Interleave.prefix Zeta.Interleave.src Prims.int Prims.op_Subtraction FStar.Pervasives.Native.tuple2 Zeta.Interleave.i2s_map FStar.Pervasives.Native.Mktuple2 Prims.eq2
let interleaving_snoc (#a #n: _) (il: interleaving a n {length il > 0})
    : Lemma
    (ensures
      (let i = length il - 1 in
        let ss = s_seq il in
        let is = i_seq il in
        let il' = prefix il i in
        let ss' = s_seq il' in
        let is' = i_seq il' in
        let x = index il i in
        let t = src il i in
        i2s_map il i = (t, S.length (S.index ss' t)) /\ ss' == sseq_prefix ss t /\
        is' = SA.prefix is i)) =
  
let i = length il - 1 in
let ss = s_seq il in
let is = i_seq il in
let t = src il i in
let il' = prefix il i in
let ss' = s_seq il' in
let is' = i_seq il' in
assert (is' = SA.prefix is i);
i2s_map_snoc il;
let ss'2 = sseq_prefix ss t in
let aux (tid: _) : Lemma (ensures (S.index ss' tid = S.index ss'2 tid)) =
  let fm = seq_i_fm a n tid in
  IF.lemma_filter_map_snoc fm il;
  let s' = S.index ss' tid in
  if tid = t then lemma_prefix1_append s' (index il i)
in
forall_intro aux;
assert (S.equal ss' ss'2);
()