val lemma_map_opt_dec_len
      (#a #b #z: _)
      (top: z)
      (f: (x: a{x << top} -> option b))
      (xs: list a {xs << top})
    : Lemma (requires (Some? (map_opt_dec top f xs)))
      (ensures (L.length (Some?.v (map_opt_dec top f xs)) == L.length xs))
      [SMTPat (map_opt_dec top f xs)]
let rec lemma_map_opt_dec_len #a #b #z (top:z) (f : (x:a{x << top}) -> option b) (xs : list a{xs << top})
  : Lemma (requires (Some? (map_opt_dec top f xs)))
          (ensures (L.length (Some?.v (map_opt_dec top f xs)) == L.length xs))
          [SMTPat (map_opt_dec top f xs)]
  = match xs with
    | [] -> ()
    | x::xs -> lemma_map_opt_dec_len top f xs
val lemma_map_opt_dec_len
      (#a #b #z: _)
      (top: z)
      (f: (x: a{x << top} -> option b))
      (xs: list a {xs << top})
    : Lemma (requires (Some? (map_opt_dec top f xs)))
      (ensures (L.length (Some?.v (map_opt_dec top f xs)) == L.length xs))
      [SMTPat (map_opt_dec top f xs)]
let rec lemma_map_opt_dec_len
      #a
      #b
      #z
      (top: z)
      (f: (x: a{x << top} -> option b))
      (xs: list a {xs << top})
    : Lemma (requires (Some? (map_opt_dec top f xs)))
      (ensures (L.length (Some?.v (map_opt_dec top f xs)) == L.length xs))
      [SMTPat (map_opt_dec top f xs)] =
match xs with
| [] -> ()
| x :: xs -> lemma_map_opt_dec_len top f xs
Pulse.Common.fst.checked
prims.fst.checked FStar.Tactics.fst.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.List.Tot.fst.checked FStar.Classical.fsti.checked
Pulse.Common.fst
Prims.precedes FStar.Pervasives.Native.option Prims.list Pulse.Common.lemma_map_opt_dec_len Prims.unit Prims.b2t FStar.Pervasives.Native.uu___is_Some Pulse.Common.map_opt_dec Prims.squash Prims.eq2 Prims.nat FStar.List.Tot.Base.length FStar.Pervasives.Native.__proj__Some__item__v Prims.Cons FStar.Pervasives.pattern FStar.Pervasives.smt_pat Prims.Nil
module Pulse.Common

module L = FStar.List.Tot
open FStar.Tactics

let (let?) (f:option 'a) (g:'a -> option 'b) : option 'b =
  match f with
  | None -> None
  | Some x -> g x

// let lem_bind_opt_some (x : option 'a) (f : 'a -> option 'b)
//   : Lemma (requires Some? ((let?) x f))
//           (ensures Some? x /\ Some? (f (Some?.v x)))
//           [SMTPat (Some? ((let?) x f))]
//   = ()

// let lem_bind_opt_none (x : option 'a) (f : 'a -> option 'b)
//   : Lemma (requires None? ((let?) x f))
//           (ensures None? x \/ None? (f (Some?.v x)))
//           [SMTPat (Some? ((let?) x f))]
//   = ()

let rec for_all_dec (top:'a) (l : list 'b{l << top}) (f : (x:'b{x << l} -> bool)) : bool =
  match l with
  | [] -> true
  | x::xs -> f x && for_all_dec top xs f

let rec map_dec (top:'a) (l : list 'b{l << top}) (f : (x:'b{x << l} -> 'c)) : list 'c =
  match l with
  | [] -> []
  | x::xs -> f x :: map_dec top xs f

let rec zipWith (f : 'a -> 'b -> Tac 'c) (l : list 'a) (m : list 'b)
  : Tac (l':(list 'c){L.length l' == min (L.length l) (L.length m)})
  =
  match l, m with
  | [], [] -> []
  | x::xs, y::ys -> f x y :: zipWith f xs ys
  | _ -> fail "zipWith: length mismatch"
  
val zip : (#a:Type) -> (#b:Type) -> l1:list a -> l2:list b ->
  Tot (l:list (a * b){L.length l == min (L.length l1) (L.length l2)})
let rec zip #a #b l1 l2 = match l1, l2 with
    | x::xs, y::ys -> (x,y) :: (zip xs ys)
    | _ -> []

let rec map_opt f l = match l with
  | [] -> Some []
  | x::xs ->
    let? y = f x in
    let? ys = map_opt f xs in
    Some (y::ys)

let rec map_opt_dec #a #b #z (top:z) (f : (x:a{x << top}) -> option b) (l : list a{l << top}) : option (list b)
= match l with
  | [] -> Some []
  | x::xs ->
    let? y = f x in
    let? ys = map_opt_dec top f xs in
    Some (y::ys)

let rec concat_map_opt #a #b (f : a -> option (list b)) (l : list a) : option (list b) =
  match l with
  | [] -> Some []
  | x::xs ->
    let? y = f x in
    let? ys = concat_map_opt f xs in
    Some (y@ys)

let rec lemma_map_opt_dec_len #a #b #z (top:z) (f : (x:a{x << top}) -> option b) (xs : list a{xs << top})
  : Lemma (requires (Some? (map_opt_dec top f xs)))
          (ensures (L.length (Some?.v (map_opt_dec top f xs)) == L.length xs))
val lemma_map_opt_dec_len
      (#a #b #z: _)
      (top: z)
      (f: (x: a{x << top} -> option b))
      (xs: list a {xs << top})
    : Lemma (requires (Some? (map_opt_dec top f xs)))
      (ensures (L.length (Some?.v (map_opt_dec top f xs)) == L.length xs))
      [SMTPat (map_opt_dec top f xs)]
top: z -> f: (x: a{x << top} -> FStar.Pervasives.Native.option b) -> xs: Prims.list a {xs << top}
  -> FStar.Pervasives.Lemma (requires Some? (Pulse.Common.map_opt_dec top f xs))
      (ensures
        FStar.List.Tot.Base.length (Some?.v (Pulse.Common.map_opt_dec top f xs)) ==
        FStar.List.Tot.Base.length xs)
      [SMTPat (Pulse.Common.map_opt_dec top f xs)]