Tree indices

Tree_indices.v

Inductive Tree :=
  | Branch : forall {n}, Vector.t Tree n -> Tree.

Inductive TreeNode : Tree -> Type :=
  | Root : forall {t : Tree}, TreeNode t
  | InBranch : forall {n : nat} {xs : Vector.t Tree n}
      (i : Fin.t n), 
      TreeNode (Vector.nth xs i) -> TreeNode (Branch xs).

Lemma fin_dec : forall {n : nat} (x y : Fin.t n),
  {x = y} + {x <> y}.
Proof.
(* Can use a proof from my finite library *)
Admitted.

Definition subTreeNode {n} {xs : Vector.t _ n} (node : TreeNode (Branch xs)) 
  : option (sigT (fun i => TreeNode (Vector.nth xs i))) .
Proof. refine (
  match node in TreeNode t return match t with
  Branch _ xs' => option (sigT (fun i => TreeNode (Vector.nth xs' i))) 
  end with
  | Root t => _
  | InBranch _ _ i next =>
    Some (existT (fun i => TreeNode (Vector.nth _ i)) i next)
  end). destruct t. exact None.
Defined.

Lemma TN_dec_eq : forall {t : Tree} (x y : TreeNode t),
  {x = y} + {x <> y}.
Proof.
intros.
induction x. 
- induction y.
  + left; reflexivity.
  + right. unfold not. intros contra. inversion contra. 
- refine (
  (match y as y' in TreeNode t return (match t 
  return forall (y'' : TreeNode t), _ with
  Branch n' xs' => fun y'' : TreeNode (Branch xs') =>
    forall (i' : Fin.t n') (x' : TreeNode (Vector.nth xs' i'))
      (IHx' : forall y0, {x' = y0} + {x' <> y0}),
    {InBranch i' x' = y''} + {InBranch i' x' <> y''}
  end y')
  with
  | Root _ => _
  | InBranch _ _ _ _ => _
  end) i x IHx
  ). 
  + destruct t. intros. right. unfold not. intros contra. 
    inversion contra.
  + intros. destruct (fin_dec i0 i').
    * induction e. specialize (IHx' t). destruct IHx'.
      { left. induction e. reflexivity. }
      { right. unfold not. intros contra. apply n1.
        assert (subTreeNode (InBranch i0 x') = subTreeNode (InBranch i0 t)).
        rewrite contra. reflexivity.
        simpl in H. inversion H. 
        Require Import EqdepFacts.
        apply eq_sigT_iff_eq_dep in H1.
        apply Eqdep_dec.eq_dep_eq_dec in H1. assumption.
        apply fin_dec. }
   * right. unfold not. intros contra.
     apply n1.
     assert (subTreeNode (InBranch i' x') = subTreeNode (InBranch i0 t)).
     rewrite contra. reflexivity.
     simpl in H. inversion H. reflexivity.
Qed.