val to_list_aux_lower_bounded (#a: eqtype) {| _: ordered a |} (t: heap a) (m: _)
    : Lemma (requires lower_bounded_heap t m) (ensures lower_bounded (to_list_aux t) m)
val to_list_aux_lower_bounded (#a: eqtype) {| _: ordered a |} (t: heap a) (m: _)
    : Lemma (requires lower_bounded_heap t m) (ensures lower_bounded (to_list_aux t) m)
let rec to_list_aux_lower_bounded (#a: eqtype) {| _ : ordered a |} (t: heap a) m:
  Lemma (requires lower_bounded_heap t m) (ensures lower_bounded (to_list_aux t) m)
= match t with
  | Leaf -> ()
  | Node k l r _ -> (
    to_list_aux_lower_bounded l k;
    lower_bounded_trans (to_list_aux l) k m;
    to_list_aux_lower_bounded r k;
    lower_bounded_trans (to_list_aux r) k m;
    merge_lower_bounded (to_list_aux l) (to_list_aux r) m
  )
(*
   Copyright 2023 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 LeftistHeap

// -----------------------------------------------------------------
// Elimination rules for the ordered type class, and instantiations
// -----------------------------------------------------------------

let gt (#t: eqtype) {| _ : ordered t |} (a b: t) =
  leq b a && a <> b

let transitivity #a {| p : ordered a |} (x y z: a):
  Lemma (requires leq x y /\ leq y z)
  (ensures leq x z)
= p.properties

let reflexivity #a {| p : ordered a |} (x: a):
  Lemma (ensures leq x x)
= p.properties

let antisymmetry (#a: eqtype) {| p : ordered a |} (x y: a):
  Lemma (requires leq x y /\ leq y x) (ensures x = y)
= p.properties

let total_order (#a: eqtype) {| p : ordered a |} (x y: a):
  Lemma (ensures leq x y \/ leq y x)
= p.properties

instance ints_leq : ordered int =
{
  leq = (<=);
  properties = ()
}

instance nats_leq : ordered nat =
{
  leq = (<=);
  properties = ()
}

// -----------------------------------------------------------------
// Useful functions and lemmas for lists
// -----------------------------------------------------------------

let delta (#a: eqtype) (x y:a): GTot int = (if x = y then 1 else 0)

let rec count (#a: eqtype) (l: list a) y: GTot nat =
  match l with
  | [] -> 0
  | t::q -> delta t y + count q y

let rec lower_bounded #a {| _ : ordered a |} (l: list a) m: GTot bool =
  match l with
  | [] -> true
  | t::q -> leq m t && lower_bounded q m

let rec lower_bounded_trans #a {| _ : ordered a |} (l: list a) m1 m2:
  Lemma (requires lower_bounded l m1 /\ leq m2 m1) (ensures lower_bounded l m2)
= match l with
  | [] -> ()
  | t::q -> (transitivity m2 m1 t; lower_bounded_trans q m1 m2)

let rec sorted_then_lower_bounded #a {| _ : ordered a |} (t: a) (q: list a):
  Lemma (requires sorted (t::q)) (ensures lower_bounded (t::q) t)
= match q with
  | [] -> reflexivity t
  | a::b ->
    (if Cons? b then transitivity t a (Cons?.hd b) else ();
    sorted_then_lower_bounded t b; assert (lower_bounded q t))

// Any element in the list is greater than or equal to a lower bound of the list
let rec lower_bounded_and_count (#a: eqtype) {| _ : ordered a |} (l: list a) (m x: a):
  Lemma (requires lower_bounded l m /\ count l x > 0) (ensures leq m x)
= match l with
  | [] -> ()
  | t::q -> if (t = x) then () else lower_bounded_and_count q m x

// Two sorted lists with the same elements (with the same multiplicities) are the same
#push-options "--split_queries always"
#push-options "--z3rlimit 30"
let rec injectivity_count_sorted (#t: eqtype) {| _ : ordered t |} (a b: list t):
  Lemma (requires (forall y. count a y = count b y) /\ sorted a /\ sorted b)
  (ensures a = b)
= match a, b with
  | ta::qa, tb::qb -> (
    // 1. ta <= tb
    eliminate forall y. count a y = count b y with tb;
    assert (count a tb > 0);
    sorted_then_lower_bounded ta qa;
    lower_bounded_and_count a ta tb;
    // 2. ta <= tb
    eliminate forall y. count a y = count b y with ta;
    assert (count b ta > 0);
    sorted_then_lower_bounded tb qb;
    lower_bounded_and_count b tb ta;
    // 3. induction hypothesis
    antisymmetry ta tb;
    injectivity_count_sorted #t qa qb
    )
  | _ -> ()
#pop-options
#pop-options

let rec merge_count (#t: eqtype) {| _: ordered t |} (a b: list t) y:
  Lemma (ensures count (merge a b) y = count a y + count b y)
= match a, b with
  | ta::qa, tb::qb -> if (leq ta tb) then merge_count qa b y else merge_count a qb y
  | _ -> ()

let rec sorted_merge #t {| _ : ordered t |} (a b: list t):
  Lemma (requires sorted #t a /\ sorted #t b) (ensures sorted (merge #t a b))
= match a, b with
  | ta::qa, tb::qb -> if (leq ta tb)
  then sorted_merge #t qa b
  else (sorted_merge #t a qb; total_order ta tb)
  | _ -> ()

let rec merge_lower_bounded (#t: eqtype) {| _ : ordered t |} (a b: list t) m:
  Lemma (requires lower_bounded a m /\ lower_bounded b m) (ensures lower_bounded (merge a b) m)
= match a, b with
  | ta::qa, tb::qb -> if (leq ta tb)
  then merge_lower_bounded qa b m
  else merge_lower_bounded a qb m
  | _ -> ()

// -----------------------------------------------------------------
// Useful functions and lemmas for heaps
// -----------------------------------------------------------------

type heap a =  
  | Leaf: heap a
  | Node: key:a -> left:heap a -> right:heap a -> rank:nat-> heap a

let rec size t: GTot nat =
  match t with
  | Leaf -> 0
  | Node _ l r _ -> 1 + size l + size r

// recursively updates the lower bound, as opposed to the list one
let rec lower_bounded_heap (#a: eqtype) {| _ : ordered a |} (t: heap a) (m: a): GTot bool =
  match t with
  | Leaf -> true
  | Node k l r _ -> lower_bounded_heap l k && lower_bounded_heap r k && leq m k

let heap_property (#a: eqtype) {| _ : ordered a |} (t: heap a): prop =
  match t with
  | Leaf -> True
  | Node k l r _ -> lower_bounded_heap l k /\ lower_bounded_heap r k

let rec count_heap (#a: eqtype) {| _ : ordered a |} (t: heap a) y: GTot nat =
  match t with
  | Leaf -> 0
  | Node k l r _ -> delta k y + count_heap l y + count_heap r y

// -----------------------------------------------------------------
// List representations of heaps
// -----------------------------------------------------------------

let rec to_list_aux (#a: eqtype) {| _ : ordered a |} (t: heap a): GTot (list a) =
  match t with
  | Leaf -> []
  | Node k l r _ -> k :: merge (to_list_aux l) (to_list_aux r)
/
prims.fst.checked FStar.Tactics.Typeclasses.fsti.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.Classical.Sugar.fsti.checked FStar.Calc.fsti.checked
LeftistHeap.fst
{| _: LeftistHeap.ordered a |} -> t: LeftistHeap.heap a -> m: a
  -> FStar.Pervasives.Lemma (requires LeftistHeap.lower_bounded_heap t m)
      (ensures LeftistHeap.lower_bounded (LeftistHeap.to_list_aux t) m)
Prims.eqtype LeftistHeap.ordered LeftistHeap.heap Prims.nat LeftistHeap.merge_lower_bounded LeftistHeap.to_list_aux Prims.unit LeftistHeap.lower_bounded_trans LeftistHeap.to_list_aux_lower_bounded Prims.b2t LeftistHeap.lower_bounded_heap Prims.squash LeftistHeap.lower_bounded Prims.Nil FStar.Pervasives.pattern
let rec to_list_aux_lower_bounded (#a: eqtype) {| _: ordered a |} (t: heap a) m
    : Lemma (requires lower_bounded_heap t m) (ensures lower_bounded (to_list_aux t) m) =
  
match t with
| Leaf -> ()
| Node k l r _ ->
  (to_list_aux_lower_bounded l k;
    lower_bounded_trans (to_list_aux l) k m;
    to_list_aux_lower_bounded r k;
    lower_bounded_trans (to_list_aux r) k m;
    merge_lower_bounded (to_list_aux l) (to_list_aux r) m)