FingerTree verified in Rocq. Includes proofs of: operations maintaining balance invariants, algebraic property validity, and abstraction to list (partially complete).

FingerTree.v

From Stdlib Require Import List.
From Stdlib Require Import Lia.

(* helper functions for lists *)

Fixpoint list_init {t : Type} (n : nat) (f : nat -> t) : list t :=
  match n with
  | O => nil
  | S m => (list_init m f) ++ ((f n) :: nil)
  end.

Definition identity {t : Type} (x : t) : t := x.

Definition test_list : list nat :=  (list_init 100 identity).

(* core types *)

Inductive node {t : Type} : Type :=
  | Leaf : t -> node
  | Node2 : (node * node) -> node
  | Node3 : (node * node * node) -> node.

Inductive digit {t : Type} : Type :=
  | One : @node t -> digit
  | Two : (@node t * @node t) -> digit
  | Three : (@node t * @node t * @node t) -> digit
  | Four : (@node t * @node t * @node t * @node t) -> digit.

Inductive fingertree {t : Type} : Type :=
  | Empty : fingertree
  | Single : @node t -> fingertree
  | Deep : @digit t * fingertree  * @digit t -> fingertree.

(* abstraction types *)

Definition flatten_node_once {t : Type} (no : @node t) : list (@node t) :=
  match no with
  | Leaf a => (Leaf a) :: nil (* weird case *)
  | Node2 (a, b) => a :: b :: nil
  | Node3 (a, b, c) => a :: b :: c :: nil
  end.

Definition flatten_nodes_once {t : Type} (li : list (@node t)) : list (@node t) :=
  concat (map flatten_node_once li).

Definition node_list_of_digit {t : Type} (dig : digit) : list (@node t) :=
  match dig with
  | One a => a :: nil
  | Two (a, b) => a :: b :: nil
  | Three (a, b, c) => a :: b :: c :: nil
  | Four (a, b, c, d) => a :: b :: c :: d :: nil
  end.

Fixpoint node_list_of_tree {t : Type} (tree : fingertree) : list (@node t) :=
  match tree with
  | Empty => nil
  | Single no => no :: nil
  | Deep (pr, m, sf) =>
      (node_list_of_digit pr) ++ (flatten_nodes_once (node_list_of_tree m)) ++ (node_list_of_digit sf)
  end.

Fixpoint items_of_node {t : Type} (no : @node t) :=
  match no with
  | Leaf x => x :: nil
  | Node2 (a, b) => (items_of_node a) ++ (items_of_node b)
  | Node3 (a, b, c) => (items_of_node a) ++ (items_of_node b) ++ (items_of_node c)
  end.

Definition Abs {t : Type} (tree : fingertree) : list t :=
  concat (map items_of_node (node_list_of_tree tree)).

(* adding to the tree *)

Definition digit_add_l {t : Type} (item : @node t) (dig : digit) : digit :=
  match dig with
  | One a => Two (item, a)
  | Two (a, b) => Three (item, a, b)
  | Three (a, b, c) => Four (item, a, b, c)
  | Four (a, b, c, d) => Four (a, b, c, d) (* SHOULD NOT OCCUR *)
  end.

Fixpoint add_l_help {t : Type} (item : @node t) (tree : fingertree) : fingertree :=
  match item, tree with
  | a, Empty => Single a
  | a, (Single b) => Deep ((One a), Empty, (One b))
  | x, Deep (Four (a, b, c, d), m, sf) =>
      Deep (Two (x, a), add_l_help (Node3 (b, c, d)) m, sf)
  | a, Deep (pr, m, sf) =>
      Deep ((digit_add_l a pr), m, sf)
  end.

Definition add_l {t : Type} (item : t) (tree : fingertree) : fingertree :=
  add_l_help (Leaf item) tree.

Definition digit_add_r {t : Type} (item : @node t) (dig : digit) : digit :=
  match dig with
  | One a => Two (a, item)
  | Two (a, b) => Three (a, b, item)
  | Three (a, b, c) => Four (a, b, c, item)
  | Four (a, b, c, d) => Four (a, b, c, d) (* SHOULD NOT OCCUR *)
  end.

Fixpoint add_r_help {t : Type} (item : @node t) (tree : fingertree) : fingertree :=
  match tree, item with
  | Empty, a => Single a
  | (Single a), b => Deep ((One a), Empty, (One b))
  | Deep (pr, m, Four (a, b, c, d)), x =>
      Deep (pr, add_r_help (Node3 (a, b, c)) m, Two (d, x))
  | Deep (pr, m, sf), a =>
      Deep (pr, m, digit_add_r a sf)
  end.

Definition add_r {t : Type} (item : t) (tree : fingertree) : fingertree :=
  add_r_help (Leaf item) tree.

Fixpoint tree_of_list {t : Type} (li : list t) : fingertree :=
  match li with
  | nil => Empty
  | a :: d => add_l a (tree_of_list d)
  end.

Fixpoint tree_of_list_rev {t : Type} (li : list t) : fingertree :=
  match li with
  | nil => Empty
  | a :: d => add_r a (tree_of_list_rev d)
  end.

(* test adding and conversions *)

Example test_add_1 : (1 :: nil) = Abs (add_l 1 Empty).
Proof. reflexivity. Qed.

Example test_add_2 : (1 :: nil) = Abs (add_r 1 Empty).
Proof. reflexivity. Qed.

Example test_add_3 : (1 :: 2 :: nil) = Abs (add_l 1 (add_l 2 Empty)).
Proof. reflexivity. Qed.

Example test_add_4 : (1 :: 2 :: nil) = Abs (add_r 2 (add_r 1 Empty)).
Proof. reflexivity. Qed.

Example test_add_5 : (1 :: 2 :: 3 :: nil) = Abs (add_l 1 (add_r 3 (add_l 2 Empty))).
Proof. reflexivity. Qed.

Example test_conversion_1 : test_list = Abs (tree_of_list test_list).
Proof. reflexivity. Qed.

Example test_conversion_2 : (rev test_list) = (Abs (tree_of_list_rev test_list)).
Proof. reflexivity. Qed.

