Require Import Coq.Arith.Arith.
Require Import Coq.Logic.ProofIrrelevance.
Require Import Omega.

Inductive game : Set :=
 | gameCons : gamelist -> gamelist -> game
with gamelist : Set :=
 | emptylist : gamelist
 | listCons : game -> gamelist -> gamelist.

Fixpoint measGame (g1 : game) : nat :=
  match g1 with
  | gameCons gl1 gl2 => S (measGameList gl1 + measGameList gl2)
  end
with measGameList (gl1 : gamelist) : nat :=
  match gl1 with
  | emptylist       => 0
  | listCons g1 gl2 => S (measGame g1 + measGameList gl2)
  end.

Definition side :=
 game -> gamelist.

Definition leftSide (g : game) : gamelist :=
 match g with
  | gameCons gll glr => gll
 end.

Definition rightSide (g : game) : gamelist :=
 match g with
  | gameCons gll glr => glr
 end.

Inductive compare_quest : Set :=
 | lessOrEq : compare_quest
 | greatOrEq : compare_quest
 | lessOrConf : compare_quest
 | greatOrConf : compare_quest.

Definition g1side (c : compare_quest) : side :=
 match c with
  | lessOrEq => leftSide
  | greatOrEq => rightSide
  | lessOrConf => rightSide
  | greatOrConf => leftSide
 end.

Definition g2side (c : compare_quest) : side :=
 match c with 
  | lessOrEq => rightSide
  | greatOrEq => leftSide
  | lessOrConf => leftSide
  | greatOrConf => rightSide
 end.

Definition combiner :=
 Prop -> Prop -> Prop.

Definition compareCombiner (c : compare_quest) : combiner :=
 match c with
  | lessOrEq => and
  | greatOrEq => and
  | lessOrConf => or
  | greatOrConf => or
 end.

Definition nextCompare (c : compare_quest) : compare_quest :=
 match c with
  | lessOrEq => lessOrConf
  | greatOrEq => greatOrConf
  | lessOrConf => lessOrEq
  | greatOrConf => greatOrEq
 end.

Definition cbn_init (cbn : combiner) : Prop :=
 ~ (cbn False True).

Inductive gameCompareDom : compare_quest ->  game -> game -> Prop :=
  | gameCompareDom1 : forall c g1 g2, innerGCompareDom (nextCompare c) (compareCombiner c) g1 (g1side c g1) g2 (g2side c g2) -> gameCompareDom c g1 g2

with innerGCompareDom : compare_quest -> combiner -> game -> gamelist -> game -> gamelist -> Prop :=
  | innerGCompareDom1 : forall next_c cbn g1 g1s g2 g2s, listGameCompareDom next_c cbn g1s g2 -> gameListCompareDom next_c cbn g1 g2s -> innerGCompareDom next_c cbn g1 g1s g2 g2s

with listGameCompareDom : compare_quest -> combiner -> gamelist -> game -> Prop :=
  | listGameCompareDom1 : forall c cbn g1s g2, g1s = emptylist -> listGameCompareDom c cbn g1s g2
  | listGameCompareDom2 : forall c cbn g1s g2 g1s_car g1s_cdr, g1s = listCons g1s_car g1s_cdr -> gameCompareDom c g1s_car g2 -> listGameCompareDom c cbn g1s_cdr g2 -> listGameCompareDom c cbn g1s g2

with gameListCompareDom : compare_quest -> combiner -> game -> gamelist -> Prop :=
  | gameListCompareDom1 : forall c cbn g1 g2s, g2s = emptylist -> gameListCompareDom c cbn g1 g2s
  | gameListCompareDom2 : forall c cbn g1 g2s g2s_car g2s_cdr, g2s = listCons g2s_car g2s_cdr -> gameCompareDom c g1 g2s_car -> gameListCompareDom c cbn g1 g2s_cdr -> gameListCompareDom c cbn g1 g2s.

Lemma gameCompareDom1Inv : forall c g1 g2, gameCompareDom c g1 g2 -> innerGCompareDom (nextCompare c) (compareCombiner c) g1 (g1side c g1) g2 (g2side c g2).
Proof.
intros. inversion H. apply H0.
Defined.

Lemma innerGCompareDom1Inv1 : forall next_c cbn g1 g1s g2 g2s, innerGCompareDom next_c cbn g1 g1s g2 g2s -> listGameCompareDom next_c cbn g1s g2.
Proof.
intros. inversion H. apply H0.
Defined.

