val lemma_splitAt_fst_length (#a: Type) (n: nat) (l: list a)
    : Lemma (requires (n <= length l)) (ensures (length (fst (FLT.splitAt n l)) = n))
let rec lemma_splitAt_fst_length (#a:Type) (n:nat) (l:list a) :
  Lemma
    (requires (n <= length l))
    (ensures  (length (fst (FLT.splitAt n l)) = n)) =
  match n, l with
  | 0, _ -> ()
  | _, [] -> ()
  | _, _ :: l' -> lemma_splitAt_fst_length (n - 1) l'
val lemma_splitAt_fst_length (#a: Type) (n: nat) (l: list a)
    : Lemma (requires (n <= length l)) (ensures (length (fst (FLT.splitAt n l)) = n))
let rec lemma_splitAt_fst_length (#a: Type) (n: nat) (l: list a)
    : Lemma (requires (n <= length l)) (ensures (length (fst (FLT.splitAt n l)) = n)) =
match n, l with
| 0, _ -> ()
| _, [] -> ()
| _, _ :: l' -> lemma_splitAt_fst_length (n - 1) l'
FStar.Sequence.Base.fst.checked
prims.fst.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.List.Tot.Properties.fst.checked FStar.List.Tot.fst.checked FStar.Classical.Sugar.fsti.checked
FStar.Sequence.Base.fst
Prims.nat Prims.list FStar.Pervasives.Native.Mktuple2 Prims.int FStar.Sequence.Base.lemma_splitAt_fst_length Prims.op_Subtraction Prims.unit Prims.b2t Prims.op_LessThanOrEqual FStar.Sequence.Base.length Prims.squash Prims.op_Equality FStar.Pervasives.Native.fst FStar.List.Tot.Base.splitAt Prims.Nil FStar.Pervasives.pattern
(*
   Copyright 2008-2021 Jay Lorch, Rustan Leino, Alex Summers, Dan
   Rosen, Nikhil Swamy, Microsoft Research, and contributors to
   the Dafny Project

   Licensed under the Apache License, Version 2.0 (the "License");
   you may not use this file except in compliance with the License.
   You may obtain a copy of the License at

       http://www.apache.org/licenses/LICENSE-2.0

   Unless required by applicable law or agreed to in writing, software
   distributed under the License is distributed on an "AS IS" BASIS,
   WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
   See the License for the specific language governing permissions and
   limitations under the License.

   Includes material from the Dafny project
   (https://github.com/dafny-lang/dafny) which carries this license
   information:

     Created 9 February 2008 by Rustan Leino.
     Converted to Boogie 2 on 28 June 2008.
     Edited sequence axioms 20 October 2009 by Alex Summers.
     Modified 2014 by Dan Rosen.
     Copyright (c) 2008-2014, Microsoft.
     Copyright by the contributors to the Dafny Project
     SPDX-License-Identifier: MIT
*)

(**
This module declares a type and functions used for modeling sequences
as they're modeled in Dafny. It also states and proves some properties
about sequences, and provides a lemma `all_seq_facts_lemma` one
can call to bring them into context.  The properties are modeled after
those in the Dafny sequence axioms, with patterns for quantifiers
chosen as in those axioms.

@summary Type, functions, and properties of sequences
*)
module FStar.Sequence.Base

module FLT = FStar.List.Tot

/// Internally, we represent a sequence as a list.

type seq (ty: Type) = list ty

/// We represent the Dafny function `Seq#Length` with `length`:
///
/// function Seq#Length<T>(Seq T): int;

let length = FLT.length

/// We represent the Dafny function `Seq#Empty` with `empty`:
/// 
/// function Seq#Empty<T>(): Seq T;

let empty (#ty: Type) : seq ty = []

/// We represent the Dafny function `Seq#Singleton` with `singleton`:
///
/// function Seq#Singleton<T>(T): Seq T;

let singleton (#ty: Type) (v: ty) : seq ty =
  [v]

/// We represent the Dafny function `Seq#Index` with `index`:
///
/// function Seq#Index<T>(Seq T, int): T;

let index (#ty: Type) (s: seq ty) (i: nat{i < length s}) : ty =
  FLT.index s i

/// We represent the Dafny function `Seq#Build` with `build`:
/// 
/// function Seq#Build<T>(s: Seq T, val: T): Seq T;

let build (#ty: Type) (s: seq ty) (v: ty) : seq ty =
  FLT.append s [v]

/// We represent the Dafny function `Seq#Append` with `append`:
///
/// function Seq#Append<T>(Seq T, Seq T): Seq T;

let append = FLT.append

/// We represent the Dafny function `Seq#Update` with `update`:
///
/// function Seq#Update<T>(Seq T, int, T): Seq T;

let update (#ty: Type) (s: seq ty) (i: nat{i < length s}) (v: ty) : seq ty =
  let s1, _, s2 = FLT.split3 s i in
  append s1 (append [v] s2)

/// We represent the Dafny function `Seq#Contains` with `contains`:
///
/// function Seq#Contains<T>(Seq T, T): bool;

let contains (#ty: Type) (s: seq ty) (v: ty) : Type0 =
  FLT.memP v s

/// We represent the Dafny function `Seq#Take` with `take`:
///
/// function Seq#Take<T>(s: Seq T, howMany: int): Seq T;

let take (#ty: Type) (s: seq ty) (howMany: nat{howMany <= length s}) : seq ty =
  let result, _ = FLT.splitAt howMany s in
  result

/// We represent the Dafny function `Seq#Drop` with `drop`:
///
/// function Seq#Drop<T>(s: Seq T, howMany: int): Seq T;

let drop (#ty: Type) (s: seq ty) (howMany: nat{howMany <= length s}) : seq ty =
  let _, result = FLT.splitAt howMany s in
  result

/// We represent the Dafny function `Seq#Equal` with `equal`.
///
/// function Seq#Equal<T>(Seq T, Seq T): bool;

let equal (#ty: Type) (s0: seq ty) (s1: seq ty) : Type0 =
  length s0 == length s1 /\
    (forall j.{:pattern index s0 j \/ index s1 j}
      0 <= j && j < length s0 ==> index s0 j == index s1 j)

/// Instead of representing the Dafny function `Seq#SameUntil`, which
/// is only ever used in Dafny to represent prefix relations, we
/// instead use `is_prefix`.
///
/// function Seq#SameUntil<T>(Seq T, Seq T, int): bool;

let is_prefix (#ty: Type) (s0: seq ty) (s1: seq ty) : Type0 =
    length s0 <= length s1
  /\ (forall (j: nat).{:pattern index s0 j \/ index s1 j}
     j < length s0 ==> index s0 j == index s1 j)

/// We represent the Dafny function `Seq#Rank` with `rank`.
///
/// function Seq#Rank<T>(Seq T): int;

let rank (#ty: Type) (v: ty) = v

/// We now prove each of the facts that comprise `all_seq_facts`.
/// For fact `xxx_fact`, we prove it with `xxx_lemma`.  Sometimes, that
/// requires a helper lemma, which we call `xxx_helper`.  In some cases,
/// we need multiple helpers, so we suffix their names with integers.

private let length_of_empty_is_zero_lemma () : Lemma (length_of_empty_is_zero_fact) =
  ()

private let length_zero_implies_empty_lemma () : Lemma (length_zero_implies_empty_fact) =
  ()

private let singleton_length_one_lemma () : Lemma (singleton_length_one_fact) =
  ()

private let build_increments_length_lemma () : Lemma (build_increments_length_fact) =
  introduce forall (ty: Type) (s: seq ty) (v: ty). length (build s v) = 1 + length s
  with (
    FLT.append_length s [v]
  )

private let rec index_into_build_helper (#ty: Type) (s: list ty) (v: ty) (i: nat{i < length (append s [v])})
  : Lemma (requires i <= length s)
          (ensures  index (append s [v]) i == (if i = length s then v else index s i)) =
  FLT.append_length s [v];
  match s with
  | [] -> ()
  | hd :: tl ->
      if i = 0 then () else index_into_build_helper tl v (i - 1)

private let index_into_build_lemma ()
  : Lemma (requires build_increments_length_fact u#a)
          (ensures  index_into_build_fact u#a ()) =
  introduce forall (ty: Type) (s: seq ty) (v: ty) (i: nat{i < length (build s v)}).
                (i = length s ==> index (build s v) i == v)
              /\ (i <> length s ==> index (build s v) i == index s i)
  with (
    index_into_build_helper u#a s v i
  )

private let append_sums_lengths_lemma () : Lemma (append_sums_lengths_fact) =
  introduce forall (ty: Type) (s0: seq ty) (s1: seq ty). length (append s0 s1) = length s0 + length s1
  with (
    FLT.append_length s0 s1
  )

private let index_into_singleton_lemma (_: squash (singleton_length_one_fact u#a)) : Lemma (index_into_singleton_fact u#a ()) =
  ()

private let rec index_after_append_helper (ty: Type) (s0: list ty) (s1: list ty) (n: nat)
  : Lemma (requires n < length (append s0 s1) && length (append s0 s1) = length s0 + length s1)
          (ensures  index (append s0 s1) n == (if n < length s0 then index s0 n else index s1 (n - length s0))) =
  match s0 with
  | [] -> ()
  | hd :: tl -> if n = 0 then () else index_after_append_helper ty tl s1 (n - 1)

private let index_after_append_lemma (_: squash (append_sums_lengths_fact u#a)) : Lemma (index_after_append_fact u#a ()) =
  introduce
    forall (ty: Type) (s0: seq ty) (s1: seq ty) (n: nat{n < length (append s0 s1)}).
        (n < length s0 ==> index (append s0 s1) n == index s0 n)
      /\ (length s0 <= n ==> index (append s0 s1) n == index s1 (n - length s0))
  with (
    index_after_append_helper ty s0 s1 n
  )

private let rec lemma_splitAt_fst_length (#a:Type) (n:nat) (l:list a) :
  Lemma
    (requires (n <= length l))
val lemma_splitAt_fst_length (#a: Type) (n: nat) (l: list a)
    : Lemma (requires (n <= length l)) (ensures (length (fst (FLT.splitAt n l)) = n))
n: Prims.nat -> l: Prims.list a
  -> FStar.Pervasives.Lemma (requires n <= FStar.Sequence.Base.length l)
      (ensures
        FStar.Sequence.Base.length (FStar.Pervasives.Native.fst (FStar.List.Tot.Base.splitAt n l)) =
        n)