Definition test_tree := tree_of_list test_list.

(* checking emptiness and tests *)

Definition tree_is_empty {t : Type} (tree : @fingertree t) : bool :=
  match tree with
  | Empty => true
  | _ => false
  end.

Example test_empty_1 : (@tree_is_empty nat Empty) = true.
Proof. reflexivity. Qed.

Example test_empty_2 : (tree_is_empty test_tree) = false.
Proof. reflexivity. Qed.

(* helpers for head and tail functions *)

Fixpoint tree_of_node_list {t : Type} (nl : list (@node t)) : fingertree :=
  match nl with
  | nil => Empty
  | a :: b => add_l_help a (tree_of_node_list b)
  end.

Definition digit_of_node {t : Type} (no : @node t) : @digit t :=
  match no with
  | Leaf a => One (Leaf a) (* should not occur *)
  | Node2 (a, b) => Two (a, b)
  | Node3 (a, b, c) => Three (a, b, c)
  end.

(* left side head and tail *)

Definition digit_head_l {t : Type} (d : digit) : @node t :=
  match d with
  | One a => a
  | Two (a, _) => a
  | Three (a, _, _) => a
  | Four (a, _, _, _) => a
  end.

Definition tree_head_node_l {t : Type} (ft : fingertree) : option (@node t) :=
  match ft with
  | Empty => None
  | Single x => Some x
  | Deep (pr, m, sf) => Some (digit_head_l pr)
  end.

Fixpoint node_head_l {t : Type} (no : @node t) : t :=
  match no with
  | Leaf x => x
  | Node2 (a, b) => node_head_l a
  | Node3 (a, b, c) => node_head_l a
  end.

Definition tree_head_l {t : Type} (ft : fingertree) : option t :=
  option_map node_head_l (tree_head_node_l ft).

Definition digit_tail_l {t : Type} (d : @digit t) : option digit :=
  match d with
  | One _ => None
  | Two (_, b) => Some (One b)
  | Three (_, b, c) => Some (Two (b, c))
  | Four (_, b, c, d) => Some (Three (b, c, d))
  end.

Inductive left_view {t : Type} : Type :=
| NilL
| ConsL (a : @node t) (d : @fingertree t).

Fixpoint view_l {t : Type} (ft : @fingertree t) : left_view :=
  match ft with
  | Empty => NilL
  | Single x => ConsL x Empty
  | Deep (pr, m, sf) =>
      ConsL
        (digit_head_l pr)
        match (digit_tail_l pr) with
        | None =>
            match view_l m with
            | NilL => tree_of_node_list (node_list_of_digit sf)
            | ConsL a d => Deep (digit_of_node a, d, sf)
            end
        | Some pr1 => Deep (pr1, m, sf)
        end
  end.

Definition tree_tail_l {t : Type} (ft : @fingertree t) : option fingertree :=
  match view_l ft with
  | NilL => None
  | ConsL a d => Some d
  end.

Definition default_empty_tree {t : Type} (ft : option fingertree) : @fingertree t :=
  match ft with
  | Some x => x
  | None => Empty
  end.

Example test_head_tail_l_1 : (tree_head_l (tree_of_list (1 :: 2 :: 3 :: nil))) = Some 1.
Proof. reflexivity. Qed.

Example test_head_tail_l_2 :
  (Abs (default_empty_tree (tree_tail_l (tree_of_list (1 :: 2 :: 3 :: nil)))))
  =
  (2 :: 3 :: nil).
Proof. reflexivity. Qed.

Example test_head_tail_l_3 : tree_head_l (tree_of_list test_list) = hd_error test_list.
Proof. reflexivity. Qed.

Example test_head_tail_l_4 :
  Abs (default_empty_tree (tree_tail_l (tree_of_list test_list))) = (tl test_list).
Proof. reflexivity. Qed.

(* right side head and tail *)

Definition digit_head_r {t : Type} (d : digit) : @node t :=
  match d with
  | One x => x
  | Two (_, x) => x
  | Three (_, _, x) => x
  | Four (_, _, _, x) => x
  end.

Definition tree_head_node_r {t : Type} (ft : fingertree) : option (@node t) :=
  match ft with
  | Empty => None
  | Single x => Some x
  | Deep (pr, m, sf) => Some (digit_head_r sf)
  end.

Fixpoint node_head_r {t : Type} (no : @node t) : t :=
  match no with
  | Leaf x => x
  | Node2 (a, b) => node_head_l b
  | Node3 (a, b, c) => node_head_l c
  end.

Definition tree_head_r {t : Type} (ft : fingertree) : option t :=
  option_map node_head_r (tree_head_node_r ft).

(* TODO once left side works *)

Example test_head_tail_r_1 : (tree_head_r (tree_of_list_rev (1 :: 2 :: 3 :: nil))) = Some 1.
Proof. reflexivity. Qed.

(* Example test_head_tail_r_2 : *)
(*   (list_of_tree (default_empty_tree (tree_tail_r (tree_of_list_rev (Abs_of_list_t (1 :: 2 :: 3 :: nil)))))) *)
(*   = *)
(*   rev (Abs_of_list_t (2 :: 3 :: nil)). *)
(* Proof. reflexivity. Qed. *)

Example test_head_tail_r_3 : (tree_head_r (tree_of_list_rev test_list)) = (hd_error test_list).
Proof. reflexivity. Qed.

(* Example test_head_tail_r_4 : *)
(*   (list_of_tree (default_empty_tree (tree_tail_r (tree_of_list_rev test_Abs)))) = rev (tl test_Abs). *)
(* Proof. reflexivity. Qed. *)

(* concatenation *)

Fixpoint node_list_of_list {t : Type} (li : list (@node t)) : list (@node t)  :=
  match li with
  | nil => nil
  | a :: nil => (Node2 (a, a)) :: nil (* SHOULD NOT OCCUR *)
  | a :: b :: nil => (Node2 (a, b)) :: nil
  | a :: b :: c :: nil => (Node3 (a, b, c)) :: nil
  | a :: b :: c :: d :: nil => (Node2 (a, b)) :: (Node2 (c, d)) :: nil
  | a :: b :: c :: xs => (Node3 (a, b, c)) :: (node_list_of_list xs)
  end.