Lemma innerGCompareDom1Inv2 : forall next_c cbn g1 g1s g2 g2s, innerGCompareDom next_c cbn g1 g1s g2 g2s -> gameListCompareDom next_c cbn g1 g2s.
Proof.
intros. inversion H. apply H1.
Defined.

Lemma listGameCompareDom2Inv1 : forall c cbn g1s g2 g1s_car g1s_cdr, listGameCompareDom c cbn g1s g2 -> g1s = listCons g1s_car g1s_cdr -> gameCompareDom c g1s_car g2.
Proof.
intros. subst. inversion H.
  inversion H0.
  inversion H0. apply H1.
Defined.

Lemma listGameCompareDom2Inv2 : forall c cbn g1s g2 g1s_car g1s_cdr, listGameCompareDom c cbn g1s g2 -> g1s = listCons g1s_car g1s_cdr -> listGameCompareDom c cbn g1s_cdr g2.
Proof.
intros. subst. inversion H.
  inversion H0.
  inversion H0. apply H2.
Defined.

Lemma gameListCompareDom2Inv1 : forall c cbn g1 g2s g2s_car g2s_cdr, gameListCompareDom c cbn g1 g2s -> g2s = listCons g2s_car g2s_cdr -> gameCompareDom c g1 g2s_car.
Proof.
intros. subst. inversion H.
  inversion H0.
  inversion H0. apply H1.
Defined.

Lemma gameListCompareDom2Inv2 : forall c cbn g1 g2s g2s_car g2s_cdr, gameListCompareDom c cbn g1 g2s -> g2s = listCons g2s_car g2s_cdr -> gameListCompareDom c cbn g1 g2s_cdr.
Proof.
intros. subst. inversion H.
  inversion H0.
  inversion H0. apply H2.
Defined.

Fixpoint gameCompareAux (c : compare_quest) (g1 : game) (g2 : game) (H1 : gameCompareDom c g1 g2) : Prop :=
  innerGCompareAux (nextCompare c) (compareCombiner c) g1 (g1side c g1) g2 (g2side c g2) (gameCompareDom1Inv _ _ _ H1)

with innerGCompareAux (next_c : compare_quest) (cbn : combiner) (g1 : game) (g1s : gamelist) (g2 : game) (g2s : gamelist) (H1 : innerGCompareDom next_c cbn g1 g1s g2 g2s) : Prop :=
  cbn (listGameCompareAux next_c cbn g1s g2 (innerGCompareDom1Inv1 _ _ _ _ _ _ H1)) (gameListCompareAux next_c cbn g1 g2s (innerGCompareDom1Inv2 _ _ _ _ _ _ H1))

with listGameCompareAux (c : compare_quest) (cbn : combiner) (g1s : gamelist) (g2 : game) (H1 : listGameCompareDom c cbn g1s g2) : Prop :=
  match g1s as gl1 return g1s = gl1 -> Prop with
  | emptylist                => fun H2 => cbn_init cbn
  | listCons g1s_car g1s_cdr => fun H2 => cbn (gameCompareAux c g1s_car g2 (listGameCompareDom2Inv1 _ _ _ _ _ _ H1 H2)) (listGameCompareAux c cbn g1s_cdr g2 (listGameCompareDom2Inv2 _ _ _ _ _ _ H1 H2))
  end eq_refl

with gameListCompareAux (c : compare_quest) (cbn : combiner) (g1 : game) (g2s : gamelist) (H1 : gameListCompareDom c cbn g1 g2s) : Prop :=
  match g2s as gl1 return g2s = gl1 -> Prop with
  | emptylist                => fun H2 => cbn_init cbn
  | listCons g2s_car g2s_cdr => fun H2 => cbn (gameCompareAux c g1 g2s_car (gameListCompareDom2Inv1 _ _ _ _ _ _ H1 H2)) (gameListCompareAux c cbn g1 g2s_cdr (gameListCompareDom2Inv2 _ _ _ _ _ _ H1 H2))
  end eq_refl.

Lemma Triv1 : forall n1 n2 n3 n4 n5 n6, n1 + n2 + n3 + n6 < n1 + n2 + S (S (n3 + n4 + n5)) + n6.
Proof. intros. omega. Qed.

Lemma Triv2 : forall n1 n2 n3 n4 n5 n6, n1 + n2 + n4 + n6 < n1 + n2 + S (S (n3 + n4 + n5)) + n6.
Proof. intros. omega. Qed.

