Breadth First Reconstruction

[DmxLarchey]

BFR is a generalization of BFN. Given a tree t and a list l of values, provided l is of length equal to the size of the tree t, it redecorates the tree t with the values in l, in BF order.

let rec bfr_f p = function
  | [] -> q_nil
  | x::mm -> let t,p1 = q_deq p in
    (match t with
       | Leaf _ ->         q_enq (bfr_f p1 mm) (Leaf y)
       | Node (a, _, b) -> let u,q1 = q_deq (bfr_f (q_enq (q_enq p1 a) b) mm) in
                           let v,q2 = q_deq q1 
                           in q_enq q2 (Node (v, x, u)))

let bfr t l = let t',_ = q_deq (bfr_f (q_enq q_nil t) l) in t'

We implement BFR as bfr_3q in bfr_fifo_3q_full.v and show the BFN is a particular case of BFR as theorem bfr_bfn_3q

This PR also contains an axiomatic characterization of DF and BF orders on branches in bt.v

[DmxLarchey]

I have updated this introductory comment with the extracted code.

[rmatthes]

Function bfn2 in bfn_stream.v is now considered as ill-formed. I tried to compile with Coq 8.8.2 and 8.8.1. The project does not compile any longer with 8.7.2, so I could not see if the function was still okay there.