Want more features on Pastebin? Sign Up, it's FREE!
Guest

Untitled

By: a guest on Jul 16th, 2013  |  syntax: None  |  size: 16.07 KB  |  views: 38  |  expires: Never
download  |  raw  |  embed  |  report abuse  |  print
Text below is selected. Please press Ctrl+C to copy to your clipboard. (⌘+C on Mac)
  1. Require Import Coq.Arith.Arith.
  2. Require Import Coq.Logic.ProofIrrelevance.
  3. Require Import Omega.
  4.  
  5. Inductive game : Set :=
  6.  | gameCons : gamelist -> gamelist -> game
  7. with gamelist : Set :=
  8.  | emptylist : gamelist
  9.  | listCons : game -> gamelist -> gamelist.
  10.  
  11. Fixpoint measGame (g1 : game) : nat :=
  12.   match g1 with
  13.   | gameCons gl1 gl2 => S (measGameList gl1 + measGameList gl2)
  14.   end
  15. with measGameList (gl1 : gamelist) : nat :=
  16.   match gl1 with
  17.   | emptylist       => 0
  18.   | listCons g1 gl2 => S (measGame g1 + measGameList gl2)
  19.   end.
  20.  
  21. Definition side :=
  22.  game -> gamelist.
  23.  
  24. Definition leftSide (g : game) : gamelist :=
  25.  match g with
  26.   | gameCons gll glr => gll
  27.  end.
  28.  
  29. Definition rightSide (g : game) : gamelist :=
  30.  match g with
  31.   | gameCons gll glr => glr
  32.  end.
  33.  
  34. Inductive compare_quest : Set :=
  35.  | lessOrEq : compare_quest
  36.  | greatOrEq : compare_quest
  37.  | lessOrConf : compare_quest
  38.  | greatOrConf : compare_quest.
  39.  
  40. Definition g1side (c : compare_quest) : side :=
  41.  match c with
  42.   | lessOrEq => leftSide
  43.   | greatOrEq => rightSide
  44.   | lessOrConf => rightSide
  45.   | greatOrConf => leftSide
  46.  end.
  47.  
  48. Definition g2side (c : compare_quest) : side :=
  49.  match c with
  50.   | lessOrEq => rightSide
  51.   | greatOrEq => leftSide
  52.   | lessOrConf => leftSide
  53.   | greatOrConf => rightSide
  54.  end.
  55.  
  56. Definition combiner :=
  57.  Prop -> Prop -> Prop.
  58.  
  59. Definition compareCombiner (c : compare_quest) : combiner :=
  60.  match c with
  61.   | lessOrEq => and
  62.   | greatOrEq => and
  63.   | lessOrConf => or
  64.   | greatOrConf => or
  65.  end.
  66.  
  67. Definition nextCompare (c : compare_quest) : compare_quest :=
  68.  match c with
  69.   | lessOrEq => lessOrConf
  70.   | greatOrEq => greatOrConf
  71.   | lessOrConf => lessOrEq
  72.   | greatOrConf => greatOrEq
  73.  end.
  74.  
  75. Definition cbn_init (cbn : combiner) : Prop :=
  76.  ~ (cbn False True).
  77.  
  78. Inductive gameCompareDom : compare_quest ->  game -> game -> Prop :=
  79.   | gameCompareDom1 : forall c g1 g2, innerGCompareDom (nextCompare c) (compareCombiner c) g1 (g1side c g1) g2 (g2side c g2) -> gameCompareDom c g1 g2
  80.  
  81. with innerGCompareDom : compare_quest -> combiner -> game -> gamelist -> game -> gamelist -> Prop :=
  82.   | 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
  83.  
  84. with listGameCompareDom : compare_quest -> combiner -> gamelist -> game -> Prop :=
  85.   | listGameCompareDom1 : forall c cbn g1s g2, g1s = emptylist -> listGameCompareDom c cbn g1s g2
  86.   | 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
  87.  
  88. with gameListCompareDom : compare_quest -> combiner -> game -> gamelist -> Prop :=
  89.   | gameListCompareDom1 : forall c cbn g1 g2s, g2s = emptylist -> gameListCompareDom c cbn g1 g2s
  90.   | 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.
  91.  
  92. Lemma gameCompareDom1Inv : forall c g1 g2, gameCompareDom c g1 g2 -> innerGCompareDom (nextCompare c) (compareCombiner c) g1 (g1side c g1) g2 (g2side c g2).
  93. Proof.
  94. intros. inversion H. apply H0.
  95. Defined.
  96.  
  97. Lemma innerGCompareDom1Inv1 : forall next_c cbn g1 g1s g2 g2s, innerGCompareDom next_c cbn g1 g1s g2 g2s -> listGameCompareDom next_c cbn g1s g2.
  98. Proof.
  99. intros. inversion H. apply H0.
  100. Defined.
  101.  
  102. Lemma innerGCompareDom1Inv2 : forall next_c cbn g1 g1s g2 g2s, innerGCompareDom next_c cbn g1 g1s g2 g2s -> gameListCompareDom next_c cbn g1 g2s.
  103. Proof.
  104. intros. inversion H. apply H1.
  105. Defined.
  106.  
  107. 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.
  108. Proof.
  109. intros. subst. inversion H.
  110.   inversion H0.
  111.   inversion H0. apply H1.
  112. Defined.
  113.  
  114. 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.
  115. Proof.
  116. intros. subst. inversion H.
  117.   inversion H0.
  118.   inversion H0. apply H2.
  119. Defined.
  120.  
  121. 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.
  122. Proof.
  123. intros. subst. inversion H.
  124.   inversion H0.
  125.   inversion H0. apply H1.
  126. Defined.
  127.  
  128. 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.
  129. Proof.
  130. intros. subst. inversion H.
  131.   inversion H0.
  132.   inversion H0. apply H2.
  133. Defined.
  134.  
  135. Fixpoint gameCompareAux (c : compare_quest) (g1 : game) (g2 : game) (H1 : gameCompareDom c g1 g2) : Prop :=
  136.   innerGCompareAux (nextCompare c) (compareCombiner c) g1 (g1side c g1) g2 (g2side c g2) (gameCompareDom1Inv _ _ _ H1)
  137.  
  138. 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 :=
  139.   cbn (listGameCompareAux next_c cbn g1s g2 (innerGCompareDom1Inv1 _ _ _ _ _ _ H1)) (gameListCompareAux next_c cbn g1 g2s (innerGCompareDom1Inv2 _ _ _ _ _ _ H1))
  140.  
  141. with listGameCompareAux (c : compare_quest) (cbn : combiner) (g1s : gamelist) (g2 : game) (H1 : listGameCompareDom c cbn g1s g2) : Prop :=
  142.   match g1s as gl1 return g1s = gl1 -> Prop with
  143.   | emptylist                => fun H2 => cbn_init cbn
  144.   | 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))
  145.   end eq_refl
  146.  
  147. with gameListCompareAux (c : compare_quest) (cbn : combiner) (g1 : game) (g2s : gamelist) (H1 : gameListCompareDom c cbn g1 g2s) : Prop :=
  148.   match g2s as gl1 return g2s = gl1 -> Prop with
  149.   | emptylist                => fun H2 => cbn_init cbn
  150.   | 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))
  151.   end eq_refl.
  152.  
  153. Lemma Triv1 : forall n1 n2 n3 n4 n5 n6, n1 + n2 + n3 + n6 < n1 + n2 + S (S (n3 + n4 + n5)) + n6.
  154. Proof. intros. omega. Qed.
  155.  
  156. Lemma Triv2 : forall n1 n2 n3 n4 n5 n6, n1 + n2 + n4 + n6 < n1 + n2 + S (S (n3 + n4 + n5)) + n6.
  157. Proof. intros. omega. Qed.
  158.  
  159. Lemma Triv3 : forall n1 n2 n3 n4 n5 n6, n1 + n2 + n3 + n4 < n2 + S (n5 + n4) + S (n1 + n6) + n3.
  160. Proof. intros. omega. Qed.
  161.  
  162. Lemma Triv4 : forall n1 n2 n3 n4 n5 n6, n1 + n2 + n3 + n4 < n2 + S (n4 + n5) + S (n1 + n3) + n6.
  163. Proof. intros. omega. Qed.
  164.  
  165. Lemma Triv5 : forall n1 n2 n3 n4 n5, n1 + n2 + n3 + n4 < n1 + n2 + S (n5 + n3) + n4.
  166. Proof. intros. omega. Qed.
  167.  
  168. Lemma Triv6 : forall n1 n2 n3 n4 n5 n6, n1 + n2 + n3 + n4 < S (n3 + n5 + n1 + n6 + S (n2 + n4)).
  169. Proof. intros. omega. Qed.
  170.  
  171. Lemma Triv7 : forall n1 n2 n3 n4 n5 n6, n1 + n2 + n3 + n4 < S (n5 + n3 + n1 + n6 + S (n2 + n4)).
  172. Proof. intros. omega. Qed.
  173.  
  174. Lemma Triv8 : forall n1 n2 n3 n4 n5 n6, n1 + n2 + n3 + n4 < n1 + n2 + n3 + S (S (n5 + n4 + n6)).
  175. Proof. intros. omega. Qed.
  176.  
  177. Lemma Triv9 : forall n1 n2 n3 n4 n5 n6, n1 + n2 + n3 + n4 < n1 + n2 + n3 + S (S (n4 + n5 + n6)).
  178. Proof. intros. omega. Qed.
  179.  
  180. Lemma Triv10 : forall n1 n2 n3 n4 n5, n1 + n2 + n3 + n4 < n1 + n2 + n3 + S (n5 + n4).
  181. Proof. intros. omega. Qed.
  182.  
  183. Lemma listGameGameListCompareTot : forall g1 g2 g1s g2s,
  184.   (forall c cbn, listGameCompareDom c cbn g1s g2) /\
  185.   (forall c cbn, gameListCompareDom c cbn g1 g2s).
  186. Proof.
  187. intros.
  188. remember (measGame g1 + measGame g2 + measGameList g1s + measGameList g2s) as n1.
  189. revert g1 g2 g1s g2s Heqn1.
  190. induction n1 using lt_wf_ind.
  191. intros.
  192. subst.
  193. split.
  194.  
  195.   intros.
  196.   destruct g1s.
  197.  
  198.     apply listGameCompareDom1.
  199.     apply eq_refl.
  200.  
  201.     eapply listGameCompareDom2.
  202.  
  203.       apply eq_refl.
  204.  
  205.       apply gameCompareDom1.
  206.       apply innerGCompareDom1.
  207.  
  208.         destruct g.
  209.         destruct c.
  210.  
  211.           simpl in *.
  212.           assert (H2 := H (measGame g1 + measGame g2 + measGameList g + measGameList g2s) (Triv1 _ _ _ _ _ _) _ _ _ _ eq_refl).
  213.           inversion H2 as [H3 H4].
  214.           apply H3.
  215.  
  216.           simpl in *.
  217.           assert (H2 := H (measGame g1 + measGame g2 + measGameList g0 + measGameList g2s) (Triv2 _ _ _ _ _ _) _ _ _ _ eq_refl).
  218.           inversion H2 as [H3 H4].
  219.           apply H3.
  220.  
  221.           simpl in *.
  222.           assert (H2 := H (measGame g1 + measGame g2 + measGameList g0 + measGameList g2s) (Triv2 _ _ _ _ _ _) _ _ _ _ eq_refl).
  223.           inversion H2 as [H3 H4].
  224.           apply H3.
  225.  
  226.           simpl in *.
  227.           assert (H2 := H (measGame g1 + measGame g2 + measGameList g + measGameList g2s) (Triv1 _ _ _ _ _ _) _ _ _ _ eq_refl).
  228.           inversion H2 as [H3 H4].
  229.           apply H3.
  230.  
  231.         destruct g2.
  232.         destruct c.
  233.  
  234.           simpl in *.
  235.           assert (H2 := H (measGame g + measGame g1 + measGameList g2s + measGameList g2) (Triv3 _ _ _ _ _ _) _ _ _ _ eq_refl).
  236.           inversion H2 as [H3 H4].
  237.           apply H4.
  238.  
  239.           simpl in *.
  240.           assert (H2 := H (measGame g + measGame g1 + measGameList g1s + measGameList g0) (Triv4 _ _ _ _ _ _) _ _ _ _ eq_refl).
  241.           inversion H2 as [H3 H4].
  242.           apply H4.
  243.  
  244.           simpl in *.
  245.           assert (H2 := H (measGame g + measGame g1 + measGameList g1s + measGameList g0) (Triv4 _ _ _ _ _ _) _ _ _ _ eq_refl).
  246.           inversion H2 as [H3 H4].
  247.           apply H4.
  248.  
  249.           simpl in *.
  250.           assert (H2 := H (measGame g + measGame g1 + measGameList g2s + measGameList g2) (Triv3 _ _ _ _ _ _) _ _ _ _ eq_refl).
  251.           inversion H2 as [H3 H4].
  252.           apply H4.
  253.  
  254.       simpl in *.
  255.       assert (H2 := H (measGame g1 + measGame g2 + measGameList g1s + measGameList g2s) (Triv5 _ _ _ _ _) _ _ _ _ eq_refl).
  256.       inversion H2 as [H3 H4].
  257.       apply H3.
  258.  
  259.   intros.
  260.   destruct g2s.
  261.  
  262.     apply gameListCompareDom1.
  263.     apply eq_refl.
  264.  
  265.     eapply gameListCompareDom2.
  266.  
  267.       apply eq_refl.
  268.  
  269.       apply gameCompareDom1.
  270.       apply innerGCompareDom1.
  271.  
  272.         destruct g1.
  273.         destruct c.
  274.  
  275.           simpl in *.
  276.           assert (H2 := H (measGame g2 + measGame g + measGameList g0 + measGameList g2s) (Triv6 _ _ _ _ _ _) _ _ _ _ eq_refl).
  277.           inversion H2 as [H3 H4].
  278.           apply H3.
  279.  
  280.           simpl in *.
  281.           assert (H2 := H (measGame g2 + measGame g + measGameList g1 + measGameList g2s) (Triv7 _ _ _ _ _ _) _ _ _ _ eq_refl).
  282.           inversion H2 as [H3 H4].
  283.           apply H3.
  284.  
  285.           simpl in *.
  286.           assert (H2 := H (measGame g2 + measGame g + measGameList g1 + measGameList g2s) (Triv7 _ _ _ _ _ _) _ _ _ _ eq_refl).
  287.           inversion H2 as [H3 H4].
  288.           apply H3.
  289.  
  290.           simpl in *.
  291.           assert (H2 := H (measGame g2 + measGame g + measGameList g0 + measGameList g2s) (Triv6 _ _ _ _ _ _) _ _ _ _ eq_refl).
  292.           inversion H2 as [H3 H4].
  293.           apply H3.
  294.  
  295.         destruct g.
  296.         destruct c.
  297.  
  298.           simpl in *.
  299.           assert (H2 := H (measGame g1 + measGame g2 + measGameList g1s + measGameList g0) (Triv8 _ _ _ _ _ _) _ _ _ _ eq_refl).
  300.           inversion H2 as [H3 H4].
  301.           apply H4.
  302.  
  303.           simpl in *.
  304.           assert (H2 := H (measGame g1 + measGame g2 + measGameList g1s + measGameList g) (Triv9 _ _ _ _ _ _) _ _ _ _ eq_refl).
  305.           inversion H2 as [H3 H4].
  306.           apply H4.
  307.  
  308.           simpl in *.
  309.           assert (H2 := H (measGame g1 + measGame g2 + measGameList g1s + measGameList g) (Triv9 _ _ _ _ _ _) _ _ _ _ eq_refl).
  310.           inversion H2 as [H3 H4].
  311.           apply H4.
  312.  
  313.           simpl in *.
  314.           assert (H2 := H (measGame g1 + measGame g2 + measGameList g1s + measGameList g0) (Triv8 _ _ _ _ _ _) _ _ _ _ eq_refl).
  315.           inversion H2 as [H3 H4].
  316.           apply H4.
  317.  
  318.       simpl in *.
  319.       assert (H2 := H (measGame g1 + measGame g2 + measGameList g1s + measGameList g2s) (Triv10 _ _ _ _ _) _ _ _ _ eq_refl).
  320.       inversion H2 as [H3 H4].
  321.       apply H4.
  322. Qed.
  323.  
  324. Lemma listGameCompareTot : forall g2 g1s c cbn,
  325.   listGameCompareDom c cbn g1s g2.
  326. Proof.
  327. intros.
  328. apply (listGameGameListCompareTot g2 g2 g1s g1s).
  329. Qed.
  330.  
  331. Lemma gameListCompareTot : forall g1 g2s c cbn,
  332.   gameListCompareDom c cbn g1 g2s.
  333. Proof.
  334. intros.
  335. apply (listGameGameListCompareTot g1 g1 g2s g2s).
  336. Qed.
  337.  
  338. Lemma innerGCompareTot : forall next_c cbn g1 g1s g2 g2s,
  339.   innerGCompareDom next_c cbn g1 g1s g2 g2s.
  340. Proof.
  341. intros.
  342. apply innerGCompareDom1.
  343.  
  344.   apply listGameCompareTot.
  345.  
  346.   apply gameListCompareTot.
  347. Qed.
  348.  
  349. Lemma gameCompareTot : forall c g1 g2, gameCompareDom c g1 g2.
  350. Proof.
  351. intros.
  352. apply gameCompareDom1.
  353. apply innerGCompareTot.
  354. Qed.
  355.  
  356. Definition gameCompare (c : compare_quest) (g1 : game) (g2 : game) : Prop :=
  357.   gameCompareAux c g1 g2 (gameCompareTot _ _ _).
  358.  
  359. Definition innerGCompare (next_c : compare_quest) (cbn : combiner) (g1 : game) (g1s : gamelist) (g2 : game) (g2s : gamelist) : Prop :=
  360.   innerGCompareAux next_c cbn g1 g1s g2 g2s (innerGCompareTot _ _ _ _ _ _).
  361.  
  362. Definition listGameCompare (c : compare_quest) (cbn : combiner) (g1s : gamelist) (g2 : game) : Prop :=
  363.   listGameCompareAux c cbn g1s g2 (listGameCompareTot _ _ _ _).
  364.  
  365. Definition gameListCompare (c : compare_quest) (cbn : combiner) (g1 : game) (g2s : gamelist) : Prop :=
  366.   gameListCompareAux c cbn g1 g2s (gameListCompareTot _ _ _ _).
  367.  
  368. Lemma gameCompareEq : forall c g1 g2, gameCompare c g1 g2 =
  369.   innerGCompare (nextCompare c) (compareCombiner c) g1 (g1side c g1) g2 (g2side c g2).
  370. Proof.
  371. intros.
  372. unfold gameCompare.
  373. unfold innerGCompare.
  374. destruct (gameCompareTot c g1 g2).
  375. simpl.
  376. apply f_equal.
  377. apply proof_irrelevance.
  378. Qed.
  379.  
  380. Lemma innerGCompareEq : forall next_c cbn g1 g1s g2 g2s, innerGCompare next_c cbn g1 g1s g2 g2s =
  381.   cbn (listGameCompare next_c cbn g1s g2) (gameListCompare next_c cbn g1 g2s).
  382. Proof.
  383. intros.
  384. unfold innerGCompare.
  385. unfold listGameCompare.
  386. unfold gameListCompare.
  387. destruct (innerGCompareTot next_c cbn g1 g1s g2 g2s).
  388. simpl.
  389. assert (H1 : cbn (listGameCompareAux next_c cbn g1s g2 l) = cbn (listGameCompareAux next_c cbn g1s g2 (listGameCompareTot g2 g1s next_c cbn))).
  390.  
  391.   apply f_equal.
  392.   apply f_equal.
  393.   apply proof_irrelevance.
  394.  
  395.   rewrite H1.
  396.   apply f_equal.
  397.   apply f_equal.
  398.   apply proof_irrelevance.
  399. Qed.
  400.  
  401. Lemma listGameCompareEq : forall c cbn g1s g2, listGameCompare c cbn g1s g2 =
  402.   match g1s with
  403.   | emptylist                => cbn_init cbn
  404.   | listCons g1s_car g1s_cdr => cbn (gameCompare c g1s_car g2) (listGameCompare c cbn g1s_cdr g2)
  405.   end.
  406. Proof.
  407. intros.
  408. unfold listGameCompare.
  409. unfold gameCompare.
  410. destruct (listGameCompareTot g2 g1s c cbn).
  411.  
  412.   simpl.
  413.   rewrite e.
  414.   apply eq_refl.
  415.  
  416.   simpl.
  417.   rewrite e.
  418.   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))).
  419.  
  420.     apply f_equal.
  421.     apply f_equal.
  422.     apply proof_irrelevance.
  423.  
  424.     rewrite H1.
  425.     apply f_equal.
  426.     apply f_equal.
  427.     apply proof_irrelevance.
  428. Qed.
  429.  
  430. Lemma gameListCompareEq : forall c cbn g1 g2s, gameListCompare c cbn g1 g2s =
  431.   match g2s with
  432.   | emptylist                => cbn_init cbn
  433.   | listCons g2s_car g2s_cdr => cbn (gameCompare c g1 g2s_car) (gameListCompare c cbn g1 g2s_cdr)
  434.   end.
  435. Proof.
  436. intros.
  437. unfold gameListCompare.
  438. unfold gameCompare.
  439. destruct (gameListCompareTot g1 g2s c cbn).
  440.  
  441.   simpl.
  442.   rewrite e.
  443.   apply eq_refl.
  444.  
  445.   simpl.
  446.   rewrite e.
  447.   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))).
  448.  
  449.     apply f_equal.
  450.     apply f_equal.
  451.     apply proof_irrelevance.
  452.  
  453.     rewrite H1.
  454.     apply f_equal.
  455.     apply f_equal.
  456.     apply proof_irrelevance.
  457. Qed.
  458.  
  459. Definition game_eq (g1 : game) (g2 : game) : Prop :=
  460.  (gameCompare lessOrEq g1 g2) /\ (gameCompare greatOrEq g1 g2).
clone this paste RAW Paste Data