Lemma Triv3 : forall n1 n2 n3 n4 n5 n6, n1 + n2 + n3 + n4 < n2 + S (n5 + n4) + S (n1 + n6) + n3.
Proof. intros. omega. Qed.

Lemma Triv4 : forall n1 n2 n3 n4 n5 n6, n1 + n2 + n3 + n4 < n2 + S (n4 + n5) + S (n1 + n3) + n6.
Proof. intros. omega. Qed.

Lemma Triv5 : forall n1 n2 n3 n4 n5, n1 + n2 + n3 + n4 < n1 + n2 + S (n5 + n3) + n4.
Proof. intros. omega. Qed.

Lemma Triv6 : forall n1 n2 n3 n4 n5 n6, n1 + n2 + n3 + n4 < S (n3 + n5 + n1 + n6 + S (n2 + n4)).
Proof. intros. omega. Qed.

Lemma Triv7 : forall n1 n2 n3 n4 n5 n6, n1 + n2 + n3 + n4 < S (n5 + n3 + n1 + n6 + S (n2 + n4)).
Proof. intros. omega. Qed.

Lemma Triv8 : forall n1 n2 n3 n4 n5 n6, n1 + n2 + n3 + n4 < n1 + n2 + n3 + S (S (n5 + n4 + n6)).
Proof. intros. omega. Qed.

Lemma Triv9 : forall n1 n2 n3 n4 n5 n6, n1 + n2 + n3 + n4 < n1 + n2 + n3 + S (S (n4 + n5 + n6)).
Proof. intros. omega. Qed.

Lemma Triv10 : forall n1 n2 n3 n4 n5, n1 + n2 + n3 + n4 < n1 + n2 + n3 + S (n5 + n4).
Proof. intros. omega. Qed.

Lemma listGameGameListCompareTot : forall g1 g2 g1s g2s,
  (forall c cbn, listGameCompareDom c cbn g1s g2) /\
  (forall c cbn, gameListCompareDom c cbn g1 g2s).