Fixpoint add_all_nodes_l {t : Type} (li : list (@node t)) (ft : fingertree) : fingertree :=
  match li with
  | nil => ft
  | a :: d => add_l_help a (add_all_nodes_l d ft)
  end.

Definition add_all_nodes_r_help {t : Type} (li : list (@node t)) (ft : fingertree) : fingertree :=
  fold_right add_r_help ft li.
  (* match li with *)
  (* | nil => ft *)
  (* | a :: d => add_r_help a (add_all_nodes_r_help d ft) *)
  (* end. *)

Definition add_all_nodes_r {t : Type} (li : list (@node t)) (ft : fingertree) : fingertree :=
  add_all_nodes_r_help (rev li) ft.

Fixpoint tree_append_help {t : Type} (ft1 : fingertree) (nl : list (@node t)) (ft2 : fingertree) :=
  match ft1, nl, ft2 with
  | Empty, _, _ => add_all_nodes_l nl ft2
  | _, _, Empty => add_all_nodes_r nl ft1
  | Single x, _, _ => add_l_help x (add_all_nodes_l nl ft2)
  | _, _, Single x => add_r_help x (add_all_nodes_r nl ft1)
  | Deep (pr1, m1, sf1), nl, Deep (pr2, m2, sf2) =>
      Deep
        (pr1,
        tree_append_help m1 (node_list_of_list ((node_list_of_digit sf1) ++ nl ++ (node_list_of_digit pr2))) m2,
        sf2)
  end.

Check tree_append_help.

Definition tree_append {t : Type} (ft1 : fingertree) (ft2 : fingertree) : @fingertree t :=
  tree_append_help ft1 nil ft2.

Definition small_test_list : list nat := 1 :: 2 :: 3 :: 4 :: 5 :: nil.
Definition small_test_tree : fingertree := tree_of_list small_test_list.

Example test_append_1 : (@tree_append nat Empty Empty) = Empty.
Proof. reflexivity. Qed.

Example test_append_2 : Abs (tree_append (Single (Leaf 1)) (Single (Leaf 2))) = (1 :: 2 :: nil).
Proof. reflexivity. Qed.

Example test_append_3 :
  Abs (tree_append small_test_tree small_test_tree) = (small_test_list ++ small_test_list).
Proof. reflexivity. Qed.

Example test_append_4 : Abs (tree_append test_tree test_tree) = (test_list ++ test_list).
Proof. reflexivity. Qed.

(* theorems *)

(* nodes are balanced *)
Inductive BN {t : Type} : nat -> @node t -> Prop :=
  | BN_Leaf : forall a, BN 0 (Leaf a)
  | BN_Node2 : forall n a b, BN n a -> BN n b -> BN (S n) (Node2 (a, b))
  | BN_Node3 : forall n a b c, BN n a -> BN n b -> BN n c -> BN (S n) (Node3 (a, b, c)).

(* digits are balanced *)
Inductive BD {t : Type} : nat -> @digit t -> Prop :=
  | BD_One : forall n a, BN n a  -> BD n (One a)
  | BD_Two : forall n a b, BN n a -> BN n b -> BD n (Two (a, b))
  | BD_Three : forall n a b c, BN n a -> BN n b -> BN n c -> BD n (Three (a, b, c))
  | BD_Four : forall n a b c d, BN n a -> BN n b -> BN n c -> BN n d -> BD n (Four (a, b, c, d)).

(* fingertrees are balanced *)
Inductive BFT {t : Type} : nat -> @fingertree t -> Prop :=
  | BFT_Empty : forall n, BFT n Empty
  | BFT_Single : forall n no, BN n no -> BFT n (Single no)
  | BFT_Deep : forall n pr m sf, BD n pr -> BFT (S n) m -> BD n sf -> BFT n (Deep (pr, m, sf)).

(* operations preserve BFT properties *)

