(* * linear tictactoe: prove that in optimal games, nobody can win (take 3 consecutive numbers in Z) * arithmetic tictactoe: - show that the 1st player can take up to 5 equidistant numbers in Z *) Require Import ZArith List SetoidList. Require Import Recdef. Open Scope Z_scope. (* Some basic automation *) Lemma not_in_nil : forall (A:Type) (a:A), ~In a nil. Proof. intros A a H. elim H. Qed. Hint Resolve not_in_nil. Ltac decons := repeat (constructor; auto). (* Destruct the first term whose type is a dependent disjunction *) Ltac cases_dec := match goal with |- context[ ?x ] => match type of x with sumbool _ _ => destruct x end end. (* Use case_eq rather than destruct, to allow rewriting later *) Ltac cases_dec' := match goal with |- context[ ?x ] => match type of x with sumbool _ _ => case_eq x; intros end end. (* Destruct a disjunction in the hypotheses *) Ltac cases_or := match goal with H: _ \/ _ |- _ => destruct H end. (* Variant of omega: try also proving a contradiction. *) Ltac omega' := (contradiction || (abstract omega) || elimtype False; (abstract omega)). (* Capture the application of a function. *) Ltac capture x f := match goal with |- context [f ?t] => set (x := f t) in * end. Ltac capture' x f := capture x f; clearbody x. Definition In_decZ := In_dec Z_eq_dec. (* Start our definition of the game *) (* A trace is the alternated list of the positions taken by the two players. It starts with the last move. *) Definition trace := list Z. Definition trace_ok (t : trace) := NoDup t. (* A valid trace may not contain duplicates *) (* mine and hers recover the moves of each player *) Fixpoint mine (t : trace) := match t with | x :: _ :: l => x :: mine l | x :: nil => x :: nil | nil => nil end. Fixpoint hers (t : trace) := match t with | _ :: x :: l => x :: hers l | _ => nil end. (* Some properties of traces *) Lemma mine_hers : forall t z, mine (z :: t) = z :: hers t. Proof. intros. apply proj1 with (B:=forall y, mine (z :: y :: t) = z :: hers (y :: t)). revert z; induction t; intros. auto. split. destruct (IHt z). auto. simpl in *. destruct (IHt a); clear IHt. congruence. Qed. Lemma In_either : forall x t, In x t -> {In x (mine t)}+{In x (hers t)}. Proof. induction t; simpl; intros. elim H. destruct (Z_eq_dec a x). subst. left. destruct t; simpl; auto. destruct (In_dec Z_eq_dec x t). destruct (IHt i). destruct t. elim i. right. rewrite <- mine_hers. auto. left. destruct t. auto. destruct t. elim i0. simpl hers in i0. rewrite mine_hers. simpl; auto. elim n0. destruct H; contradiction. Qed. Lemma incl_mine : forall t, incl (mine t) t. Proof. intros. apply proj1 with (B:=incl (hers t) t). induction t. simpl; split; intro; intros; auto. simpl. destruct t. simpl; split; intro; intros; auto. elim H. rewrite mine_hers in IHt. split. destruct t. simpl; intro; intros; auto. simpl in H. cases_or; simpl; auto. rewrite mine_hers. destruct IHt as [_ H]. simpl in H. intro; intros. simpl in H0. cases_or. simpl; auto. right. auto. right. intuition. Qed. Lemma trace_ok_exclusive : forall x t, trace_ok t -> In x (mine t) -> In x (hers t) -> False. Proof. induction 1; simpl; intros. elim H. destruct l. elim H2. simpl in H1. rewrite <- mine_hers in H2. destruct H1. subst. elim H. apply incl_mine. auto. specialize (IHNoDup H2); clear H2. destruct l. elim H1. rewrite mine_hers in H1. contradiction. Qed. (* A strategy is a function from a trace to the next move, such that it chooses a free position. *) Definition is_strategy f := forall t, trace_ok t -> trace_ok (f t::t). Definition strategy := {f:trace -> Z | is_strategy f}. (* Play n turns starting from trace t, using strategies f1 and f2. *) Fixpoint play (f1 f2:strategy) t (n:nat) {struct n} : trace := match n with | O => t | S n' => play f2 f1 (proj1_sig f1 t::t) n' end. (* Properties of play *) Lemma play_cont : forall a d t n1 n2, play a d t (2*n1+n2) = play a d (play a d t (2*n1)) n2. Proof. intros. revert t; induction n1. auto. replace (2*S n1)%nat with (S (S (2*n1))) by omega. simpl; intros. rewrite IHn1. auto. Qed. Lemma play_ok : forall n a d t, trace_ok t -> trace_ok (play a d t n). Proof. induction n; simpl; intros. auto. apply IHn. destruct a; simpl. auto. Qed. (* Utility function: (any x) is a strategy that returns x if x is free, or an arbitrary free position otherwise *) (* Proving its termination is a bit cumbersome *) Fixpoint count_ge (t : trace) (x : Z) {struct t} : nat := match t with | nil => O | y :: t' => if Z_le_dec x y then S (count_ge t' x) else count_ge t' x end. Lemma count_ge_decr : forall x t, (count_ge t x >= count_ge t (x+1))%nat. Proof. induction t. simpl. omega. simpl. repeat cases_dec; auto. omega. assert (x = a) by omega. subst. omega. Qed. Section Any. Variable t : trace. Function any (x:Z) {measure (count_ge t) x} : Z := if In_dec Z_eq_dec x t then any (x+1) else x. Proof. intros. clear teq. induction t. elim anonymous. simpl in *. cases_dec. cases_or. subst; omega'. cases_dec. specialize (IHt0 H). omega. omega'. cases_dec. assert (x = a) by omega. specialize (count_ge_decr x t0); intro. omega. cases_or. subst; omega'. auto. Defined. Lemma any_ok : forall x, ~In (any x) t. Proof. intros. functional induction (any x); auto. Qed. End Any. Hint Resolve any_ok. (* Linear tictactoe: a winner must take 3 consecutive positions. *) Definition winner t := exists n, In n (mine t) /\ In (n+1) (mine t) /\ In (n+2) (mine t). (* Our undefeatable defence: take either the position just after or just before the last move if free, any position otherwise. *) Definition defence0 (t : trace) := match t with | nil => 0 | n :: t' => if In_dec Z_eq_dec (n+1) t' then if In_dec Z_eq_dec (n-1) t' then any t 0 else n-1 else n+1 end. Lemma defence0_strat : is_strategy defence0. intro; intros. constructor; auto. clear. destruct t; simpl; intro. auto. destruct (In_dec Z_eq_dec (z+1) t). destruct (In_dec Z_eq_dec (z-1) t). elim (any_ok (z::t) 0 H). destruct H. omega'. elim (n H). destruct H. omega'. elim (n H). Qed. Definition defence : strategy. exists defence0. apply defence0_strat. Defined. (* A trace is safe if all her positions are either followed by one of mine, or I own both (n-1) and (n+2) *) Definition safe (t : trace) := forall n, In n (hers t) -> In (n+1) (mine t) \/ In (n-1) (mine t) /\ In (n+2) (mine t). (* My strategy is safe for any attacker! *) Lemma safe_defence : forall attack n, safe (play attack defence nil (2*n)). Proof. assert (safe nil). intro; intros. elim H. assert (Hok: trace_ok nil). constructor. intros. revert H Hok; generalize (@nil Z). induction n; intros. simpl. auto. replace (2 * S n)%nat with (2+2*n)%nat by omega. simpl. apply IHn; clear IHn; destruct attack as [attack Hatk]; simpl; specialize (Hatk _ Hok). repeat cases_dec. destruct (In_either _ _ i). intro; intros. simpl in H0. cases_or. subst; simpl; intuition. destruct (H _ H0); simpl; intuition. destruct (H _ i1). destruct (In_either _ _ i0). intro; intros. simpl in H1; destruct H1. subst. right; simpl. rewrite <- Zplus_assoc in H0. simpl in H0. intuition. destruct (H _ H1); simpl; intuition. destruct (H _ i2). replace (attack l - 1 + 1) with (attack l) in H1 by omega. inversion Hatk. subst. elim H4. apply incl_mine with (1:=H1). destruct H1. clear - i1 H2 Hok. elim (trace_ok_exclusive _ _ Hok H2). replace (attack l - 1 + 2) with (attack l + 1) by omega. auto. destruct H0. clear -H0 Hatk. inversion Hatk; subst. elim H2. replace (attack l) with (attack l + 1 - 1) by omega. apply incl_mine with (1:=H0). destruct (In_either _ _ i). intro; simpl; intros. destruct H0. subst; auto. destruct (H _ H0); intuition. destruct (H _ i0). intro; simpl; intros. destruct H1. subst. replace (attack l+2) with (attack l + 1 + 1) by omega. intuition. destruct (H _ H1); intuition. destruct H0. clear -H0 Hatk. inversion Hatk; subst. elim H2. apply incl_mine. replace (attack l) with (attack l + 1 - 1) by omega. auto. intro; simpl; intros. destruct H0. subst; auto. destruct (H _ H0); intuition. repeat cases_dec; decons; simpl; intros [Hh|Ht]; omega'. Qed. (* If I use my strategy, she cannot win. *) Theorem cannot_win : exists defence : strategy, forall attack : strategy, forall n, ~winner (play attack defence nil (2*n+1)). Proof. exists defence. intros. rewrite play_cont. simpl. intros [m [h0 [h1 h2]]]. repeat (rewrite mine_hers in *) . specialize (safe_defence attack n); intro. replace (n+(n+0))%nat with (2*n)%nat in * by auto. set (t:=play attack defence nil (2 * n)) in *. assert (trace_ok t). apply play_ok. constructor. clearbody t. destruct attack as [attack Hatk]; simpl in *. specialize (Hatk _ H0). destruct h0. subst. repeat (cases_or; try omega). destruct (H _ H2). elim (trace_ok_exclusive _ _ H0 H3). replace (attack t + 1 + 1) with (attack t + 2) by omega. auto. destruct H3. inversion Hatk; subst. elim H7. apply incl_mine. replace (attack t + 1 - 1) with (attack t) in H3 by omega. auto. destruct h1. destruct h2. omega. destruct (H _ H1). inversion Hatk; subst. elim H7. rewrite H2. apply incl_mine; auto. destruct H4. elim (trace_ok_exclusive _ _ H0 H5 H3). destruct h2. destruct (H _ H1). elim (trace_ok_exclusive _ _ H0 H4 H2). destruct H4. inversion Hatk; subst. elim H8. rewrite H3. apply incl_mine; auto. destruct (H _ H2). elim (trace_ok_exclusive _ _ H0 H4). replace (m+1+1) with (m+2) by omega. auto. destruct H4. elim (trace_ok_exclusive _ _ H0 H4). replace (m+1-1) with m by omega. auto. Qed. (* Arithmetic tictactoe *) (* 3 equidistant positions: an easy win *) Definition winner3 t := exists n, exists d, d > 0 /\ In n (mine t) /\ In (n+d) (mine t) /\ In (n+2*d) (mine t). Definition attack0 (t : trace) := match t with | nil => 0 | n :: m :: nil => if Z_le_dec n m then m + 2 else m - 2 | _ :: _ :: n :: m :: nil => if Z_le_dec n m then if In_decZ (m + 1) t then if In_decZ (m + 4) t then any t 0 else m+4 else m+1 else if In_decZ (m - 1) t then if In_decZ (m - 4) t then any t 0 else m - 4 else m - 1 | _ => any t 0 end. Lemma attack0_is_strat : is_strategy attack0. Proof. intro; intros. destruct t. decons. destruct t. simpl. decons. destruct t. simpl. cases_dec. decons. simpl; intro. repeat cases_or; omega'. decons. simpl; intro. repeat cases_or; omega'. destruct t. simpl; decons. destruct t. unfold attack0. repeat cases_dec; decons. simpl. decons. Qed. Definition attack : strategy. exists attack0. apply attack0_is_strat. Defined. Theorem attack_wins : forall defence, winner3 (play attack defence nil 5). Proof. red. intros [defender Hdef]. unfold attack. remember 2%nat as two. simpl. cases_dec. exists 0. rewrite Heqtwo. simpl. cases_dec; try omega'. clear z0. cases_dec. repeat cases_or; try omega'. rewrite H. cases_dec; try omega'. exists 2. intuition; omega. exists 1. intuition; omega. rewrite Heqtwo. simpl. cases_dec; try omega'. clear n0. cases_dec. repeat cases_or; try omega'. rewrite H. cases_dec; try omega'. exists (-4); exists 2. intuition; omega. exists (-2); exists 1. intuition; omega. Qed. (* 4 equidistant positions: a bit harder *) Definition winner4 t := exists n, exists d, d <> 0 /\ In n (mine t) /\ In (n+d) (mine t) /\ In (n+d*2) (mine t) /\ In (n+d*3) (mine t). Require Import Sumbool. (* Defining the strategy is a bit tricky, since we must check our previous moves at each step. *) Definition attack4 (t : trace) := match t with | nil => 0 | n :: m :: nil => n*(-6) | n' :: m' :: n :: m :: nil => if sumbool_or _ _ _ _ (Z_eq_dec n' (m'*2)) (Z_eq_dec n' (-m')) then n*(-3) else if Z_eq_dec n' (m'*3) then -m' else m'*2 | n'' :: m'' :: n' :: m' :: n :: m :: nil => if Z_eq_dec m' (m''*2) then if Z_eq_dec n'' (m''*3) then -m'' else m''*3 else if Z_eq_dec m'' (-m') then if Z_eq_dec n'' (-m'*2) then m'*2 else -m'*2 else if Z_eq_dec n'' (-m') then m'*3 else -m' | _ => 0 end. Lemma attack4_is_strat : is_strategy (fun t => any t (attack4 t)). Proof. intro; intros. decons. Qed. Definition attack4' : strategy. esplit. apply attack4_is_strat. Defined. (* Some tactics replacing (any x) by x *) Ltac remove_any n := match goal with |- context [any ?t n] => let e := fresh "E" in assert (e: any t n = n); [ rewrite any_equation; cases_dec; [elimtype False | reflexivity] | rewrite e in *; clear e ] end. Ltac remove_any' n := match goal with |- context [any ?t n] => replace (any t n) with n in * by abstract (rewrite any_equation; cases_dec; auto; simpl in *; cases_or; omega') end. Theorem attack4_wins : forall defence, winner4 (play attack4' defence nil 7). Proof. red. intros [defender Hdef]. unfold attack4'. remember 2%nat as two. simpl. replace (any nil 0) with 0 by reflexivity. set (n:=defender(0::nil)). assert (Ht0: trace_ok (n::0::nil)). apply Hdef. decons. assert (nn0: n <> 0). inversion Ht0; subst. intro Hn; elim H1; rewrite Hn. simpl; auto. remove_any' (n * -6). cases_dec. remove_any' (n * -3). rewrite Heqtwo. destruct o as [o|o]; rewrite o; simpl. cases_dec; try omega'. clear e. cases_dec. rewrite e. remove_any' (-(n * -3)). exists (-(n * -3)); exists (n* -3). intuition; omega. capture n'' defender. exists 0; exists (n * -3). remove_any' (n * -3 * 3). intuition; omega. cases_dec; try omega'. cases_dec. rewrite e0. remove_any' (-(n * -3)). exists (-(n * -3)); exists (n* -3). intuition; omega. capture n'' defender. exists 0; exists (n * -3). remove_any' (n * -3 * 3). intuition; omega. destruct a as [Hn'1 Hn'2]. cases_dec. rewrite e in *. remove_any' (-(n * -6)). rewrite Heqtwo; simpl. cases_dec; try omega'. cases_dec; try omega'. clear n0 e0. cases_dec. rewrite e0. remove_any' (n * -6 * 2). exists (-(n * -6)); exists (n * -6). intuition; omega. capture n'' defender. remove_any' (- (n * -6) * 2). exists (- (n * -6) * 2); exists (n * -6). intuition; omega. remove_any' (n * -6 * 2). rewrite Heqtwo; simpl. cases_dec; try omega'. cases_dec; try omega'. set (n' := defender (n * -6 :: n :: 0 :: nil)) in *. cases_dec. rewrite e. remove_any' (n * -6 * 3). exists 0; exists (n * -6). intuition; omega. capture n'' defender. remove_any' (- (n * -6)). exists (- (n * -6)); exists (n * -6). intuition; omega. Qed. (* Alternative way to define s strategy: At each step we return a move and a continuation taking the opponent's move as argument. This way we don't need to rebuild our context over. *) Section Player. (* Needs to be coinductive, so we can define any_move *) CoInductive player : Set := Move : Z -> (Z -> player) -> player. CoFixpoint any_move (z:Z) : player := Move 0 any_move. Variable p : player. Fixpoint run_player (t : trace) : player := match t with | nil | _ :: nil => p | n :: _ :: t' => match run_player t' with Move _ f => f n end end. Definition strat_of_player t := match run_player t with Move m _ => any t m end. Lemma is_strat_player : is_strategy strat_of_player. Proof. intro; intros. unfold strat_of_player. case (run_player t). intros. decons. Qed. End Player. Definition attack4a : player := let m := 0 in let f n := let m' := n * -6 in let f' n' := if sumbool_or _ _ _ _ (Z_eq_dec n' (m'*2)) (Z_eq_dec n' (-m')) then let m'' := n * -3 in let f'' n'' := Move (if Z_eq_dec n'' (m''*3) then -m'' else m''*3) any_move in Move m'' f'' else if Z_eq_dec n' (m'*3) then let m'' := -m' in let f'' n'' := Move (if Z_eq_dec n'' (-m'*2) then m'*2 else -m'*2) any_move in Move m'' f'' else let m'' := m'*2 in let f'' n'' := Move (if Z_eq_dec n'' (-m') then m'*3 else -m') any_move in Move m'' f'' in Move m' f' in Move m f. Definition attack4s : strategy. esplit. apply (is_strat_player attack4a). Defined. Theorem attack4a_wins : forall defence, winner4 (play attack4s defence nil 7). Proof. (* The proof almost doesn't change *) red. intros [defender Hdef]. unfold attack4s, strat_of_player. remember 2%nat as two. simpl. replace (any nil 0) with 0 by reflexivity. set (n:=defender(0::nil)). assert (Ht0: trace_ok (n::0::nil)). apply Hdef. decons. assert (nn0: n <> 0). inversion Ht0; subst. intro Hn; elim H1; rewrite Hn. simpl; auto. remove_any' (n * -6). cases_dec. remove_any' (n * -3). rewrite Heqtwo. destruct o as [o|o]; rewrite o; simpl. cases_dec; try omega'. destruct o0; try omega'. clear H. cases_dec. rewrite e. remove_any' (-(n * -3)). exists (-(n * -3)); exists (n* -3). intuition; omega. capture n'' defender. exists 0; exists (n * -3). remove_any' (n * -3 * 3). intuition; omega. cases_dec; try omega'. cases_dec. rewrite e. remove_any' (-(n * -3)). exists (-(n * -3)); exists (n* -3). intuition; omega. capture n'' defender. exists 0; exists (n * -3). remove_any' (n * -3 * 3). intuition; omega. destruct a as [Hn'1 Hn'2]. cases_dec. rewrite e in *. remove_any' (-(n * -6)). rewrite Heqtwo; simpl. cases_dec; try omega'. cases_dec; try omega'. clear a e0. cases_dec. rewrite e0. remove_any' (n * -6 * 2). exists (-(n * -6)); exists (n * -6). intuition; omega. capture n'' defender. remove_any' (- (n * -6) * 2). exists (- (n * -6) * 2); exists (n * -6). intuition; omega. remove_any' (n * -6 * 2). rewrite Heqtwo; simpl. cases_dec; try omega'. cases_dec; try omega'. set (n' := defender (n * -6 :: n :: 0 :: nil)) in *. cases_dec. rewrite e. remove_any' (n * -6 * 3). exists 0; exists (n * -6). intuition; omega. capture n'' defender. remove_any' (- (n * -6)). exists (- (n * -6)); exists (n * -6). intuition; omega. Qed. Definition winner5 t := exists n, exists d, d <> 0 /\ In n (mine t) /\ In (n+d) (mine t) /\ In (n+d*2) (mine t) /\ In (n+d*3) (mine t) /\ In (n+d*4) (mine t). Fixpoint make_list s b (n : nat) {struct n} := match n with | O => (b :: nil) | S n' => (s * Z_of_nat n + b :: make_list s b n') end. Eval compute in make_list 2 1 3. (* Whether it is safe, when we have points at 0 and 2s, to add a 3rd point at 4s *) Definition unsafe_dec s n' := In_decZ n' (make_list s (s * -4) 12). (* Finish when we have points at b, 2s+b and 4s+b *) Let finish s b n3 := if Z_eq_dec n3 (s * -2 + b) then let m4 := s * 6 + b in let f4 n4 := if Z_eq_dec n4 (s * 8 + b) then let m5 := s * 3 + b in let f5 n5 := Move (if Z_eq_dec n5 (s+b) then s * 5 + b else s + b) any_move in Move m5 f5 else Move (s * 8 + b) any_move in Move m4 f4 else if Z_eq_dec n3 (s * 6 + b) then let m4 := s * -2 + b in let f4 n4 := if Z_eq_dec n4 (s * -4 + b) then let m5 := s + b in let f5 n5 := Move (if Z_eq_dec n5 (-s+b) then s * 3 + b else -s + b) any_move in Move m5 f5 else Move (s * -4 + b) any_move in Move m4 f4 else if Z_eq_dec n3 (s * 8 + b) then let m4 := s * -2 + b in let f4 n4 := Move (if Z_eq_dec n4 (s*6+b) then (s* -4 +b) else (s*6+b)) any_move in Move m4 f4 else let m4 := s * 6 + b in let f4 n4 := Move (if Z_eq_dec n4 (s*8+b) then (s* -2 +b) else (s*8+b)) any_move in Move m4 f4. Definition attack5a : player := let m := 0 in let f n := let m1 := n * -6 in let f1 n1 := if unsafe_dec (n * -3) n1 then let m2 := m1 * 10 in let f2 n2 := if unsafe_dec (m1 * 5) n2 then Move (m1 * 19) (finish (n * -27) m1) else Move (m1 * 20) (finish (m1 * 5) 0) in Move m2 f2 else Move (m1 * 2) (finish (n * -3) 0) in Move m1 f1 in Move m f. Definition attack5 : strategy. esplit. apply (is_strat_player attack5a). Defined. (* A more clever tactic to remove any *) Ltac remove_any_i := match goal with |- context [ any _ ?n ] => match n with _ + _ => idtac | _ * _ => idtac end; remove_any n; [ match goal with H: In n _ |- _ => simpl in H end; intuition; try omega; try match goal with H: ?n' = _ |- _ => match goal with | H': In n' _ |- _ => simpl in H' | H': In n' _ -> False |- _ => simpl in H' end; omega end | ] end. (* First prove the subcase where she didn't use any of the positions we might want to use. *) Lemma attack5_other : forall defence n n', n <> 0 -> ~ In n' (make_list (n * -3) (n * -3 * -4) 12) -> winner5 (play defence attack5 (n * -6 * 2 :: n' :: n * -6 :: n :: 0 :: nil) 8). Proof. intros [defender Hdef] n n' nn0 n1. remember 4%nat as two. rewrite Heqtwo in n1. unfold attack5, strat_of_player. simpl. cases_dec'; try contradiction. clear n1. capture' n2 defender. unfold finish. cases_dec. subst n2. remove_any_i. capture' n3 defender. cases_dec. subst n3. remove_any_i. subst two; simpl. rewrite H. unfold finish. cases_dec; try omega'. cases_dec; try omega'. clear e e0. capture a any_move. destruct a. capture' n5 defender. capture' n4 defender. cases_dec. rewrite e in *; clear e. remove_any_i. exists (n * -6); exists (n * -3); simpl; omega'. remove_any_i. exists 0; exists (n * -3); simpl; omega'. remove_any_i. subst two; simpl. rewrite H. unfold finish. cases_dec; try omega'. clear e. exists 0; exists (n * -6). cases_dec; simpl; omega'. cases_dec. clear n1; subst n2. remove_any_i. subst two; simpl. rewrite H. unfold finish. cases_dec; try omega'. cases_dec; try omega'. clear e n1. cases_dec. rewrite e; clear e. capture a any_move. destruct a. remove_any_i. cases_dec. rewrite e; clear e. remove_any_i. exists 0; exists (n * -3); simpl; omega'. remove_any_i. exists (n * 6); exists (n * -3); simpl; omega'. remove_any_i. exists (n * 12); exists (n * -6); simpl; omega'. cases_dec. clear n1 n3; subst n2. remove_any_i. subst two; simpl; rewrite H. unfold finish. cases_dec; try omega'. cases_dec; try omega'. cases_dec; try omega'. clear e n1 n2. cases_dec. rewrite e; clear e. remove_any_i. exists (n * 12); exists (n * -6); simpl; omega'. remove_any_i. exists (n * 6); exists (n * -6); simpl; omega'. remove_any_i. subst two; simpl; rewrite H. unfold finish. cases_dec; try omega'. cases_dec; try omega'. cases_dec; try omega'. clear n5 n6 n7. cases_dec. rewrite e; clear e. remove_any_i. exists (n * 6); exists (n * -6); simpl; omega'. remove_any_i. exists 0; exists (n * -6); simpl; omega'. Qed. (* Now prove the remaining cases. *) Theorem attack5_wins : forall defence, winner5 (play attack5 defence nil 13). Proof. remember 4%nat as two. remember (S(S(S(S two)))) as six. intros [defender Hdef]. unfold attack5, strat_of_player. simpl. replace (any nil 0) with 0 by reflexivity. capture n defender. assert (Ht0: trace_ok (n::0::nil)). apply Hdef. decons. assert (nn0: n <> 0). inversion Ht0; subst. intro Hn; elim H1; rewrite Hn. simpl; auto. remove_any' (n * -6). capture n' defender. clearbody n n'. subst six. cases_dec'; remove_any_i; [|subst two; apply attack5_other; assumption]. simpl. rewrite H. capture' n2 defender. cases_dec'; remove_any_i. capture' n3 defender. unfold finish. cases_dec. subst n3 two. remove_any_i. simpl. rewrite H, H0. capture' n4 defender. unfold finish. cases_dec; try omega'. clear e. cases_dec; remove_any_i. subst n4. capture' n5 defender. cases_dec; remove_any_i. subst n5. exists (n * -6 * 10); exists (n * -27); clear -nn0; simpl; intuition; omega'. exists (n * -6); exists (n * -27); clear -nn0; simpl; intuition; omega'. capture a any_move. destruct a. exists (n * -6); exists (n * -54); simpl; omega'. cases_dec. clear n0. subst n3 two. remove_any_i. simpl. rewrite H, H0. capture' n4 defender. unfold finish. cases_dec; try omega'. cases_dec; try omega'. clear n0 e. cases_dec; remove_any_i. subst n4. capture' n5 defender. cases_dec; remove_any_i. subst n5. exists (n * -6); exists (n * -27); simpl; omega'. exists (n * 48); exists (n * -27); simpl; omega'. capture a any_move. destruct a. exists (n * 102); exists (n * -54); simpl; omega'. cases_dec; remove_any_i. subst n3 two; clear n0 n1. simpl. rewrite H, H0. capture' n4 defender. unfold finish. cases_dec; try omega'. cases_dec; try omega'. cases_dec; try omega'. clear n0 n1 e. cases_dec; remove_any_i. subst n4. exists (n * 102); exists (n * -54); simpl; omega'. exists (n * 48); exists (n * -54); simpl; omega'. subst two; simpl. rewrite H, H0. unfold finish. cases_dec; try omega'. cases_dec; try omega'. cases_dec; try omega'. capture a any_move. destruct a. cases_dec; remove_any_i. exists (n * 48); exists (n * -54); simpl; omega'. exists (n * -6); exists (n * -54); simpl; omega'. unfold finish. capture' n3 defender. cases_dec. subst n3. remove_any_i. subst two; simpl. rewrite H, H0. capture' n4 defender. unfold finish. cases_dec; try omega'. clear e. cases_dec; remove_any_i. subst n4. capture' n5 defender. cases_dec; remove_any_i. exists (n * -60); exists (n * -30); simpl; omega'. exists 0; exists (n * -30); simpl; omega'. capture a any_move. destruct a. exists 0; exists (n * -60); simpl; omega'. cases_dec. clear n1; subst n3. remove_any_i. subst two; simpl. rewrite H, H0. capture' n4 defender. unfold finish. cases_dec; try omega'. cases_dec; try omega'. clear n1 e. cases_dec; remove_any_i. subst n4. capture' n5 defender. cases_dec; remove_any_i. exists 0; exists (n * -30); simpl; omega'. exists (n * 60); exists (n * -30); simpl; omega'. capture a any_move; destruct a. exists (n * 120); exists (n * -60); simpl; omega'. cases_dec; remove_any_i. clear n1 n4; subst n3 two; simpl. rewrite H, H0. capture' n4 defender. unfold finish. cases_dec; try omega'. cases_dec; try omega'. cases_dec; try omega'. clear n1 n3 e. cases_dec; remove_any_i. subst n4. exists (n * 120); exists (n * -60); simpl; omega'. exists (n * 60); exists (n * -60); simpl; omega'. subst two; simpl. rewrite H, H0. unfold finish. cases_dec; try omega'. cases_dec; try omega'. cases_dec; try omega'. capture a any_move. destruct a. cases_dec; remove_any_i. rewrite e; clear e. exists (n * 60); exists (n * -60); simpl; omega'. exists 0; exists (n * -60); simpl; omega'. Qed. (* took 13'30'' and more than 3GB to compile with 8.2pl2 on OSX (2.8GHz core 2 duo, 4GB DDR3 memory, ocaml 64bit) *) (* down to 5'16'' and 1.11GB by splitting attack5_wins in two *)