Require Import List ListDec PeanoNat Lia Relation_Operators Operators_Properties Permutation.
Import ListNotations.
Require Import Undecidability.MinskyMachines.MM2.
Require Import Undecidability.MinskyMachines.Util.MM2_facts.
Import MM2Notations.

Require Import ssreflect ssrbool ssrfun.

Set Default Goal Selector "!".

Module Facts.

Lemma unnest : (A B C : Type), A (B C) (A B) C.
Proof. auto. Qed.

Lemma prod_nat_nat_eq_dec (x y : * ) : {x = y} + {x y}.
Proof. by do ? decide equality. Qed.

Lemma Exists_sig {X : Type} P (HP : ( x, {P x} + { P x})) (L : list X) :
  Exists P L { x | In x L P x}.
Proof.
  elim: L. { by move /Exists_nil. }
  move x L IH /Exists_cons H.
  have [/IH|?] := Exists_dec P L HP.
  - move [y [? ?]]. exists y. by split; [right|].
  - exists x. by split; [left|tauto].
Qed.


Lemma NoDup_map_ext {X Y : Type} (f : X Y) (l : list X) :
  ( x1, In l x2, In l f = f = ) NoDup l NoDup (map f l).
Proof.
  elim: l. { move *. by constructor. }
  move x l IH /= H /NoDup_cons_iff [Hxl] /IH {}IH. constructor.
  - move /in_map_iff [x'] [/H] ? . have ? : x' = x by tauto.
    subst x'. exact: (Hxl ).
  - apply: IH. move Hx1l Hx2l /H. tauto.
Qed.


Lemma pigeonhole {X : Type} (L L' : list X) :
  incl L L' length L' < length L not (NoDup L).
Proof.
  move ?? HL. suff: length L = length L' by .
  apply /Permutation_length /NoDup_Permutation_bis; by [|].
Qed.


Lemma nth_error_seq {i start len} :
  i < len nth_error (seq start len) i = Some (start + i).
Proof.
  elim: len i start; first by .
  move len IH [|i] start.
  { move ?. congr Some. . }
  move ?. rewrite /= IH; first by .
  congr Some. .
Qed.


Section DiscreteList.

Context {X : Type} (X_eq_dec : (x y : X), {x = y} + {x y}).

Lemma not_NoDup_consE {x} {l: list X} : (not (NoDup (x :: l))) In x l not (NoDup l).
Proof using X_eq_dec.
  have [?|?] := In_dec X_eq_dec x l.
  { move ?. by left. }
  move Hxl. right Hl. apply: Hxl.
  by constructor.
Qed.


Lemma not_NoDupE {l : list X} : not (NoDup l)
   '(i, j), i < j < length l nth_error l i = nth_error l j.
Proof using X_eq_dec.
  elim: l. { move H. exfalso. apply: H. by constructor. }
  move x l IH.
  move /not_NoDup_consE [|].
  - move /(@In_nth_error X) [j] Hj.
    have ? : not (length l j).
    { move /nth_error_None. by rewrite Hj. }
    exists (0, S j) /=. split; [|done].
  - move /IH [[i j]] [? ?].
    exists (S i, S j) /=. split; [|done].
Qed.


Lemma not_inclE (L L' : list X) : (not (incl L L')) { x | In x L not (In x L')}.
Proof using X_eq_dec.
  elim: L. { move H. exfalso. by apply: H. }
  move x L IH /=.
  have [|?] := In_dec X_eq_dec x L'.
  - move ? HxLL'. have /IH [y [? ?]] : incl L L'.
    { move H. apply: HxLL'. by move y /= [|/H]. }
    exists y. tauto.
  - move _. exists x. tauto.
Qed.


Lemma dup_seq (f : X) start len :
  not (NoDup (map f (seq start len)))
   '(i, j), f i = f j (start i i < j j < start+len).
Proof using X_eq_dec.
  move /not_NoDupE [[i j]]. rewrite map_length seq_length.
  move [? H]. exists (start+i, start+j). split; last .
  move: H. rewrite ?nth_error_map ?nth_error_seq; [||].
  by move [].
Qed.


End DiscreteList.

End Facts.

Import Facts.

Section Construction.
Variable M : list mm2_instr.

#[local] Notation bounded := (MM2.mm2_bounded M).
#[local] Notation step := (MM2.mm2_step M).
#[local] Notation reaches := (clos_refl_trans _ step).
#[local] Notation trace := (MM2.mm2_trace M).

#[local] Arguments Nat.min !n !m /.

Lemma option_mm2_state_eq_dec (x y: option mm2_state) : {x = y} + {x y}.
Proof. by do ? decide equality. Qed.

Lemma bounded_monotone {k k' x} : k k' bounded k x bounded k' x.
Proof. move ? [L [? ?]]. exists L. split; [|done]. Qed.

Fixpoint steps k x :=
  match k with
  | 0 Some x
  | S k
    match mm2_sig_step_dec M x with
    | inleft (exist _ y _) steps k y
    | inright _ None
    end
  end.

Lemma steps_plus' {k x k'} :
  steps (k + k') x = obind (steps k') (steps k x).
Proof.
  elim: k x. { done. }
  move k IH x /=.
  case: (mm2_sig_step_dec M x) [[y]|]; last done.
  move _. by apply: IH.
Qed.


Lemma steps_k_monotone {k x} k' : steps k x = None k k' steps k' x = None.
Proof.
  move Hk ?. have : k' = k + (k' - k) by .
  by rewrite steps_plus' Hk.
Qed.


Lemma steps_sub {i j x y z} :
  steps i x = Some y
  steps j x = Some z
  i j
  steps (j-i) y = Some z.
Proof.
  move Hi + ?. rewrite [in steps j x](ltac:() : j = i + (j - i)).
  by rewrite steps_plus' Hi.
Qed.


Lemma steps_reaches {k x y} : steps k x = Some y reaches x y.
Proof.
  elim: k x. { move ? []. by apply: rt_refl. }
  move k IH x /=.
  case: (mm2_sig_step_dec M x) [[z]|]; last done.
  move ? /IH. apply: rt_trans. by apply: rt_step.
Qed.


Lemma reaches_steps {x y} : reaches x y k, steps k x = Some y.
Proof.
  move /clos_rt_rt1n_iff. elim.
  - move >. by exists 0.
  - move {}x {}y z Hxy _ [k Hk]. exists (S k) /=.
    case: (mm2_sig_step_dec M x) [[y' Hxy']|].
    + by move: Hxy Hxy' /mm2_step_det /[apply] .
    + move H. by move: Hxy /H.
Qed.


Lemma step_values_bound x y : steps 1 x = Some y
  value1 y + value2 y 1 + value1 x + value2 x
  value1 x + value2 x 1 + value1 y + value2 y
  value1 x 1 + value1 y value1 y 1 + value1 x
  value2 x 1 + value2 y value2 y 1 + value2 x.
Proof.
  move /=.
  case: (mm2_sig_step_dec M x) [[?]|]; last done.
  by move /mm2_step_values_bound ? [].
Qed.


Lemma steps_values_bound k x y : steps k x = Some y
  value1 y + value2 y k + value1 x + value2 x
  value1 x + value2 x k + value1 y + value2 y
  value1 x k + value1 y value1 y k + value1 x
  value2 x k + value2 y value2 y k + value2 x.
Proof.
  elim: k x. { move ? []. . }
  move k IH x.
  rewrite (steps_plus' (k := 1) (k' := k)).
  case Hxz: (steps 1 x) [z|]; last done.
  move /IH.
  move: Hxz /step_values_bound. .
Qed.


Definition path k x := map ( n steps n x) (seq 0 k).

Lemma path_length {k x} : length (path k x) = k.
Proof. by rewrite /path map_length seq_length. Qed.

Lemma In_pathE K x oy : In oy (path K x) k, k < K steps k x = oy.
Proof.
  move /in_map_iff [k] [] /in_seq ?.
  exists k. split; [|done].
Qed.


Lemma In_None_pathE k x :
  In None (path k x) steps k x = None.
Proof.
  move /In_pathE [k' [?]] /(steps_k_monotone k). apply. .
Qed.


Lemma In_pathI k x K : k < K In (steps k x) (path K x).
Proof.
  move ?. apply /in_map_iff. exists k. split; first done.
  apply /in_seq. .
Qed.


Lemma path_S {k x} y : steps 1 x = Some y path (S k) x = (Some x) :: (path k y).
Proof.
  move Hxy. rewrite /path /= -seq_shift map_map.
  congr cons. apply: map_ext - ? /=.
  move: Hxy /=.
  case: (mm2_sig_step_dec M x) [[?]|]; last done.
  by move _ [].
Qed.


Lemma path_plus {k k' x} y : steps k x = Some y
  path (k+k') x = path k x path k' y.
Proof.
  move Hxy. rewrite /path seq_app map_app /=.
  congr app.
  have : seq k k' = map ( i k+i) (seq 0 k').
  { elim: k'; first done.
    move k' IH. have : S k' = k' + 1 by .
    by rewrite ?seq_app IH map_app. }
  rewrite map_map. apply: map_ext - ?.
  by rewrite steps_plus' Hxy.
Qed.


Lemma path_S_last {k x} : path (S k) x = (path k x) [steps k x].
Proof. by rewrite /path seq_S map_app. Qed.

Lemma steps_loop_mod {K x k} : steps (S K) x = Some x
  steps k x = steps (k mod (S K)) x.
Proof.
  rewrite [in steps k x](Nat.div_mod_eq k (S K)).
  move: (k mod (S K)) k' Hx. elim: (k / S K).
  - congr steps. .
  - move n IH. have : S K * S n + k' = S K + (S K * n + k') by .
    by rewrite steps_plus' Hx.
Qed.


Lemma path_loopE K x : In (steps K x) (path K x)
   k, In (steps k x) (path K x).
Proof.
  elim: K x; first done.
  move K IH x. rewrite (steps_plus' (k := 1) (k' := K)).
  case Hxz: (steps 1 x) [z|].
  - move H. rewrite (path_S z Hxz) /= in H. case: H.
    + move Hzx k. have /steps_loop_mod : steps (S K) x = Some x.
      { by rewrite (steps_plus' (k := 1) (k' := K)) Hxz. }
      by apply /In_pathI /(Nat.mod_upper_bound k (S K)).
    + rewrite (path_S z Hxz).
      move /IH {}IH [|k]; first by left.
      rewrite (steps_plus' (k := 1) (k' := k)) Hxz. right. by apply: IH.
  - move /in_map_iff [k] [Hk] /in_seq HK.
    move k'. have [|Hkk'] : k' < k k k' by .
    + move ?. apply: In_pathI. .
    + move: (Hk) /(steps_k_monotone k') /(_ Hkk') .
      rewrite /= in Hk. rewrite -Hk. apply: In_pathI. .