Proof.
intros.
remember (measGame g1 + measGame g2 + measGameList g1s + measGameList g2s) as n1.
revert g1 g2 g1s g2s Heqn1.
induction n1 using lt_wf_ind.
intros.
subst.
split.

  intros.
  destruct g1s.

    apply listGameCompareDom1.
    apply eq_refl.

    eapply listGameCompareDom2.

      apply eq_refl.

      apply gameCompareDom1.
      apply innerGCompareDom1.

        destruct g.
        destruct c.

          simpl in *.
          assert (H2 := H (measGame g1 + measGame g2 + measGameList g + measGameList g2s) (Triv1 _ _ _ _ _ _) _ _ _ _ eq_refl).
          inversion H2 as [H3 H4].
          apply H3.

          simpl in *.
          assert (H2 := H (measGame g1 + measGame g2 + measGameList g0 + measGameList g2s) (Triv2 _ _ _ _ _ _) _ _ _ _ eq_refl).
          inversion H2 as [H3 H4].
          apply H3.

          simpl in *.
          assert (H2 := H (measGame g1 + measGame g2 + measGameList g0 + measGameList g2s) (Triv2 _ _ _ _ _ _) _ _ _ _ eq_refl).
          inversion H2 as [H3 H4].
          apply H3.

          simpl in *.
          assert (H2 := H (measGame g1 + measGame g2 + measGameList g + measGameList g2s) (Triv1 _ _ _ _ _ _) _ _ _ _ eq_refl).
          inversion H2 as [H3 H4].
          apply H3.

        destruct g2.
        destruct c.

          simpl in *.
          assert (H2 := H (measGame g + measGame g1 + measGameList g2s + measGameList g2) (Triv3 _ _ _ _ _ _) _ _ _ _ eq_refl).
          inversion H2 as [H3 H4].
          apply H4.

          simpl in *.
          assert (H2 := H (measGame g + measGame g1 + measGameList g1s + measGameList g0) (Triv4 _ _ _ _ _ _) _ _ _ _ eq_refl).
          inversion H2 as [H3 H4].
          apply H4.

          simpl in *.
          assert (H2 := H (measGame g + measGame g1 + measGameList g1s + measGameList g0) (Triv4 _ _ _ _ _ _) _ _ _ _ eq_refl).
          inversion H2 as [H3 H4].
          apply H4.

          simpl in *.
          assert (H2 := H (measGame g + measGame g1 + measGameList g2s + measGameList g2) (Triv3 _ _ _ _ _ _) _ _ _ _ eq_refl).
          inversion H2 as [H3 H4].
          apply H4.

      simpl in *.
      assert (H2 := H (measGame g1 + measGame g2 + measGameList g1s + measGameList g2s) (Triv5 _ _ _ _ _) _ _ _ _ eq_refl).
      inversion H2 as [H3 H4].
      apply H3.

  intros.
  destruct g2s.

    apply gameListCompareDom1.
    apply eq_refl.

    eapply gameListCompareDom2.

      apply eq_refl.

      apply gameCompareDom1.
      apply innerGCompareDom1.

        destruct g1.
        destruct c.

          simpl in *.
          assert (H2 := H (measGame g2 + measGame g + measGameList g0 + measGameList g2s) (Triv6 _ _ _ _ _ _) _ _ _ _ eq_refl).
          inversion H2 as [H3 H4].
          apply H3.

          simpl in *.
          assert (H2 := H (measGame g2 + measGame g + measGameList g1 + measGameList g2s) (Triv7 _ _ _ _ _ _) _ _ _ _ eq_refl).
          inversion H2 as [H3 H4].
          apply H3.

          simpl in *.
          assert (H2 := H (measGame g2 + measGame g + measGameList g1 + measGameList g2s) (Triv7 _ _ _ _ _ _) _ _ _ _ eq_refl).
          inversion H2 as [H3 H4].
          apply H3.

          simpl in *.
          assert (H2 := H (measGame g2 + measGame g + measGameList g0 + measGameList g2s) (Triv6 _ _ _ _ _ _) _ _ _ _ eq_refl).
          inversion H2 as [H3 H4].
          apply H3.

        destruct g.
        destruct c.

          simpl in *.
          assert (H2 := H (measGame g1 + measGame g2 + measGameList g1s + measGameList g0) (Triv8 _ _ _ _ _ _) _ _ _ _ eq_refl).
          inversion H2 as [H3 H4].
          apply H4.

          simpl in *.
          assert (H2 := H (measGame g1 + measGame g2 + measGameList g1s + measGameList g) (Triv9 _ _ _ _ _ _) _ _ _ _ eq_refl).
          inversion H2 as [H3 H4].
          apply H4.

          simpl in *.
          assert (H2 := H (measGame g1 + measGame g2 + measGameList g1s + measGameList g) (Triv9 _ _ _ _ _ _) _ _ _ _ eq_refl).
          inversion H2 as [H3 H4].
          apply H4.

          simpl in *.
          assert (H2 := H (measGame g1 + measGame g2 + measGameList g1s + measGameList g0) (Triv8 _ _ _ _ _ _) _ _ _ _ eq_refl).
          inversion H2 as [H3 H4].
          apply H4.

      simpl in *.
      assert (H2 := H (measGame g1 + measGame g2 + measGameList g1s + measGameList g2s) (Triv10 _ _ _ _ _) _ _ _ _ eq_refl).
      inversion H2 as [H3 H4].
      apply H4.
Qed.

Lemma listGameCompareTot : forall g2 g1s c cbn,
  listGameCompareDom c cbn g1s g2.
Proof.
intros.
apply (listGameGameListCompareTot g2 g2 g1s g1s).
Qed.

Lemma gameListCompareTot : forall g1 g2s c cbn,
  gameListCompareDom c cbn g1 g2s.
Proof.
intros.
apply (listGameGameListCompareTot g1 g1 g2s g2s).
Qed.

Lemma innerGCompareTot : forall next_c cbn g1 g1s g2 g2s,
  innerGCompareDom next_c cbn g1 g1s g2 g2s.
Proof.
intros.
apply innerGCompareDom1.

  apply listGameCompareTot.

  apply gameListCompareTot.
Qed.

Lemma gameCompareTot : forall c g1 g2, gameCompareDom c g1 g2.
Proof.
intros.
apply gameCompareDom1.
apply innerGCompareTot.
Qed.

Definition gameCompare (c : compare_quest) (g1 : game) (g2 : game) : Prop :=
  gameCompareAux c g1 g2 (gameCompareTot _ _ _).

Definition innerGCompare (next_c : compare_quest) (cbn : combiner) (g1 : game) (g1s : gamelist) (g2 : game) (g2s : gamelist) : Prop :=
  innerGCompareAux next_c cbn g1 g1s g2 g2s (innerGCompareTot _ _ _ _ _ _).

