Set Warnings "-extraction-opaque-accessed,-extraction".
Set Warnings "-notation-overridden,-parsing".

Require Import mathcomp.ssreflect.ssreflect.
From mathcomp Require Import ssrfun ssrbool ssrnat eqtype.
Require Import ZArith.

(* Goal: @eq (list SplitPath) (@cons SplitPath (@cons SplitDirection s1 s2) l0) (@cons (list SplitDirection) (@nil SplitDirection) (@nil (list SplitDirection))) *)
(* Goal: @eq RandomSeed s (f (@nil SplitDirection)) *)
(* We axiomatize a random number generator
(* Goal: @eq (list SplitPath) (@cons SplitPath (@cons SplitDirection s1 s2) l0) (@cons (list SplitDirection) (@nil SplitDirection) (@nil (list SplitDirection))) *)
(* Goal: @eq RandomSeed s (f (@nil SplitDirection)) *)
   (currently written in OCaml only) *)
Axiom RandomSeed : Type.
Axiom randomSeed_inhabited : inhabited RandomSeed.

(* Goal: @eq (list SplitPath) (@cons SplitPath s0 l0) (@cons (list SplitDirection) (@nil SplitDirection) (@nil (list SplitDirection))) *)
(* Goal: @eq RandomSeed s (f (@nil SplitDirection)) *)
Axiom randomNext     : RandomSeed -> Z * RandomSeed.
Axiom randomGenRange : RandomSeed -> Z * Z.
(* Goal: @eq (list SplitPath) (@cons SplitPath s0 l0) (@cons (list SplitDirection) (@nil SplitDirection) (@nil (list SplitDirection))) *)
(* Goal: @eq RandomSeed s (f (@nil SplitDirection)) *)
Axiom mkRandomSeed   : Z          -> RandomSeed.
Axiom newRandomSeed  : RandomSeed.

(* Goal: @eq (list SplitPath) (@cons SplitPath (@cons SplitDirection s1 s2) l0) (@cons (list SplitDirection) (@nil SplitDirection) (@nil (list SplitDirection))) *)
(* Goal: @eq RandomSeed s (f (@nil SplitDirection)) *)
(* begin randomSplitAssumption *)
Axiom randomSplit : RandomSeed -> RandomSeed * RandomSeed.
Axiom randomSplitAssumption :
  forall s1 s2 : RandomSeed, exists s, randomSplit s = (s1,s2).
(* Goal: @eq (list SplitPath) (@cons SplitPath (@cons SplitDirection s1 s2) l0) (@cons (list SplitDirection) (@nil SplitDirection) (@nil (list SplitDirection))) *)
(* Goal: @eq RandomSeed s (f (@nil SplitDirection)) *)
(* end randomSplitAssumption *)

CoInductive RandomSeedTree :=
(* Goal: @eq (list SplitPath) (@cons SplitPath s0 l0) (@cons (list SplitDirection) (@nil SplitDirection) (@nil (list SplitDirection))) *)
(* Goal: @eq RandomSeed s (f (@nil SplitDirection)) *)
| RstNode : RandomSeed -> RandomSeedTree -> RandomSeedTree -> RandomSeedTree.

Definition root_rst (rst : RandomSeedTree) : RandomSeed :=
  match rst with
  | RstNode root _ _ => root
  end.

Definition left_rst (rst : RandomSeedTree) : RandomSeedTree :=
  match rst with
  | RstNode _ t1 _ => t1
  end.

Definition right_rst (rst : RandomSeedTree) : RandomSeedTree :=
  match rst with
  | RstNode _ _ t2 => t2
  end.

Lemma rst_eta : forall rst : RandomSeedTree,
  rst = RstNode (root_rst rst) (left_rst rst) (right_rst rst).
(* Goal: forall rst : RandomSeedTree, @eq RandomSeedTree rst (RstNode (root_rst rst) (left_rst rst) (right_rst rst)) *)
Proof. destruct rst. reflexivity. Qed.

CoFixpoint mkSeedTree (s : RandomSeed) : RandomSeedTree :=
  let (s1, s2) := randomSplit s in
  RstNode s (mkSeedTree s1) (mkSeedTree s2).

Lemma mkSeedTreeHelper r :
  mkSeedTree r = RstNode r (mkSeedTree (randomSplit r).1) (mkSeedTree (randomSplit r).2).
Proof. by rewrite [mkSeedTree _]rst_eta /=; case: (randomSplit r). Qed.

Inductive SplitDirection := Left | Right.

Definition SplitPath := list SplitDirection.

Require Import List. Import ListNotations.
Fixpoint varySeedAux (p : SplitPath) (rst : RandomSeedTree) : RandomSeed :=
  let '(RstNode s t1 t2) := rst in
  match p with
    | [] => s
    | Left  :: p' => varySeedAux p' t1
    | Right :: p' => varySeedAux p' t2
  end.

Definition varySeed (p : SplitPath) (s : RandomSeed) : RandomSeed :=
  varySeedAux p (mkSeedTree s).

Inductive SeedTree :=
| SeedTreeUndef : SeedTree
(* Goal: @eq (list SplitPath) (@cons SplitPath s0 l0) (@cons (list SplitDirection) (@nil SplitDirection) (@nil (list SplitDirection))) *)
(* Goal: @eq RandomSeed s (f (@nil SplitDirection)) *)
| SeedTreeLeaf : RandomSeed -> SeedTree
(* Goal: @eq (list SplitPath) (@cons SplitPath s0 l0) (@cons (list SplitDirection) (@nil SplitDirection) (@nil (list SplitDirection))) *)
(* Goal: @eq RandomSeed s (f (@nil SplitDirection)) *)
| SeedTreeNode : SeedTree -> SeedTree -> SeedTree.

(* Goal: @eq (list SplitPath) (@cons SplitPath s0 l0) (@cons (list SplitDirection) (@nil SplitDirection) (@nil (list SplitDirection))) *)
(* Goal: @eq RandomSeed s (f (@nil SplitDirection)) *)
Inductive SubSeedTree : SeedTree -> RandomSeedTree -> Prop :=
| SubUndef : forall (rst : RandomSeedTree), SubSeedTree SeedTreeUndef rst
| SubLeaf  : forall (s : RandomSeed) (rst1 rst2 : RandomSeedTree),
               SubSeedTree (SeedTreeLeaf s) (RstNode s rst1 rst2)
| SubNode  : forall (st1 st2 : SeedTree) (rst1 rst2 : RandomSeedTree) (s : RandomSeed),
(* Goal: @eq (list SplitPath) (@cons SplitPath s0 l0) (@cons (list SplitDirection) (@nil SplitDirection) (@nil (list SplitDirection))) *)
(* Goal: @eq RandomSeed s (f (@nil SplitDirection)) *)
               SubSeedTree st1 rst1 ->
(* Goal: @eq (list SplitPath) (@cons SplitPath s0 l0) (@cons (list SplitDirection) (@nil SplitDirection) (@nil (list SplitDirection))) *)
(* Goal: @eq RandomSeed s (f (@nil SplitDirection)) *)
               SubSeedTree st2 rst2 ->
               SubSeedTree (SeedTreeNode st1 st2) (RstNode s rst1 rst2).

Fixpoint varySeed' (st : SeedTree) (p : SplitPath) : option RandomSeed :=
  match st with
    | SeedTreeUndef => None
    | SeedTreeLeaf s =>
      match p with
        | [] => Some s
        | _  => None
      end
    | SeedTreeNode st1 st2 =>
      match p with
        | [] => None
        | Left  :: p' => varySeed' st1 p'
        | Right :: p' => varySeed' st2 p'
      end
  end.

Lemma pathAgreesOnSubTree : forall (st : SeedTree) (rst : RandomSeedTree) (p : SplitPath)
                                   (s : RandomSeed),
(* Goal: @eq (list SplitPath) (@cons SplitPath s0 l0) (@cons (list SplitDirection) (@nil SplitDirection) (@nil (list SplitDirection))) *)
(* Goal: @eq RandomSeed s (f (@nil SplitDirection)) *)
                              SubSeedTree st rst ->
(* Goal: @eq (list SplitPath) (@cons SplitPath s0 l0) (@cons (list SplitDirection) (@nil SplitDirection) (@nil (list SplitDirection))) *)
(* Goal: @eq RandomSeed s (f (@nil SplitDirection)) *)
                              varySeed' st p = Some s ->
                              varySeedAux p rst = s.
