proposition: Lemma next_waypoint p a b : terminating (p, (a, b)) + { '(p', a') | forall n, exists k, 0 < k <= l - p /\ steps k (p, (n+a, b)) = Some (p', (n+a', 0)) } + { '(p', b') | forall n, exists k, 0 < k <= l - p /\ steps k (p, (a, n+b)) = Some (p', (0, n+b')) }.
proof: Proof. move Hn: (l - p) => n. elim: n p Hn a b. { move=> p ? a b. left. left. exists 1. rewrite /= /step. by have ->: nth_error M (state (p, (a, b))) = None by (rewrite nth_error_None /=; lia). } move=> n IH p ? a b. case Hi: (nth_error M (state (p, (a, b)))) => [i|]; first last. { left. left. exists 1. by rewrite /= /step Hi. } move: i Hi => /= []. - move=> Hi. left. left. exists 1. by rewrite /= /step Hi. - case. + move=> Hi. left. right. exists (S p, a). move=> n'. exists 1. split; first by lia. by rewrite /= /step /= Hi. + move=> Hi. right. exists (S p, b). move=> n'. exists 1. split; first by lia. by rewrite /= /step /= Hi. - case. + move=> Hi. have [[|[[p' a'] HSp]]|[[p' b'] HSp]] := IH (S p) ltac:(lia) a (S b). * move=> /reaches_terminating HSp. left. left. apply: HSp. exists 1. by rewrite /= /step Hi. * left. right. exists (p', a'). move=> n'. have [k [? <-]] := (HSp n'). exists (1+k). split; first by lia. apply: steps_plus. by rewrite /= /step Hi. * right. exists (p', b'). move=> n'. have [k [? <-]] := (HSp n'). exists (1+k). split; first by lia. apply: steps_plus. by rewrite /= /step Hi Nat.add_succ_r. + move=> Hi. have [[|[[p' a'] HSp]]|[[p' b'] HSp]] := IH (S p) ltac:(lia) (S a) b. * move=> /reaches_terminating HSp. left. left. apply: HSp. exists 1. by rewrite /= /step Hi. * left. right. exists (p', a'). move=> n'. have [k [? <-]] := (HSp n'). exists (1+k). split; first by lia. apply: steps_plus. by rewrite /= /step Hi Nat.add_succ_r. * right. exists (p', b'). move=> n'. have [k [? <-]] := (HSp n'). exists (1+k). split; first by lia. apply: steps_plus. by rewrite /= /step Hi. - case=> q Hi. + move: b => [|b]. { left. right. exists (q, a) => n'. exists 1. split; first by lia. by rewrite /= /step Hi. } have [[|[[p' a'] HSp]]|[[p' b'] HSp]] := IH (S p) ltac:(lia) a b. * move=> /reaches_terminating HSp. left. left. apply: HSp. exists 1. by rewrite /= /step Hi. * left. right. exists (p', a'). move=> n'. have [k [? <-]] := (HSp n'). exists (1+k). split; first by lia. apply: steps_plus. by rewrite /= /step Hi. * right. exists (p', b'). move=> n'. have [k [? <-]] := (HSp n'). exists (1+k). split; first by lia. apply: steps_plus. by rewrite /= /step Hi Nat.add_succ_r. + move: a => [|a]. { right. exists (q, b) => n'. exists 1. split; first by lia. by rewrite /= /step Hi. } have [[|[[p' a'] HSp]]|[[p' b'] HSp]] := IH (S p) ltac:(lia) a b. * move=> /reaches_terminating HSp. left. left. apply: HSp. exists 1. by rewrite /= /step Hi. * left. right. exists (p', a'). move=> n'. have [k [? <-]] := (HSp n'). exists (1+k). split; first by lia. apply: steps_plus. by rewrite /= /step Hi Nat.add_succ_r. * right. exists (p', b'). move=> n'. have [k [? <-]] := (HSp n'). exists (1+k). split; first by lia. apply: steps_plus. by rewrite /= /step Hi. Qed.
imports: List ssrfun List PeanoNat Lia Operators_Properties ssreflect ssrbool ssrfun