Qed.


Lemma path_loopE' K x : In (steps K x) (path K x)
   y, reaches x y In (Some y) (path K x).
Proof.
  move /path_loopE H y /reaches_steps [k] H'. move: (H k).
  by congr In.
Qed.


Lemma loop_bounded K x : In (steps K x) (path K x) bounded K x.
Proof.
  move /path_loopE' H.
  exists (map ( oy if oy is Some y then y else x) (path K x)).
  split. { by rewrite map_length path_length. }
  move y /H {}H. apply /in_map_iff. by exists (Some y).
Qed.


Lemma path_noloopI k x :
   In (steps k x) (path k x) NoDup (path (k + 1) x).
Proof.
  elim: k x.
  { move ??. constructor; [done| constructor]. }
  move k IH x.
  rewrite path_S_last /steps in_app_iff /= -/(steps k x).
  move /Decidable.not_or.
  have [|/IH ?] := In_dec option_mm2_state_eq_dec (steps k x) (path k x).
  - move /path_loopE /(_ (S k)). tauto.
  - move [?] ?.
    apply /(NoDup_Add (a := steps (S k) x) (l := path (k + 1) x)).
    + rewrite path_S_last.
      have := Add_app (steps (k + 1) x) (path (k + 1) x) [].
      congr Add.
      * congr steps. .
      * by rewrite app_nil_r.
    + constructor; first done.
      have : k + 1 = S k by .
      rewrite path_S_last in_app_iff /=. tauto.
