(* ================================================================= *)
(* ====                     PRIORITY QUEUES                     ==== *)
(* ================================================================= *)

(** 
A priority queue is an abstract data type in computer programming that
supports the following operations:
 - insert: add an element to the queue with an associated priority
 - next: return the element from the queue that has the highest
   priority.
 - remove_next: remove the element from the queue that has the highest
   priority

To be concrete, in the sequel, we assume that priorities are
represented by natural numbers and that if i < j, i has a greater
priority than j.

Priority queues have many applications, such as graph algorithms,
bandwidth management, computer graphics (ROAM -- Real-time optimally
adapting mesh).

Easy implementations are inefficient:
 - Sorted list implementation : O(n) insertion time, O(1) next and
   remove_next time, O(n*log(n)) to build
 - Unsorted list implementation (to add an element, append it as the
   head; to get the next element, search through all elements for the
   one with the highest priority): (O(1) insertion time, O(n)
   next and remove_next time.
   This was essentially [find-min] in previous homework.

Indeed, some ordering is necessary in order ot have efficient
next and remove_next operations. But a total ordering is too much.

Efficient implementations called heaps are based on binary trees
enjoying the following properties:
 - Partial ordering
 - Balancing

Partial ordering means that on all subtrees (including the whole tree),
the contents of the root has the highest priority; but no order is 
specified on sibling nodes.

Balancing means that the depth of all leaf belong to some
set {n, n+1}.

In an imperative setting, such trees are represented by arrays
(the trick is that node at address n has children at addresses
2.n and 2.n+1). Reasonning on such a structure is made unnecessarily
difficult because the implementation has to be taken into account
all the time, whereas we woulf like to focus an the design,
i.e. just the shape.
Therefore we will stick to a purely functional representation.

The first part of this project deals only with partially ordered
trees.  Balanced partially ordered trees (i.e., heaps) are considered
in a second stage.

*)

(* ----------------------------  Part 1 ---------------------------- *)
  

(** * Partially Ordered binary Trees  (Step 1)  *)

(** ** Data structure

Design an inductive type called [tree] for binary-tree-based priority
queues.
Specify a predicate [pot] on them saying that elements are partially
ordered according to the above definition. 

*)

(** ** Functional Insertion

Design a function [insert_pot] for inserting an element in a binary
tree, such that inserting an element in a pot returns a pot.

Remark: several solutions are possible

Prove that [insert_pot] has the required property about sorting.

Prove that [insert_pot x t] contains all elements among [t] and [x],
and conversely.

*)


(** ** Relational Insertion

Design a inductive relation [rel_insert_pot] such that any suitable
[insert_pot] solution to the previous question should satisfy
rel_insert_pot x l (insert_pot x l).

Prove it for your version of [insert_pot].

Prove that [rel_insert_pot] has the required property about sorting.

Prove that if [rel_insert_pot x t xt], then [xt] contains all elements
among [t] and [x], and conversely.

*)

(** ** Deletion

Design a function [remove_pot] for removing an element in a binary
tree, such that removing an element in a pot returns a pot.

Hint: design first a suitable [merge] function which merges 2 pots
into one pot.

Prove that [remove_pot] has the required property about sorting.

Prove that [remove_pot t] contains all elements among [t] but its min
and conversely.

*)



(* ----------------------------  Part 2 ---------------------------- *)


(** * Heaps (Step 2) 

Heaps are well-balanced pots. When inserting a new element, we can
choose to go on the left branch or on the right branch. A simple
criterium for making this decision is based on the size (i.e. the
number of elements): if the size of the left sub-tree is less than the
size of the right sub-tree, insertion will be performed on the left
sub-tree; and conversely.

Defining the size of a tree is easy, but using this definition
in the algorithm would entail a terrible loss of performance
(for a single insertion, the same computation would be performed
again and again; do you see why?).

Our implementation of heaps will then involve a enriched type
here the size of each tree is kept at its root.
A suitable type for a heap is then 
type heap = 
  | L : heap 
  | N : nat -> heap -> nat -> heap -> heap 

In a heap [h = N s l x r], [s] is expected to be the size of [h].

Note: there is no need to add a similar nat s in the constructor L, since 
this s can only be 0. However it is strongly recommanded to use the
following trivial function in the sequel (for reasonning purposes):

Definition given_size (h: heap) : nat :=
  match h with
  | l => 0
  | N s _ _ _ => s
  end.

Define a predicate is_heap, which holds iff its argument
is a pot and the expected size is the real one (everywhere).

Adapt the previous algorithm for pot-insertion to heaps
and prove

forall h, is_heap h -> forall x, is_heap (insert_h x h)

Optional exercise: define a suitable predicate [balanced] 
and prove 
forall h, balanced h -> forall x, balanced (insert_h x h)

*)