(* -*- coq-prog-args: ("-emacs-U" "-R" "." "FingerTree" "-R" "../safe" "Safe" "-R" "../monads" "Monad") -*- *)
Require Import FingerTree.Reduce.
Require Import FingerTree.Digit.
Require Import Coq.subtac.Utils.
Require Import Safe.List.
Require Import FingerTree.Monoid.
Set Implicit Arguments.

Module MeasuredFingerTree(M : Monoid).
  Import M.
  Variable A : Type.
  Variable measure : A -> v.

  Section Nodes.    
    Inductive node (A : Type) : Type :=
    | Node2 : v -> A -> A -> node A
    | Node3 : v -> A -> A -> A -> node A.

    Variable A : Type.
    Variable measure : A -> v.
    Notation " 'lparr' x 'rparr' " := (measure x) (x ident, no associativity).
    Definition node2 (x y : A) : node A := Node2 (lparr x rparr cdot lparr y rparr) x y.
    Definition node3 (x y z : A) : node A := Node3 (lparr x rparr cdot lparr y rparr cdot lparr z rparr) x y z.
  
    Definition node_measure : node A -> v :=
      fun n =>
        match n with
          | Node2 v _ _ => v
          | Node3 v _ _ _ => v
        end.
    
    Section NodesReduce.
      Variables X Y : Type.
      Variable reducer : X -> Y -> Y.
      Variable reducel : Y -> X -> Y.
      Notation " x <_n y " := (reducer x y) (right associativity, at level 30).
      Notation " x >_n y " := (reducel x y) (left associativity, at level 21).

      Definition node_reducer (n : node X) w :=
        match n with
          | Node2 _ x y => x <_n y <_n w
          | Node3 _ x y z => x <_n y <_n z <_n w
        end.
      

      Definition node_reducel w (n : node X) :=
        match n with
          | Node2 _ x y => w >_n y >_n x
          | Node3 _ x y z => w >_n z >_n y >_n x
        end.
    End NodesReduce.

    Definition nodeReduce := mkReduce node_reducer node_reducel.

    Definition node_to_digit (A : Type) (n : node A) : digit A :=
      match n with
        | Node2 _ x y => Two x y
        | Node3 _ x y z => Three x y z
      end.
  End Nodes.

  Notation nodeMeasure := (@node_measure _).

  Section Measures.
    Variable A : Type.
    Variable measure : A -> v.

    Notation " 'lparr' x 'rparr' " := (measure x) (x ident, no associativity).

    Definition digit_measure : digit A -> v :=
      (digit_reducel (fun i a => i cdot lparr a rparr) epsilon).
  End Measures.

  Inductive fingertree (A : Type) : Type :=
  | Empty : fingertree A
  | Single : A -> fingertree A
  | Deep : v -> digit A -> fingertree (node A) -> digit A -> 
      fingertree A.

  Implicit Arguments Single [A].
  Implicit Arguments Empty [A].
  Implicit Arguments Deep [A].
  
  Definition tree_measure (A : Type) (measure : A -> v) (t : fingertree A) : v :=
    match t with
      | Empty => epsilon
      | Single x => measure x
      | Deep v _ _ _ => v
    end.

  Section SmartConstructors.
    Variables A : Type.
    Variable measure : A -> v.

    Definition deep pr m' sf := Deep ((digit_measure measure pr) cdot 
      (tree_measure nodeMeasure m') cdot (digit_measure measure sf))
      pr m' sf.

  End SmartConstructors.

  
  Section TreeReduce.
    
    Fixpoint tree_reducer (X Y : Type) (redr : X -> Y -> Y) (n : fingertree X) (w : Y) {struct n} : Y :=
      match n with
        | Empty => w
        | Single x => redr x w
        | Deep _ pr m sf => 
          let rd := reducer digitReduce redr in
          let rt := tree_reducer (reducer nodeReduce redr) in
            rd pr (rt m (rd sf w))
      end.

    Fixpoint tree_reducel (X Y : Type) (redl : Y -> X -> Y) (w : Y) (n : fingertree X) {struct n} : Y :=
      match n with
        | Empty => w
        | Single x => redl w x
        | Deep _ pr m sf => 
          let rd := reducel digitReduce redl in
          let rt := tree_reducel (reducel nodeReduce redl) in
            rd (rt (rd w pr) m) sf
      end.
  
    Definition treeReduce := mkReduce tree_reducer tree_reducel.

  End TreeReduce.

  Section add.
        
    Program Fixpoint add_left A (measure : A -> v) (a : A) (t : fingertree A) {struct t} : fingertree A :=
      match t with
        | Empty => Single a
        | Single b => deep measure (One a) Empty (One b)
        | Deep _ pr t' sf => 
          match pr with
            | Four b c d e => deep measure (Two a b) (add_left nodeMeasure (node3 measure c d e) t') sf
            | x => deep measure (add_digit_left a pr) t' sf
          end
      end.

    Next Obligation.
    Proof.
      intros.
      destruct pr ; simpl ; auto.
      elim H0 with a0 a1 a2 a3 ; eauto.
    Defined.

    Solve Obligations using red ; intros ; discriminate.

    Program Fixpoint add_right A (measure : A -> v) (t : fingertree A) (a : A) {struct t} : fingertree A :=
      match t with
        | Empty => Single a
        | Single b => deep measure (One b) Empty (One a)
        | Deep _ pr t' sf =>
          match sf with
            | Four b c d e => deep measure pr (add_right nodeMeasure t' (node3 measure b c d)) (Two e a)
            | _ => deep measure pr t' (add_digit_right sf a)
          end
      end.

    Next Obligation.
    Proof.
      intros.
      red ; intros.
      destruct sf ; simpl in * ; auto.
      apply H0 with a0 a1 a2 a3 ; eauto.
    Defined.
    
    Solve Obligations using red ; intros ; discriminate.

    Section add_reduce.
      Variable f : Type -> Type.
      Variable red : Reduce f.
      Variable A : Type.
      Variable measure : A -> v.

      Definition add_left_red := reducer red (@add_left A measure).
      Definition add_right_red := reducel red (@add_right A measure).

      Definition toTree s := add_left_red s Empty.

    End add_reduce.

  End add.

  Section view_L.
    Inductive View_L (s : Type -> Type) (a : Type) : Type := 
    | nil_L : View_L s a
    | cons_L : a -> s a -> View_L s a.
    
    Implicit Arguments nil_L [s a].
    Implicit Arguments cons_L [s a].

    Program Fixpoint view_L (A : Type) (measure : A -> v) (t : fingertree A) { struct t } : View_L fingertree A := 
      match t with
        | Empty => nil_L
        | Single x => cons_L x Empty
        | Deep _ pr t' sf => 
          match pr with
            | One x => match view_L nodeMeasure t' with
                         | nil_L => cons_L x (toTree digitReduce _ sf)
                         | cons_L a t' => cons_L x (deep measure (node_to_digit a) t' sf)
                       end
            | y => cons_L (digit_head y) (deep measure (digit_tail y) t' sf)
          end
      end.
    
    Next Obligation.
    Proof.
      intros.
      destruct pr ; simpl in * ; auto.
      red ; intros.
      apply H0 with a ; auto.
    Defined.

    Solve Obligations using red ; intros ; discriminate.

    Program Definition deep_L (A : Type) (measure : A -> v) (d : option (digit A)) (mid : fingertree (node A)) (sf : digit A) : fingertree A :=
      match d with
        | Some pr => deep measure pr mid sf
        | None =>  
          match view_L nodeMeasure mid with
            | nil_L => toTree digitReduce _ sf
            | cons_L a m' => deep measure (node_to_digit a) m' sf
          end
      end.
      
  End view_L.

  Section view_R.

    Inductive View_R (s : Type -> Type) (a : Type) : Type := 
    | nil_R : View_R s a
    | cons_R : s a -> a -> View_R s a.

    Implicit Arguments nil_R [s a].
    Implicit Arguments cons_R [s a].

    Program Fixpoint view_R (A : Type) (measure : A -> v) (t : fingertree A) { struct t } : View_R fingertree A := 
      match t with
        | Empty => nil_R
        | Single x => cons_R Empty x
        | Deep _ pr t' sf => 
          match sf with
            | One x => cons_R (match view_R nodeMeasure t' with
                                | nil_R => toTree digitReduce _ pr
                                | cons_R m' a => deep measure pr m' (node_to_digit a)
                              end) x
            | y => cons_R (deep measure pr t' (digit_liat y)) (digit_last y) 
          end
      end.

    Next Obligation.
    Proof.
      intros.
      destruct sf ; simpl in * ; auto. 
      elim H0 with a ; auto.
    Defined.

    Solve Obligations using red ; intros ; discriminate.

    Program Definition deep_R (A : Type) (measure : A -> v) (pr : digit A) (mid : fingertree (node A)) (sf : option (digit A)) : fingertree A :=
      match sf with
        | Some sf => deep measure pr mid sf
        | None =>  
          match view_R nodeMeasure mid with
            | nil_R => toTree digitReduce _ pr
            | cons_R mid' a => deep measure pr mid' (node_to_digit a)
          end
      end.
      
  End view_R.

  Section View.
    Variable A : Type.
    Variable measure : A -> v.
    Notation viewL := (view_L measure).

    Definition isEmpty t := match viewL t with
                              | nil_L => true
                              | cons_L _ _ => false
                            end.
    Require Import Coq.subtac.Utils.
  
    Program Definition head (t : fingertree A | isEmpty t = false) : A := 
      match viewL t with
        | cons_L hd _ => hd
        | nil_L => !
      end.

    Next Obligation.
    Proof.
      intros.
      destruct x ; unfold isEmpty in * ;  simpl in * ; try discriminate.
      destruct d ; simpl in * ; try discriminate.
      destruct (view_L nodeMeasure x) ; discriminate.
    Qed.
    
    Program Definition tail (t : fingertree A | isEmpty t = false) : fingertree A := 
      match viewL t with
        | cons_L _ tl => tl
        | nil_L => !
      end.

    Next Obligation.
    Proof.
      intros.
      destruct x ; unfold isEmpty in * ;  simpl in * ; try discriminate.
      destruct d ; simpl in * ; try discriminate.
      destruct (view_L nodeMeasure x) ; discriminate.
    Qed.

    Definition viewR := view_R measure.

    Program Definition last (t : fingertree A | isEmpty t = false) : A :=
      match viewR t with
        | cons_R _ x => x
        | nil_R => !
      end.

    Next Obligation.
    Proof.
      intros.
      destruct x ; unfold isEmpty in * ;  simpl in * ; try discriminate.
      destruct d0 ; simpl in * ; try discriminate.
    Qed.
    
    Program Definition liat (t : fingertree A | isEmpty t = false) : fingertree A := 
      match viewR t with
        | cons_R prev last => prev
        | nil_R => !
      end.

    Next Obligation.
    Proof.
      intros.
      destruct x ; unfold isEmpty in * ;  simpl in * ; try discriminate.
      destruct d0 ; simpl in * ; try discriminate.
    Qed.

  End View.

  Section CatList.
    (** Concatenation using lists *)
    Program Fixpoint nodes_right (A : Type) (measure : A -> v) (m : list A | m <> nil) (r : digit A) {measure length m} : list (node A) :=
      match m with
        | (cons x (cons y (cons z m'))) => node2 measure x y :: nodes_right (cons z m') r
        | (cons u (cons v nil)) =>
          match r with
            | One w => [node3 measure u v w]
            | Two w x => node2 measure u v :: [node2 measure w x]
            | Three w x y => node3 measure u v w :: [node2 measure x y]
            | Four w x y z => node3 measure u v w :: [node3 measure x y z]
          end
        | cons u nil =>
          match r with
            | One v => [node2 measure u v]
            | Two v w => [node3 measure u v w]
            | Three v w x => node2 measure u v :: [node2 measure w x]
            | Four v w x y => node3 measure u v w :: [node2 measure x y]
          end
        | nil => !
      end.

    Program Definition nodes (A : Type) (measure : A -> v) (l : digit A) (m : list A) (r : digit A) : list (node A) :=
      nodes_right measure (toList digitReduce _ l ++ m) r.

    Next Obligation.
    Proof.
      intros.
      induction l ; simpl ; red ; intros ; discriminate.
    Qed.          

    Fixpoint app3 (A : Type) (measure : A -> v) (xs : fingertree A) (ts : list A) (ys : fingertree A) {struct xs} : fingertree A :=
      match xs, ys with
        | Empty, ys => add_left_red listReduce measure ts ys
        | xs, Empty => add_right_red listReduce measure xs ts
        | Single x, ys => add_left measure x (add_left_red listReduce measure ts ys)
        | xs, Single y => add_right measure (add_right_red listReduce measure xs ts) y
        | Deep _ pr mid sf, Deep _ pr' mid' sf' => deep measure pr (app3 nodeMeasure mid (nodes measure sf ts pr') mid') sf'

      end.

    Definition concat (A : Type) (measure : A -> v) (x y : fingertree A) : fingertree A := 
      app3 measure x [] y.

  End CatList.
  
  Section Cat.
    (** Concatenation still using digits. *)
    Notation " x <_i y " := (add_right_red idReduce _ x y) (left associativity, at level 22).
    Notation " x >_i y " := (add_left_red idReduce _ x y) (right associativity, at level 30).

    Fixpoint appendTree0 (A : Type) (measure : A -> v) (xs ys : fingertree A) {struct xs} : fingertree A :=
      match xs, ys with
        | Empty, ys => ys
        | xs, Empty => xs
        | Single x, ys => add_left measure x ys
        | xs, Single y => add_right measure xs y
        | Deep _ pr mid sf, Deep _ pr' mid' sf' => 
          let f := 
            fun (A : Type) (measure : A -> v) (xs : fingertree (node A)) (dl : digit A) (dr : digit A) (ys : fingertree (node A)) =>
            match dl with
              | One a => 
                match dr with
                  | One b => appendTree1 nodeMeasure xs (node2 measure a b) ys
                  | Two b c => appendTree1 nodeMeasure xs (node3 measure a b c) ys
                  | Three b c d => appendTree2 nodeMeasure xs (node2 measure a b) (node2 measure c d) ys
                  | Four b c d e => appendTree2 nodeMeasure xs (node3 measure a b c) (node2 measure d e) ys
                end
              | Two a b =>
                match dr with
                  | One c => appendTree1 nodeMeasure xs (node3 measure a b c) ys
                  | Two c d => appendTree2 nodeMeasure xs (node2 measure a b) (node2 measure c d) ys
                  | Three c d e => appendTree2 nodeMeasure xs (node3 measure a b c) (node2 measure d e) ys
                  | Four c d e f => appendTree2 nodeMeasure xs (node3 measure a b c) (node3 measure d e f) ys
                end
              | Three a b c =>
                match dr with
                  | One d => appendTree2 nodeMeasure xs (node2 measure a b) (node2 measure c d) ys
                  | Two d e => appendTree2 nodeMeasure xs (node3 measure a b c) (node2 measure d e) ys
                  | Three d e f => appendTree2 nodeMeasure xs (node3 measure a b c) (node3 measure d e f) ys
                  | Four d e f g => appendTree3 nodeMeasure xs (node3 measure a b c) (node2 measure d e) (node2 measure f g) ys
                end
              | Four a b c d =>
                match dr with
                  | One e => appendTree2 nodeMeasure xs (node3 measure a b c) (node2 measure d e) ys
                  | Two e f => appendTree2 nodeMeasure xs (node3 measure a b c) (node3 measure d e f) ys
                  | Three e f g => appendTree3 nodeMeasure xs (node3 measure a b c) (node2 measure d e) (node2 measure f g) ys
                  | Four e f g h => appendTree3 nodeMeasure xs (node3 measure a b c) (node3 measure d e f) (node2 measure g h) ys
                end
            end
            in
            deep measure pr (f _ measure mid sf pr' mid') sf'
      end

    with appendTree1 (A : Type) (measure : A -> v) (xs : fingertree A) (d : A) (ys : fingertree A) {struct xs} : fingertree A :=
      let al x y := add_left measure x y in
      let ar x y := add_right measure x y in
      match xs, ys with
        | Empty, ys => al d ys
        | xs, Empty => ar xs d
        | Single x, ys => add_left measure x (al d ys)
        | xs, Single y => add_right measure (ar xs d) y
        | Deep _ pr mid sf, Deep _ pr' mid' sf' => 
          let addDigits1 := 
            fun (A : Type) (measure : A -> v) (xs : fingertree (node A)) (dl : digit A) (x : A) (dr : digit A) (ys : fingertree (node A)) =>
      match dl with
        | One a => 
          match dr with
            | One b => appendTree1 nodeMeasure xs (node3 measure a x b) ys
            | Two b c => appendTree2 nodeMeasure xs (node2 measure a x) (node2 measure b c) ys
            | Three b c d => appendTree2 nodeMeasure xs (node3 measure a x b) (node2 measure c d) ys
            | Four b c d e => appendTree2 nodeMeasure xs (node3 measure a x b) (node3 measure c d e) ys
          end
        | Two a b =>
          match dr with
            | One c => appendTree2 nodeMeasure xs (node2 measure a b) (node2 measure x c) ys
            | Two c d => appendTree2 nodeMeasure xs (node3 measure a b x) (node2 measure c d) ys
            | Three c d e => appendTree2 nodeMeasure xs (node3 measure a b x) (node3 measure c d e) ys
            | Four c d e f => appendTree3 nodeMeasure xs (node3 measure a b x) (node2 measure c d) (node2 measure e f) ys
          end
        | Three a b c =>
          match dr with
            | One d => appendTree2 nodeMeasure xs (node3 measure a b c) (node2 measure x d) ys
            | Two d e => appendTree2 nodeMeasure xs (node3 measure a b c) (node3 measure x d e) ys
            | Three d e f => appendTree3 nodeMeasure xs (node3 measure a b c) (node2 measure x d) (node2 measure e f) ys
            | Four d e f g => appendTree3 nodeMeasure xs (node3 measure a b c) (node3 measure x d e) (node2 measure f g) ys
          end
        | Four a b c d =>
          match dr with
            | One e => appendTree2 nodeMeasure xs (node3 measure a b c) (node3 measure d x e) ys
            | Two e f => appendTree3 nodeMeasure xs (node3 measure a b c) (node2 measure d x) (node2 measure e f) ys
            | Three e f g => appendTree3 nodeMeasure xs (node3 measure a b c) (node3 measure d x e) (node2 measure f g) ys
            | Four e f g h => appendTree3 nodeMeasure xs (node3 measure a b c) (node3 measure d x e) (node3 measure f g h) ys
          end
      end
      in deep measure pr (addDigits1 _ measure mid sf d pr' mid') sf'
      end
      
    with appendTree2 (A : Type) (measure : A -> v) (xs : fingertree A) (a b : A) (ys : fingertree A) {struct xs} : fingertree A :=
      let al x y := add_left measure x y in
      let ar x y := add_right measure x y in
      match xs, ys with
        | Empty, ys => al a (al b ys)
        | xs, Empty => ar (ar xs a) b
        | Single x, ys => add_left measure x (al a (al b ys))
        | xs, Single y => add_right measure (ar (ar xs a) b) y
        | Deep _ pr mid sf, Deep _ pr' mid' sf' => 
          let addDigits2 := fun (A : Type) (measure : A -> v) (xs : fingertree (node A)) (dl : digit A) (x y : A) (dr : digit A) (ys : fingertree (node A)) =>
      match dl with
        | One a => 
          match dr with
            | One b => appendTree2 nodeMeasure xs (node2 measure a x) (node2 measure y b) ys
            | Two b c => appendTree2 nodeMeasure xs (node3 measure a x y) (node2 measure b c) ys
            | Three b c d => appendTree2 nodeMeasure xs (node3 measure a x y) (node3 measure b c d) ys
            | Four b c d e => appendTree3 nodeMeasure xs (node3 measure a x y) (node2 measure b c) (node2 measure d e) ys
          end
        | Two a b =>
          match dr with
            | One c => appendTree2 nodeMeasure xs (node3 measure a b x) (node2 measure y c) ys
            | Two c d => appendTree2 nodeMeasure xs (node3 measure a b x) (node3 measure y c d) ys
            | Three c d e => appendTree3 nodeMeasure xs (node3 measure a b x) (node2 measure y c) (node2 measure d e) ys
            | Four c d e f => appendTree3 nodeMeasure xs (node3 measure a b x) (node3 measure y c d) (node2 measure e f) ys
          end
        | Three a b c =>
          match dr with
            | One d => appendTree2 nodeMeasure xs (node3 measure a b c) (node3 measure x y d) ys
            | Two d e => appendTree3 nodeMeasure xs (node3 measure a b c) (node2 measure x y) (node2 measure d e) ys
            | Three d e f => appendTree3 nodeMeasure xs (node3 measure a b c) (node3 measure x y d) (node2 measure e f) ys
            | Four d e f g => appendTree3 nodeMeasure xs (node3 measure a b c) (node3 measure x y d) (node3 measure e f g) ys
          end
        | Four a b c d =>
          match dr with
            | One e => appendTree3 nodeMeasure xs (node3 measure a b c) (node2 measure d x) (node2 measure y e) ys
            | Two e f => appendTree3 nodeMeasure xs (node3 measure a b c) (node3 measure d x y) (node2 measure e f) ys
            | Three e f g => appendTree3 nodeMeasure xs (node3 measure a b c) (node3 measure d x y) (node3 measure e f g) ys
            | Four e f g h => appendTree4 nodeMeasure xs (node3 measure a b c) (node3 measure d x y) (node2 measure e f) (node2 measure g h) ys
          end
      end
      in deep measure pr (addDigits2 _ measure mid sf a b pr' mid') sf'
      end


    with appendTree3 (A : Type) (measure : A -> v) (xs : fingertree A) (a b c : A) (ys : fingertree A) {struct xs} : fingertree A :=
      let al x y := add_left measure x y in
      let ar x y := add_right measure x y in
      match xs, ys with
        | Empty, ys => al a (al b (al c ys))
        | xs, Empty => ar (ar (ar xs a) b) c
        | Single x, ys => add_left measure x (al a (al b (al c ys)))
        | xs, Single y => add_right measure (ar (ar (ar xs a) b) c) y
        | Deep _ pr mid sf, Deep _ pr' mid' sf' =>
          let addDigits3 := fun (A : Type) (measure : A -> v) (xs : fingertree (node A)) (dl : digit A) (x y z : A) (dr : digit A) (ys : fingertree (node A)) =>
      match dl with
        | One a => 
          match dr with
            | One b => appendTree2 nodeMeasure xs (node3 measure a x y) (node2 measure z b) ys
            | Two b c => appendTree2 nodeMeasure xs (node3 measure a x y) (node3 measure z b c) ys
            | Three b c d => appendTree3 nodeMeasure xs (node3 measure a x y) (node2 measure z b) (node2 measure c d) ys
            | Four b c d e => appendTree3 nodeMeasure xs (node3 measure a x y) (node3 measure z b c) (node2 measure d e) ys
          end
        | Two a b =>
          match dr with
            | One c => appendTree2 nodeMeasure xs (node3 measure a b x) (node3 measure y z c) ys
            | Two c d => appendTree3 nodeMeasure xs (node3 measure a b x) (node2 measure y z) (node2 measure c d) ys
            | Three c d e => appendTree3 nodeMeasure xs (node3 measure a b x) (node3 measure y z c) (node2 measure d e) ys
            | Four c d e f => appendTree3 nodeMeasure xs (node3 measure a b x) (node3 measure y z c) (node3 measure d e f) ys
          end
        | Three a b c =>
          match dr with
            | One d => appendTree3 nodeMeasure xs (node3 measure a b c) (node2 measure x y) (node2 measure z d) ys
            | Two d e => appendTree3 nodeMeasure xs (node3 measure a b c) (node3 measure x y z) (node2 measure d e) ys
            | Three d e f => appendTree3 nodeMeasure xs (node3 measure a b c) (node3 measure x y z) (node3 measure d e f) ys
            | Four d e f g => appendTree4 nodeMeasure xs (node3 measure a b c) (node3 measure x y z) (node2 measure d e) (node2 measure f g) ys
          end
        | Four a b c d =>
          match dr with
            | One e => appendTree3 nodeMeasure xs (node3 measure a b c) (node3 measure d x y) (node2 measure z e) ys
            | Two e f => appendTree3 nodeMeasure xs (node3 measure a b c) (node3 measure d x y) (node3 measure z e f) ys
            | Three e f g => appendTree4 nodeMeasure xs (node3 measure a b c) (node3 measure d x y) (node2 measure z e) (node2 measure f g) ys
            | Four e f g h => appendTree4 nodeMeasure xs (node3 measure a b c) (node3 measure d x y) (node3 measure z e f) (node2 measure g h) ys
          end
      end
      in deep measure pr (addDigits3 _ measure mid sf a b c pr' mid') sf'
      end

    with appendTree4 (A : Type) (measure : A -> v) (xs : fingertree A) (a b c d : A) (ys : fingertree A) {struct xs} : fingertree A :=
      let al x y := add_left measure x y in
      let ar x y := add_right measure x y in
      match xs, ys with
        | Empty, ys => al a (al b (al c (al d ys)))
        | xs, Empty => ar (ar (ar (ar xs a) b) c) d 
        | Single x, ys => add_left measure x (al a (al b (al c (al d ys))))
        | xs, Single y => add_right measure (ar (ar (ar (ar xs a) b) c) d) y
        | Deep _ pr mid sf, Deep _ pr' mid' sf' =>
          let addDigits4 := fun (A : Type) (measure : A -> v) (xs : fingertree (node A)) (dl : digit A) (x y z w : A) (dr : digit A) (ys : fingertree (node A)) =>
      match dl with
        | One a => 
          match dr with
            | One b => appendTree2 nodeMeasure xs (node3 measure a x y) (node3 measure z w b) ys
            | Two b c => appendTree3 nodeMeasure xs (node3 measure a x y) (node2 measure z w) (node2 measure b c) ys
            | Three b c d => appendTree3 nodeMeasure xs (node3 measure a x y) (node3 measure z w b) (node2 measure c d) ys
            | Four b c d e => appendTree3 nodeMeasure xs (node3 measure a x y) (node3 measure z w b) (node3 measure c d e) ys
          end
        | Two a b =>
          match dr with
            | One c => appendTree3 nodeMeasure xs (node3 measure a b x) (node2 measure y z) (node2 measure w c) ys
            | Two c d => appendTree3 nodeMeasure xs (node3 measure a b x) (node3 measure y z w) (node2 measure c d) ys
            | Three c d e => appendTree3 nodeMeasure xs (node3 measure a b x) (node3 measure y z w) (node3 measure c d e) ys
            | Four c d e f => appendTree4 nodeMeasure xs (node3 measure a b x) (node3 measure y z w) (node2 measure c d) (node2 measure e f) ys
          end
        | Three a b c =>
          match dr with
            | One d => appendTree3 nodeMeasure xs (node3 measure a b c) (node3 measure x y z) (node2 measure w d) ys
            | Two d e => appendTree3 nodeMeasure xs (node3 measure a b c) (node3 measure x y z) (node3 measure w d e) ys
            | Three d e f => appendTree4 nodeMeasure xs (node3 measure a b c) (node3 measure x y z) (node2 measure w d) (node2 measure e f) ys
            | Four d e f g => appendTree4 nodeMeasure xs (node3 measure a b c) (node3 measure x y z) (node3 measure w d e) (node2 measure f g) ys
          end
        | Four a b c d =>
          match dr with
            | One e => appendTree3 nodeMeasure xs (node3 measure a b c) (node3 measure d x y) (node3 measure z w e) ys
            | Two e f => appendTree4 nodeMeasure xs (node3 measure a b c) (node3 measure d x y) (node2 measure z w) (node2 measure e f) ys
            | Three e f g => appendTree4 nodeMeasure xs (node3 measure a b c) (node3 measure d x y) (node3 measure z w e) (node2 measure f g) ys
            | Four e f g h => appendTree4 nodeMeasure xs (node3 measure a b c) (node3 measure d x y) (node3 measure z w e) (node3 measure f g h) ys
          end
      end in deep measure pr (addDigits4 _ measure mid sf a b c d pr' mid') sf'
      end.

    Definition app (A : Type) (measure : A -> v) (x y : fingertree A) : fingertree A := 
      appendTree0 measure x y.
  
  End Cat.
  
  Definition option_measure (A : Type) (measure : A -> v) (x : option A) := 
    match x with Some x => measure x | None => epsilon end.

  Section Split.
    Inductive split (f : Type -> Type) (a : Type) : Type := mkSplit : f a -> a -> f a -> split f a.

    Implicit Arguments mkSplit [f a].

    Ltac splitTac := 
      subtac_simpl ; myinjection ; intuition ; right ; unfold option_measure ; unfold digit_measure ; simpl ; 
        repeat rewrite monoid_id_l ; auto ; repeat rewrite <- monoid_assoc ; auto.

    Obligations Tactic := splitTac.

    Section Digits.
    Variable A : Type.
    Variable measure : A -> v.
    Notation " 'lparr' x 'rparr' " := (measure x) (x ident, no associativity).

    Definition digitToList (x : digit A) : list A := toList digitReduce _ x.
    Definition optionDigitToList (x : option (digit A)) : list A := match x with None => [] | Some x => digitToList x end.

    Program Definition splitDigit (p : v -> bool) (i : v) (d : digit A) : 
      { s : split (fun A => option (digit A)) A | forall l x r, s = mkSplit l x r ->
        digitToList d = optionDigitToList l ++ [x] ++ optionDigitToList r /\
        (l = None \/ p (i cdot (option_measure (digit_measure measure) l)) = false) /\
        (r = None \/ p (i cdot (option_measure (digit_measure measure) l) cdot (measure x)) = true) } :=
      match d with
        | One x => mkSplit None x None
        | Two x y => 
          let i' := i cdot lparr x rparr in
          lif p i' then mkSplit None x (Some (One y))
          else mkSplit (Some (One x)) y None
        | Three x y z =>
          let i' := i cdot lparr x rparr in
          let i'' := i' cdot lparr y rparr in
            lif p i' then
              mkSplit None x (Some (Two y z))
            else lif p i'' then
              mkSplit (Some (One x)) y (Some (One z))
            else 
              mkSplit (Some (Two x y)) z None
        | Four x y z w =>
          let i' := i cdot lparr x rparr in
            lif p i' then
              mkSplit None x (Some (Three y z w))
            else let i'' := i' cdot lparr y rparr in
              lif p i'' then
                mkSplit (Some (One x)) y (Some (Two z w))
              else let i''' := i'' cdot lparr z rparr in
                lif p i''' then
                  mkSplit (Some (Two x y)) z (Some (One w))
                else 
                  mkSplit (Some (Three x y z)) w None
      end.

    End Digits.
    
    Section Nodes.
    Variable A : Type.
    Variable measure : A -> v.
    Notation " 'lparr' x 'rparr' " := (measure x) (x ident, no associativity).
  
    Definition nodeToList := toList nodeReduce.

    Program Definition splitNode (p : v -> bool) (i : v) (n : node A) : 
      { s : split (fun A => option (digit A)) A | forall l x r, s = mkSplit l x r ->
        nodeToList n = optionDigitToList l ++ [x] ++ optionDigitToList r /\
        (l = None \/ p (i cdot (option_measure (digit_measure measure) l)) = false) /\
        (r = None \/ p (i cdot (option_measure (digit_measure measure) l) cdot (measure x)) = true) } :=
      match n with
        | Node2 _ x y => 
          let i' := i cdot lparr x rparr in
          lif p i' then mkSplit None x (Some (One y))
          else mkSplit (Some (One x)) y None
        | Node3 _ x y z =>
          let i' := i cdot lparr x rparr in
          let i'' := i' cdot lparr y rparr in
            lif p i' then
              mkSplit None x (Some (Two y z))
            else lif p i'' then
              mkSplit (Some (One x)) y (Some (One z))
            else 
              mkSplit (Some (Two x y)) z None
      end.

    End Nodes.

    Fixpoint fingertree_size (A : Type) (t : fingertree A) : nat :=
      match t with
        | Empty => 1
        | Single x => 1
        | Deep _ pr m sf => S (fingertree_size m)
      end.

    Definition extend A B (f : A -> option B) (ex : B) := fun x => match f x with Some y => y | None => ex end.
    Definition try_extend A B (f : A -> B) (x : option A) (def : B) := match x with Some y => f y | None => def end.

    Definition mappendVal (A : Type) (measure : A -> v) (x : v) (t : fingertree A) : v :=
      match t with Empty => x | t => x cdot (tree_measure measure t) end.

    Definition tree_to_list A := toList treeReduce A.

    Fixpoint nodeList_toList A (l : list (node A)) : list A :=
      match l with
        | Node2 _ x y :: tl => x :: y :: nodeList_toList tl
        | Node3 _ x y z :: tl => x :: y :: z :: nodeList_toList tl
        | [] => []
      end.
    Hint Unfold tree_reducer node_reducer digit_reducer : ft.
(*
    Section toListFacts.
      
      Section Simple.
      Variable A B : Type.
      Variable f : A -> list B -> list B.
      Variable hf : forall x l l', f x (l ++ l') = f x l ++ l'.
      
      Lemma digit_list : forall x l l', digit_reducer f x (l ++ l') = (digit_reducer f x l) ++ l'.
      Proof.
        induction x ; simpl ; intros ; repeat rewrite hf ; auto.
      Qed.

      Lemma node_list : forall x l l', node_reducer f x (l ++ l') = (node_reducer f x l) ++ l'.
      Proof.
        induction x ; simpl ; intros ; repeat rewrite hf ; auto.
      Qed.
      End Simple.

      Lemma tree_list : forall A B (f : B -> list A -> list A) (hf : forall x l l', f x (l ++ l') = f x l ++ l') x l l',
        tree_reducer f x (l ++ l') = tree_reducer f x l ++ l'.
      Proof.
        induction x ; simpl ; intros ; auto.
        repeat rewrite digit_list ; auto.
        rewrite (@IHx (node_reducer f)) ; auto.
        rewrite digit_list ; auto.
        intros.
        rewrite node_list ; auto.
      Qed.

      Lemma cons_H : forall (A : Type) (x : A) l l', cons x (l ++ l') = cons x l ++ l'.
      Proof.
        auto with datatypes.
      Qed.

      Lemma digit_reduce_app : forall A x l, digit_reducer (cons (A:=A)) x l = digit_reducer (cons (A:=A)) x [] ++ l.
      Proof.
        intros.
        pose (digit_list (cons (A:=A0)) (@cons_H A0)).
        apply (e x [] l).
      Qed.

      Lemma node_reduce_app : forall A x l, node_reducer (cons (A:=A)) x l = node_reducer (cons (A:=A)) x [] ++ l.
      Proof.
        intros.
        pose (node_list (cons (A:=A0)) (@cons_H A0)).
        apply (e x [] l).
      Qed.

      Lemma tree_reduce_app : forall A x l, tree_reducer (cons (A:=A)) x l = tree_reducer (cons (A:=A)) x [] ++ l.
      Proof.
        intros.
        pose (tree_list (cons (A:=A0)) (@cons_H A0)).
        apply (e x [] l).
      Qed.

      Lemma tree_reduce_node_app : forall A x l, tree_reducer (node_reducer (cons (A:=A))) x l = tree_reducer (node_reducer (cons (A:=A))) x [] ++ l.
      Proof.
        intros.
        assert(forall (A:Type) x l l', (node_reducer (cons (A:=A))) x (l ++ l') = (node_reducer (cons (A:=A))) x l ++ l').
        intros.
        rewrite node_list ; auto.
        apply (tree_list (node_reducer (cons (A:=A0))) (H A0) x [] l).
      Qed.

(*         Notation nodeList_toList := (@nodeList_toList _). *)

(*       Lemma tree_node_nodeList : forall A (f : forall B, B -> list B -> list B) (hf : forall A (x : A) l l', f A x (l ++ l') = f A x l ++ l')  *)
(*         m, *)
(*         tree_reducer (node_reducer (f A)) m [] = *)
(*         nodeList_toList # (tree_reducer (f (node A))) m []. *)
(*       Proof. *)
(*         intros. *)
(*         induction m0. *)
(*         unfold nodeList_toList. *)
(*         destruct m0. *)

      Definition digit_tail_option (A : Type) (d : digit A) :=
        match d with
          | One x => None
          | Two x y => Some (One y)
          | Three x y z => Some (Two y z)
          | Four x y z w => Some (Three y z w)
        end.

    Lemma toList_Deep : forall A (measure : v) r m sf, tree_to_list (Deep measure r m sf) = digitToList r ++ 
      tree_reducer (node_reducer (cons (A:=A))) m [] ++ digitToList sf.
    Proof.
      intros.
      induction_on_subterm (Deep measure0 r m0 sf) ; simpl ; intros ; try discriminate.
      unfold tree_to_list ; simpl.
      rewrite digit_reduce_app ; f_equal ; auto.
      rewrite tree_reduce_node_app ; f_equal ; auto.
    Qed.
    Check digit_measure.
    Check node_measure.
    Lemma view_L_Deep : forall (A : Type) v r m sf,
      view_L measure (Deep v r m sf) = cons_L _ (digit_head r) t' (* (deep_L measure (digit_tail_option r) m sf) *).
    Proof.
      intros.
      induction_on_subterm (deep measure0 r m0 sf).
      destruct r ; simpl ; auto ; try destruct (view_L nodeMeasure m0) ; eapply ex_intro ; simpl ; auto.
    Qed.

    Lemma toList_deep_L : forall A (measure : A -> v) r m sf, tree_to_list (deep_L measure r m sf) = optionDigitToList r ++ 
      tree_reducer (node_reducer (cons (A:=A))) m [] ++ digitToList sf.
    Proof.
      destruct r ; simpl ; intros ; auto.
      unfold deep.
      rewrite toList_Deep ; auto.
             
      destruct m0. 
      simpl ; auto ; try discriminate.
      destruct sf ; simpl in * ; auto ; try discriminate.
      simpl.
      unfold deep.
      rewrite toList_Deep.
      f_equal.
      destruct n ; simpl ; auto.
      
      
      destruct (view_L_Deep nodeMeasure d m0 d0 v0).
      rewrite H.
      unfold deep.
      rewrite toList_Deep.
      simpl.
      rewrite ass_app.
      f_equal.
      destruct d ; simpl ; auto.
      destruct n ; simpl ; auto.
      f_equal.
      f_equal.
      destruct m0 ; simpl ;auto.
      

      unfold view_L ; simpl.
      

      
      
      



      Check node_reducer.
      Lemma digit_node_commute : forall A (g : forall B, B -> list A -> list A)
        (d : digit (node A)), digit_reducer (node_reducer (g A)) d [] = digit_reducer (g (node A)) d [].
      Proof.
        induction d ; unfold node_reducer ; simpl ; auto.
        destruct a ; simpl ; auto.
        simpl.
      c
    

    Admitted.
    End toListFacts.

    Obligations Tactic := splitTac.

    Program Fixpoint splitTree' (A : Type) (measure : A -> v) (p : v -> bool) (i : v) (t : fingertree A) (pr : unit | ~ t = Empty)
      { struct t } : { s : split fingertree A | forall l x r, s = mkSplit l x r ->
        tree_to_list t = tree_to_list l ++ (x :: tree_to_list r) /\
        (l = Empty \/ p (i cdot (tree_measure measure l)) = false) /\
        (r = Empty \/ p (i cdot (tree_measure measure l) cdot (measure x)) = true) } :=
      match t with
        | Empty => !
        | Single x => mkSplit Empty x Empty
        | Deep _ pr mid sf =>
          let vpr := i cdot (digit_measure measure pr) in
            lif p vpr then
              match splitDigit measure p i pr with
                | mkSplit l x r => mkSplit (try_extend (toTree digitReduce measure) l Empty) x (deep_L measure r mid sf)
              end
            else
              let vpm := vpr cdot (treeNodeMeasure mid) in
                lif p vpm then
                  match @splitTree' _ nodeMeasure p vpr mid tt with
                    mkSplit ml x mr =>
                     match splitNode measure p (mappendVal nodeMeasure vpr ml) x with
                       | mkSplit l x r =>
                         mkSplit (deep_R measure pr ml l) x (deep_L measure r mr sf)
                     end
                  end
                else
                  let vsf := vpm cdot (digit_measure measure sf) in
                    match splitDigit measure p vpm sf with
                      | mkSplit l x r =>
                        mkSplit (deep_R measure pr mid l) x (try_extend (toTree digitReduce measure) r Empty)
                    end
      end.

    Lemma measure_com : forall A (measure : A -> v) l, option_measure (digit_measure measure) l = tree_measure measure (try_extend (toTree digitReduce measure) l Empty).
    Proof.
      intros.
      destruct l.
      destruct d ; simpl ; repeat rewrite monoid_id_l ; try rewrite monoid_id_r ; try rewrite monoid_assoc ; auto with datatypes.
      simpl ; auto.
    Qed.

    Lemma node_digit_reduce : forall (X Y : Type) (f : X -> Y -> Y) x y, node_reducer f x y = digit_reducer f (node_to_digit x) y.
    Proof.
      intros.
      induction x ; simpl ; intros ; auto.
    Qed.


    Scheme fingertree_dep := Induction for fingertree Sort Prop.

    Lemma tree_to_list_view : forall A t (measure : A -> v), 
      tree_to_list t = 
      (match view_L measure t with
         | nil_L => []
         | cons_L x t' => x :: tree_to_list t'
       end).
    Proof.
      induction t using fingertree_dep ; simpl ; intros ; auto.
      unfold tree_to_list ; simpl.
      destruct d ; simpl ; auto.
      generalize (IHt nodeMeasure).
      destruct (view_L nodeMeasure t) ; simpl ; auto.
      intros.
      cut (t = Empty) ; intros ; subst.
      simpl ; destruct d0 ; simpl ; auto.
      destruct t ; unfold tree_to_list in H ; simpl in H ; auto ; try discriminate.
      destruct d ; simpl in H ; discriminate.        
      rewrite <- node_digit_reduce.
      intros.
      unfold tree_to_list, toList, treeReduce in H ; simpl in H.
      f_equal.
      generalize (digit_reducer (cons (A:=A0)) d0 []) ; intros.
      rewrite node_reduce_app.
      rewrite tree_reduce_node_app.
      pattern (tree_reducer (node_reducer (cons (A:=A0))) f l).
      rewrite tree_reduce_node_app.
      rewrite ass_app.
      rewrite <- node_reduce_app.
      f_equal ; auto.
    Admitted.
    
    Obligations Tactic := idtac.
    
    Lemma optionDigitToList_reduce : forall A (measure : A -> v) (l : option (digit A)), 
      optionDigitToList l = tree_reducer (cons (A:=A)) (try_extend (toTree digitReduce measure) l Empty) [].
    Proof.
      induction l ; simpl ; auto.
      induction a ; simpl ; auto.
    Qed.
    
    Hint Resolve optionDigitToList_reduce : ft.

    Next Obligation.
    Proof.
      intros.
      split.
      subst.
      subtac_simpl.
      clear splitTree'.
      destruct (splitDigit measure0 p i pr0) ; subtac_simpl.
      destruct (a l x r) ; auto ; clear a.
      inversion H2 ; subst ; clear H2.
      clear H1.
      unfold tree_to_list at 1.
      simpl.
      unfold digitToList in H.
      simpl in H.
      rewrite digit_reduce_app.
      rewrite H.
      rewrite <- ass_app.
      unfold tree_to_list.
      simpl.
      f_equal ; f_equal ; auto with ft.
      rewrite 

      rewrite (optionDigitToList_reduce measure0 r).
      
      


      rewrite (tree_to_list_view (Deep wildcard pr0 mid sf) measure0).

      (* Destruct prefix *)
      destruct l ; simpl in H ; try discriminate ;
        unfold digitToList in H ; inversion H ; subst vpr ; subst.

      (* One *)
      simpl.
      unfold deep_L.
      destruct l ; try destruct d ; unfold optionDigitToList in H2 ; simpl in * ; try discriminate.
      destruct r ; try destruct d ; unfold optionDigitToList in H2 ; simpl in * ; try discriminate.
      inversion H2 ; subst.
      destruct (view_L nodeMeasure mid) ; simpl ; auto.
      destruct sf ; simpl ; auto.

      (* Two *)
      simpl.
      unfold deep_L.
      destruct l ; try destruct d ; unfold optionDigitToList in H2 ; simpl in * ; try discriminate.
      destruct r ; try destruct d ; unfold digitToList in H2 ; simpl in * |- ; try discriminate.
      inversion H2 ; subst.
      f_equal.
      unfold digit_tail ; simpl.
      unfold deep ; simpl.
      rewrite (tree_to_list_view (Deep
        ((epsilon cdot measure0 x0)
         cdot treeNodeMeasure mid cdot digit_measure measure0 sf) 
        (One x0) mid sf) measure0).
      destruct (view_L nodeMeasure mid) ; simpl ; auto.
      destruct (view_L nodeMeasure mid) ; simpl ; auto.
      destruct sf ; simpl ; auto.
      destruct sf ; simpl ; auto.
      


      unfold view_L at 1 ; simpl.

      unfold 

      
      (* Three *)
      inversion H4.
      subst.
      intuition ; try discriminate.

      (* Four *)
      inversion H4.
      subst.
      intuition ; try discriminate.

      (* p x not true in prefix *)
      subst vpr.
      destruct H2.
      subst.
      simpl in H.
      intuition.

      rewrite (tree_to_list_view (Deep wildcard pr0 mid sf) measure0).
      desrtuct (view_L emas
      

      subst.
      
    


    Admitted.

     
    Next Obligation.
    Proof.
      intros.
      subtac_simpl.
      red ; intros.
      subst vpm.
      subst mid.
      simpl in H1.
      rewrite (monoid_id_r) in H1.
      rewrite <- H1 in H0 ; discriminate.
    Defined.

    Next Obligation.
    Proof.
      intros.
      subtac_simpl.
      subst vpm vpr.
    Admitted.

    Next Obligation.
    Proof.
      intros.
    Admitted.

    Lemma splitTree : forall A (measure : A -> v) p i (t : fingertree A) H, 
      forall l x r, @splitTree' A measure p i t H = mkSplit l x r -> 
        (l = Empty \/ p (i cdot (tree_measure measure l)) = false) /\
        (r = Empty \/ p (i cdot (tree_measure measure l) cdot (measure x)) = true).
    Proof.
      induction t ; intros ; try discriminate.
      subtac_simpl ; elim n ; auto.
      simpl in H0 ; inversion H0 ; subst.
      intuition.

      simpl in H0.
      subtac_simpl.
      destruct (p (i cdot tree_measure measure l)).

      .
      pose (IHt nodeMeasure H l x r).
    
      


  End Split.

  Section Splits.
    Variable A : Type.
    Variable measure : A -> v.
    Variable p : v -> bool.

    Program Definition splitTree (t : fingertree A) : (fingertree A * fingertree A)%type :=
      match t with
        | Empty => (Empty, Empty)
        | x => 
          if p (tree_measure measure x) 
          then 
            let (l, x, r) := @splitTree' _ measure p epsilon t tt in
              (l, add_left measure x r)
          else (x, Empty)
      end.
        
    Definition takeUntil t := fst (splitTree t).
    Definition dropUntil t := snd (splitTree t).
*)        
  End Split.
End MeasuredFingerTree.