Definition listGameCompare (c : compare_quest) (cbn : combiner) (g1s : gamelist) (g2 : game) : Prop :=
  listGameCompareAux c cbn g1s g2 (listGameCompareTot _ _ _ _).

Definition gameListCompare (c : compare_quest) (cbn : combiner) (g1 : game) (g2s : gamelist) : Prop :=
  gameListCompareAux c cbn g1 g2s (gameListCompareTot _ _ _ _).

Lemma gameCompareEq : forall c g1 g2, gameCompare c g1 g2 =
  innerGCompare (nextCompare c) (compareCombiner c) g1 (g1side c g1) g2 (g2side c g2).
Proof.
intros.
unfold gameCompare.
unfold innerGCompare.
destruct (gameCompareTot c g1 g2).
simpl.
apply f_equal.
apply proof_irrelevance.
Qed.

Lemma innerGCompareEq : forall next_c cbn g1 g1s g2 g2s, innerGCompare next_c cbn g1 g1s g2 g2s =
  cbn (listGameCompare next_c cbn g1s g2) (gameListCompare next_c cbn g1 g2s).
Proof.
intros.
unfold innerGCompare.
unfold listGameCompare.
unfold gameListCompare.
destruct (innerGCompareTot next_c cbn g1 g1s g2 g2s).
simpl.
assert (H1 : cbn (listGameCompareAux next_c cbn g1s g2 l) = cbn (listGameCompareAux next_c cbn g1s g2 (listGameCompareTot g2 g1s next_c cbn))).

  apply f_equal.
  apply f_equal.
  apply proof_irrelevance.

  rewrite H1.
  apply f_equal.
  apply f_equal.
  apply proof_irrelevance.
Qed.

Lemma listGameCompareEq : forall c cbn g1s g2, listGameCompare c cbn g1s g2 =
  match g1s with
  | emptylist                => cbn_init cbn
  | listCons g1s_car g1s_cdr => cbn (gameCompare c g1s_car g2) (listGameCompare c cbn g1s_cdr g2)
  end.
Proof.
intros.
unfold listGameCompare.
unfold gameCompare.
destruct (listGameCompareTot g2 g1s c cbn).

  simpl.
  rewrite e.
  apply eq_refl.

  simpl.
  rewrite e.
  assert (H1 : cbn (gameCompareAux c g1s_car g2 (listGameCompareDom2Inv1 c cbn (listCons g1s_car g1s_cdr) g2 g1s_car g1s_cdr (listGameCompareDom2 c cbn (listCons g1s_car g1s_cdr) g2 g1s_car g1s_cdr eq_refl g l) eq_refl)) = cbn (gameCompareAux c g1s_car g2 (gameCompareTot c g1s_car g2))).

    apply f_equal.
    apply f_equal.
    apply proof_irrelevance.

    rewrite H1.
    apply f_equal.
    apply f_equal.
    apply proof_irrelevance.
Qed.

Lemma gameListCompareEq : forall c cbn g1 g2s, gameListCompare c cbn g1 g2s =
  match g2s with
  | emptylist                => cbn_init cbn
  | listCons g2s_car g2s_cdr => cbn (gameCompare c g1 g2s_car) (gameListCompare c cbn g1 g2s_cdr)
  end.
Proof.
intros.
unfold gameListCompare.
unfold gameCompare.
destruct (gameListCompareTot g1 g2s c cbn).

  simpl.
  rewrite e.
  apply eq_refl.

  simpl.
  rewrite e.
  assert (H1 : cbn (gameCompareAux c g1 g2s_car (gameListCompareDom2Inv1 c cbn g1 (listCons g2s_car g2s_cdr) g2s_car g2s_cdr (gameListCompareDom2 c cbn g1 (listCons g2s_car g2s_cdr) g2s_car g2s_cdr eq_refl g g0) eq_refl)) = cbn (gameCompareAux c g1 g2s_car (gameCompareTot c g1 g2s_car))).

    apply f_equal.
    apply f_equal.
    apply proof_irrelevance.

    rewrite H1.
    apply f_equal.
    apply f_equal.
    apply proof_irrelevance.
Qed.

Definition game_eq (g1 : game) (g2 : game) : Prop :=
 (gameCompare lessOrEq g1 g2) /\ (gameCompare greatOrEq g1 g2).