val collect_abs_order' (bds: binders) (tt t: term)
    : Lemma (requires t << tt /\ bds <<: tt)
      (ensures
        (let bds', body = collect_abs' bds t in
          (bds' <<: tt /\ body << tt)))
      (decreases t)
let rec collect_abs_order' (bds: binders) (tt t: term)
  : Lemma (requires t << tt /\ bds <<: tt)
          (ensures (let bds', body = collect_abs' bds t in
                    (bds' <<: tt /\ body << tt)))
          (decreases t)
  = match inspect_ln_unascribe t with
    | Tv_Abs b body -> collect_abs_order' (b::bds) tt body
    | _ -> ()
val collect_abs_order' (bds: binders) (tt t: term)
    : Lemma (requires t << tt /\ bds <<: tt)
      (ensures
        (let bds', body = collect_abs' bds t in
          (bds' <<: tt /\ body << tt)))
      (decreases t)
let rec collect_abs_order' (bds: binders) (tt t: term)
    : Lemma (requires t << tt /\ bds <<: tt)
      (ensures
        (let bds', body = collect_abs' bds t in
          (bds' <<: tt /\ body << tt)))
      (decreases t) =
match inspect_ln_unascribe t with
| Tv_Abs b body -> collect_abs_order' (b :: bds) tt body
| _ -> ()
FStar.Reflection.V2.Derived.Lemmas.fst.checked
prims.fst.checked FStar.Reflection.V2.Derived.fst.checked FStar.Reflection.V2.Data.fsti.checked FStar.Reflection.V2.Builtins.fsti.checked FStar.Reflection.Types.fsti.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.List.Tot.fst.checked FStar.Classical.fsti.checked
FStar.Reflection.V2.Derived.Lemmas.fst
FStar.Reflection.Types.binders FStar.Reflection.Types.term FStar.Reflection.V2.Derived.inspect_ln_unascribe FStar.Reflection.Types.binder FStar.Reflection.V2.Derived.Lemmas.collect_abs_order' Prims.Cons FStar.Reflection.V2.Data.term_view Prims.unit Prims.l_and Prims.precedes FStar.Reflection.V2.Derived.Lemmas.op_Less_Less_Colon Prims.squash Prims.list FStar.Pervasives.Native.tuple2 FStar.Reflection.V2.Derived.collect_abs' Prims.Nil FStar.Pervasives.pattern
(*
   Copyright 2008-2018 Microsoft Research

   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.
*)
module FStar.Reflection.V2.Derived.Lemmas

open FStar.Reflection.Types
open FStar.Reflection.V2.Builtins
open FStar.Reflection.V2.Data
open FStar.Reflection.V2.Derived
open FStar.List.Tot

let rec forall_list (p:'a -> Type) (l:list 'a) : Type =
    match l with
    | [] -> True
    | x::xs -> p x /\ forall_list p xs

let forallP (p: 'a -> Type) (l: list 'a): Type
  = forall (x: 'a). memP x l ==> p x
// Precedence relation on the element of a list
unfold let (<<:) (l: list 'a) (r: 'r)
  = forallP (fun x -> x << r) l

// A glorified `id`
val list_ref : (#a:Type) -> (#p:(a -> Type)) -> (l:list a) ->
                    Pure (list (x:a{p x}))
                         (requires (forallP p l))
                         (ensures (fun _ -> True))
let rec list_ref #a #p l =
    match l with
    | [] -> []
    | x::xs -> x :: list_ref #a #p xs

val collect_app_order' : (args:list argv) -> (tt:term) -> (t:term) ->
             Lemma (requires args <<: tt /\ t << tt)
                   (ensures (let fn, args' = collect_app_ln' args t in
                             args' <<: tt /\ fn << tt))
                   (decreases t)
let rec collect_app_order' args tt t =
    match inspect_ln_unascribe t with
    | Tv_App l r -> collect_app_order' (r::args) tt l
    | _ -> ()

val collect_app_order : (t:term) ->
            Lemma (ensures (forall (f:term). forall (s:list argv). (f,s) == collect_app_ln t ==>
                              (f << t /\ s <<: t)
                            \/ (f == t /\ s == [])))
let collect_app_order t =
    match inspect_ln_unascribe t with
    | Tv_App l r -> collect_app_order' [r] t l
    | _ -> ()

val collect_app_ref : (t:term) -> (h:term{h == t \/ h << t}) * list (a:argv{fst a << t})
let collect_app_ref t =
    let h, a = collect_app_ln t in
    collect_app_order t;
    h, list_ref a

(**** [collect_abs_ln t] is smaller than [t] *)
let rec collect_abs_order' (bds: binders) (tt t: term)
  : Lemma (requires t << tt /\ bds <<: tt)
          (ensures (let bds', body = collect_abs' bds t in
                    (bds' <<: tt /\ body << tt)))
val collect_abs_order' (bds: binders) (tt t: term)
    : Lemma (requires t << tt /\ bds <<: tt)
      (ensures
        (let bds', body = collect_abs' bds t in
          (bds' <<: tt /\ body << tt)))
      (decreases t)

    bds: FStar.Reflection.Types.binders ->
    tt: FStar.Reflection.Types.term ->
    t: FStar.Reflection.Types.term
  -> FStar.Pervasives.Lemma (requires t << tt /\ bds <<: tt)
      (ensures
        (let _ = FStar.Reflection.V2.Derived.collect_abs' bds t in
          (let FStar.Pervasives.Native.Mktuple2 #_ #_ bds' body = _ in
            bds' <<: tt /\ body << tt)
          <:
          Type0))
      (decreases t)