Qed.


Lemma mortal_bounded {K x} : steps K x = None bounded K x.
Proof.
  move HK.
  exists (map ( oy if oy is Some y then y else x) (path K x)).
  split. { by rewrite map_length path_length. }
  move y /reaches_steps [k]. have [?|?] : k < K K k by .
  - move Hk. apply /in_map_iff. exists (Some y).
    split; first done.
    rewrite -Hk. by apply: In_pathI.
  - by move: HK /(steps_k_monotone k) /(_ ltac:()) .
Qed.


Lemma NoDup_not_bounded {K x y} :
  steps K x = Some y NoDup (path (K + 1) x) not (bounded K x).
Proof.
  move Hxy HK [L [? HL]].
  apply: (pigeonhole (path (K+1) x) (map Some L)).
  - move [z|] /in_map_iff [k] [Hk] /in_seq ?.
    { apply /in_map_iff. exists z. split; first done.
      apply: HL. by apply: (steps_reaches Hk). }
    by move: Hk Hxy /(steps_k_monotone K) /(_ ltac:()) .
  - rewrite map_length path_length. .
  - done.
Qed.


Lemma pointwise_decision K x : {bounded K x} + {not (bounded K x)}.
Proof.
  case HK: (steps K x) [y|].
  - have [Hy|Hy] := In_dec option_mm2_state_eq_dec (Some y) (path K x).
    + left. apply: loop_bounded. by rewrite HK.
    + right. apply: (NoDup_not_bounded HK).
      apply: path_noloopI. by rewrite HK.
  - left. by apply: mortal_bounded.
