a variant of TD5 exo1 with even more dependent types

solutions/td5b.v

+(* TD5 *)
+
+Require Import Arith List.
+Import ListNotations.
+
+Set Implicit Arguments.
+
+(* Exercise 2 of TD4, this time with dependent types expressing that
+   trees are necessarily perfect + strictly sorted by depth
+
+   Thanks to Enrique for the initial idea.
+*)
+
+Module BList_via_HollowIndexedList.
+
+Inductive fulltree (A:Type) : nat -> Type :=
+| FLeaf : A -> fulltree A 0
+| FNode n : fulltree A n -> fulltree A n -> fulltree A (S n).
+
+Arguments FLeaf {A}.
+Arguments FNode {A} {n}.
+
+(* Hilist : hollow + indexed lists.
+   Hollow : an element may be skipped via the Hole constructor.
+   Indexed : if present, the n-th slot of a (hilist B k) has type
+     (B (n+k)).
+
+   Roughly, hilist = list (option ..) where the types of elements
+   are dependent.
+*)
+
+Inductive hilist (B : nat -> Type) : nat -> Type :=
+ | Nil n : hilist B n
+ | Hole n : hilist B (S n) -> hilist B n
+ | Cons n : B n -> hilist B (S n) -> hilist B n.
+
+Arguments Nil {B} {n}.
+Arguments Hole {B} {n}.
+Arguments Cons {B} {n}.
+
+Definition innerblist A n := hilist (fulltree A) n.
+Definition blist A := innerblist A 0.
+
+Definition empty_blist {A} : blist A := Nil.
+
+Definition size1_blist {A} (a:A) : blist A :=
+  Cons (FLeaf a) Nil.
+
+Definition size2_blist {A} (a b:A) : blist A :=
+  Hole (Cons (FNode (FLeaf a) (FLeaf b)) Nil).
+
+(* etc. The size of the trees are the binary decomposition of the total
+   number of elements in the blist. Eg :
+   1 = 1
+   2 = 0 + 2
+   3 = 1 + 2
+   4 = 0 + 0 + 2
+   Here, zeros in the decomposition are coded by constructor Hole.
+*)
+
+(* Important auxiliary function : putting a tree on the left of a bl. *)
+(* invariant : depth t = depth of leftmost option tree in the bl *)
+Fixpoint constree {A} {n:nat} (bl:innerblist A n) :
+  fulltree A n -> innerblist A n :=
+ match bl with
+ | Nil => fun t => Cons t Nil
+ | Hole bl' => fun t => Cons t bl'
+ | Cons t' bl' => fun t => Hole (constree bl' (FNode t t'))
+ end.
+
+Definition cons {A} (a:A) bl : blist A := constree bl (FLeaf a).
+
+Compute cons 2 (cons 3 (size2_blist 5 7)).
+
+(* digression : from regular list to blist and back *)
+Fixpoint list_to_blist {A} (l:list A) : blist A :=
+ match l with
+ | [] => empty_blist
+ | x::l => cons x (list_to_blist l)
+ end.
+
+Compute list_to_blist [1;2;3;4;5;6;7].
+
+Fixpoint tree_to_list {A} {n} (t:fulltree A n) : list A :=
+ match t with
+ | FLeaf a => [a]
+ | FNode t t' => tree_to_list t ++ tree_to_list t'
+ end.
+
+Fixpoint innerblist_to_list {A} {n} (bl:innerblist A n) :=
+ match bl with
+ | Nil => []
+ | Hole bl => innerblist_to_list bl
+ | Cons t bl' => tree_to_list t ++ innerblist_to_list bl'
+ end.
+Definition blist_to_list {A} (bl : blist A) := innerblist_to_list bl.
+(* end of digression *)
+
+Fixpoint unconstree {A} {n} (t:fulltree A n) : innerblist A n -> A * blist A :=
+ match t with
+ | FLeaf a => fun bl => (a, bl)
+ | FNode t t' => fun bl => unconstree t (Cons t' bl)
+ end.
+
+Fixpoint inner_uncons {A} {n} (bl : innerblist A n) : option (A * blist A) :=
+ match bl with
+ | Nil => None
+ | Hole bl => inner_uncons bl
+ | Cons t bl => Some (unconstree t (Hole bl))
+ end.
+Definition uncons {A} (bl : blist A) : option (A * blist A) :=
+ inner_uncons bl.
+
+(* invariant : n < size t (which is 2^depth t) *)
+Fixpoint nthtree {A} {d} (t:fulltree A d) n : option A :=
+ match t with
+ | FLeaf a => Some a (* normally here n must be 0 *)
+ | FNode t1 t2 =>
+   let size_t1 := 2^(pred d) in
+   if n <? size_t1 then nthtree t1 n
+   else nthtree t2 (n-size_t1)
+ end.
+
+Fixpoint inner_nth {A} {d} (bl: innerblist A d) n pow2 : option A :=
+ match bl with
+ | Nil => None
+ | Hole bl' => inner_nth bl' n (2*pow2)
+ | Cons t bl' =>
+   if n <? pow2 then nthtree t n
+   else inner_nth bl' (n-pow2) (2*pow2)
+ end.
+Definition nth {A} (bl : blist A) n := inner_nth bl n 1.
+
+Compute nth (list_to_blist [1;2;3;4;5;6;7]) 6.
+
+End BList_via_HollowIndexedList.