Lemma add_l_help_preserves_BFT : forall (t : Type) n ft, BFT n ft -> forall (no : node), BN n no -> @BFT t n (add_l_help no ft).
Proof.
  intros t n ft HBFT. (* intros no HBN. *)
  unfold add_l_help.
  induction HBFT as [| n' no' IHn | n' pr m sf IHpr IHm IHn IHsf].
  { apply BFT_Single. }
  { intros no HBN.
    apply BFT_Deep.
    { apply BD_One. apply HBN. }
    { apply BFT_Empty. }
    { apply BD_One. apply IHn. } }
  { destruct pr.
    { intros no HBN.
      apply BFT_Deep.
      { simpl. apply BD_Two.
        { apply HBN. }
        { inversion IHpr.
          apply H1. } }
      { apply IHm. }
      { apply IHsf. } }
    { intros no HBN.
      simpl.
      destruct p as [a b].
      apply BFT_Deep.
      { apply BD_Three.
        { apply HBN. }
        { inversion IHpr.
          apply H2. }
        { inversion IHpr.
          apply H3. } }
      { apply IHm. }
      { apply IHsf. } }
    { intros no HBN.
      simpl.
      destruct p as [[a b] c].
      apply BFT_Deep; auto.
      { apply BD_Four; inversion IHpr; auto. } }
    { destruct p as [[[a b] c] d].
      intros no HBN.
      apply BFT_Deep.
      { apply BD_Two.
        { apply HBN. }
        { inversion IHpr.
          apply H4. } }
      { destruct m.
        { apply BFT_Single.
          apply BN_Node3.
          all: inversion IHpr; auto. }
        { apply BFT_Deep.
          { apply BD_One.
            apply BN_Node3.
            all: inversion IHpr; auto. }
          { apply BFT_Empty. }
          { apply BD_One.
            inversion IHm.
            apply H1. } }
        { apply IHn.
          apply BN_Node3.
          all: inversion IHpr; auto. } }
      { apply IHsf. } } }
Qed.

Theorem add_l_preserves_BFT_0 : forall (t : Type) ft (x : t), BFT 0 ft -> BFT 0 (add_l x ft).
Proof.
  intros t ft x HBFT.
  unfold add_l.
  apply add_l_help_preserves_BFT.
  { apply HBFT. }
  { apply BN_Leaf. }
Qed.

Ltac try_prove_BFT :=
  repeat
  match goal with
  | |- BD _ (One _) => constructor
  | |- BD _ (Two _) => constructor
  | |- BD _ (Three _) => constructor
  | |- BD _ (Four _) => constructor
  | |- BFT _ (Single _) => constructor
  | |- BFT _ Empty => constructor
  | |- BFT _ (Deep _) => constructor
  | H: BN ?n (Leaf _) |- BN ?n (Leaf _) => inversion H; constructor
  | H: BD ?n (One (Leaf _)) |- BN ?n (Leaf _) => inversion H; clear H
  | H: BN (S ?n) (Leaf ?t) |- BN ?n (Leaf ?t) => inversion H; clear H
  | H: BN (S ?n) (Node2 (?no, _)) |- BN ?n ?no => inversion H; clear H
  | H: BN (S ?n) (Node2 (_, ?no)) |- BN ?n ?no => inversion H; clear H
  | H: BN (S ?n) (Node3 (?no, _, _)) |- BN ?n ?no => inversion H; clear H
  | H: BN (S ?n) (Node3 (_, ?no, _)) |- BN ?n ?no => inversion H; clear H
  | H: BN (S ?n) (Node3 (_, _, ?no)) |- BN ?n ?no => inversion H; clear H
  | H: BD _ (One (Node2 (?no, _))) |- BN _ ?no => inversion H; auto
  | H: BD _ (One (Node2 (_, ?no))) |- BN _ ?no => inversion H; auto
  | H: BD _ (One (Node3 (?no, _, _))) |- BN _ ?no => inversion H; auto
  | H: BD _ (One (Node3 (_, ?no, _))) |- BN _ ?no => inversion H; auto
  | H: BD _ (One (Node3 (_, _, ?no))) |- BN _ ?no => inversion H; auto
  | H: BD _ (One ?no) |- BN _ ?no => inversion H; auto
  | H: BD _ (Two (?no, _)) |- BN _ ?no  => inversion H; auto
  | H: BD _ (Two (_, ?no)) |- BN _ ?no  => inversion H; auto
  | H: BD _ (Three (?no, _, _)) |- BN _ ?no => inversion H; auto
  | H: BD _ (Three (_, ?no, _)) |- BN _ ?no => inversion H; auto
  | H: BD _ (Three (_, _, ?no)) |- BN _ ?no => inversion H; auto
  | H: BD _ (Four (?no, _, _, _)) |- BN _ ?no => inversion H; auto
  | H: BD _ (Four (_, ?no, _, _)) |- BN _ ?no => inversion H; auto
  | H: BD _ (Four (_, _, ?no, _)) |- BN _ ?no => inversion H; auto
  | H: BD _ (Four (_, _, _, ?no)) |- BN _ ?no => inversion H; auto
  | H: BFT _ (Deep (One (Node2 (?n, _)), _, _)) |- BN _ ?n => inversion H; clear H
  | H: BFT _ (Deep (One (Node2 (_, ?n)), _, _)) |- BN _ ?n => inversion H; clear H
  | H: BFT ?n (Single ?no) |- BN ?n ?no => inversion H; clear H
  | H: BFT _ (Single (Leaf ?t)) |- BN _ (Leaf ?t) => inversion H; clear H
  | H: BFT _ (Single (Node2 (?n, _))) |- BN _ ?n => inversion H; clear H
  | H: BFT _ (Single (Node2 (_, ?n))) |- BN _ ?n => inversion H; clear H
  | H: BFT _ (Single (Node3 (?n, _, _))) |- BN _ ?n => inversion H; clear H
  | H: BFT _ (Single (Node3 (_, ?n, _))) |- BN _ ?n => inversion H; clear H
  | H: BFT _ (Single (Node3 (_, _, ?n))) |- BN _ ?n => inversion H; clear H
  | H: BFT ?n (Deep (One ?no, _, _)) |- BN ?n ?no => inversion H; clear H
  | H: BFT ?n (Deep (Two (?no, _), _, _)) |- BN ?n ?no => inversion H; clear H
  | H: BFT ?n (Deep (Two (_, ?no), _, _)) |- BN ?n ?no => inversion H; clear H
  | H: BFT ?n (Deep (Three (?no, _, _), _, _)) |- BN ?n ?no => inversion H; clear H
  | H: BFT ?n (Deep (Three (_, ?no, _), _, _)) |- BN ?n ?no => inversion H; clear H
  | H: BFT ?n (Deep (Three (_, _, ?no), _, _)) |- BN ?n ?no => inversion H; clear H
  | H: BFT ?n (Deep (Four (?no, _, _, _), _, _)) |- BN ?n ?no => inversion H; clear H
  | H: BFT ?n (Deep (Four (_, ?no, _, _), _, _)) |- BN ?n ?no => inversion H; clear H
  | H: BFT ?n (Deep (Four (_, _, ?no, _), _, _)) |- BN ?n ?no => inversion H; clear H
  | H: BFT ?n (Deep (Four (_, _, _, ?no), _, _)) |- BN ?n ?no => inversion H; clear H
  | H: BFT ?n (Deep (_, _, One ?no)) |- BN ?n ?no => inversion H; clear H
  | H: BFT ?n (Deep (_, _, Two (?no, _))) |- BN ?n ?no => inversion H; clear H
  | H: BFT ?n (Deep (_, _, Two (_, ?no))) |- BN ?n ?no => inversion H; clear H
  | H: BFT ?n (Deep (_, _, Three (?no, _, _))) |- BN ?n ?no => inversion H; clear H
  | H: BFT ?n (Deep (_, _, Three (_, ?no, _))) |- BN ?n ?no => inversion H; clear H
  | H: BFT ?n (Deep (_, _, Three (_, _, ?no))) |- BN ?n ?no => inversion H; clear H
  | H: BFT ?n (Deep (_, _, Four (?no, _, _, _))) |- BN ?n ?no => inversion H; clear H
  | H: BFT ?n (Deep (_, _, Four (_, ?no, _, _))) |- BN ?n ?no => inversion H; clear H
  | H: BFT ?n (Deep (_, _, Four (_, _, ?no, _))) |- BN ?n ?no => inversion H; clear H
  | H: BFT ?n (Deep (_, _, Four (_, _, _, ?no))) |- BN ?n ?no => inversion H; clear H
  | H: BFT _ (Deep (?d, _, _)) |- BD _ ?d => inversion H; clear H
  | H: BFT _ (Deep (_, _, ?d)) |- BD _ ?d => inversion H; clear H
  | H: BN _ ?no |- BD _ (digit_of_node ?no) => inversion H; clear H
  | H: BD _ (One ?no) |- BD _ (digit_of_node ?no) => inversion H; clear H
  | H: BFT _ (Single ?no) |- BD _ (digit_of_node ?no) => inversion H; clear H
  | H: BFT _ (Deep (One ?no, _, _)) |- BD _ (digit_of_node ?no) => inversion H; clear H
  | H: BFT _ (Deep (_, Single ?no, _)) |- BD _ (digit_of_node ?no) => inversion H; clear H
  | H: BFT _ (Deep (_, Deep (One ?no, _, _), _)) |- BD _ (digit_of_node ?no) => inversion H; clear H
  | H: BFT _ (Deep (_, Deep (Two (?no, _), _, _), _)) |- BD _ (digit_of_node ?no) => inversion H; clear H
  | H: BFT _ (Deep (_, Deep (Two (_, ?no), _, _), _)) |- BD _ (digit_of_node ?no) => inversion H; clear H
  | H: BFT _ (Deep (_, Deep (Three (?no, _, _), _, _), _)) |- BD _ (digit_of_node ?no) => inversion H; clear H
  | H: BFT _ (Deep (_, Deep (Three (_, ?no, _), _, _), _)) |- BD _ (digit_of_node ?no) => inversion H; clear H
  | H: BFT _ (Deep (_, Deep (Three (_, _, ?no), _, _), _)) |- BD _ (digit_of_node ?no) => inversion H; clear H
  | H: BFT _ (Deep (_, Deep (Four (?no, _, _, _), _, _), _)) |- BD _ (digit_of_node ?no) => inversion H; clear H
  | H: BFT _ (Deep (_, Deep (Four (_, ?no, _, _), _, _), _)) |- BD _ (digit_of_node ?no) => inversion H; clear H
  | H: BFT _ (Deep (_, Deep (Four (_, _, ?no, _), _, _), _)) |- BD _ (digit_of_node ?no) => inversion H; clear H
  | H: BFT _ (Deep (_, Deep (Four (_, _, _, ?no), _, _), _)) |- BD _ (digit_of_node ?no) => inversion H; clear H
  | H: BFT ?no (Deep (_, ?f, _)) |- BFT (S ?no) ?f => inversion H; clear H; subst
  | H: Some _ = Some _ |- _ => inversion H; try constructor; clear H
  | H: Some (Deep _) = Some (Single _) |- _ => inversion H; clear H
  | H: _ = ?s |- BFT _ ?s => rewrite <- H; simpl
  end; simpl in *; auto.

Lemma add_r_help_preserves_BFT : forall (t : Type) n ft, BFT n ft -> forall (no : node), BN n no -> @BFT t n (add_r_help no ft).
Proof.
  intros t n ft HBFT. (* intros no HBN. *)
  unfold add_l_help.
  induction HBFT as [| n' no' IHn | n' pr m sf IHpr IHm IHn IHsf].
  { apply BFT_Single. }
  { intros no HBN.
    apply BFT_Deep.
    { apply BD_One. apply IHn. }
    { apply BFT_Empty. }
    { apply BD_One. apply HBN. } }
  { destruct sf; intros no HBN; simpl; repeat destruct p; try_prove_BFT.
    apply IHn.
    inversion IHsf.
    constructor; auto. }
Qed.

Theorem add_r_preserves_BFT_0 : forall (t : Type) ft (x : t), BFT 0 ft -> BFT 0 (add_r x ft).
Proof.
  intros t ft x HBFT.
  unfold add_r.
  apply add_r_help_preserves_BFT.
  { apply HBFT. }
  { apply BN_Leaf. }
Qed. (* only works properly on BFT 0, because it's adding a leaf node *)

Lemma node_list_of_digit_preserves_n :
  forall (t : Type) n (dig : (@digit t)), BD n dig -> Forall (BN n) (node_list_of_digit dig).
Proof.
  intros t n dig HBD.
  destruct dig; repeat destruct p; simpl; repeat apply Forall_cons; try constructor; try_prove_BFT.
Qed.

Lemma tree_of_node_list_preserves_n :
  forall (t : Type) n (li : list (@node t)), Forall (BN n) li -> BFT n (tree_of_node_list li).
Proof.
  intros t n li HBN.
  induction HBN.
  { constructor. }
  { simpl.
    apply add_l_help_preserves_BFT.
    { apply IHHBN. }
    { apply H. } }
Qed.

Lemma digit_of_node_Sn_becomes_n :
  forall (t : Type) n (no : @node t), BN (S n) no -> BD n (digit_of_node no).
Proof.
  intros t n no HBN.
  destruct no.
  { inversion HBN. }
  { repeat destruct p; simpl; try_prove_BFT. }
  { repeat destruct p; simpl; try_prove_BFT. }
Qed.

Lemma digit_head_l_preserves_n :
  forall (t : Type) n (dig : @digit t), BD n dig -> BN n (digit_head_l dig).
Proof.
  intros t n dig HBD.
  destruct dig; simpl; repeat destruct p; try_prove_BFT.
Qed.

Theorem tail_l_preserves_BFT :
  forall (t : Type) n (ft : @fingertree t), BFT n ft ->
  forall (ftr : @fingertree t), tree_tail_l ft = Some ftr -> BFT n ftr.
Proof.
  intros t n ft HBFT.
  induction HBFT.
  { intros ftr Httl. inversion Httl. }
  { intros ftr Httl. inversion Httl. constructor. }
  { intros ftr Httl.
    assert (BFT n (Deep (pr, m, sf))) as HBFTprmsf.
    { constructor; auto. }
    destruct ftr.
    { constructor. }
    { constructor.
      inversion Httl.
      destruct pr; simpl in *; destruct m; repeat destruct p; simpl in *; try inversion H2.
      { inversion HBFTprmsf; subst.
        assert (BFT n (tree_of_node_list (node_list_of_digit sf))).
        { apply tree_of_node_list_preserves_n.
          apply node_list_of_digit_preserves_n.
          auto. }
        rewrite H2 in H1.
        try_prove_BFT. } }
    { repeat destruct p.
      inversion Httl.
      destruct pr; simpl in *; destruct m; repeat destruct p; simpl in *; try_prove_BFT.
      { apply tree_of_node_list_preserves_n.
        apply node_list_of_digit_preserves_n.
        try_prove_BFT. }
      { subst. try_prove_BFT. }
      { subst. try_prove_BFT. }
      { apply digit_of_node_Sn_becomes_n.
        apply digit_head_l_preserves_n.
        try_prove_BFT. } } }
Qed.

(* TODO *)
(* Theorem tail_r_preserves_BFT : *)
(*   forall (t : Type) n (ft : @fingertree t), BFT n ft -> BFT n (default_empty_tree (tree_tail_r ft)). *)
(* Proof. Admitted. *)

(* Theorem tree_append_help_preserves_BFT : *)
(*   forall (t : Type) n (nol : list (@node t)), Forall (BN n) nol -> *)
(*   forall ft1 ft2, BFT n ft1 -> BFT n ft2 -> BFT n (tree_append_help ft1 nol ft2). *)
(* Proof. *)
(*   intros t n nol Hnol. *)
(*   induction nol. *)
(*   { intros ft1 ft2 HBFT1 HBFT2. *)
(*     induction ft1; destruct ft2; simpl; repeat destruct p; auto. *)
(*     { try_prove_BFT. } *)
(*     { destruct d0; repeat destruct p; simpl; try_prove_BFT. *) 
(*       apply add_l_help_preserves_BFT; inversion HBFT2; inversion H3; auto; constructor; auto. } *)
(*     { destruct d; repeat destruct p; simpl; try_prove_BFT. *)
(*       apply add_r_help_preserves_BFT; inversion HBFT1; inversion H5; auto; constructor; auto. } *)
(*     { destruct p0 as [[pr m] sf]. try_prove_BFT. *)
(*       assert (Forall (BN n) (node_list_of_digit d)) as BNd. *)
(*       { inversion HBFT1; subst; apply node_list_of_digit_preserves_n; auto. } *)
(*       assert (Forall (BN n) (node_list_of_digit pr)) as BNpr. *)
(*       { inversion HBFT2; subst; apply node_list_of_digit_preserves_n; auto. } *)
(*       simpl. *)

(* Theorem tree_append_help_preserves_BFT : *)
(*   forall (t : Type) n (nol : list (@node t)), Forall (BN n) nol -> *)
(*   forall ft1 ft2, BFT n ft1 -> BFT n ft2 -> BFT n (tree_append_help ft1 nol ft2). *)
(* Proof. *)
(*   intros t n nol Hnol. *)
(*   induction nol. *)
(*   { intros ft1 ft2 HBFT1 HBFT2. *)
(*     induction HBFT1; induction HBFT2; simpl; repeat destruct p; simpl; try_prove_BFT. *)
(*     { unfold add_all_nodes_r; simpl; constructor; auto. } *)
(*     { destruct pr; repeat destruct p; simpl; try_prove_BFT. *)
(*       apply add_l_help_preserves_BFT; inversion H0; auto; constructor; auto. } *)
(*     { unfold add_all_nodes_r; simpl; constructor; auto. } *)
(*     { destruct sf; repeat destruct p; simpl; try_prove_BFT. *)
(*       apply add_r_help_preserves_BFT; inversion H0; auto; constructor; auto. } *)
(*     { subst. simpl in *. *)
(*       unfold tree_append_help. *)
(*       admit. (1* seems to require induction hypothesis in the base case somehow *1) (1* TODO *1) *)
(*     } } *)
(*   { intros ft1 ft2 HBFT1 HBFT2. *)
(*     induction HBFT1; induction HBFT2; simpl; repeat destruct p; simpl; try_prove_BFT. *)
(* Admitted. *)

Lemma add_all_nodes_l_preserves_BFT :
  forall (t : Type) n (nol : list (@node t)), Forall (BN n) nol ->
  forall ft, BFT n ft -> BFT n (add_all_nodes_l nol ft).
Proof.
  intros t n nol Hno.
  induction Hno.
  { intros ft HBFT. auto. }
  { intros ft HBFT; simpl.
    apply add_l_help_preserves_BFT.
    { apply IHHno; auto. }
    { auto. } }
Qed.

Lemma add_all_nodes_r_rev_preserves_BFT :
  forall (t : Type) n (nol : list (@node t)), Forall (BN n) nol ->
  forall ft, BFT n ft -> BFT n (add_all_nodes_r (rev nol) ft).
Proof.
  intros t n nol Hno.
  induction Hno.
  { intros ft HBFT. auto. }
  { intros ft HBFT.
    unfold add_all_nodes_r; simpl.
    rewrite rev_app_distr; simpl.
    unfold add_all_nodes_r in IHHno.
    apply add_r_help_preserves_BFT.
    { apply IHHno; auto. }
    { auto. } }
Qed.

Lemma add_all_nodes_r_preserves_BFT :
  forall (t : Type) n (nol : list (@node t)), Forall (BN n) nol ->
  forall ft, BFT n ft -> BFT n (add_all_nodes_r nol ft).
Proof.
  intros t n nol Hno.
  induction Hno.
  { intros ft HBFT. auto. }
  { intros ft HBFT.
    unfold add_all_nodes_r in *; simpl in *.
    unfold add_all_nodes_r_help in *.
    rewrite fold_right_app; simpl.
    apply IHHno.
    apply add_r_help_preserves_BFT; auto. }
Qed.

Lemma node_list_of_list_incr_n :
  forall (t : Type) n li, Forall (BN n) li -> Forall (@BN t (S n)) (node_list_of_list li).
Proof.
  intros t n li HBNS.
  induction HBNS; auto.
  simpl.
  destruct l.
  apply Forall_cons; try_prove_BFT; constructor; auto.
  destruct l.
  apply Forall_cons; apply Forall_inv in HBNS; try_prove_BFT; constructor; auto.
  destruct l.
  apply Forall_inv in HBNS as HBNS0.
  apply Forall_inv_tail in HBNS as HBNS1.
  apply Forall_inv in HBNS1.
  apply Forall_cons; try_prove_BFT; constructor; auto.
  destruct l.
  apply Forall_inv in HBNS as HBNS0.
  apply Forall_inv_tail in HBNS.
  apply Forall_inv in HBNS as HBNS1.
  apply Forall_inv_tail in HBNS.
  apply Forall_inv in HBNS as HBNS2.
  apply Forall_cons; try_prove_BFT; constructor; auto; constructor; auto.
  apply Forall_inv in HBNS as HBNS0.
  apply Forall_inv_tail in HBNS.
  apply Forall_inv in HBNS as HBNS1.
  apply Forall_cons.
  constructor; auto.
  simpl in *.
Admitted. 
      
Lemma tree_append_help_preserves_BFT :
  forall (t : Type) n (nol : list (@node t)), Forall (BN n) nol ->
  forall ft1 ft2, BFT n ft1 -> BFT n ft2 -> BFT n (tree_append_help ft1 nol ft2).
Proof.
  intros t n nol HBN ft1 ft2 HBFT1 HBFT2.
  generalize dependent nol. generalize dependent ft2.
  induction HBFT1; simpl; try_prove_BFT.
  { intros. apply add_all_nodes_l_preserves_BFT; auto. }
  { intros.
    destruct ft2.
    inversion HBFT2.
    { apply add_all_nodes_r_preserves_BFT; auto; try_prove_BFT. }
    { apply add_l_help_preserves_BFT; try apply add_all_nodes_l_preserves_BFT; auto. }
    { apply add_l_help_preserves_BFT; try apply add_all_nodes_l_preserves_BFT; auto. } }
  { intros.
    destruct ft2.
    { apply add_all_nodes_r_preserves_BFT; auto; try_prove_BFT. }
    { apply add_r_help_preserves_BFT; try apply add_all_nodes_r_preserves_BFT; try_prove_BFT. }
    { repeat destruct p. constructor; try_prove_BFT.
      inversion HBFT2; subst.
      apply IHHBFT1; auto.
      (* TODO: should be straightforward from here *)
      (* looks like it wasn't :( *)
Admitted.

(* correctness theorems *)

Theorem head_l_undoes_add_l : forall (t : Type) (x : t) ft, tree_head_l (add_l x ft) = Some x.
Proof.
  intros t x ft.
  destruct ft.
  { reflexivity. }
  { reflexivity. }
  { destruct p as [[pr m] sf].
    simpl.
    destruct pr.
    { reflexivity. }
    { destruct p as [a b]. reflexivity. }
    { destruct p as [[a b] c]. reflexivity. }
    { destruct p as [[[a b] c] d].
      destruct m; auto. } }
Qed.

Theorem head_r_undoes_add_r : forall (t : Type) (x : t) ft, tree_head_r (add_r x ft) = Some x.
Proof.
  intros t x ft.
  destruct ft.
  { reflexivity. }
  { reflexivity. }
  { destruct p as [[pr m] sf].
    simpl.
    destruct sf.
    { reflexivity. }
    { destruct p as [a b]. reflexivity. }
    { destruct p as [[a b] c]. reflexivity. }
    { destruct p as [[[a b] c] d].
      destruct m; auto. } }
Qed.

(* theorems about abstraction to list *)

Lemma abs_add_l_help :
  forall (t : Type) n ft, BFT n ft ->
  forall (no : @node t), BN n no -> 
  node_list_of_tree (add_l_help no ft) = no :: (node_list_of_tree ft).
Proof.
  intros t n ft HBFT.
  induction HBFT as [| n' no' IHn | n' pr m sf IHpr IHm IHn IHsf].
  { reflexivity. }
  { reflexivity. }
  { intros no HBN.
    unfold add_l_help.
    destruct pr; simpl; repeat destruct p; try reflexivity.
    fold (@add_l_help t).
    unfold node_list_of_tree.
    fold (@node_list_of_tree t).
    simpl.
    unfold flatten_nodes_once.
    destruct m; auto.
    assert (BN (S n') (Node3 (n2, n0, n))) as HBNbcd.
    { inversion IHpr; constructor; auto. }
    apply IHn in HBNbcd.
    rewrite HBNbcd. simpl. auto. }
Qed.

Theorem abs_add_l :
  forall (t : Type) (x : t) ft, BFT 0 ft -> Abs (add_l x ft) = x :: (Abs ft).
Proof.
  intros t x ft HBFT.
  unfold Abs.
  unfold add_l.
  assert (BN 0 (Leaf x)) by constructor.
  assert (node_list_of_tree (add_l_help (Leaf x) ft) = (Leaf x) :: (node_list_of_tree ft)).
  { apply abs_add_l_help with 0; auto. }
  rewrite H0.
  reflexivity.
Qed.

Lemma abs_add_r_help :
  forall (t : Type) n ft, BFT n ft ->
  forall (no : @node t), BN n no ->
  node_list_of_tree (add_r_help no ft) = (node_list_of_tree ft) ++ (no :: nil).
Proof.
  intros t n ft HBFT.
  induction HBFT as [| n' no' IHn | n' pr m sf IHpr IHm IHn IHsf].
  { reflexivity. }
  { reflexivity. }
  { intros no HBN.
    unfold add_r_help.
    destruct sf; simpl; repeat destruct p; repeat rewrite <- app_assoc; try reflexivity.
    fold (@add_r_help t).
    unfold node_list_of_tree.
    fold (@node_list_of_tree t).
    simpl.
    assert (BN (S n') (Node3 (n1, n2, n0))) as HBNn120.
    { inversion IHsf; constructor; auto. }
    apply IHn in HBNn120.
    rewrite HBNn120.
    unfold flatten_nodes_once.
    rewrite map_last.
    rewrite concat_app.
    simpl.
    repeat rewrite <- app_assoc.
    assert ((n1 :: n2 :: n0 :: nil) ++ n :: no :: nil = n1 :: n2 :: n0 :: n :: no :: nil) by auto.
    rewrite H.
    auto. }
Qed.

Theorem abs_add_r :
  forall (t : Type) (x : t) ft, BFT 0 ft -> Abs (add_r x ft) = (Abs ft) ++ (x :: nil).
Proof.
  intros t x ft HBFT.
  unfold Abs.
  unfold add_r.
  assert (BN 0 (Leaf x)) by constructor.
  assert (node_list_of_tree (add_r_help (Leaf x) ft) = (node_list_of_tree ft) ++ (Leaf x) :: nil).
  { apply abs_add_r_help with 0; auto. }
  rewrite H0.
  simpl.
  rewrite map_app.
  simpl.
  rewrite concat_app.
  reflexivity.
Qed.

Lemma abs_head_l_help :
  forall (t : Type) n (ft : @fingertree t), BFT n ft -> (tree_head_node_l ft) = hd_error (node_list_of_tree ft).
Proof.
  intros t n ft HBFT.
  induction HBFT.
  { reflexivity. }
  { destruct no; repeat destruct p; auto. }
  { destruct pr.
    { destruct n0; repeat destruct p; auto. }
    { repeat destruct p; destruct n0; repeat destruct p; auto. }
    { repeat destruct p; destruct n1; repeat destruct p; auto. }
    { repeat destruct p; destruct n2; repeat destruct p; auto. } }
Qed.

Lemma hd_error_app : forall (t : Type) (a : list t) (b : list t), a <> nil -> hd_error (a ++ b) = hd_error a.
Proof.
  intros t a b Ha.
  unfold hd_error.
  destruct a.
  { simpl.
    destruct b.
    { auto. }
    { contradiction. } }
  { destruct b; auto. }
Qed.

Lemma items_of_node_not_nil : forall (t : Type) n (no : @node t), BN n no -> items_of_node no <> nil.
Proof.
  intros t n no HBN.
  induction HBN.
  { discriminate. }
  { repeat destruct p. simpl.
    intros H.
    apply app_eq_nil in H.
    inversion H.
    contradiction. }
  { intros H.
    inversion H.
    apply app_eq_nil in H1.
    inversion H1.
    contradiction. }
Qed.


Lemma node_head_l_hd_items_of_node :
  forall t n (l : @node t), BN n l -> Some (node_head_l l) = hd_error (items_of_node l).
Proof.
  intros t n l HBN.
  induction HBN.
  { simpl; auto. }
  { simpl. rewrite IHHBN1.
    rewrite hd_error_app.
    auto.
    apply (items_of_node_not_nil t n a).
    auto. }
  { simpl. rewrite IHHBN1.
    rewrite hd_error_app.
    auto.
    apply (items_of_node_not_nil t n a).
    auto. }
Qed.

Lemma flatten_node_once_decr_n :
  forall (t : Type) n no, BN (S n) no -> Forall (@BN t n) (flatten_node_once no).
Proof.
  intros t n no HBN.
  induction no.
  { inversion HBN. }
  { repeat destruct p. simpl. inversion HBN; auto. }
  { repeat destruct p. simpl. inversion HBN; auto. }
Qed.

Lemma flatten_nodes_once_decr_n :
  forall (t : Type) n li, Forall (BN (S n)) li -> Forall (@BN t n) (flatten_nodes_once li).
Proof.
  intros t n li HBNS.
  induction HBNS; auto.
  unfold flatten_nodes_once.
  rewrite map_cons.
  simpl.
  apply Forall_app.
  split.
  { apply flatten_node_once_decr_n; auto. }
  { unfold flatten_nodes_once in IHHBNS; auto. }
Qed.

Lemma node_list_of_tree_preserves_n :
  forall (t : Type) n ft, BFT n ft -> (forall (no : @node t), In no (node_list_of_tree ft) -> BN n no).
Proof.
  intros t n ft HBFT no Hno.
  induction HBFT.
  { inversion Hno. }
  { simpl in Hno.
    inversion Hno; subst; auto.
    inversion H0. }
  { simpl in Hno.
    apply in_app_or in Hno.
    destruct Hno.
    { Check node_list_of_digit_preserves_n.
      pose proof (node_list_of_digit_preserves_n _ _ _ H).
      Search (Forall).
      rewrite Forall_forall in H2.
      apply H2; auto. }
    { apply in_app_or in H1.
      destruct H1.
      give_up.
      (* { give_up. } (1* TODO: here. *1) *) 
      (* { apply node_list_of_digit_preserves_n in H0. *)
      (*   rewrite Forall_forall in H0. *)
      (*   apply H0; auto. } *)
    { Check node_list_of_digit_preserves_n.
      pose proof (node_list_of_digit_preserves_n _ _ _ H0).
      Search (Forall).
      rewrite Forall_forall in H2.
      apply H2; auto. } }
Admitted.

Theorem abs_head_l :
  forall (t : Type) (ft : @fingertree t), BFT 0 ft -> tree_head_l ft = hd_error (Abs ft).
Proof.
  intros t ft HBFT.
  unfold tree_head_l.
  unfold Abs.
  rewrite (abs_head_l_help t 0 ft); auto.
  remember (node_list_of_tree ft);
  induction l; auto.
  simpl.
  rewrite hd_error_app.
  apply (askjdlf t 0 a).
  apply node_list_of_tree_preserves_n with ft; auto.
  rewrite <- Heql; simpl; auto.
  apply items_of_node_not_nil with 0.
  apply node_list_of_tree_preserves_n with ft; auto.
  rewrite <- Heql; simpl; auto.
Qed.