Qed.


Lemma shift_steps_a k K p a b :
  k K
  steps k (p, (K + a, b)) =
  match steps k (p, (K, b)) with
  | Some (p', (a', b')) Some (p', (a' + a, b'))
  | None None
  end.
Proof.
  elim: k K p a b. { done. }
  move k IH [|K] p a b ? /=; [|].
  case: (mm2_sig_step_dec M (p, (S (K + a), b))) [[[ [ ]]]|].
  - move /(mm2_step_parallel (p, (S K, b))) /= /(_ ltac:()).
    move [[ [ ]]] /= [+] [?] ?.
    move /[dup] /mm2_step_values_bound /= ?.
    case: (mm2_sig_step_dec M (p, _)) [[?]|] /=; first last.
    { by move /[apply]. }
    move /mm2_step_det /[apply] . subst .
    have [ ]: = K + ( - K) = K + ( - K) by .
    have : = by .
    rewrite IH; [|]. rewrite IH; [|].
    case: (steps k (, (K, ))); last done.
    move [? [? ?]] /=. congr (Some (_, (_, _))); .
  - move /mm2_stop_index_iff /= ?.
    case: (mm2_sig_step_dec M (p, (S K, b))) [[?]|]; last done.
    move [?] [/mm2_instr_at_bounds] /=. .
Qed.


Lemma shift_steps_b k K p a b :
  k K
  steps k (p, (a, K + b)) =
  match steps k (p, (a, K)) with
  | Some (p', (a', b')) Some (p', (a', b' + b))
  | None None
  end.
Proof.
  elim: k K p a b. { done. }
  move k IH [|K] p a b ? /=; [|].
  case: (mm2_sig_step_dec M (p, (a, S (K + b)))) [[[ [ ]]]|].
  - move /(mm2_step_parallel (p, (a, S K))) /= /(_ ltac:()).
    move [[ [ ]]] /= [+] [?] ?.
    move /[dup] /mm2_step_values_bound /= ?.
    case: (mm2_sig_step_dec M (p, _)) [[?]|] /=; first last.
    { by move /[apply]. }
    move /mm2_step_det /[apply] . subst .
    have [ ]: = K + ( - K) = K + ( - K) by .
    have : = by .
    rewrite IH; [|]. rewrite IH; [|].
    case: (steps k (, (, K))); last done.
    move [? [? ?]] /=. congr (Some (_, (_, _))); .
  - move /mm2_stop_index_iff /= ?.
    case: (mm2_sig_step_dec M (p, (a, S K))) [[?]|]; last done.
    move [?] [/mm2_instr_at_bounds] /=. .
Qed.


Lemma shift_path_a K p a b :
  path (K+1) (p, (K+a, b)) =
  map ( oy if oy is Some (p', (a', b')) then Some (p', (a'+a, b')) else None) (path (K+1) (p, (K, b))).
Proof.
  rewrite /path map_map. apply: map_ext_in k /in_seq ?.
  apply: shift_steps_a. .
Qed.


Lemma shift_path_b K p a b :
  path (K+1) (p, (a, K+b)) =
  map ( oy if oy is Some (p', (a', b')) then Some (p', (a', b'+b)) else None) (path (K+1) (p, (a, K))).
Proof.
  rewrite /path map_map. apply: map_ext_in k /in_seq ?.
  apply: shift_steps_b. .
Qed.


Lemma path_NoDup_a_bound K p a b : K a NoDup (path (K+1) (p, (a, b))) NoDup (path (K+1) (p, (K, b))).
Proof.
  move ?. have : a = K+(a-K) by .
  rewrite shift_path_a. by apply: NoDup_map_inv.
Qed.


