proposition: Lemma eval_rec5_correct n t ht i : depth i <= n -> let f1 := eval_rec n t in let f2 := eval_rec5 n t in [/\ [/\ ht_valid ht -> ht_valid (f2 eloss edraw ht i), ht_valid ht -> f1 i = loss -> f2 eloss edraw ht i = eloss :> estate, ht_valid ht -> f1 i = draw -> edraw <= f2 eloss edraw ht i <= drawwin & ht_valid ht -> f1 i = win -> drawwin <= f2 eloss edraw ht i], [/\ ht_valid ht -> ht_valid (f2 edraw ewin ht i), ht_valid ht -> f1 i = win -> f2 edraw ewin ht i = ewin :> estate, ht_valid ht -> f1 i = draw -> lossdraw <= f2 edraw ewin ht i <= draw & ht_valid ht -> f1 i = loss -> f2 edraw ewin ht i <= lossdraw] & ((ht_valid ht -> ht_valid (f2 eloss ewin ht i)) /\ (ht_valid ht -> f2 eloss ewin ht i = f1 i :> estate))].
proof: Proof. elim: n t ht i => [/=|n IH] t ht i Hi. case: ieval (depth_ieval t i); last by rewrite eqxx; case: depth Hi. by case. have HHiv : Hiv (eval_rec n (flip t)) (eval_rec5 n (flip t)) (moves t i). have F i1 : i1 \in moves t i -> depth i1 <= n. move=> Hi1. rewrite (moves_depth Hi1) -ltnS (leq_trans _ Hi) // prednK //. have := depth_ieval t i; rewrite liveness. by case: depth Hi1 => //; case: moves => //=. by (repeat split) => // i1 ht1 Hi1 Hv1; have [[H1 H2 H3 H4] [H5 H6 H7 H8] [H9 H10]] := IH (flip t) ht1 i1 (F _ Hi1); (apply: H1 || apply: H2 ||apply: H3 ||apply: H4 ||apply: H5 || apply: H6 ||apply: H7 ||apply: H8 ||apply: H9 || apply: H10). have evalE : eval_rec n.+1 t i = eval t i. by apply: eval_rec_stable; rewrite leqnn. repeat split => //=. - move=> Hv; case E1 : ieval => //. rewrite /= E1 in evalE. case: hget (Hv i t) => [|_]; last first. case E2 : process_eval_rec5 => [ht1 res2] /=. apply: hput_correct => //. rewrite -[ht_valid ht1]/(ht_valid (Pres ht1 res2)) -E2. by apply: (process_eval_rec5_draw_win_valid HHiv). rewrite -evalE -[res2]/(Pres ht1 res2 : estate) -E2. case E3 : (\smin_(_ <- _) _). - by rewrite (process_eval_rec5_draw_win_win HHiv). - have := process_eval_rec5_draw_win_loss win HHiv Hv E3. by case: process_eval_rec5 => h [] //. have := process_eval_rec5_draw_win_draw HHiv Hv E3 (isT : lossdraw <= ewin). by case: process_eval_rec5 => h [] //. move=> es /(_ es (refl_equal _)) Hes. have [//|E2] := boolP (is_state es). case: es Hes E1 E2 => //= He _ _. case E : process_eval_rec5 => [ht1 res2] /=. case: eqP => [[E1]| E1]. apply: hput_correct => //. rewrite -[ht_valid ht1]/(ht_valid (Pres ht1 res2)) -E. by apply: (process_eval_rec5_draw_win_valid HHiv) => //. move: E1 He. rewrite -evalE -[res2]/(Pres ht1 res2 : estate) -E. case E3 : (\smin_(_ <- _) _) => //. by rewrite (process_eval_rec5_draw_win_win HHiv). apply: hput_correct => //. rewrite -[ht_valid ht1]/(ht_valid (Pres ht1 res2)) -E. by apply: (process_eval_rec5_draw_win_valid HHiv) => //. move: E1 He. rewrite -evalE -[res2]/(Pres ht1 res2 : estate) -E. case E3 : (\smin_(_ <- _) _) => //. by rewrite (process_eval_rec5_draw_win_win HHiv). have := process_eval_rec5_draw_win_draw HHiv Hv E3 (isT : lossdraw <= ewin). by case: process_eval_rec5 => h []. - move=> Hv; case E : ieval => [a|]; first by move=>->. move=> /(@sflip_inj _ win) Hs. case: hget (Hv i t) => [|_ ]; last first. case E1 : process_eval_rec5 => [ht1 res2] /=. rewrite -[res2]/(Pres ht1 res2 : estate) -E1. by rewrite (process_eval_rec5_draw_win_win HHiv). move=> es /(_ es (refl_equal _)) Hes. have Hs1 : eval t i = loss by rewrite -evalE /= E Hs. rewrite Hs1 in Hes. have [//|E1] := boolP (is_state es); first by case: es Hes. case: es Hes E1 => // Hes E1. case E2 : process_eval_rec5 => [ht1 res2] /=. rewrite -[res2]/(Pres ht1 res2 : estate) -E2. by rewrite (process_eval_rec5_draw_win_win HHiv). - move=> Hv; case E : ieval => [a|]; first by move=>->. move=> /(@sflip_inj _ draw) Hs. case: hget (Hv i t) => [|_ ]; last first. case E1 : process_eval_rec5 => [ht1 res2] /=. rewrite -[res2]/(Pres ht1 res2 : estate) -E1. by rewrite (process_eval_rec5_draw_win_draw HHiv). move=> es /(_ es (refl_equal _)) Hes. have Hs1 : eval t i = draw by rewrite -evalE /= E Hs. rewrite Hs1 in Hes. have [//|E1] := boolP (is_state es); first by case: es Hes. case: es Hes E1 => // _ _. case E1 : process_eval_rec5 => [ht1 res2] /=. rewrite -[res2]/(Pres ht1 res2 : estate) -E1. have := process_eval_rec5_draw_win_draw HHiv Hv Hs (isT : lossdraw <= ewin). by case: process_eval_rec5 => h []. - move=> Hv; case E : ieval => [a|]; first by move=>->. move=> /(@sflip_inj _ loss) Hs. case: hget (Hv i t) => [|_ ]; last first. case E1 : process_eval_rec5 => [ht1 res2] /=. rewrite -[res2]/(Pres ht1 res2 : estate) -E1. by rewrite (process_eval_rec5_draw_win_loss win HHiv). move=> es /(_ es (refl_equal _)) Hes. have Hs1 : eval t i = win by rewrite -evalE /= E Hs. rewrite Hs1 in Hes. have [//|E1] := boolP (is_state es); first by case: es Hes. by case: es Hes E1. - move=> Hv; case E1 : ieval => //. rewrite /= E1 in evalE. case: hget (Hv i t) => [|_]; last first. case E2 : process_eval_rec5 => [ht1 res2] /=. apply: hput_correct => //. rewrite -[ht_valid ht1]/(ht_valid (Pres ht1 res2)) -E2. by apply: (process_eval_rec5_loss_draw_valid HHiv). rewrite -evalE -[res2]/(Pres ht1 res2 : estate) -E2. case E3 : (\smin_(_ <- _) _). - have := process_eval_rec5_loss_draw_win HHiv Hv E3 (isT : drawwin <= ewin). by case: process_eval_rec5 => h [] //. - by rewrite (process_eval_rec5_loss_draw_loss ewin HHiv). have := process_eval_rec5_loss_draw_draw HHiv Hv E3 (isT : draw <= ewin). by case: process_eval_rec5 => h [] //. move=> es /(_ es (refl_equal _)) Hes. have [//|E2] := boolP (is_state es). case: es Hes E1 E2 => //= He _ _. case E : process_eval_rec5 => [ht1 res2] /=. case: eqP => [[E1]| E1]. apply: hput_correct => //. rewrite -[ht_valid ht1]/(ht_valid (Pres ht1 res2)) -E. by apply: (process_eval_rec5_loss_draw_valid HHiv) => //. move: E1 He. rewrite -evalE -[res2]/(Pres ht1 res2 : estate) -E. case E3 : (\smin_(_ <- _) _) => //. by rewrite (process_eval_rec5_loss_draw_loss win HHiv). apply: hput_correct => //. rewrite -[ht_valid ht1]/(ht_valid (Pres ht1 res2)) -E. by apply: (process_eval_rec5_loss_draw_valid HHiv) => //. move: E1 He. rewrite -evalE -[res2]/(Pres ht1 res2 : estate) -E. case E3 : (\smin_(_ <- _) _) => //. by rewrite (process_eval_rec5_loss_draw_loss win HHiv). have := process_eval_rec5_loss_draw_draw HHiv Hv E3 (isT : draw <= ewin). by case: process_eval_rec5 => h []. - move=> Hv; case E : ieval => [a|]; first by move=>->. move=> /(@sflip_inj _ loss) Hs. case: hget (Hv i t) => [|_ ]; last first. case E1 : process_eval_rec5 => [ht1 res2] /=. rewrite -[res2]/(Pres ht1 res2 : estate) -E1. by apply: (process_eval_rec5_loss_draw_loss _ HHiv). move=> es /(_ es (refl_equal _)) Hes. have Hs1 : eval t i = win by rewrite -evalE /= E Hs. rewrite Hs1 in Hes. have [//|E1] := boolP (is_state es); first by case: es Hes. case: es Hes E1 => // _ _. case E1 : process_eval_rec5 => [ht1 res2] /=. rewrite -[res2]/(Pres ht1 res2 : estate) -E1. by rewrite (process_eval_rec5_loss_draw_loss _ HHiv). - move=> Hv; case E : ieval => [a|]; first by move=>->. move=> /(@sflip_inj _ draw) Hs. case: hget (Hv i t) => [|_ ]; last first. case E1 : process_eval_rec5 => [ht1 res2] /=. rewrite -[res2]/(Pres ht1 res2 : estate) -E1. by apply: (process_eval_rec5_loss_draw_draw HHiv). move=> es /(_ es (refl_equal _)) Hes. have Hs1 : eval t i = draw by rewrite -evalE /= E Hs. rewrite Hs1 in Hes. have [//|E1] := boolP (is_state es); first by case: es Hes. case: es Hes E1 => // _ _. case E1 : process_eval_rec5 => [ht1 res2] /=. rewrite -[res2]/(Pres ht1 res2 : estate) -E1. have := process_eval_rec5_loss_draw_draw HHiv Hv Hs (isT : draw <= ewin). by case: process_eval_rec5 => h []. - move=> Hv; case E : ieval => [a|]; first by move=>->. move=> /(@sflip_inj _ win) Hs. case: hget (Hv i t) => [|_ ]; last first. case E1 : process_eval_rec5 => [ht1 res2] /=. rewrite -[res2]/(Pres ht1 res2 : estate) -E1. by apply: (process_eval_rec5_loss_draw_win HHiv). move=> es /(_ es (refl_equal _)) Hes. have Hs1 : eval t i = loss by rewrite -evalE /= E Hs. rewrite Hs1 in Hes. have [//|E1] := boolP (is_state es); first by case: es Hes. by case: es Hes E1. - move=> Hv; case E : ieval => //. case: hget (Hv i t) => [|_ ]; last first. case E1 : process_eval_rec5 => [ht1 res2] /=. rewrite -[res2]/(Pres ht1 res2 : estate) -E1. apply: hput_correct => //. rewrite -[ht1]/(Pres ht1 res2 : htable) -E1. by apply: (process_eval_rec5_loss_win_valid HHiv). rewrite (process_eval_rec5_loss_win HHiv) //. by rewrite -evalE /= E; case: sflip. by apply: le_win. move=> es /(_ es (refl_equal _)) Hes. have [//|E1] := boolP (is_state es). case: es Hes E1 => // Hes E1. case E2 : process_eval_rec5 => [ht1 res2] /=. rewrite -[res2]/(Pres ht1 res2 : estate) -E2. case: eqP => [[E3]| E3]. apply: hput_correct => //. rewrite -[ht_valid ht1]/(ht_valid (Pres ht1 res2)) -E2. by apply: (process_eval_rec5_draw_win_valid HHiv). move: E3 Hes. case E4 : eval => //. move: E4; rewrite -evalE /= E => /(@sflip_inj _ win) E4. by rewrite (process_eval_rec5_draw_win_win HHiv). apply: hput_correct => //. rewrite -[ht_valid ht1]/(ht_valid (Pres ht1 res2)) -E2. by apply: (process_eval_rec5_draw_win_valid HHiv). case E4 : process_eval_rec5 => [ht2 res3] /=. rewrite -[res3]/(Pres ht2 res3 : estate) -E4. case E5 : eval Hes => //. move: E5; rewrite -evalE /= E => /(@sflip_inj _ win) E5. by rewrite (process_eval_rec5_draw_win_win HHiv). move: E5; rewrite -evalE /= E => /(@sflip_inj _ draw) E5. have := process_eval_rec5_draw_win_draw HHiv Hv E5 (isT: lossdraw <= ewin). by case: process_eval_rec5 => h []. case E2 : process_eval_rec5 => [ht1 res2] /=. rewrite -[res2]/(Pres ht1 res2 : estate) -E2. case: eqP => [[E3]| E3]. apply: hput_correct => //. rewrite -[ht_valid ht1]/(ht_valid (Pres ht1 res2)) -E2. by apply: (process_eval_rec5_loss_draw_valid HHiv). move: E3 Hes. case E4 : eval => //. move: E4; rewrite -evalE /= E => /(@sflip_inj _ loss) E4. by rewrite (process_eval_rec5_loss_draw_loss win HHiv). apply: hput_correct => //. rewrite -[ht_valid ht1]/(ht_valid (Pres ht1 res2)) -E2. by apply: (process_eval_rec5_loss_draw_valid HHiv). case E4 : process_eval_rec5 => [ht2 res3] /=. rewrite -[res3]/(Pres ht2 res3 : estate) -E4. case E5 : eval Hes => //. move: E5; rewrite -evalE /= E => /(@sflip_inj _ loss) E5. by rewrite (process_eval_rec5_loss_draw_loss win HHiv). move: E5; rewrite -evalE /= E => /(@sflip_inj _ draw) E5. have := process_eval_rec5_loss_draw_draw HHiv Hv E5 (isT: draw <= ewin). by case: process_eval_rec5 => h []. move=> Hv; case E : ieval => [a|] //. case: hget (Hv i t) => [|_ ]; last first. case E1 : process_eval_rec5 => [ht1 res2] /=. rewrite -[res2]/(Pres ht1 res2 : estate) -E1. apply: (process_eval_rec5_loss_win HHiv) => //. by apply: le_win. move=> es /(_ es (refl_equal _)) Hes. rewrite -evalE /= E in Hes. have [//|E1] := boolP (is_state es). by case: es Hes => //=; case: sflip. case: es Hes E1 => //. case E1 : (\smin_(i0 <- moves t i) eval_rec n (flip t) i0) => //= _ _. case E2 : process_eval_rec5 => [ht1 res1] /=. rewrite -[res1]/(Pres ht1 res1 : estate) -E2. by rewrite (process_eval_rec5_draw_win_win HHiv) //. case E2 : process_eval_rec5 => [ht1 res1] /=. rewrite -[res1]/(Pres ht1 res1 : estate) -E2. have := process_eval_rec5_draw_win_draw HHiv Hv E1 (isT : lossdraw <= ewin). by case: process_eval_rec5 => h []. case E1 : (\smin_(i0 <- moves t i) eval_rec n (flip t) i0) => //= _ _. case E2 : process_eval_rec5 => [ht1 res1] /=. rewrite -[res1]/(Pres ht1 res1 : estate) -E2. by rewrite (process_eval_rec5_loss_draw_loss win HHiv). case E2 : process_eval_rec5 => [ht1 res1] /=. rewrite -[res1]/(Pres ht1 res1 : estate) -E2. have := process_eval_rec5_loss_draw_draw HHiv Hv E1 (isT : draw <= ewin). by case: process_eval_rec5 => h []. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(all_algebra)