let function seq_numof (p: 'a -> bool) (s: seq 'a) : int =
    seq_numof_r p s 0 (length s)

  let lemma seq_contains_tail (x : 'a) (s: seq 'a)
    requires { s <> empty }
    requires { seq_contains x s }
    requires { s[0] <> x }
    ensures {  seq_contains x s[1..] }
  = ()

  let lemma seq_contains_snoc1 (x y : 'a) (s: seq 'a)
    requires { seq_contains x (snoc s y) }
    requires { x <> y }
    ensures {  seq_contains x s }
  = ()

  let lemma seq_contains_snoc2 (x y : 'a) (s: seq 'a)
    requires { seq_contains x s }
    ensures {  seq_contains x (snoc s y) }
  = ()

  let lemma seq_contains_suffix_snoc (x : 'a) (s s': seq 'a)
    requires { s' == snoc s x }
    ensures { forall i. 0 <= i < length s' -> seq_contains x s'[i..] }
  = for k = 0 to length s'-1 do
      invariant { forall i. 0 <= i < k -> seq_contains x s'[i..] }
      invariant { forall i. 0 <= i < k -> x = s'[i..][length s' -1 -i] }
      assert { x = s'[k..][length s'-1-k] };
    done

  let function p2i (p: 'a -> bool) (x : 'a) : int
    ensures { 0 <= result <= 1 }
  =
    if p x then 1 else 0

  let lemma seq_numof_snoc (s: seq 'a) (p: 'a -> bool) (x: 'a)
    ensures { seq_numof p (snoc s x) = seq_numof p s + p2i p x }
  = let l = length s in
    let s'= snoc s x in
    if l > 0 then
    begin
      assert { seq_numof_r p s' 0 l = seq_numof_r p s'[..l] 0 l };
    end

  let rec lemma seq_numof_app (s1 s2: seq 'a) (p: 'a -> bool)
      ensures { seq_numof p (s1 ++ s2) = seq_numof p s1 + seq_numof p s2 }
      variant { length s2 }
  = let l2 = length s2 in
    if l2 > 0 then
      let x = s2[l2-1] in
      let s2' = s2[..l2-1] in
      begin
        seq_numof_app s1 s2' p;
        assert { (s1 ++ s2) == snoc (s1 ++ s2') x };
        assert { seq_numof p (s1 ++ s2) = seq_numof p (s1 ++ s2') + p2i p x }
      end

  let lemma seq_numof_cons1 (s: seq 'a) (p: 'a -> bool) (x: 'a)
    ensures { seq_numof p (cons x s) = p2i p x + seq_numof p s }
  = if p x then
      assert { seq_numof p (cons x s) = 1 + seq_numof p s }
    else
      assert { seq_numof p (cons x s) = seq_numof p s }

  let rec lemma seq_numof_cons (p: 'a -> bool) (s: seq 'a) (x : 'a)
    ensures { seq_numof p (cons x s) >= seq_numof p s }
  = if p x then
      assert { seq_numof p (cons x s) = 1 + seq_numof p s }
    else
      assert { seq_numof p (cons x s) = seq_numof p s }

  let lemma seq_numof_r_decomp (p: 'a -> bool) (s: seq 'a) (i j k : int)
    requires { 0 <= i <= j <= k <= length s }
    ensures { seq_numof_r p s i k = seq_numof_r p s i j + seq_numof_r p s j k }
  = ()

  let lemma seq_numof_split (p: 'a -> bool) (s: seq 'a) (j : int)
    requires { 0 <= j < length s }
    ensures { p s[j] -> seq_numof p s = seq_numof p s[..j] + 1 + seq_numof p s[j+1..] }
    ensures { (not p s[j]) -> seq_numof p s = seq_numof p s[..j] + seq_numof p s[j+1..] }
    ensures { seq_numof p s = seq_numof p s[..j] + (if p s[j] then 1 else 0) + seq_numof p s[j+1..] }
  =
    assert { s == s[..j] ++ (cons s[j] s[j+1..]) };
    assert { seq_numof p s = seq_numof p (s[..j] ++ (cons s[j] s[j+1..])) }

  let lemma seq_numof_all (p: 'a -> bool) (s: seq 'a)
    requires { forall k. 0 <= k < length s -> p s[k] }
    ensures { seq_numof p s = length s }
  = ()

  let rec lemma seq_numof_eq_prefix_k (s1 s2: seq 'a) (p: 'a -> bool) (k : int)
    requires { length s1 = length s2 }
    requires { forall i. 0 <= i < length s1 -> p s1[i] = p s2[i] }
    requires { 0 <= k <= length s1 }
    ensures { seq_numof p s1[..k] = seq_numof p s2[..k] }
    variant { length s1 }
  =
    if length s1 = 0 then return;
    if k > 0 then
      seq_numof_eq_prefix_k s1[..k-1] s2[..k-1] p (k-1)

  let lemma seq_numof_eq_prefix (s1 s2: seq 'a) (p: 'a -> bool)
    requires { length s1 = length s2 }
    requires { forall i. 0 <= i < length s1 -> p s1[i] = p s2[i] }
    ensures { forall k. 0 <= k <= length s1 -> seq_numof p s1[..k] = seq_numof p s2[..k] }
  =
    ()

  let rec lemma seq_numof_eq_suffix_k (s1 s2: seq 'a) (p: 'a -> bool) (k : int)
    requires { length s1 = length s2}
    requires { forall i. 0 <= i < length s1 -> p s1[i] = p s2[i] }
    requires { 0 <= k <= length s1 }
    ensures { seq_numof p s1[k..] = seq_numof p s2[k..] }
    variant { length s1 }
  =
    if length s1 = 0 then return;
    if k > 0 then
      seq_numof_eq_suffix_k s1[k..] s2[k..] p 0;
    ()

  let lemma seq_numof_eq_suffix (s1 s2: seq 'a) (p: 'a -> bool)
    requires { length s1 = length s2 }
    requires { forall i. 0 <= i < length s1 -> p s1[i] = p s2[i] }
    ensures { forall k. 0 <= k <= length s1 -> seq_numof p s1[k..] = seq_numof p s2[k..] }
  =
    ()

  let lemma seq_numof_equiv (s1 s2: seq 'a) (p: 'a -> bool)
    requires { length s1 = length s2}
    requires { forall i. 0 <= i < length s1 -> p s1[i] = p s2[i] }
    ensures { seq_numof p s1 = seq_numof p s2 }
  =
    ()

  use seq.Permut
  use seq.Occ
  let lemma seq_permut_split (s1 s2 : seq 'a) (i j : int)
    requires { permut_all s1 s2 }
    requires { 0 <= i < length s1 }
    requires { 0 <= j < length s2 }
    requires { s1[i] = s2[j] }
    ensures { permut_all (s1[0..i] ++ s1[i+1..]) (s2[0..j] ++ s2[j+1..]) }
  =
    if length s1 = 0 then return;
    assert { s1 == (s1[0..i] ++ (cons s1[i] s1[i+1..])) };
    assert { s2 == (s2[0..j] ++ (cons s2[j] s2[j+1..])) };
    let s1p = s1[0..i] ++ s1[i+1..] in
    let s2p = s2[0..j] ++ s2[j+1..] in
    assert { forall x. x = s1[i] -> occ_all x s1p + 1 = occ_all x s1 = occ_all x s2 = occ_all x s2p + 1 };
    assert { forall x. x <> s1[i] -> occ_all x s1p = occ_all x s1 = occ_all x s2 = occ_all x s2p };
    assert { forall x. occ_all x s1p = occ_all x s2p };
    assert { length s1p = length s2p };
    assert { permut s1p s2p 0 (length s1p) };
    assert { permut_all s1p s2p };
    ()

  let rec lemma seq_numof_permut (s1 s2 : seq 'a) (p : 'a -> bool)
    requires { permut_all s1 s2 }
    ensures { seq_numof p s1 = seq_numof p s2 }
    variant { length s1 }
  =
    if length s1 = 0 then return;
    let j = any (j : int) ensures { 0 <= j < length s2 && s2[j] = s1[0] } in
    assert { p s1[0] = p s2[j] };
    assert { permut_all s1[1..] (s2[0..j] ++ s2[j+1..]) };
    if p s1[0] then begin
      assert { seq_numof p s1 = 1 + seq_numof p s1[1..] };
      assert { seq_numof p s2 = seq_numof p s2[0..j] + 1 + seq_numof p s2[j+1..] };
      seq_numof_permut s1[1..] (s2[0..j] ++ s2[j+1..]) p;
    end else begin
      assert { seq_numof p s1 = seq_numof p s1[1..] };
      assert { seq_numof p s2 = seq_numof p s2[0..j] + seq_numof p s2[j+1..] };
      seq_numof_permut s1[1..] (s2[0..j] ++ s2[j+1..]) p;
    end

  let lemma seq_contains_non_empty (s : seq 'a)
    requires { length s > 0 }
    ensures { exists x. seq_contains x s }
  = if length s > 0 then
      assert { seq_contains s[0] s }

  let lemma seq_forall_cons (s': seq 'a) (x : 'a) (s : seq 'a) (p: 'a -> bool)
     requires { s' = cons x s }
     requires { seq_forall p s }
     requires { p x }
     ensures { seq_forall p s' }
  = ()

  let lemma seq_prefix_snoc (s : seq 'a) (i : int)
    requires { 0 < length s }
    requires { 0 <= i <= length s - 1 }
    ensures { s[..i+1] == snoc s[..i] s[i] }
  = ()

  let lemma seq_suffix_cons (s : seq 'a) (i : int)
    requires { 0 < length s }
    requires { 0 <= i <= length s - 1 }
    ensures { s[i..] == cons s[i] s[i+1..] }
    ensures { forall k. 0 <= k < length s[i+1..] ->
       	      	s[i+1..][k] = s[i..][k+1] }
  = ()

  let lemma seq_suffix_snoc (s' s: seq 'a) (x : 'a)
    requires { s' == snoc s x }
    ensures { forall i. 0 <= i <= length s ->
    	      s'[i..] == snoc s[i..] x }
  = ()

  let lemma seq_cat_dec (s : seq 'a) (i j k : int)
    requires { 0 <= i <= j <= k <= length s }
    ensures { s[i..k] = s[i..j] ++ s[j..k] }
  =
    FreeMonoid.cat_dec s[i..k] (j-i)

  use seq.Distinct
  use seq.Occ

  let lemma seq_occ_eq_exist (s : seq 'a) (x : 'a)
    requires { occ_all x s > 0 }
    ensures { exists i. 0 <= i < length s && s[i] = x }
  =
    ()

  let rec lemma seq_uniqueness (s : seq 'a)
    requires { distinct s }
    ensures { forall i. 0 <= i < length s -> occ_all s[i] s = 1 }
    variant { length s }
  =
    let l = length s in
    if l <= 1 then
      return;
    assert { occ_all s[l-1] s[..l-1] = 0 };
    seq_uniqueness s[..l-1]

  let lemma seq_occ_2 (s : seq 'a) (i j : int)
    requires { 0 <= i < j < length s }
    requires { s[i] = s[j] }
    ensures { occ_all s[i] s >= 2 }
  =
    assert { occ_all s[i] s = occ_all s[i] s[..i] + occ_all s[i] s[i..] };
    assert { occ_all s[i] s[i..] = occ_all s[i] (s[i..j] ++ s[j..]) };
    assert { occ_all s[i] s[i..] = occ_all s[i] s[i..j] + occ_all s[i] s[j..] };
    assert { occ_all s[i] s[i..j]  >= 1 };
    assert { occ_all s[i] s[j..] >= 1 }

  let rec lemma seq_occ_0 (s : seq 'a) (x : 'a)
    ensures { occ_all x s = 0 <-> forall i. 0 <= i < length s -> s[i] <> x }
    variant { length s }
  =
    if length s > 0 then
      seq_occ_0 s[1..] x

  let lemma seq_contains_suff_pref (s : seq 'a) (x : 'a) (i : int)
    requires { 0 <= i < length s }
    ensures { seq_contains x s[..i] -> seq_contains x s }
    ensures { seq_contains x s[i..] -> seq_contains x s }
  = ()

  let lemma seq_forall_suffix (s : seq 'a) (p : 'a -> bool)
    requires { seq_forall p s }
    ensures { forall i. 0 <= i <= length s -> seq_forall p s[i..] }
  =
    ()

  let lemma seq_forall_prefix (s : seq 'a) (p : 'a -> bool)
    requires { seq_forall p s }
    ensures { forall i. 0 <= i <= length s -> seq_forall p s[..i] }
  =
    ()

  let lemma seq_forall_eq (s1 s2 : seq 'a) (p : 'a -> bool)
    requires { length s1 = length s2 }
    requires { forall i. 0 <= i < length s1 -> p s1[i] = p s2[i] }
    ensures { seq_forall p s1 = seq_forall p s2 }
  =
    ()

  let lemma seq_forall_eq_suffix (s1 s2 : seq 'a) (p : 'a -> bool)
    requires { length s1 = length s2 }
    requires { forall i. 0 <= i < length s1 -> p s1[i] = p s2[i] }
    ensures { forall i. 0 <= i <= length s1 -> seq_forall p s1[i..] = seq_forall p s2[i..] }
  =
    ()

  let lemma seq_forall_eq_prefix (s1 s2 : seq 'a) (p : 'a -> bool)
    requires { length s1 = length s2 }
    requires { forall i. 0 <= i < length s1 -> p s1[i] = p s2[i] }
    ensures { forall i. 0 <= i <= length s1 -> seq_forall p s1[..i] = seq_forall p s2[..i] }
  =
    ()

end

(* generated on Thu Nov 21 02:04:27 UTC 2024 from rev:  *)