Lemma path_NoDup_b_bound K p a b : K b NoDup (path (K+1) (p, (a, b))) NoDup (path (K+1) (p, (a, K))).
Proof.
  move ?. have : b = K+(b-K) by .
  rewrite shift_path_b. by apply: NoDup_map_inv.
Qed.


#[local] Notation l := (length M).

Lemma fixed_decision K :
  { x : mm2_state, bounded K x} + { ( x : mm2_state, bounded K x)}.
Proof.
  have := Forall_dec ( 'x bounded K x) (pointwise_decision K)
    (list_prod (seq 1 l) (list_prod (seq 0 (K+1)) (seq 0 (K+1)))).
  case; first last.
  { move H. right HK. apply /H /Forall_forall. move ??. by apply: HK. }
  wlog: K /(0 < K).
  { move: K [|K] H HK.
    - right. move /(_ (0, (0, 0))) [[|? L] [/= ? /(_ (0, (0, 0))) HL]].
      + apply: HL. by apply: rt_refl.
      + .
    - apply: H; [|done]. }
  move ? HK. left x.
  have [|/path_noloopI] := In_dec option_mm2_state_eq_dec (steps K x) (path K x).
  { by apply: loop_bounded. }
  case Hz: (steps K x) [z|]; first last.
  { move _. by apply: mortal_bounded. }
  
  move Hx. exfalso.
  move: x Hx Hz [p [a b]] Hx Hz.
  have Hp : 0 < p l.
  { move: Hz. have : K = 1 + (K - 1) by .
    rewrite steps_plus' /=.
    case: (mm2_sig_step_dec M (p, (a, b))) [[?]|]; last done.
    by move [?] [/mm2_instr_at_bounds] /=. }
  move: Hx Hz.
  wlog: a b z /(a K b K); first last.
  { move ? Hx Hz. suff: bounded K (p, (a, b)).
    { by apply: (NoDup_not_bounded Hz). }
    move: HK /Forall_forall.
    apply. apply: in_prod; [|apply: in_prod]; apply /in_seq; . }
  move .
  wlog: a b z /(a K).
  { move H. have [/H|] : a K a = K + (a - K) by .
    { by apply. }
    move /path_NoDup_a_bound /(_ ltac:()) /H {H}.
    rewrite shift_steps_a; first done.
    case: (steps K (p, (K, b))) [y|]; last done.
    move H _. by apply: (H y). }
  move ?. have [?|] : b K b = K + (b - K) by .
  { move / H /H. by apply. }
  move /path_NoDup_b_bound /(_ ltac:()) /.
  rewrite shift_steps_b; first done.
  case: (steps K (p, (a, K))) [y|]; last done.
  move H _. by apply: (H y).
Qed.


Lemma uniform_decision_aux1 x : let n := l*(l+1) in
  (bounded (l*n*n+1) x) +
  { y | ( k, k l*n*n steps k x = Some y) (n value1 y n value2 y) }.
Proof.
  move n.
  have [|/path_noloopI Hx] :=
    In_dec option_mm2_state_eq_dec (steps (l*n*n) x) (path (l*n*n) x).
  { move /loop_bounded H. left. apply: (bounded_monotone _ H). . }
  case Hxy: (steps (l*n*n+1) x) [y|]; first last.
  { left. by apply: mortal_bounded. }
  right.
  have [/pigeonhole|] := incl_dec option_mm2_state_eq_dec (path (l*n*n+1) x)
    (map Some (list_prod (seq 1 l) (list_prod (seq 0 n) (seq 0 n)))).
  { move H. exfalso. apply: (H _ Hx).
    rewrite path_length map_length ?prod_length ?seq_length. . }
  move /(not_inclE option_mm2_state_eq_dec) [[z|]].
  - move H. exists z.
    move: H [/in_map_iff] [k] [Hk] /in_seq ? H.
    split. { exists k. split; [|done]. }
    suff : not (value1 z < n value2 z < n) by .
    move H'. apply: H. apply /in_map_iff. exists z. split; first done.
    have := steps_sub Hk Hxy ltac:().
    have /=: l * n * n + 1 - k = S (Nat.pred (l * n * n + 1 - k)) by .
    case: (mm2_sig_step_dec M z) [[?]|]; [|done].
    move: z {Hk} H' [? [? ?]] /= ? [?] /= [/mm2_instr_at_bounds ? _] _.
    apply /in_prod; [|apply /in_prod]; apply /in_seq; .
  - move [/in_map_iff] H. exfalso.
    move: H [k] [+ /in_seq ?].
    move /(steps_k_monotone (l*n*n+1)) /(_ ltac:()).
    by rewrite Hxy.
Qed.


Lemma k_step_iter k p a1 b1 a2 b2 :
  (k = ) (k = )
  steps k (p, (, )) = Some (p, (, ))
  let ca := if Nat.eq_dec then 0 else 1 in
  let cb := if Nat.eq_dec then 0 else 1 in
   i n a b, i n
    steps (i*k) (p, (+ca*(a+n*),+cb*(b+n*))) =
      Some (p, (+ca*(a+(n-i)*+i*),+cb*(b+(n-i)*+i*))).
Proof.
  move Ha Hb Hk ca cb. elim.
  { move ????. congr (Some (_, (_, _))); . }
  move i IH [|n] a b; first by .
  move /(iffRL (Nat.succ_le_mono _ _)) /IH {}IH.
  rewrite /= steps_plus'.
  have := IH (+a) (+b). congr eq; first last.
  { congr (Some (_, (_, _))); . }
  have : steps (i * k) (p, ( + ca * ( + a + n * ), + cb * ( + b + n * ))) =
    obind (steps (i * k)) (Some (p, ( + ca * ( + a + n * ), + cb * ( + b + n * )))) by done.
  congr obind.
  rewrite /ca /cb.
  move: (Nat.eq_dec ) (Nat.eq_dec ) [?|?] [?|?] /=.
  - rewrite ?Nat.add_0_r Hk.
    congr (Some (_, (_, _))); .
  - rewrite shift_steps_b; first .
    rewrite ?Nat.add_0_r Hk.
    congr (Some (_, (_, _))); .
  - rewrite shift_steps_a; first .
    rewrite ?Nat.add_0_r Hk.
    congr (Some (_, (_, _))); .
  - rewrite shift_steps_a; first .
    rewrite shift_steps_b; first .
    rewrite ?Nat.add_0_r Hk.
    congr (Some (_, (_, _))); .
Qed.


Lemma not_uniformly_boundedI k p a1 b1 a2 b2 :
  (k = ) (k = )
  ( )
  steps k (p, (, )) = Some (p, (, ))
  not (mm2_uniformly_bounded M).
Proof.
  move /k_step_iter H /H {}H Hab /H /= + [K].
  move /(_ _ K 0 0) /=.
  move Ha: ( + _ * _) a.
  move Hb: ( + _ * _) b.
  move {}H /(_ (p, (a, b))) [L [? HL]].
  have : incl (map ( i steps (i * k) (p, (a, b))) (seq 0 (K+1))) (map Some L).
  { move z /in_map_iff [i] [ /in_seq ?]. rewrite H; first by .
    apply: in_map. apply: HL. apply: (steps_reaches (k := (i*k))). rewrite H; [|done]. }
  move /pigeonhole. apply.
  { rewrite ?map_length seq_length. . }
  under map_ext_in.
  { move i /in_seq ?. rewrite H; first by . over. }
  apply: NoDup_map_ext; last by apply: seq_NoDup.
  move /in_seq ? /in_seq ? [].
  move: (Nat.eq_dec ) (Nat.eq_dec ) [?|?] [?|?] /=; nia.
Qed.


Lemma uniform_decision_aux2 x : ({l*(l+1) value1 x} + {l*(l+1) value2 x})
  (bounded (l*l+1) x) + (not (mm2_uniformly_bounded M)) +
    { y | ( k, k l*l steps k x = Some y) (l value1 y l value2 y) }.
Proof.
  move Hlx.
  have [|/path_noloopI Hx] :=
    In_dec option_mm2_state_eq_dec (steps (l*l) x) (path (l*l) x).
  { move /loop_bounded H. left. left. apply: (bounded_monotone _ H). . }
  case Hxy: (steps (l*l+1) x) [y|]; first last.
  { left. left. by apply: mortal_bounded. }
  pose P := oz : option mm2_state if oz is Some z then
    (if Hlx then l value2 z else l value1 z) else True.
  have HP : x, {P x} + {not (P x)}.
  { move [? /= |]; last by left. clear P.
    case: Hlx ?; by apply: Compare_dec.le_dec. }
  have [|] := Exists_dec P (path (l * l + 1) x) HP.
  { move /(Exists_sig P HP) [[z|]] [Hz /= ].
    - right. exists z. move: Hz /In_pathE [k [? Hk]]. split.
      + exists k. split; [|done].
      + move: Hk /steps_values_bound. clear P HP.
        case: Hlx /=; .
    - exfalso. by move: Hz Hxy /In_None_pathE . }
  
  left. right. subst P.
  have /pigeonhole : incl
    (map ( oz if oz is Some (p, (a, b)) then (if Hlx then (p, b) else (p, a)) else (0, 0)) (path (l * l + 1) x))
    (list_prod (seq 1 l) (seq 0 l)).
  { move [p c] /in_map_iff [[[p' [a' b']]|]]; first last.
    { move [_ /In_pathE].
      move [?] [?] /(steps_k_monotone (l * l + 1)) /(_ ltac:()).
      by rewrite Hxy. }
    move [+ H].
    have ? : 0 < p' l.
    { move: H /in_map_iff [k'] [Hk' /in_seq ?].
      have := steps_sub Hk' Hxy ltac:().
      have /=: l * l + 1 - k' = S (l * l + 1 - k' - 1) by .
      case: (mm2_sig_step_dec M (p', (a', b'))) [[?]|]; [|done].
      by move [?] [/mm2_instr_at_bounds]. }
    case: Hlx HP /= ? HP.
    - move [? ?]. subst p c.
      move: H /Forall_Exists_neg /Forall_forall H /H{H} /= ?.
      apply /in_prod; apply /in_seq; .
    - move [? ?]. subst p c.
      move: H /Forall_Exists_neg /Forall_forall H /H{H} /= ?.
      apply /in_prod; apply /in_seq; . }
  apply: unnest. { rewrite map_length ?prod_length ?seq_length path_length. . }
  rewrite /path map_map. move /(dup_seq prod_nat_nat_eq_dec) [[i j]].
  move [+ ?].
  case Hi: (steps i x) [[p [ ]]|]; first last.
  { move: Hi /(steps_k_monotone (l*l+1)) /(_ ltac:()). by rewrite Hxy. }
  case Hj: (steps j x) [[p' [ ]]|]; first last.
  { move: Hj /(steps_k_monotone (l*l+1)) /(_ ltac:()). by rewrite Hxy. }
  clear .
  have ? : not (p = p' = = ).
  { move [? [? ?]]. subst p' .
    move: Hx. rewrite /path.
    have : l*l+1 = i + (S (j-i-1)) + (S (l*l -j)) by .
    rewrite seq_app seq_app /= ?map_app /= (NoDup_count_occ option_mm2_state_eq_dec).
    move /(_ (Some (p, (, )))). have : i + S (j - i - 1) = j by .
    rewrite Hi Hj ?count_occ_app /=. case: (option_mm2_state_eq_dec _ _); [|done]. }
  case: Hlx HP /= ? HP.
  - move [? ?]. subst p' .
    have ? : by .
    have ? : j-i .
    { move: Hi /steps_values_bound /=. . }
    move: Hi Hj /steps_sub H /H{H} /(_ ltac:()).
    move /not_uniformly_boundedI. apply; .
  - move [? ?]. subst p' .
    have ? : by .
    have ? : j-i .
    { move: Hi /steps_values_bound /=. . }
    move: Hi Hj /steps_sub H /H{H} /(_ ltac:()).
    move /not_uniformly_boundedI. apply; .
Qed.


Lemma uniform_decision_aux3 x : l value1 x l value2 x (bounded (l+1) x) + (not (mm2_uniformly_bounded M)).
Proof.
  move ??.
  have [|/path_noloopI Hx] :=
    In_dec option_mm2_state_eq_dec (steps (l) x) (path (l) x).
  { move /loop_bounded H. left. apply: (bounded_monotone _ H). . }
  case Hxy: (steps (l+1) x) [y|]; first last.
  { left. by apply: mortal_bounded. }
  right.   have /pigeonhole : incl
    (map ( oz if oz is Some (p, (a, b)) then p else 0) (path (l + 1) x))
    (seq 1 l).
  { move p /in_map_iff [[[p' [a' b']]|]]; first last.
    { move [_ /In_pathE].
      move [?] [?] /(steps_k_monotone (l + 1)) /(_ ltac:()).
      by rewrite Hxy. }
    move [] H. apply /in_seq.
    move: H /in_map_iff [k'] [Hk' /in_seq ?].
    have := steps_sub Hk' Hxy ltac:().
    have /=: l + 1 - k' = S (l + 1 - k' - 1) by .
    case: (mm2_sig_step_dec M (p, (a', b'))) [[?]|]; [|done].
    move [?] [/mm2_instr_at_bounds] /=. . }
  apply: unnest. { rewrite map_length ?seq_length path_length. . }
  rewrite /path map_map. move /(dup_seq Nat.eq_dec) [[i j]].
  move [+ ?].
  case Hi: (steps i x) [[p [ ]]|]; first last.
  { move: Hi /(steps_k_monotone (l+1)) /(_ ltac:()). by rewrite Hxy. }
  case Hj: (steps j x) [[p' [ ]]|]; first last.
  { move: Hj /(steps_k_monotone (l+1)) /(_ ltac:()). by rewrite Hxy. }
  move ?. subst p'.
  have ? : .
  { suff : not ( = = ) by . move [??]. subst .
    move: Hx. rewrite /path.
    have : l+1 = i + (S (j-i-1)) + (S (l -j)) by .
    rewrite seq_app seq_app /= ?map_app /= (NoDup_count_occ option_mm2_state_eq_dec).
    move /(_ (Some (p, (, )))). have : i + S (j - i - 1) = j by .
    rewrite Hi Hj ?count_occ_app /=. case: (option_mm2_state_eq_dec _ _); [|done]. }
  have ?: j - i j - i .
  { move: Hi /steps_values_bound /=. . }
  have := steps_sub Hi Hj ltac:().
  move /not_uniformly_boundedI. apply; .
Qed.


Lemma uniformly_bounded_empty : mm2_uniformly_bounded [].
Proof.
  exists 1. move x. exists [x]. split; first done.
  move y /clos_rt_rt1n_iff [].
  - by left.
  - by move ?? [?] [] [[|??]] [?] [].
Qed.


Lemma reaches_bounded {K k x y} : steps k x = Some y bounded K y bounded (k+K) x.
Proof.
  elim: k x. { by move x /= []. }
  move k IH x /=.
  case: (mm2_sig_step_dec M x) [[z /mm2_step_det Hxz]|]; last done.
  move /IH /[apply] - [L] [H1L H2L]. exists (x::L) /=.
  split; [|].
  move z' /clos_rt_rt1n_iff Hxz'. case: Hxz' Hxz.
  - move *. by left.
  - move > + /clos_rt_rt1n_iff + Hxz /Hxz /H2L ?. by right.
Qed.


Lemma bound_on_uniform_bound : mm2_uniformly_bounded M
   x, bounded ((l+1)*(l+1)*(l+1)*(l+1)*(l+1)) x.
Proof.
  move HM x.
  set K := ((l+1)*(l+1)*(l+1)*(l+1)*(l+1)).
    have [|[y [[ [ Hxy]] ?]]] := uniform_decision_aux1 x.
    { apply: bounded_monotone. . }
    have : K = + (K - ) by .
    apply: (reaches_bounded Hxy).
    have : {l * (l + 1) value1 y} + {l * (l + 1) value2 y}.
    { case H: (l * (l + 1) - value1 y) [|?]; [left|right]; . }
    move /uniform_decision_aux2 [[|]|[z]].
    - apply: bounded_monotone. .
    - by move /(_ HM).
    - move [[ [? Hyz]]] [/uniform_decision_aux3 H /H{H}].
      move [/bounded_monotone Hz|].
      + have : K - = + (K - - ) by .
        apply: (reaches_bounded Hyz). apply: Hz. .
      + by move /(_ HM).
Qed.


Theorem decision : (mm2_uniformly_bounded M) + (not (mm2_uniformly_bounded M)).
Proof.
  wlog ? : /(l > 0).
  { move: (M) [|? ?] /=.
    - move _. left. by apply: uniformly_bounded_empty.
    - apply. . }
  pose K := (l+1)*(l+1)*(l+1)*(l+1)*(l+1).
  have [?|HK] := fixed_decision K. { left. by exists K. }
  
  right. move /bound_on_uniform_bound HM.
  apply: HK x. by apply: HM.
Qed.


End Construction.

Require Import Undecidability.Synthetic.Definitions.

Definition decide : list mm2_instr bool :=
   M
    match decision M with
    | inl _ true
    | inr _ false
    end.

Lemma decide_spec : decider decide MM2_UBOUNDED.
Proof.
  rewrite /decider /reflects /decide M.
  case: (decision M); intuition done.
Qed.