Proof.
(* Goal: forall (st : SeedTree) (rst : RandomSeedTree) (p : SplitPath) (s : RandomSeed) (_ : SubSeedTree st rst) (_ : @eq (option RandomSeed) (varySeed' st p) (@Some RandomSeed s)), @eq RandomSeed (varySeedAux p rst) s *)
induction st.
(* Goal: @sig SeedTree (fun s : SeedTree => correspondingSeedTree (@cons SplitPath a l) f s) *)
+ intros. simpl in H0. congruence.
(* Goal: @sig SeedTree (fun s : SeedTree => correspondingSeedTree (@cons SplitPath a l) f s) *)
+ intros. simpl in H0.
(* Goal: @eq RandomSeed (varySeedAux p rst) s *)
  destruct p eqn:P.
(* Goal: @eq RandomSeed s s *)
(* Goal: @eq RandomSeed (varySeedAux (@cons SplitDirection s0 s1) rst) s *)
(* Goal: forall (rst : RandomSeedTree) (p : SplitPath) (s : RandomSeed) (_ : SubSeedTree (SeedTreeNode st1 st2) rst) (_ : @eq (option RandomSeed) (varySeed' (SeedTreeNode st1 st2) p) (@Some RandomSeed s)), @eq RandomSeed (varySeedAux p rst) s *)
  - inversion H. simpl. inversion H0. reflexivity.
(* Goal: @eq (list SplitPath) (@cons SplitPath s0 l0) (@cons (list SplitDirection) (@nil SplitDirection) (@nil (list SplitDirection))) *)
(* Goal: @eq RandomSeed s (f (@nil SplitDirection)) *)
  - inversion H0.
(* Goal: @sig SeedTree (fun s : SeedTree => correspondingSeedTree (@cons SplitPath a l) f s) *)
+ intros. simpl in H0.
(* Goal: @eq RandomSeed (varySeedAux p rst) s *)
  destruct p eqn:P.
(* Goal: @eq (list SplitPath) (@cons SplitPath s0 l0) (@cons (list SplitDirection) (@nil SplitDirection) (@nil (list SplitDirection))) *)
(* Goal: @eq RandomSeed s (f (@nil SplitDirection)) *)
  - inversion H0.
(* Goal: @eq (list SplitPath) (@cons SplitPath s0 l0) (@cons (list SplitDirection) (@nil SplitDirection) (@nil (list SplitDirection))) *)
(* Goal: @eq RandomSeed s (f (@nil SplitDirection)) *)
  - inversion H; subst.
(* Goal: @eq (list SplitPath) (@cons SplitPath s0 l0) (@cons (list SplitDirection) (@nil SplitDirection) (@nil (list SplitDirection))) *)
(* Goal: @eq RandomSeed s (f (@nil SplitDirection)) *)
    destruct s0 eqn:S0.
(* Goal: @eq RandomSeed (varySeedAux (@cons SplitDirection Right s1) (RstNode s2 rst1 rst2)) s *)
    * simpl. apply IHst1; auto.
(* Goal: @eq RandomSeed (varySeedAux (@cons SplitDirection Right s1) (RstNode s2 rst1 rst2)) s *)
    * simpl. apply IHst2; auto.
Qed.

Lemma splitExpand st : exists s, SubSeedTree st (mkSeedTree s).
Proof.
(* Goal: @ex RandomSeed (fun s : RandomSeed => SubSeedTree st (mkSeedTree s)) *)
elim: st => [|r|st1 [s1 st_s1] st2 [s2 st_s2]].
(* Goal: @sig SeedTree (fun s : SeedTree => correspondingSeedTree (@cons SplitPath a l) f s) *)
+ by case: randomSeed_inhabited=> seed; exists seed; apply: SubUndef.
(* Goal: @sig SeedTree (fun s : SeedTree => correspondingSeedTree (@cons SplitPath a l) f s) *)
+ by exists r; rewrite mkSeedTreeHelper; constructor.
(* Goal: @ex RandomSeed (fun s : RandomSeed => SubSeedTree (SeedTreeNode st1 st2) (mkSeedTree s)) *)
have [s eq_s] := randomSplitAssumption s1 s2.
(* Goal: @antisymmetric bool (fun b1 b2 : bool => implb b1 b2) *)
by exists s; rewrite mkSeedTreeHelper eq_s; constructor.
Qed.

(* Goal: @eq (list SplitPath) (@cons SplitPath s0 l0) (@cons (list SplitDirection) (@nil SplitDirection) (@nil (list SplitDirection))) *)
(* Goal: @eq RandomSeed s (f (@nil SplitDirection)) *)
Inductive PrefixFree : list SplitPath -> Prop :=
| FreeNil : PrefixFree []
| FreeCons : forall (p : SplitPath) (l : list SplitPath),
(* Goal: @eq (list SplitPath) (@cons SplitPath s0 l0) (@cons (list SplitDirection) (@nil SplitDirection) (@nil (list SplitDirection))) *)
(* Goal: @eq RandomSeed s (f (@nil SplitDirection)) *)
               PrefixFree l ->
(* Goal: @eq (list SplitPath) (@cons SplitPath s0 l0) (@cons (list SplitDirection) (@nil SplitDirection) (@nil (list SplitDirection))) *)
(* Goal: @eq RandomSeed s (f (@nil SplitDirection)) *)
               (forall (p' : SplitPath), In p' l ->
(* Goal: @sig SeedTree (fun s : SeedTree => correspondingSeedTree (@cons SplitPath a l) f s) *)
                                        (forall p1 p2, p' ++ p1 = p ++ p2-> False)) ->
                                        PrefixFree (p :: l).

Lemma prefixFreeSingleton : forall p, PrefixFree [p].
(* Goal: forall p : SplitPath, PrefixFree (@cons SplitPath p (@nil SplitPath)) *)
intro.
(* Goal: PrefixFree (@cons SplitPath p (@nil SplitPath)) *)
apply FreeCons.
(* Goal: @sig SeedTree (fun s : SeedTree => correspondingSeedTree (@cons SplitPath a l) f s) *)
+ apply FreeNil.
(* Goal: @sig SeedTree (fun s : SeedTree => correspondingSeedTree (@cons SplitPath a l) f s) *)
+ intros. inversion H.
Qed.

(* Goal: @eq (list SplitPath) (@cons SplitPath s0 l0) (@cons (list SplitDirection) (@nil SplitDirection) (@nil (list SplitDirection))) *)
(* Goal: @eq RandomSeed s (f (@nil SplitDirection)) *)
Lemma prefixFreeEmpty : forall l, PrefixFree ([] :: l) -> l = [].
(* Goal: forall (_ : N.le x y) (_ : N.le y x), @eq N x y *)
intros.
destruct l; auto.
(* Goal: PrefixFree l *)
inversion H.
(* Goal: @In (list SplitDirection) (@cons SplitDirection d p) l *)
subst.
pose proof H3 l.
assert (In l (l :: l0)) by (left; auto).
eapply H0 in H1. inversion H1.
instantiate (2 := []). rewrite app_nil_r; simpl; eauto.
Qed.

(* Goal: @eq (list SplitPath) (@cons SplitPath s0 l0) (@cons (list SplitDirection) (@nil SplitDirection) (@nil (list SplitDirection))) *)
(* Goal: @eq RandomSeed s (f (@nil SplitDirection)) *)
Inductive correspondingSeedTree (l : list SplitPath) (f : SplitPath -> RandomSeed)
          (st : SeedTree) : Prop :=
(* Goal: @eq (list SplitPath) (@cons SplitPath s0 l0) (@cons (list SplitDirection) (@nil SplitDirection) (@nil (list SplitDirection))) *)
(* Goal: @eq RandomSeed s (f (@nil SplitDirection)) *)
| Corresponding : (forall (p : SplitPath) s, varySeed' st p = Some s -> In p l) ->
(* Goal: @eq (list SplitPath) (@cons SplitPath s0 l0) (@cons (list SplitDirection) (@nil SplitDirection) (@nil (list SplitDirection))) *)
(* Goal: @eq RandomSeed s (f (@nil SplitDirection)) *)
                  (forall (p : SplitPath), In p l -> varySeed' st p = Some (f p)) ->
(* Goal: @eq (list SplitPath) (@cons SplitPath s0 l0) (@cons (list SplitDirection) (@nil SplitDirection) (@nil (list SplitDirection))) *)
(* Goal: @eq RandomSeed s (f (@nil SplitDirection)) *)
                  PrefixFree l ->
                  correspondingSeedTree l f st.

Lemma corrEmptyUndef : forall f, correspondingSeedTree [] f SeedTreeUndef.
(* Goal: forall f : forall _ : SplitPath, RandomSeed, correspondingSeedTree (@nil SplitPath) f SeedTreeUndef *)
  intro f.
(* Goal: correspondingSeedTree (@nil SplitPath) f SeedTreeUndef *)
  apply Corresponding.
(* Goal: @sig SeedTree (fun s : SeedTree => correspondingSeedTree (@cons SplitPath a l) f s) *)
  + intros p s Contra.
(* Goal: @In SplitPath p (@nil SplitPath) *)
(* Goal: forall (p : SplitPath) (_ : @In SplitPath p (@nil SplitPath)), @eq (option RandomSeed) (varySeed' SeedTreeUndef p) (@Some RandomSeed (f p)) *)
(* Goal: PrefixFree (@nil SplitPath) *)
    inversion Contra.
(* Goal: @sig SeedTree (fun s : SeedTree => correspondingSeedTree (@cons SplitPath a l) f s) *)
  + intros p InNil. inversion InNil.
(* Goal: @sig SeedTree (fun s : SeedTree => correspondingSeedTree (@cons SplitPath a l) f s) *)
  + apply FreeNil.
Qed.

Ltac fireInLeft name :=
  match goal with
(* Goal: @eq (list SplitPath) (@cons SplitPath s0 l0) (@cons (list SplitDirection) (@nil SplitDirection) (@nil (list SplitDirection))) *)
(* Goal: @eq RandomSeed s (f (@nil SplitDirection)) *)
    | [H : In ?X (?X :: ?XS) -> _ |- _ ] =>
      assert (In X (X :: XS)) as name by (left; auto); apply H in name; clear H
  end.

(* Goal: @eq (list SplitPath) (@cons SplitPath s0 l0) (@cons (list SplitDirection) (@nil SplitDirection) (@nil (list SplitDirection))) *)
(* Goal: @eq RandomSeed s (f (@nil SplitDirection)) *)
Lemma corrUndefEmpty : forall l f, correspondingSeedTree l f SeedTreeUndef -> l = [].
(* Goal: forall (l : list SplitPath) (f : forall _ : SplitPath, RandomSeed) (_ : correspondingSeedTree l f SeedTreeUndef), @eq (list SplitPath) l (@nil SplitPath) *)
intros l f Corr.
(* Goal: and (@eq (list SplitPath) l (@cons (list SplitDirection) (@nil SplitDirection) (@nil (list SplitDirection)))) (@eq RandomSeed s (f (@nil SplitDirection))) *)
inversion Corr as [Vary_In In_Vary Pref]; clear Corr.
(* Goal: @eq (list SplitPath) l (@nil SplitPath) *)
destruct l as [ | p ps]; auto.
(* Goal: @eq (list SplitPath) (@cons SplitPath p ps) (@nil SplitPath) *)
clear Vary_In Pref.
(* Goal: @eq (list SplitPath) (@cons SplitPath p ps) (@nil SplitPath) *)
pose proof (In_Vary p) as Contra; clear In_Vary.
(* Goal: @eq (list SplitPath) (@cons SplitPath p ps) (@nil SplitPath) *)
fireInLeft Hyp.
(* Goal: @eq (list SplitPath) (@cons SplitPath p ps) (@nil SplitPath) *)
inversion Hyp.
Qed.

(* Goal: @eq (list SplitPath) (@cons SplitPath s0 l0) (@cons (list SplitDirection) (@nil SplitDirection) (@nil (list SplitDirection))) *)
(* Goal: @eq RandomSeed s (f (@nil SplitDirection)) *)
Lemma PrefixFreeWithNil : forall l, PrefixFree ([] :: l) -> l = [].
(* Goal: forall (_ : N.le x y) (_ : N.le y x), @eq N x y *)
  intros.
(* Goal: @eq RandomSeed (varySeedAux (@cons SplitDirection s0 s1) rst) s *)
  inversion H; subst.
  destruct l eqn:L; auto.
  pose proof (H3 l0).
  assert (In l0 (l0 :: l1)) by (left; auto).
  eapply H0 in H1.
(* Goal: @sig SeedTree (fun s : SeedTree => correspondingSeedTree (@cons SplitPath a l) f s) *)
  + inversion H1.
(* Goal: @sig SeedTree (fun s : SeedTree => correspondingSeedTree (@cons SplitPath a l) f s) *)
  + instantiate (1 := l0). instantiate (1 := []). rewrite app_nil_r. auto.
Qed.

(* Goal: @eq (list SplitPath) (@cons SplitPath s0 l0) (@cons (list SplitDirection) (@nil SplitDirection) (@nil (list SplitDirection))) *)
(* Goal: @eq RandomSeed s (f (@nil SplitDirection)) *)
Lemma corrEmptyLeaf : forall s l f, correspondingSeedTree l f (SeedTreeLeaf s) ->
                                    l = [[]] /\ s = f [].
(* Goal: forall (s : RandomSeed) (l : list SplitPath) (f : forall _ : SplitPath, RandomSeed) (_ : correspondingSeedTree l f (SeedTreeLeaf s)), and (@eq (list SplitPath) l (@cons (list SplitDirection) (@nil SplitDirection) (@nil (list SplitDirection)))) (@eq RandomSeed s (f (@nil SplitDirection))) *)
  intros s l f Corr.
(* Goal: and (@eq (list SplitPath) l (@cons (list SplitDirection) (@nil SplitDirection) (@nil (list SplitDirection)))) (@eq RandomSeed s (f (@nil SplitDirection))) *)
  inversion Corr as [Vary_In In_Vary Pref]; clear Corr.
(* Goal: and (@eq (list SplitPath) l (@cons (list SplitDirection) (@nil SplitDirection) (@nil (list SplitDirection)))) (@eq RandomSeed s (f (@nil SplitDirection))) *)
  pose proof (Vary_In [] s) as Hyp; clear Vary_In.
(* Goal: and (@eq (list SplitPath) l (@cons (list SplitDirection) (@nil SplitDirection) (@nil (list SplitDirection)))) (@eq RandomSeed s (f (@nil SplitDirection))) *)
  simpl in Hyp.
(* Goal: and (@eq (list SplitPath) l (@cons (list SplitDirection) (@nil SplitDirection) (@nil (list SplitDirection)))) (@eq RandomSeed s (f (@nil SplitDirection))) *)
  assert (InNilL : In [] l) by (apply Hyp; auto); clear Hyp.
(* Goal: and (@eq (list SplitPath) l (@cons (list SplitDirection) (@nil SplitDirection) (@nil (list SplitDirection)))) (@eq RandomSeed s (f (@nil SplitDirection))) *)
  split.
(* Goal: @sig SeedTree (fun s : SeedTree => correspondingSeedTree (@cons SplitPath a l) f s) *)
  + destruct l eqn:L.
(* Goal: @eq (list SplitPath) (@cons SplitPath s0 l0) (@cons (list SplitDirection) (@nil SplitDirection) (@nil (list SplitDirection))) *)
(* Goal: @eq RandomSeed s (f (@nil SplitDirection)) *)
    - inversion InNilL.
(* Goal: @eq (list SplitPath) (@cons SplitPath s0 l0) (@cons (list SplitDirection) (@nil SplitDirection) (@nil (list SplitDirection))) *)
(* Goal: @eq RandomSeed s (f (@nil SplitDirection)) *)
    - destruct s0 eqn : S0.
(* Goal: @eq (list SplitPath) (@cons SplitPath (@cons SplitDirection s1 s2) l0) (@cons (list SplitDirection) (@nil SplitDirection) (@nil (list SplitDirection))) *)
(* Goal: @eq RandomSeed s (f (@nil SplitDirection)) *)
      * apply PrefixFreeWithNil in Pref; subst; auto.
(* Goal: @eq (list SplitPath) (@cons SplitPath (@cons SplitDirection s1 s2) l0) (@cons (list SplitDirection) (@nil SplitDirection) (@nil (list SplitDirection))) *)
(* Goal: @eq RandomSeed s (f (@nil SplitDirection)) *)
      * pose proof (In_Vary (s1 :: s2)) as Hyp; clear In_Vary.

(* Goal: @sig SeedTree (fun s : SeedTree => correspondingSeedTree (@cons SplitPath a l) f s) *)
  + inversion Pref.
(* Goal: @eq (list SplitPath) (@cons SplitPath (@cons SplitDirection s1 s2) l0) (@cons (list SplitDirection) (@nil SplitDirection) (@nil (list SplitDirection))) *)
(* Goal: @eq RandomSeed s (f (@nil SplitDirection)) *)
    fireInLeft Hyp'. simpl in Hyp'. inversion Hyp'.

(* Goal: @sig SeedTree (fun s : SeedTree => correspondingSeedTree (@cons SplitPath a l) f s) *)
  + pose proof In_Vary [] as Hyp; clear In_Vary.
(* Goal: @eq RandomSeed s (f (@nil SplitDirection)) *)
    apply Hyp in InNilL; clear Hyp.
(* Goal: @eq (list SplitPath) (@cons SplitPath (@cons SplitDirection s1 s2) l0) (@cons (list SplitDirection) (@nil SplitDirection) (@nil (list SplitDirection))) *)
(* Goal: @eq RandomSeed s (f (@nil SplitDirection)) *)
    simpl in *.
(* Goal: @eq RandomSeed s (f (@nil SplitDirection)) *)
    congruence.
Qed.

Lemma corrNodeNonEmpty : forall st1 st2 l p f,
(* Goal: @eq (list SplitPath) (@cons SplitPath s0 l0) (@cons (list SplitDirection) (@nil SplitDirection) (@nil (list SplitDirection))) *)
(* Goal: @eq RandomSeed s (f (@nil SplitDirection)) *)
                           correspondingSeedTree l f (SeedTreeNode st1 st2) ->
(* Goal: @eq (list SplitPath) (@cons SplitPath s0 l0) (@cons (list SplitDirection) (@nil SplitDirection) (@nil (list SplitDirection))) *)
(* Goal: @eq RandomSeed s (f (@nil SplitDirection)) *)
                           In p l -> p <> [].
(* Goal: @In (list SplitDirection) (@cons SplitDirection d p) l *)
unfold not; intros st1 st2 l p f Corr InPL PNil; subst.
(* Goal: @eq (option RandomSeed) (varySeed' st2 p) (@Some RandomSeed (refineFunction f Right p)) *)
(* Goal: PrefixFree (refineList Right l) *)
inversion Corr as [_ In_Vary _]; clear Corr.
(* Goal: False *)
pose proof (In_Vary []) as Hyp; clear In_Vary.
(* Goal: False *)
apply Hyp in InPL; clear Hyp.
(* Goal: False *)
simpl in InPL.
(* Goal: False *)
inversion InPL.
Qed.

Hint Resolve corrEmptyUndef.
Hint Resolve corrNodeNonEmpty.
Definition Direction_eq_dec : forall (d1 d2 : SplitDirection),
(* Goal: @sig SeedTree (fun s : SeedTree => correspondingSeedTree (@cons SplitPath a l) f s) *)
                                {d1 = d2} + {d1 <> d2}.
(* Goal: forall d1 d2 : SplitDirection, sumbool (@eq SplitDirection d1 d2) (not (@eq SplitDirection d1 d2)) *)
decide equality.
Qed.

Definition eq_dir_b (d1 d2 : SplitDirection) : bool :=
  match d1,d2 with
    | Left, Left => true
    | Right, Right => true
    | _, _ => false
  end.

(* Goal: @eq (list SplitPath) (@cons SplitPath s0 l0) (@cons (list SplitDirection) (@nil SplitDirection) (@nil (list SplitDirection))) *)
(* Goal: @eq RandomSeed s (f (@nil SplitDirection)) *)
Lemma eq_dir_b_eq : forall d1 d2, eq_dir_b d1 d2 = true <-> d1 = d2.
(* Goal: forall (_ : N.le x y) (_ : N.le y x), @eq N x y *)
intros.
(* Goal: iff (@eq bool (eq_dir_b d1 d2) true) (@eq SplitDirection d1 d2) *)
unfold eq_dir_b.
(* Goal: @In SplitPath p (@nil SplitPath) *)
(* Goal: forall (p : SplitPath) (_ : @In SplitPath p (@nil SplitPath)), @eq (option RandomSeed) (varySeed' SeedTreeUndef p) (@Some RandomSeed (f p)) *)
(* Goal: PrefixFree (@nil SplitPath) *)
destruct d1; destruct d2; split; auto; intro Contra; inversion Contra.
Qed.

Definition refineList (d : SplitDirection) (l : list SplitPath) : list SplitPath :=
  map (@tl SplitDirection) (filter (fun p => match hd_error p with
                             | Some d' => eq_dir_b d d'
                             | _       => false
                           end) l).

(* Goal: @eq (list SplitPath) (@cons SplitPath s0 l0) (@cons (list SplitDirection) (@nil SplitDirection) (@nil (list SplitDirection))) *)
(* Goal: @eq RandomSeed s (f (@nil SplitDirection)) *)
Lemma refineCorrect : forall d l p, In p (refineList d l) -> In (d :: p) l.
(* Goal: forall (d : SplitDirection) (l : list SplitPath) (p : SplitPath) (_ : @In SplitPath p (refineList d l)), @In (list SplitDirection) (@cons SplitDirection d p) l *)
intros d l p.
(* Goal: @In (list SplitDirection) p (refineList d l) *)
unfold refineList.
(* Goal: forall _ : @In (list SplitDirection) x (@filter (list SplitDirection) (fun p : list SplitDirection => match @hd_error SplitDirection p with | Some d' => eq_dir_b d d' | None => false end) l), @In (list SplitDirection) (@cons SplitDirection d p) l *)
rewrite in_map_iff.
(* Goal: forall (_ : N.le x y) (_ : N.le y x), @eq N x y *)
intros.
(* Goal: @In (list SplitDirection) (@cons SplitDirection d p) l *)
inversion H; clear H.
(* Goal: @In (list SplitDirection) (@cons SplitDirection d p) l *)
inversion H0; clear H0.
(* Goal: @In (list SplitDirection) (@cons SplitDirection d p) l *)
generalize H1; clear H1.
(* Goal: forall _ : @In (list SplitDirection) x (@filter (list SplitDirection) (fun p : list SplitDirection => match @hd_error SplitDirection p with | Some d' => eq_dir_b d d' | None => false end) l), @In (list SplitDirection) (@cons SplitDirection d p) l *)
rewrite filter_In.
(* Goal: forall (_ : N.le x y) (_ : N.le y x), @eq N x y *)
intros.
(* Goal: @In (list SplitDirection) (@cons SplitDirection d p) l *)
inversion H0; clear H0.
(* Goal: @In (list SplitDirection) (@cons SplitDirection d p) l *)
unfold tl in H.
(* Goal: @In (list SplitDirection) (@cons SplitDirection d p) l *)
destruct x eqn:X.
(* Goal: @sig SeedTree (fun s : SeedTree => correspondingSeedTree (@cons SplitPath a l) f s) *)
+ simpl in H2. inversion H2.
(* Goal: @sig SeedTree (fun s : SeedTree => correspondingSeedTree (@cons SplitPath a l) f s) *)
+ simpl in H2. apply eq_dir_b_eq in H2. subst. auto.
Qed.

(* Goal: @eq (list SplitPath) (@cons SplitPath s0 l0) (@cons (list SplitDirection) (@nil SplitDirection) (@nil (list SplitDirection))) *)
(* Goal: @eq RandomSeed s (f (@nil SplitDirection)) *)
Lemma refineCorrect' : forall d l p, In (d :: p) l -> In p (refineList d l).
(* Goal: forall (_ : N.le x y) (_ : N.le y x), @eq N x y *)
intros.
(* Goal: @In (list SplitDirection) p (refineList d l) *)
unfold refineList.
(* Goal: @In (list SplitDirection) p (@map (list SplitDirection) (list SplitDirection) (@tl SplitDirection) (@filter (list SplitDirection) (fun p : list SplitDirection => match @hd_error SplitDirection p with | Some d' => eq_dir_b d d' | None => false end) l)) *)
apply in_map_iff.
(* Goal: @ex (list SplitDirection) (fun x : list SplitDirection => and (@eq (list SplitDirection) (@tl SplitDirection x) p) (@In (list SplitDirection) x (@filter (list SplitDirection) (fun p : list SplitDirection => match @hd_error SplitDirection p with | Some d' => eq_dir_b d d' | None => false end) l))) *)
exists (d :: p).
(* Goal: @eq RandomSeed (varySeed p rst) (f p) *)
split; auto.
(* Goal: @In (list SplitDirection) (@cons SplitDirection d p) (@filter (list SplitDirection) (fun p : list SplitDirection => match @hd_error SplitDirection p with | Some d' => eq_dir_b d d' | None => false end) l) *)
apply filter_In.
(* Goal: @eq RandomSeed (varySeed p rst) (f p) *)
split; simpl; auto.
(* Goal: @eq RandomSeed (varySeed p rst) (f p) *)
unfold eq_dir_b; destruct d; auto.
Qed.

(* Goal: @eq (list SplitPath) (@cons SplitPath s0 l0) (@cons (list SplitDirection) (@nil SplitDirection) (@nil (list SplitDirection))) *)
(* Goal: @eq RandomSeed s (f (@nil SplitDirection)) *)
Lemma refinePreservesPrefixFree : forall d l, PrefixFree l -> PrefixFree (refineList d l).
(* Goal: forall (_ : N.le x y) (_ : N.le y x), @eq N x y *)
  intros.
(* Goal: @sig SeedTree (fun s : SeedTree => correspondingSeedTree l f s) *)
  induction l.
(* Goal: @eq (list SplitPath) (@cons SplitPath s0 l0) (@cons (list SplitDirection) (@nil SplitDirection) (@nil (list SplitDirection))) *)
(* Goal: @eq RandomSeed s (f (@nil SplitDirection)) *)
  - unfold refineList; constructor.
(* Goal: @eq (list SplitPath) (@cons SplitPath s0 l0) (@cons (list SplitDirection) (@nil SplitDirection) (@nil (list SplitDirection))) *)
(* Goal: @eq RandomSeed s (f (@nil SplitDirection)) *)
  - destruct a eqn:A; subst.
(* Goal: @eq RandomSeed (varySeedAux (@cons SplitDirection Right s1) (RstNode s2 rst1 rst2)) s *)
    * apply prefixFreeEmpty in H. subst. unfold refineList. simpl. constructor.
(* Goal: @eq (list SplitPath) (@cons SplitPath (@cons SplitDirection s1 s2) l0) (@cons (list SplitDirection) (@nil SplitDirection) (@nil (list SplitDirection))) *)
(* Goal: @eq RandomSeed s (f (@nil SplitDirection)) *)
    * destruct s eqn:S; destruct d; subst.
(* Goal: @sig SeedTree (fun s : SeedTree => correspondingSeedTree (@cons SplitPath a l) f s) *)
      + unfold refineList; simpl.
(* Goal: PrefixFree (@cons SplitPath p (@nil SplitPath)) *)
        eapply FreeCons.
(* Goal: @eq (list SplitPath) (@cons SplitPath s0 l0) (@cons (list SplitDirection) (@nil SplitDirection) (@nil (list SplitDirection))) *)
(* Goal: @eq RandomSeed s (f (@nil SplitDirection)) *)
        - apply IHl. inversion H; auto.
(* Goal: forall (_ : N.le x y) (_ : N.le y x), @eq N x y *)
        - intros. inversion H; subst; clear H.
          apply in_map_iff in H0.
          inversion H0; subst; clear H0.
          inversion H; subst; clear H.
          apply filter_In in H2. inversion H2; subst; clear H2.
(* Goal: @eq RandomSeed (varySeedAux (@nil SplitDirection) rst) s *)
(* Goal: @eq RandomSeed (varySeedAux (@cons SplitDirection s0 s1) rst) s *)
          destruct x eqn:X; simpl in *. inversion H0.
(* Goal: @eq (list SplitPath) (@cons SplitPath (@cons SplitDirection s1 s2) l0) (@cons (list SplitDirection) (@nil SplitDirection) (@nil (list SplitDirection))) *)
(* Goal: @eq RandomSeed s (f (@nil SplitDirection)) *)
          destruct s eqn:S; simpl in *.
          pose proof H5 (Left :: l0).
(* Goal: @eq RandomSeed (varySeed p rst) (f p) *)
          eapply H2 in H; auto.
(* Goal: @eq RandomSeed (varySeedAux (@cons SplitDirection Right s1) (RstNode s2 rst1 rst2)) s *)
          simpl. instantiate (1 := p2). instantiate (1:= p1). rewrite H1. auto.
(* Goal: @eq RandomSeed (varySeedAux (@nil SplitDirection) rst) s *)
(* Goal: @eq RandomSeed (varySeedAux (@cons SplitDirection s0 s1) rst) s *)
          inversion H0.
(* Goal: @sig SeedTree (fun s : SeedTree => correspondingSeedTree (@cons SplitPath a l) f s) *)
      + unfold refineList; simpl. apply IHl.
(* Goal: PrefixFree l *)
        inversion H. auto.
(* Goal: @sig SeedTree (fun s : SeedTree => correspondingSeedTree (@cons SplitPath a l) f s) *)
      + unfold refineList; simpl. apply IHl.
(* Goal: PrefixFree l *)
        inversion H. auto.
(* Goal: @sig SeedTree (fun s : SeedTree => correspondingSeedTree (@cons SplitPath a l) f s) *)
      + unfold refineList; simpl.
(* Goal: PrefixFree (@cons SplitPath p (@nil SplitPath)) *)
        eapply FreeCons.
(* Goal: @eq (list SplitPath) (@cons SplitPath s0 l0) (@cons (list SplitDirection) (@nil SplitDirection) (@nil (list SplitDirection))) *)
(* Goal: @eq RandomSeed s (f (@nil SplitDirection)) *)
        - apply IHl. inversion H; auto.
(* Goal: forall (_ : N.le x y) (_ : N.le y x), @eq N x y *)
        - intros. inversion H; subst; clear H.
          apply in_map_iff in H0.
          inversion H0; subst; clear H0.
          inversion H; subst; clear H.
          apply filter_In in H2. inversion H2; subst; clear H2.
(* Goal: @eq RandomSeed (varySeedAux (@nil SplitDirection) rst) s *)
(* Goal: @eq RandomSeed (varySeedAux (@cons SplitDirection s0 s1) rst) s *)
          destruct x eqn:X; simpl in *. inversion H0.
(* Goal: @eq (list SplitPath) (@cons SplitPath (@cons SplitDirection s1 s2) l0) (@cons (list SplitDirection) (@nil SplitDirection) (@nil (list SplitDirection))) *)
(* Goal: @eq RandomSeed s (f (@nil SplitDirection)) *)
          destruct s eqn:S; simpl in *.
(* Goal: @eq RandomSeed (varySeedAux (@nil SplitDirection) rst) s *)
(* Goal: @eq RandomSeed (varySeedAux (@cons SplitDirection s0 s1) rst) s *)
          inversion H0.
          pose proof H5 (Right :: l0).
(* Goal: @eq RandomSeed (varySeed p rst) (f p) *)
          eapply H2 in H; auto.
(* Goal: @eq RandomSeed (varySeedAux (@cons SplitDirection Right s1) (RstNode s2 rst1 rst2)) s *)
          simpl. instantiate (1 := p2). instantiate (1:= p1). rewrite H1. auto.
Qed.

(* Goal: @eq (list SplitPath) (@cons SplitPath s0 l0) (@cons (list SplitDirection) (@nil SplitDirection) (@nil (list SplitDirection))) *)
(* Goal: @eq RandomSeed s (f (@nil SplitDirection)) *)
Definition refineFunction (f : SplitPath -> RandomSeed) (d : SplitDirection) (arg : SplitPath) :
RandomSeed :=
  f (d :: arg).

Lemma refineFunCorrect : forall f d p, f (d :: p) = (refineFunction f d) p.
(* Goal: @eq RandomSeed (varySeed p rst) (f p) *)
auto.
Qed.

Hint Rewrite refineFunCorrect.
Hint Unfold refineFunction.
(* Goal: @eq (list SplitPath) (@cons SplitPath s0 l0) (@cons (list SplitDirection) (@nil SplitDirection) (@nil (list SplitDirection))) *)
(* Goal: @eq RandomSeed s (f (@nil SplitDirection)) *)
Program Fixpoint addToTree (st : SeedTree) (p : SplitPath) (f : SplitPath -> RandomSeed)
        (l : list SplitPath)
        (Corr : correspondingSeedTree l f st)
(* Goal: @sig SeedTree (fun s : SeedTree => correspondingSeedTree (@cons SplitPath a l) f s) *)
        (Pref : forall p', In p' l -> (forall p1 p2, p ++ p1 = p' ++ p2 -> False))
: SeedTree :=
  match st with
    | SeedTreeUndef =>
      match p with
        | [] => SeedTreeLeaf (f p)
        | Left  :: p' => SeedTreeNode (addToTree SeedTreeUndef p' (refineFunction f Left) [] _ _) SeedTreeUndef
        | Right :: p' => SeedTreeNode SeedTreeUndef (addToTree SeedTreeUndef p' (refineFunction f Right) [] _ _)
      end
(* Goal: @eq (list SplitPath) (@cons SplitPath (@cons SplitDirection s1 s2) l0) (@cons (list SplitDirection) (@nil SplitDirection) (@nil (list SplitDirection))) *)
(* Goal: @eq RandomSeed s (f (@nil SplitDirection)) *)
    | SeedTreeLeaf s => _  (* Contradiction! *)
    | SeedTreeNode st1 st2 =>
      match p with
        | [] => SeedTreeLeaf (f p)
        | Left  :: p' => SeedTreeNode (addToTree st1 p' (refineFunction f Left) (refineList Left l) _ _) st2
        | Right :: p' => SeedTreeNode st1 (addToTree st2 p' (refineFunction f Right) (refineList Right l) _ _)
      end
  end.
Next Obligation.
(* Goal: @In (list SplitDirection) (@cons SplitDirection d p) l *)
apply corrEmptyLeaf in Corr. inversion Corr; clear Corr; subst.
pose proof (Pref []).
exfalso.
eapply H.
(* Goal: @sig SeedTree (fun s : SeedTree => correspondingSeedTree (@cons SplitPath a l) f s) *)
+ left; auto.
(* Goal: @sig SeedTree (fun s : SeedTree => correspondingSeedTree (@cons SplitPath a l) f s) *)
+ instantiate (2 := []). rewrite app_nil_r. simpl. eauto.
Qed.
Next Obligation.
(* Goal: forall (_ : N.le x y) (_ : N.le y x), @eq N x y *)
eapply Corresponding; intros.
(* Goal: @sig SeedTree (fun s : SeedTree => correspondingSeedTree (@cons SplitPath a l) f s) *)
+ apply refineCorrect'.
(* Goal: @In (list SplitDirection) (@cons SplitDirection Right p) l *)
(* Goal: @eq (option RandomSeed) (varySeed' st2 p) (@Some RandomSeed (refineFunction f Right p)) *)
(* Goal: PrefixFree (refineList Right l) *)
  inversion Corr as [Vary_In _ _ ]; clear Corr.
(* Goal: @In (list SplitDirection) (@cons SplitDirection Left p) l *)
(* Goal: @eq (option RandomSeed) (varySeed' st1 p) (@Some RandomSeed (refineFunction f Left p)) *)
(* Goal: PrefixFree (refineList Left l) *)
  pose proof (Vary_In (Left :: p) s) as Hyp; clear Vary_In.
(* Goal: @eq RandomSeed (varySeed p rst) (f p) *)
  auto.
(* Goal: @sig SeedTree (fun s : SeedTree => correspondingSeedTree (@cons SplitPath a l) f s) *)
+ apply refineCorrect in H.
(* Goal: @eq (option RandomSeed) (varySeed' st2 p) (@Some RandomSeed (refineFunction f Right p)) *)
(* Goal: PrefixFree (refineList Right l) *)
  inversion Corr as [_ In_Vary _]; clear Corr.
(* Goal: @eq (option RandomSeed) (varySeed' st1 p) (@Some RandomSeed (refineFunction f Left p)) *)
(* Goal: PrefixFree (refineList Left l) *)
  pose proof (In_Vary (Left :: p)) as Hyp; clear In_Vary.
(* Goal: @eq (option RandomSeed) (varySeed' st2 p) (@Some RandomSeed (refineFunction f Right p)) *)
(* Goal: PrefixFree (refineList Right l) *)
  apply Hyp in H; clear Hyp.
(* Goal: @eq (option RandomSeed) (varySeed' st2 p) (@Some RandomSeed (refineFunction f Right p)) *)
(* Goal: PrefixFree (refineList Right l) *)
  simpl in H.
(* Goal: @eq RandomSeed (varySeed p rst) (f p) *)
  unfold refineFunction; auto.
(* Goal: @sig SeedTree (fun s : SeedTree => correspondingSeedTree (@cons SplitPath a l) f s) *)
+ inversion Corr.
(* Goal: PrefixFree (refineList Right l) *)
  apply refinePreservesPrefixFree.
(* Goal: @eq RandomSeed (varySeed p rst) (f p) *)
  auto.
Qed.
Next Obligation.
eapply Pref.
instantiate (1:= Left :: p'0).
(* Goal: @eq RandomSeed (varySeed p rst) (f p) *)
apply refineCorrect; auto.
(* Goal: @eq RandomSeed (varySeedAux (@cons SplitDirection Right s1) (RstNode s2 rst1 rst2)) s *)
instantiate (1:= p2). instantiate (1:=p1). simpl. rewrite H0. auto.
Qed.
Next Obligation.
(* Goal: forall (_ : N.le x y) (_ : N.le y x), @eq N x y *)
eapply Corresponding; intros.
(* Goal: @sig SeedTree (fun s : SeedTree => correspondingSeedTree (@cons SplitPath a l) f s) *)
+ apply refineCorrect'.
(* Goal: @In (list SplitDirection) (@cons SplitDirection Right p) l *)
(* Goal: @eq (option RandomSeed) (varySeed' st2 p) (@Some RandomSeed (refineFunction f Right p)) *)
(* Goal: PrefixFree (refineList Right l) *)
  inversion Corr as [Vary_In _ _ ]; clear Corr.
(* Goal: @In (list SplitDirection) (@cons SplitDirection Right p) l *)
(* Goal: @eq (option RandomSeed) (varySeed' st2 p) (@Some RandomSeed (refineFunction f Right p)) *)
(* Goal: PrefixFree (refineList Right l) *)
  pose proof (Vary_In (Right :: p) s) as Hyp; clear Vary_In.
(* Goal: @eq RandomSeed (varySeed p rst) (f p) *)
  auto.
(* Goal: @sig SeedTree (fun s : SeedTree => correspondingSeedTree (@cons SplitPath a l) f s) *)
+ apply refineCorrect in H.
(* Goal: @eq (option RandomSeed) (varySeed' st2 p) (@Some RandomSeed (refineFunction f Right p)) *)
(* Goal: PrefixFree (refineList Right l) *)
  inversion Corr as [_ In_Vary _]; clear Corr.
(* Goal: @eq (option RandomSeed) (varySeed' st2 p) (@Some RandomSeed (refineFunction f Right p)) *)
(* Goal: PrefixFree (refineList Right l) *)
  pose proof (In_Vary (Right :: p)) as Hyp; clear In_Vary.
(* Goal: @eq (option RandomSeed) (varySeed' st2 p) (@Some RandomSeed (refineFunction f Right p)) *)
(* Goal: PrefixFree (refineList Right l) *)
  apply Hyp in H; clear Hyp.
(* Goal: @eq (option RandomSeed) (varySeed' st2 p) (@Some RandomSeed (refineFunction f Right p)) *)
(* Goal: PrefixFree (refineList Right l) *)
  simpl in H.
(* Goal: @eq RandomSeed (varySeed p rst) (f p) *)
  unfold refineFunction; auto.
(* Goal: @sig SeedTree (fun s : SeedTree => correspondingSeedTree (@cons SplitPath a l) f s) *)
+ inversion Corr.
(* Goal: PrefixFree (refineList Right l) *)
  apply refinePreservesPrefixFree.
(* Goal: @eq RandomSeed (varySeed p rst) (f p) *)
  auto.
Qed.
Next Obligation.
eapply Pref.
instantiate (1:= Right :: p'0).
(* Goal: @eq RandomSeed (varySeed p rst) (f p) *)
apply refineCorrect; auto.
(* Goal: @eq RandomSeed (varySeedAux (@cons SplitDirection Right s1) (RstNode s2 rst1 rst2)) s *)
instantiate (1:= p2). instantiate (1:=p1). simpl. rewrite H0. auto.
Qed.

Lemma addToTreeCorrect1 : forall (st : SeedTree) (p : SplitPath)
(* Goal: @eq (list SplitPath) (@cons SplitPath s0 l0) (@cons (list SplitDirection) (@nil SplitDirection) (@nil (list SplitDirection))) *)
(* Goal: @eq RandomSeed s (f (@nil SplitDirection)) *)
  (f : SplitPath -> RandomSeed)
  (l : list SplitPath) (Corr : correspondingSeedTree l f st)
(* Goal: @sig SeedTree (fun s : SeedTree => correspondingSeedTree (@cons SplitPath a l) f s) *)
  (Pref : forall p', In p' l -> (forall p1 p2, p ++ p1 = p' ++ p2 -> False)),
  varySeed' (addToTree st p f l Corr Pref) p = Some (f p).
intros st p.
generalize dependent st.
induction p.
(* Goal: @sig SeedTree (fun s : SeedTree => correspondingSeedTree (@cons SplitPath a l) f s) *)
+ intros st f l Corr Pref.
  unfold addToTree.
  destruct st.
(* Goal: @eq (list SplitPath) (@cons SplitPath s0 l0) (@cons (list SplitDirection) (@nil SplitDirection) (@nil (list SplitDirection))) *)
(* Goal: @eq RandomSeed s (f (@nil SplitDirection)) *)
  - auto.
(* Goal: @eq (list SplitPath) (@cons SplitPath s0 l0) (@cons (list SplitDirection) (@nil SplitDirection) (@nil (list SplitDirection))) *)
(* Goal: @eq RandomSeed s (f (@nil SplitDirection)) *)
  - exfalso.
    apply corrEmptyLeaf in Corr.
    inversion Corr; clear Corr.
(* Goal: @In (list SplitDirection) (@cons SplitDirection d p) l *)
    subst.
    pose proof Pref [] as Contra; clear Pref.
    eapply Contra; clear Contra.
(* Goal: @eq (list SplitPath) (@cons SplitPath (@cons SplitDirection s1 s2) l0) (@cons (list SplitDirection) (@nil SplitDirection) (@nil (list SplitDirection))) *)
(* Goal: @eq RandomSeed s (f (@nil SplitDirection)) *)
    * left; auto.
(* Goal: @eq (list SplitPath) (@cons SplitPath (@cons SplitDirection s1 s2) l0) (@cons (list SplitDirection) (@nil SplitDirection) (@nil (list SplitDirection))) *)
(* Goal: @eq RandomSeed s (f (@nil SplitDirection)) *)
    * instantiate (1 := []). instantiate (1 := []). auto.
(* Goal: @eq (list SplitPath) (@cons SplitPath s0 l0) (@cons (list SplitDirection) (@nil SplitDirection) (@nil (list SplitDirection))) *)
(* Goal: @eq RandomSeed s (f (@nil SplitDirection)) *)
  - simpl. auto.
(* Goal: @sig SeedTree (fun s : SeedTree => correspondingSeedTree (@cons SplitPath a l) f s) *)
+ intros.
(* Goal: @eq RandomSeed (varySeed p rst) (f p) *)
  destruct st; destruct a; simpl; auto.
(* Goal: @eq (list SplitPath) (@cons SplitPath s0 l0) (@cons (list SplitDirection) (@nil SplitDirection) (@nil (list SplitDirection))) *)
(* Goal: @eq RandomSeed s (f (@nil SplitDirection)) *)
  - rewrite refineFunCorrect.
    apply IHp.
(* Goal: @eq (list SplitPath) (@cons SplitPath s0 l0) (@cons (list SplitDirection) (@nil SplitDirection) (@nil (list SplitDirection))) *)
(* Goal: @eq RandomSeed s (f (@nil SplitDirection)) *)
  - rewrite refineFunCorrect; apply IHp.
(* Goal: @eq (list SplitPath) (@cons SplitPath s0 l0) (@cons (list SplitDirection) (@nil SplitDirection) (@nil (list SplitDirection))) *)
(* Goal: @eq RandomSeed s (f (@nil SplitDirection)) *)
  - exfalso. eapply corrEmptyLeaf in Corr; inversion Corr; subst; clear Corr.
    pose proof (Pref []).
    eapply H.
(* Goal: @eq (list SplitPath) (@cons SplitPath s0 l0) (@cons (list SplitDirection) (@nil SplitDirection) (@nil (list SplitDirection))) *)
(* Goal: @eq RandomSeed s (f (@nil SplitDirection)) *)
    - subst; left; auto.
(* Goal: @eq (list SplitPath) (@cons SplitPath s0 l0) (@cons (list SplitDirection) (@nil SplitDirection) (@nil (list SplitDirection))) *)
(* Goal: @eq RandomSeed s (f (@nil SplitDirection)) *)
    - simpl. instantiate (2:= []); rewrite app_nil_r. instantiate (1 := Left ::p); auto.
(* Goal: @eq (list SplitPath) (@cons SplitPath s0 l0) (@cons (list SplitDirection) (@nil SplitDirection) (@nil (list SplitDirection))) *)
(* Goal: @eq RandomSeed s (f (@nil SplitDirection)) *)
  - exfalso. eapply corrEmptyLeaf in Corr; inversion Corr; subst; clear Corr.
    pose proof (Pref []).
    eapply H.
(* Goal: @eq (list SplitPath) (@cons SplitPath s0 l0) (@cons (list SplitDirection) (@nil SplitDirection) (@nil (list SplitDirection))) *)
(* Goal: @eq RandomSeed s (f (@nil SplitDirection)) *)
    - subst; left; auto.
(* Goal: @eq (list SplitPath) (@cons SplitPath s0 l0) (@cons (list SplitDirection) (@nil SplitDirection) (@nil (list SplitDirection))) *)
(* Goal: @eq RandomSeed s (f (@nil SplitDirection)) *)
    - simpl. instantiate (2:= []); rewrite app_nil_r. instantiate (1 := Right ::p); auto.
(* Goal: @eq (list SplitPath) (@cons SplitPath s0 l0) (@cons (list SplitDirection) (@nil SplitDirection) (@nil (list SplitDirection))) *)
(* Goal: @eq RandomSeed s (f (@nil SplitDirection)) *)
  - rewrite refineFunCorrect; apply IHp.
(* Goal: @eq (list SplitPath) (@cons SplitPath s0 l0) (@cons (list SplitDirection) (@nil SplitDirection) (@nil (list SplitDirection))) *)
(* Goal: @eq RandomSeed s (f (@nil SplitDirection)) *)
  - rewrite refineFunCorrect; apply IHp.
Qed.

Lemma addToTreeCorrect2 : forall (st : SeedTree) (p : SplitPath)
(* Goal: @eq (list SplitPath) (@cons SplitPath s0 l0) (@cons (list SplitDirection) (@nil SplitDirection) (@nil (list SplitDirection))) *)
(* Goal: @eq RandomSeed s (f (@nil SplitDirection)) *)
  (f : SplitPath -> RandomSeed)
  (l : list SplitPath) (Corr : correspondingSeedTree l f st)
(* Goal: @sig SeedTree (fun s : SeedTree => correspondingSeedTree (@cons SplitPath a l) f s) *)
  (Pref : forall p', In p' l -> (forall p1 p2, p ++ p1 = p' ++ p2 -> False)),
(* Goal: @eq (list SplitPath) (@cons SplitPath s0 l0) (@cons (list SplitDirection) (@nil SplitDirection) (@nil (list SplitDirection))) *)
(* Goal: @eq RandomSeed s (f (@nil SplitDirection)) *)
  forall p' seed, varySeed' st p' = Some seed ->
             varySeed' (addToTree st p f l Corr Pref) p' = Some seed.
intros st p.
generalize dependent st.
induction p as [ | d ds].
(* Goal: @sig SeedTree (fun s : SeedTree => correspondingSeedTree (@cons SplitPath a l) f s) *)
+ intros.
  exfalso.
  eapply Pref.
(* Goal: @eq (list SplitPath) (@cons SplitPath s0 l0) (@cons (list SplitDirection) (@nil SplitDirection) (@nil (list SplitDirection))) *)
(* Goal: @eq RandomSeed s (f (@nil SplitDirection)) *)
  - inversion Corr as [Vary_In In_Vary Pref']; clear Corr.
    eapply Vary_In; eassumption.
(* Goal: @eq (list SplitPath) (@cons SplitPath s0 l0) (@cons (list SplitDirection) (@nil SplitDirection) (@nil (list SplitDirection))) *)
(* Goal: @eq RandomSeed s (f (@nil SplitDirection)) *)
  - instantiate (1 := []); instantiate (1 := p'); rewrite app_nil_r; auto.
(* Goal: @sig SeedTree (fun s : SeedTree => correspondingSeedTree (@cons SplitPath a l) f s) *)
+ intros st f l Corr Pref p' seed VarySome.
(* Goal: @eq RandomSeed (varySeed p rst) (f p) *)
  destruct st; destruct d; simpl; auto.
(* Goal: @eq (list SplitPath) (@cons SplitPath (@cons SplitDirection s1 s2) l0) (@cons (list SplitDirection) (@nil SplitDirection) (@nil (list SplitDirection))) *)
(* Goal: @eq RandomSeed s (f (@nil SplitDirection)) *)
  * exfalso. apply corrUndefEmpty in Corr. subst. inversion VarySome.
(* Goal: @eq (list SplitPath) (@cons SplitPath (@cons SplitDirection s1 s2) l0) (@cons (list SplitDirection) (@nil SplitDirection) (@nil (list SplitDirection))) *)
(* Goal: @eq RandomSeed s (f (@nil SplitDirection)) *)
  * exfalso. apply corrUndefEmpty in Corr. subst. inversion VarySome.
(* Goal: @eq (list SplitPath) (@cons SplitPath (@cons SplitDirection s1 s2) l0) (@cons (list SplitDirection) (@nil SplitDirection) (@nil (list SplitDirection))) *)
(* Goal: @eq RandomSeed s (f (@nil SplitDirection)) *)
  * exfalso.
    apply corrEmptyLeaf in Corr; inversion Corr; subst; clear Corr.
    eapply Pref.
(* Goal: @eq RandomSeed (varySeed p rst) (f p) *)
    instantiate (1 := []); left; auto.
    instantiate (1:= Left :: ds). instantiate (1 := []). rewrite app_nil_r; simpl; auto.
(* Goal: @eq (list SplitPath) (@cons SplitPath (@cons SplitDirection s1 s2) l0) (@cons (list SplitDirection) (@nil SplitDirection) (@nil (list SplitDirection))) *)
(* Goal: @eq RandomSeed s (f (@nil SplitDirection)) *)
  * exfalso.
    apply corrEmptyLeaf in Corr; inversion Corr; subst; clear Corr.
    eapply Pref.
(* Goal: @eq RandomSeed (varySeed p rst) (f p) *)
    instantiate (1 := []); left; auto.
    instantiate (1:= Right :: ds). instantiate (1 := []). rewrite app_nil_r; simpl; auto.
(* Goal: @eq (list SplitPath) (@cons SplitPath (@cons SplitDirection s1 s2) l0) (@cons (list SplitDirection) (@nil SplitDirection) (@nil (list SplitDirection))) *)
(* Goal: @eq RandomSeed s (f (@nil SplitDirection)) *)
  * destruct p'.
(* Goal: @eq (list SplitPath) (@cons SplitPath s0 l0) (@cons (list SplitDirection) (@nil SplitDirection) (@nil (list SplitDirection))) *)
(* Goal: @eq RandomSeed s (f (@nil SplitDirection)) *)
    - simpl in VarySome. inversion VarySome.
(* Goal: @eq (list SplitPath) (@cons SplitPath s0 l0) (@cons (list SplitDirection) (@nil SplitDirection) (@nil (list SplitDirection))) *)
(* Goal: @eq RandomSeed s (f (@nil SplitDirection)) *)
    - destruct s.
(* Goal: @sig SeedTree (fun s : SeedTree => correspondingSeedTree (@cons SplitPath a l) f s) *)
      + apply IHds; auto.
(* Goal: @sig SeedTree (fun s : SeedTree => correspondingSeedTree (@cons SplitPath a l) f s) *)
      + auto.
(* Goal: @eq (list SplitPath) (@cons SplitPath (@cons SplitDirection s1 s2) l0) (@cons (list SplitDirection) (@nil SplitDirection) (@nil (list SplitDirection))) *)
(* Goal: @eq RandomSeed s (f (@nil SplitDirection)) *)
  * destruct p'.
(* Goal: @eq (list SplitPath) (@cons SplitPath s0 l0) (@cons (list SplitDirection) (@nil SplitDirection) (@nil (list SplitDirection))) *)
(* Goal: @eq RandomSeed s (f (@nil SplitDirection)) *)
    - simpl in VarySome; inversion VarySome.
(* Goal: @eq (list SplitPath) (@cons SplitPath s0 l0) (@cons (list SplitDirection) (@nil SplitDirection) (@nil (list SplitDirection))) *)
(* Goal: @eq RandomSeed s (f (@nil SplitDirection)) *)
    - destruct s.
(* Goal: @sig SeedTree (fun s : SeedTree => correspondingSeedTree (@cons SplitPath a l) f s) *)
      + auto.
(* Goal: @sig SeedTree (fun s : SeedTree => correspondingSeedTree (@cons SplitPath a l) f s) *)
      + apply IHds; auto.
Qed.

Lemma addToTreeCorrect3 : forall (st : SeedTree) (p : SplitPath)
(* Goal: @eq (list SplitPath) (@cons SplitPath s0 l0) (@cons (list SplitDirection) (@nil SplitDirection) (@nil (list SplitDirection))) *)
(* Goal: @eq RandomSeed s (f (@nil SplitDirection)) *)
  (f : SplitPath -> RandomSeed)
  (l : list SplitPath) (Corr : correspondingSeedTree l f st)
(* Goal: @sig SeedTree (fun s : SeedTree => correspondingSeedTree (@cons SplitPath a l) f s) *)
  (Pref : forall p', In p' l -> (forall p1 p2, p ++ p1 = p' ++ p2 -> False)),
(* Goal: @eq (list SplitPath) (@cons SplitPath s0 l0) (@cons (list SplitDirection) (@nil SplitDirection) (@nil (list SplitDirection))) *)
(* Goal: @eq RandomSeed s (f (@nil SplitDirection)) *)
  forall p' seed, varySeed' (addToTree st p f l Corr Pref) p' = Some seed ->
             p = p' \/ varySeed' st p' = Some seed.
intros st p. generalize dependent st.
induction p.
(* Goal: @sig SeedTree (fun s : SeedTree => correspondingSeedTree (@cons SplitPath a l) f s) *)
+ intros.
  destruct p'.
(* Goal: @eq (list SplitPath) (@cons SplitPath s0 l0) (@cons (list SplitDirection) (@nil SplitDirection) (@nil (list SplitDirection))) *)
(* Goal: @eq RandomSeed s (f (@nil SplitDirection)) *)
  - left; auto.
(* Goal: @eq (list SplitPath) (@cons SplitPath s0 l0) (@cons (list SplitDirection) (@nil SplitDirection) (@nil (list SplitDirection))) *)
(* Goal: @eq RandomSeed s (f (@nil SplitDirection)) *)
  - right.
    exfalso.
(* Goal: @eq (option RandomSeed) (varySeed' st2 p) (@Some RandomSeed (refineFunction f Right p)) *)
(* Goal: PrefixFree (refineList Right l) *)
    unfold addToTree in H; simpl in H.
(* Goal: @eq (option RandomSeed) (varySeed' st2 p) (@Some RandomSeed (refineFunction f Right p)) *)
(* Goal: PrefixFree (refineList Right l) *)
    destruct st; simpl in H.
(* Goal: PrefixFree l *)
    * inversion H.
(* Goal: @eq (list SplitPath) (@cons SplitPath (@cons SplitDirection s1 s2) l0) (@cons (list SplitDirection) (@nil SplitDirection) (@nil (list SplitDirection))) *)
(* Goal: @eq RandomSeed s (f (@nil SplitDirection)) *)
    * clear H. apply corrEmptyLeaf in Corr; inversion Corr; subst; clear Corr.
(* Goal: @In (list SplitDirection) (@cons SplitDirection d p) l *)
      subst.
      eapply Pref.
      instantiate (1 := []). left; auto.
(* Goal: @eq RandomSeed (varySeed p rst) (f p) *)
      instantiate (1 := []); instantiate (1 := []); auto.
(* Goal: PrefixFree l *)
    * inversion H.
(* Goal: @sig SeedTree (fun s : SeedTree => correspondingSeedTree (@cons SplitPath a l) f s) *)
+ intros.
(* Goal: @eq (list SplitPath) (@cons SplitPath (@cons SplitDirection s1 s2) l0) (@cons (list SplitDirection) (@nil SplitDirection) (@nil (list SplitDirection))) *)
(* Goal: @eq RandomSeed s (f (@nil SplitDirection)) *)
  destruct p'; destruct st; destruct a; simpl in *;
(* Goal: @eq (list SplitPath) (@cons SplitPath s0 l0) (@cons (list SplitDirection) (@nil SplitDirection) (@nil (list SplitDirection))) *)
(* Goal: @eq RandomSeed s (f (@nil SplitDirection)) *)
  try solve [match goal with [ H : None = Some _ |- _ ] => inversion H end].
(* Goal: @sig SeedTree (fun s : SeedTree => correspondingSeedTree (@cons SplitPath a l) f s) *)
  + exfalso. clear H. apply corrEmptyLeaf in Corr; inversion Corr; subst; clear Corr.
    eapply Pref.
(* Goal: @In (list SplitDirection) (@cons SplitDirection d p) l *)
    subst.
(* Goal: @eq RandomSeed (varySeed p rst) (f p) *)
    instantiate (1 := []) ; left; auto.
(* Goal: @eq RandomSeed (varySeed p rst) (f p) *)
    instantiate (1 := (Left :: p)); instantiate (1 := []); rewrite app_nil_r; auto.
(* Goal: @sig SeedTree (fun s : SeedTree => correspondingSeedTree (@cons SplitPath a l) f s) *)
  + exfalso. clear H. apply corrEmptyLeaf in Corr; inversion Corr; subst; clear Corr.
    eapply Pref.
(* Goal: @In (list SplitDirection) (@cons SplitDirection d p) l *)
    subst.
(* Goal: @eq RandomSeed (varySeed p rst) (f p) *)
    instantiate (1 := []) ; left; auto.
(* Goal: @eq RandomSeed (varySeed p rst) (f p) *)
    instantiate (1 := (Right :: p)); instantiate (1 := []); rewrite app_nil_r; auto.
(* Goal: @sig SeedTree (fun s : SeedTree => correspondingSeedTree (@cons SplitPath a l) f s) *)
  + destruct s; simpl in *.
(* Goal: @eq (list SplitPath) (@cons SplitPath s0 l0) (@cons (list SplitDirection) (@nil SplitDirection) (@nil (list SplitDirection))) *)
(* Goal: @eq RandomSeed s (f (@nil SplitDirection)) *)
    - assert (p = p' \/ varySeed' SeedTreeUndef p' = Some seed)
             by (eapply IHp; eauto).
(* Goal: @eq RandomSeed (varySeedAux (@nil SplitDirection) rst) s *)
(* Goal: @eq RandomSeed (varySeedAux (@cons SplitDirection s0 s1) rst) s *)
      inversion H0.
(* Goal: @eq (list SplitPath) (@cons SplitPath (@cons SplitDirection s1 s2) l0) (@cons (list SplitDirection) (@nil SplitDirection) (@nil (list SplitDirection))) *)
(* Goal: @eq RandomSeed s (f (@nil SplitDirection)) *)
      * left; subst; auto.
(* Goal: @eq (list SplitPath) (@cons SplitPath (@cons SplitDirection s1 s2) l0) (@cons (list SplitDirection) (@nil SplitDirection) (@nil (list SplitDirection))) *)
(* Goal: @eq RandomSeed s (f (@nil SplitDirection)) *)
      * simpl in H1. inversion H1.
(* Goal: @eq (list SplitPath) (@cons SplitPath s0 l0) (@cons (list SplitDirection) (@nil SplitDirection) (@nil (list SplitDirection))) *)
(* Goal: @eq RandomSeed s (f (@nil SplitDirection)) *)
    - inversion H.
(* Goal: @sig SeedTree (fun s : SeedTree => correspondingSeedTree (@cons SplitPath a l) f s) *)
  + destruct s; simpl in *.
(* Goal: @eq (list SplitPath) (@cons SplitPath s0 l0) (@cons (list SplitDirection) (@nil SplitDirection) (@nil (list SplitDirection))) *)
(* Goal: @eq RandomSeed s (f (@nil SplitDirection)) *)
    - inversion H.
(* Goal: @eq (list SplitPath) (@cons SplitPath s0 l0) (@cons (list SplitDirection) (@nil SplitDirection) (@nil (list SplitDirection))) *)
(* Goal: @eq RandomSeed s (f (@nil SplitDirection)) *)
    - assert (p = p' \/ varySeed' SeedTreeUndef p' = Some seed)
        by (eapply IHp; eauto).
(* Goal: @eq RandomSeed (varySeedAux (@nil SplitDirection) rst) s *)
(* Goal: @eq RandomSeed (varySeedAux (@cons SplitDirection s0 s1) rst) s *)
      inversion H0.
(* Goal: @eq (list SplitPath) (@cons SplitPath (@cons SplitDirection s1 s2) l0) (@cons (list SplitDirection) (@nil SplitDirection) (@nil (list SplitDirection))) *)
(* Goal: @eq RandomSeed s (f (@nil SplitDirection)) *)
      * left; subst; auto.
(* Goal: @eq (list SplitPath) (@cons SplitPath (@cons SplitDirection s1 s2) l0) (@cons (list SplitDirection) (@nil SplitDirection) (@nil (list SplitDirection))) *)
(* Goal: @eq RandomSeed s (f (@nil SplitDirection)) *)
      * simpl in H1. inversion H1.
(* Goal: @sig SeedTree (fun s : SeedTree => correspondingSeedTree (@cons SplitPath a l) f s) *)
  + exfalso.
    clear H.
    apply corrEmptyLeaf in Corr; inversion Corr; subst; clear Corr.
(* Goal: @In (list SplitDirection) (@cons SplitDirection d p) l *)
    subst.
    eapply Pref.
    instantiate (1 := []).
(* Goal: @eq (list SplitPath) (@cons SplitPath s0 l0) (@cons (list SplitDirection) (@nil SplitDirection) (@nil (list SplitDirection))) *)
(* Goal: @eq RandomSeed s (f (@nil SplitDirection)) *)
    - left; auto.
(* Goal: @eq (list SplitPath) (@cons SplitPath s0 l0) (@cons (list SplitDirection) (@nil SplitDirection) (@nil (list SplitDirection))) *)
(* Goal: @eq RandomSeed s (f (@nil SplitDirection)) *)
    - instantiate (1 := Left :: p); instantiate (1 := []); rewrite app_nil_r; auto.
(* Goal: @sig SeedTree (fun s : SeedTree => correspondingSeedTree (@cons SplitPath a l) f s) *)
  + exfalso.
    clear H.
    apply corrEmptyLeaf in Corr; inversion Corr; subst; clear Corr.
(* Goal: @In (list SplitDirection) (@cons SplitDirection d p) l *)
    subst.
    eapply Pref.
    instantiate (1 := []).
(* Goal: @eq (list SplitPath) (@cons SplitPath s0 l0) (@cons (list SplitDirection) (@nil SplitDirection) (@nil (list SplitDirection))) *)
(* Goal: @eq RandomSeed s (f (@nil SplitDirection)) *)
    - left; auto.
(* Goal: @eq (list SplitPath) (@cons SplitPath s0 l0) (@cons (list SplitDirection) (@nil SplitDirection) (@nil (list SplitDirection))) *)
(* Goal: @eq RandomSeed s (f (@nil SplitDirection)) *)
    - instantiate (1 := Right :: p); instantiate (1 := []); rewrite app_nil_r; auto.
(* Goal: @sig SeedTree (fun s : SeedTree => correspondingSeedTree (@cons SplitPath a l) f s) *)
  + destruct s eqn:S; simpl in *.
(* Goal: @eq (list SplitPath) (@cons SplitPath s0 l0) (@cons (list SplitDirection) (@nil SplitDirection) (@nil (list SplitDirection))) *)
(* Goal: @eq RandomSeed s (f (@nil SplitDirection)) *)
    - assert (p = p' \/ varySeed' st1 p' = Some seed)
        by (eapply IHp; eauto).
(* Goal: @eq RandomSeed (varySeedAux (@nil SplitDirection) rst) s *)
(* Goal: @eq RandomSeed (varySeedAux (@cons SplitDirection s0 s1) rst) s *)
      inversion H0.
(* Goal: @eq (list SplitPath) (@cons SplitPath (@cons SplitDirection s1 s2) l0) (@cons (list SplitDirection) (@nil SplitDirection) (@nil (list SplitDirection))) *)
(* Goal: @eq RandomSeed s (f (@nil SplitDirection)) *)
      * left; subst; auto.
(* Goal: @eq (list SplitPath) (@cons SplitPath (@cons SplitDirection s1 s2) l0) (@cons (list SplitDirection) (@nil SplitDirection) (@nil (list SplitDirection))) *)
(* Goal: @eq RandomSeed s (f (@nil SplitDirection)) *)
      * right; auto.
(* Goal: @eq (list SplitPath) (@cons SplitPath s0 l0) (@cons (list SplitDirection) (@nil SplitDirection) (@nil (list SplitDirection))) *)
(* Goal: @eq RandomSeed s (f (@nil SplitDirection)) *)
    - right; auto.
(* Goal: @sig SeedTree (fun s : SeedTree => correspondingSeedTree (@cons SplitPath a l) f s) *)
  + destruct s eqn:S; simpl in *.
(* Goal: @eq (list SplitPath) (@cons SplitPath s0 l0) (@cons (list SplitDirection) (@nil SplitDirection) (@nil (list SplitDirection))) *)
(* Goal: @eq RandomSeed s (f (@nil SplitDirection)) *)
    - right; auto.
(* Goal: @eq (list SplitPath) (@cons SplitPath s0 l0) (@cons (list SplitDirection) (@nil SplitDirection) (@nil (list SplitDirection))) *)
(* Goal: @eq RandomSeed s (f (@nil SplitDirection)) *)
    - assert (p = p' \/ varySeed' st2 p' = Some seed)
        by (eapply IHp; eauto).
(* Goal: @eq RandomSeed (varySeedAux (@nil SplitDirection) rst) s *)
(* Goal: @eq RandomSeed (varySeedAux (@cons SplitDirection s0 s1) rst) s *)
      inversion H0.
(* Goal: @eq (list SplitPath) (@cons SplitPath (@cons SplitDirection s1 s2) l0) (@cons (list SplitDirection) (@nil SplitDirection) (@nil (list SplitDirection))) *)
(* Goal: @eq RandomSeed s (f (@nil SplitDirection)) *)
      * left; subst; auto.
(* Goal: @eq (list SplitPath) (@cons SplitPath (@cons SplitDirection s1 s2) l0) (@cons (list SplitDirection) (@nil SplitDirection) (@nil (list SplitDirection))) *)
(* Goal: @eq RandomSeed s (f (@nil SplitDirection)) *)
      * right; auto.
Qed.

Lemma addToTreeCorrect : forall (st : SeedTree) (p : SplitPath)
(* Goal: @eq (list SplitPath) (@cons SplitPath s0 l0) (@cons (list SplitDirection) (@nil SplitDirection) (@nil (list SplitDirection))) *)
(* Goal: @eq RandomSeed s (f (@nil SplitDirection)) *)
  (f : SplitPath -> RandomSeed)
  (l : list SplitPath) (Corr : correspondingSeedTree l f st)
(* Goal: @sig SeedTree (fun s : SeedTree => correspondingSeedTree (@cons SplitPath a l) f s) *)
  (Pref : forall p', In p' l -> (forall p1 p2, p ++ p1 = p' ++ p2 -> False)),
  correspondingSeedTree (p :: l) f (addToTree st p f l Corr Pref).
(* Goal: forall (_ : N.le x y) (_ : N.le y x), @eq N x y *)
intros.
(* Goal: correspondingSeedTree (@nil SplitPath) f SeedTreeUndef *)
apply Corresponding.
(* Goal: @sig SeedTree (fun s : SeedTree => correspondingSeedTree (@cons SplitPath a l) f s) *)
+ intros p' s VarySome.
  inversion Corr as [Vary_In In_Vary Pref'].
  apply addToTreeCorrect3 in VarySome.
  inversion VarySome.
(* Goal: @eq (list SplitPath) (@cons SplitPath s0 l0) (@cons (list SplitDirection) (@nil SplitDirection) (@nil (list SplitDirection))) *)
(* Goal: @eq RandomSeed s (f (@nil SplitDirection)) *)
  - left; auto.
(* Goal: @eq (list SplitPath) (@cons SplitPath s0 l0) (@cons (list SplitDirection) (@nil SplitDirection) (@nil (list SplitDirection))) *)
(* Goal: @eq RandomSeed s (f (@nil SplitDirection)) *)
  - right. eapply Vary_In; eassumption.
(* Goal: @sig SeedTree (fun s : SeedTree => correspondingSeedTree (@cons SplitPath a l) f s) *)
+ intros p' InP'.
  inversion Corr as [Vary_In In_Vary Pref'].
  inversion InP'.
(* Goal: @eq (list SplitPath) (@cons SplitPath s0 l0) (@cons (list SplitDirection) (@nil SplitDirection) (@nil (list SplitDirection))) *)
(* Goal: @eq RandomSeed s (f (@nil SplitDirection)) *)
  - subst.
    apply addToTreeCorrect1.
(* Goal: @eq (list SplitPath) (@cons SplitPath s0 l0) (@cons (list SplitDirection) (@nil SplitDirection) (@nil (list SplitDirection))) *)
(* Goal: @eq RandomSeed s (f (@nil SplitDirection)) *)
  - apply addToTreeCorrect2. apply In_Vary. auto.
(* Goal: @sig SeedTree (fun s : SeedTree => correspondingSeedTree (@cons SplitPath a l) f s) *)
+ apply FreeCons.
(* Goal: @eq (list SplitPath) (@cons SplitPath s0 l0) (@cons (list SplitDirection) (@nil SplitDirection) (@nil (list SplitDirection))) *)
(* Goal: @eq RandomSeed s (f (@nil SplitDirection)) *)
  - inversion Corr; auto.
(* Goal: forall (_ : N.le x y) (_ : N.le y x), @eq N x y *)
  - intros.
    eapply Pref.
    eassumption.
(* Goal: @eq RandomSeed (varySeed p rst) (f p) *)
    instantiate (1 := p1); instantiate (1:= p2); subst; auto.
Qed.

(* Goal: @eq (list SplitPath) (@cons SplitPath s0 l0) (@cons (list SplitDirection) (@nil SplitDirection) (@nil (list SplitDirection))) *)
(* Goal: @eq RandomSeed s (f (@nil SplitDirection)) *)
Lemma PrefixFreeTail : forall a l, PrefixFree (a :: l) -> PrefixFree l.
(* Goal: forall (_ : N.le x y) (_ : N.le y x), @eq N x y *)
intros.
(* Goal: PrefixFree l *)
inversion H.
(* Goal: @eq RandomSeed (varySeed p rst) (f p) *)
auto.
Qed.

(* Goal: @eq (list SplitPath) (@cons SplitPath (@cons SplitDirection s1 s2) l0) (@cons (list SplitDirection) (@nil SplitDirection) (@nil (list SplitDirection))) *)
(* Goal: @eq RandomSeed s (f (@nil SplitDirection)) *)
(* LL: Why was it easier to do it like this? :P *)
(* Goal: @eq (list SplitPath) (@cons SplitPath s0 l0) (@cons (list SplitDirection) (@nil SplitDirection) (@nil (list SplitDirection))) *)
(* Goal: @eq RandomSeed s (f (@nil SplitDirection)) *)
Fixpoint listToTree (l : list SplitPath) (f : SplitPath -> RandomSeed)
        ( Pref : PrefixFree l) : {s : SeedTree | correspondingSeedTree l f s}.
Proof.
(* Goal: @sig SeedTree (fun s : SeedTree => correspondingSeedTree l f s) *)
induction l.
(* Goal: @sig SeedTree (fun s : SeedTree => correspondingSeedTree (@cons SplitPath a l) f s) *)
+ exists SeedTreeUndef. apply corrEmptyUndef.
(* Goal: @sig SeedTree (fun s : SeedTree => correspondingSeedTree (@cons SplitPath a l) f s) *)
+ remember Pref as Pref'. clear HeqPref'. apply PrefixFreeTail in Pref'.
(* Goal: @sig SeedTree (fun s : SeedTree => correspondingSeedTree (@cons SplitPath a l) f s) *)
  apply IHl in Pref'.
(* Goal: @sig SeedTree (fun s : SeedTree => correspondingSeedTree (@cons SplitPath a l) f s) *)
  inversion Pref'; clear Pref'.
(* Goal: @sig SeedTree (fun s : SeedTree => correspondingSeedTree (@cons SplitPath a l) f s) *)
  assert (forall p', In p' l -> forall p1 p2, a ++ p1 = p' ++ p2 -> False) by
      (inversion Pref; intros; subst; eapply H3; [eassumption |
    instantiate (1 := p1); instantiate (1 := p2); subst; auto]).
(* Goal: @sig SeedTree (fun s : SeedTree => correspondingSeedTree (@cons SplitPath a l) f s) *)
  exists (addToTree x a f l H H0).
(* Goal: correspondingSeedTree (@cons SplitPath a l) f (addToTree x a f l H H0) *)
  apply addToTreeCorrect.
Qed.

(* Goal: @eq (list SplitPath) (@cons SplitPath (@cons SplitDirection s1 s2) l0) (@cons (list SplitDirection) (@nil SplitDirection) (@nil (list SplitDirection))) *)
(* Goal: @eq RandomSeed s (f (@nil SplitDirection)) *)
(* begin SplitPathCompleteness *)
(* Goal: @eq (list SplitPath) (@cons SplitPath s0 l0) (@cons (list SplitDirection) (@nil SplitDirection) (@nil (list SplitDirection))) *)
(* Goal: @eq RandomSeed s (f (@nil SplitDirection)) *)
Theorem SplitPathCompleteness (l : list SplitPath) (f : SplitPath -> RandomSeed) :
(* Goal: @eq (list SplitPath) (@cons SplitPath s0 l0) (@cons (list SplitDirection) (@nil SplitDirection) (@nil (list SplitDirection))) *)
(* Goal: @eq RandomSeed s (f (@nil SplitDirection)) *)
  PrefixFree l -> exists (s : RandomSeed), forall p, In p l -> varySeed p s = f p.
(* Goal: @eq (list SplitPath) (@cons SplitPath (@cons SplitDirection s1 s2) l0) (@cons (list SplitDirection) (@nil SplitDirection) (@nil (list SplitDirection))) *)
(* Goal: @eq RandomSeed s (f (@nil SplitDirection)) *)
(* end SplitPathCompleteness *)
(* Goal: forall _ : PrefixFree l, @ex RandomSeed (fun s : RandomSeed => forall (p : SplitPath) (_ : @In SplitPath p l), @eq RandomSeed (varySeed p s) (f p)) *)
intros Pref.
(* Goal: @ex RandomSeed (fun s : RandomSeed => forall (p : SplitPath) (_ : @In SplitPath p l), @eq RandomSeed (varySeed p s) (f p)) *)
pose proof (listToTree l f Pref) as ExSeedTree.
(* Goal: @ex RandomSeed (fun s : RandomSeed => forall (p : SplitPath) (_ : @In SplitPath p l), @eq RandomSeed (varySeed p s) (f p)) *)
inversion ExSeedTree as [st Corr]; clear ExSeedTree.
(* Goal: @ex RandomSeed (fun s : RandomSeed => forall (p : SplitPath) (_ : @In SplitPath p l), @eq RandomSeed (varySeed p s) (f p)) *)
inversion Corr as [Vary_In In_Vary Pref']; clear Corr.
(* Goal: @ex RandomSeed (fun s : RandomSeed => forall (p : SplitPath) (_ : @In SplitPath p l), @eq RandomSeed (varySeed p s) (f p)) *)
pose proof (splitExpand st) as ExRst.
(* Goal: @ex RandomSeed (fun s : RandomSeed => forall (p : SplitPath) (_ : @In SplitPath p l), @eq RandomSeed (varySeed p s) (f p)) *)
inversion ExRst as [rst Sub]; clear ExRst.
(* Goal: @ex RandomSeed (fun s : RandomSeed => forall (p : SplitPath) (_ : @In SplitPath p l), @eq RandomSeed (varySeed p s) (f p)) *)
exists rst.
(* Goal: forall (p : SplitPath) (_ : @In SplitPath p l), @eq RandomSeed (varySeed p rst) (f p) *)
intros p InPL.
(* Goal: @eq RandomSeed (varySeed p rst) (f p) *)
pose proof (pathAgreesOnSubTree st (mkSeedTree rst) p (f p)) as Hyp.
(* Goal: @eq RandomSeed (varySeed p rst) (f p) *)
auto.
Qed.


(* Goal: @eq (list SplitPath) (@cons SplitPath (@cons SplitDirection s1 s2) l0) (@cons (list SplitDirection) (@nil SplitDirection) (@nil (list SplitDirection))) *)
(* Goal: @eq RandomSeed s (f (@nil SplitDirection)) *)
(* Primitive generator combinators and some basic soundness
(* Goal: @eq (list SplitPath) (@cons SplitPath (@cons SplitDirection s1 s2) l0) (@cons (list SplitDirection) (@nil SplitDirection) (@nil (list SplitDirection))) *)
(* Goal: @eq RandomSeed s (f (@nil SplitDirection)) *)
   assumptions about them *)
(* Goal: @eq (list SplitPath) (@cons SplitPath s0 l0) (@cons (list SplitDirection) (@nil SplitDirection) (@nil (list SplitDirection))) *)
(* Goal: @eq RandomSeed s (f (@nil SplitDirection)) *)
Axiom randomRBool : bool * bool -> RandomSeed -> bool * RandomSeed.
Axiom randomRBoolCorrect :
(* Goal: @eq (list SplitPath) (@cons SplitPath s0 l0) (@cons (list SplitDirection) (@nil SplitDirection) (@nil (list SplitDirection))) *)
(* Goal: @eq RandomSeed s (f (@nil SplitDirection)) *)
  forall b b1 b2, implb b1 b2 ->
(* Goal: @eq (list SplitPath) (@cons SplitPath s0 l0) (@cons (list SplitDirection) (@nil SplitDirection) (@nil (list SplitDirection))) *)
(* Goal: @eq RandomSeed s (f (@nil SplitDirection)) *)
    (implb b1 b && implb b b2 <->
    exists seed, (fst (randomRBool (b1, b2) seed)) = b).
(* Goal: @eq (list SplitPath) (@cons SplitPath s0 l0) (@cons (list SplitDirection) (@nil SplitDirection) (@nil (list SplitDirection))) *)
(* Goal: @eq RandomSeed s (f (@nil SplitDirection)) *)
Axiom randomRNat  : nat  * nat -> RandomSeed -> nat * RandomSeed.
Axiom randomRNatCorrect:
(* Goal: @eq (list SplitPath) (@cons SplitPath s0 l0) (@cons (list SplitDirection) (@nil SplitDirection) (@nil (list SplitDirection))) *)
(* Goal: @eq RandomSeed s (f (@nil SplitDirection)) *)
  forall n n1 n2, n1 <= n2 ->
(* Goal: @eq (list SplitPath) (@cons SplitPath s0 l0) (@cons (list SplitDirection) (@nil SplitDirection) (@nil (list SplitDirection))) *)
(* Goal: @eq RandomSeed s (f (@nil SplitDirection)) *)
    (n1 <= n <= n2 <->
    exists seed, (fst (randomRNat (n1, n2) seed)) = n).
(* Goal: @eq (list SplitPath) (@cons SplitPath s0 l0) (@cons (list SplitDirection) (@nil SplitDirection) (@nil (list SplitDirection))) *)
(* Goal: @eq RandomSeed s (f (@nil SplitDirection)) *)
Axiom randomRInt  : Z * Z    -> RandomSeed -> Z * RandomSeed.
Axiom randomRIntCorrect:
(* Goal: @eq (list SplitPath) (@cons SplitPath s0 l0) (@cons (list SplitDirection) (@nil SplitDirection) (@nil (list SplitDirection))) *)
(* Goal: @eq RandomSeed s (f (@nil SplitDirection)) *)
  forall z z1 z2, Z.leb z1 z2 ->
(* Goal: @eq (list SplitPath) (@cons SplitPath s0 l0) (@cons (list SplitDirection) (@nil SplitDirection) (@nil (list SplitDirection))) *)
(* Goal: @eq RandomSeed s (f (@nil SplitDirection)) *)
    (Z.leb z1 z && Z.leb z z2 <->
    exists seed, (fst (randomRInt (z1, z2) seed)) = z).
(* Goal: @eq (list SplitPath) (@cons SplitPath s0 l0) (@cons (list SplitDirection) (@nil SplitDirection) (@nil (list SplitDirection))) *)
(* Goal: @eq RandomSeed s (f (@nil SplitDirection)) *)
Axiom randomRN    : N * N    -> RandomSeed -> N * RandomSeed.
Axiom randomRNCorrect:
  forall n n1 n2,
(* Goal: @eq (list SplitPath) (@cons SplitPath s0 l0) (@cons (list SplitDirection) (@nil SplitDirection) (@nil (list SplitDirection))) *)
(* Goal: @eq RandomSeed s (f (@nil SplitDirection)) *)
    N.leb n1 n2 ->
(* Goal: @eq (list SplitPath) (@cons SplitPath s0 l0) (@cons (list SplitDirection) (@nil SplitDirection) (@nil (list SplitDirection))) *)
(* Goal: @eq RandomSeed s (f (@nil SplitDirection)) *)
    N.leb n1 n && N.leb n n2 <->
    exists seed, fst (randomRN (n1, n2) seed) = n.

(* Goal: @eq (list SplitPath) (@cons SplitPath (@cons SplitDirection s1 s2) l0) (@cons (list SplitDirection) (@nil SplitDirection) (@nil (list SplitDirection))) *)
(* Goal: @eq RandomSeed s (f (@nil SplitDirection)) *)
(* A small experiment showing that infinite random trees
(* Goal: @eq (list SplitPath) (@cons SplitPath (@cons SplitDirection s1 s2) l0) (@cons (list SplitDirection) (@nil SplitDirection) (@nil (list SplitDirection))) *)
(* Goal: @eq RandomSeed s (f (@nil SplitDirection)) *)
   are a potential model of the randomSplitAssumption *)

Module InfiniteTrees.
  CoInductive RandomSeed : Type :=
(* Goal: @eq (list SplitPath) (@cons SplitPath s0 l0) (@cons (list SplitDirection) (@nil SplitDirection) (@nil (list SplitDirection))) *)
(* Goal: @eq RandomSeed s (f (@nil SplitDirection)) *)
  | Node : bool -> RandomSeed -> RandomSeed -> RandomSeed.

  Definition randomSplit (s : RandomSeed) :=
    match s with
    | Node b s1 s2 => (s1,s2)
    end.

  Lemma randomSplitAssumption :
    forall s1 s2 : RandomSeed, exists s, randomSplit s = (s1,s2).
  Proof.
(* Goal: @antisymmetric N N.leb *)
    move => s1 s2. by exists (Node true s1 s2).
  Qed.
End InfiniteTrees.


(* Goal: @eq (list SplitPath) (@cons SplitPath (@cons SplitDirection s1 s2) l0) (@cons (list SplitDirection) (@nil SplitDirection) (@nil (list SplitDirection))) *)
(* Goal: @eq RandomSeed s (f (@nil SplitDirection)) *)
(* Type class machinery for generating things in intervals *)

Class OrdType (A: Type) :=
  {
(* Goal: @eq (list SplitPath) (@cons SplitPath s0 l0) (@cons (list SplitDirection) (@nil SplitDirection) (@nil (list SplitDirection))) *)
(* Goal: @eq RandomSeed s (f (@nil SplitDirection)) *)
    leq     : A -> A -> bool;
    refl    : reflexive leq;
    trans   : transitive leq;
    antisym : antisymmetric leq
  }.

Program Instance OrdBool : OrdType bool :=
  {
    leq b1 b2 := implb b1 b2
  }.
Next Obligation.
(* Goal: @antisymmetric bool (fun b1 b2 : bool => implb b1 b2) *)
  by case.
Qed.
Next Obligation.
(* Goal: @antisymmetric bool (fun b1 b2 : bool => implb b1 b2) *)
  by do 3! case.
Qed.
Next Obligation.
(* Goal: @antisymmetric bool (fun b1 b2 : bool => implb b1 b2) *)
  by do 2! case.
Qed.

Program Instance OrdNat : OrdType nat :=
  {
    leq := ssrnat.leq;
    refl := leqnn;
    trans := leq_trans;
    antisym := anti_leq
  }.

Program Instance OrdZ : OrdType Z :=
  {
    leq := Z.leb;
    refl := Z.leb_refl
  }.
Next Obligation.
(* Goal: @antisymmetric N N.leb *)
move=> x y z le_yx le_xz.
(* Goal: forall (_ : is_true (Z.leb x y)) (_ : is_true (Z.leb y x)), @eq Z x y *)
exact: (Zle_bool_trans y x z).
Qed.
Next Obligation.
(* Goal: @antisymmetric N N.leb *)
move=> x y /andP[].
(* Goal: forall (_ : is_true (Z.leb x y)) (_ : is_true (Z.leb y x)), @eq Z x y *)
exact: Zle_bool_antisym.
Qed.

Program Instance OrdN : OrdType N :=
  {
    leq := N.leb;
    refl := N.leb_refl
  }.
Next Obligation.
(* Goal: @antisymmetric N N.leb *)
  move=> x y z le_yx le_xz.
(* Goal: @eq (list SplitPath) (@cons SplitPath (@cons SplitDirection s1 s2) l0) (@cons (list SplitDirection) (@nil SplitDirection) (@nil (list SplitDirection))) *)
(* Goal: @eq RandomSeed s (f (@nil SplitDirection)) *)
  unfold is_true in *.
(* Goal: @eq bool (N.leb y z) true *)
  apply N.leb_le in le_yx.
(* Goal: @eq bool (N.leb y z) true *)
  apply N.leb_le in le_xz.
(* Goal: @eq bool (N.leb y z) true *)
  apply N.leb_le.
(* Goal: @eq RandomSeed (varySeed p rst) (f p) *)
  eapply N.le_trans; eauto.
Qed.
Next Obligation.
(* Goal: @antisymmetric N N.leb *)
  move=> x y /andP[].
(* Goal: forall (_ : is_true (N.leb x y)) (_ : is_true (N.leb y x)), @eq N x y *)
  unfold is_true.
(* Goal: forall (_ : @eq bool (N.leb x y) true) (_ : @eq bool (N.leb y x) true), @eq N x y *)
  repeat rewrite N.leb_le.
(* Goal: forall (_ : N.le x y) (_ : N.le y x), @eq N x y *)
  intros.
(* Goal: @eq RandomSeed (varySeed p rst) (f p) *)
  apply N.le_antisymm; auto.
Qed.

Class ChoosableFromInterval (A : Type)  :=
  {
    super :> OrdType A;
(* Goal: @eq (list SplitPath) (@cons SplitPath s0 l0) (@cons (list SplitDirection) (@nil SplitDirection) (@nil (list SplitDirection))) *)
(* Goal: @eq RandomSeed s (f (@nil SplitDirection)) *)
    randomR : A * A -> RandomSeed -> A * RandomSeed;
    randomRCorrect :
(* Goal: @eq (list SplitPath) (@cons SplitPath s0 l0) (@cons (list SplitDirection) (@nil SplitDirection) (@nil (list SplitDirection))) *)
(* Goal: @eq RandomSeed s (f (@nil SplitDirection)) *)
      forall (a a1 a2 : A), leq a1 a2 ->
(* Goal: @eq (list SplitPath) (@cons SplitPath s0 l0) (@cons (list SplitDirection) (@nil SplitDirection) (@nil (list SplitDirection))) *)
(* Goal: @eq RandomSeed s (f (@nil SplitDirection)) *)
      (leq a1 a && leq a a2 <->
       exists seed, fst (randomR (a1, a2) seed) = a)
  }.

Program Instance ChooseBool : ChoosableFromInterval bool :=
  {
    randomR := randomRBool;
    randomRCorrect := randomRBoolCorrect
  }.

Instance ChooseNat : ChoosableFromInterval nat :=
  {
    randomR := randomRNat;
    randomRCorrect := randomRNatCorrect
  }.

Instance ChooseZ : ChoosableFromInterval Z :=
  {
    randomR := randomRInt;
    randomRCorrect := randomRIntCorrect
  }.

Instance ChooseN : ChoosableFromInterval N :=
  {
    randomR := randomRN;
    randomRCorrect := randomRNCorrect
  }.
