Require Import List Lia Relation_Operators.
Import ListNotations.

From Undecidability.StackMachines.Util Require Import Nat_facts List_facts.
Require Import Undecidability.StackMachines.Reductions.CM1_HALT_to_SMNdl_UB.SMX.

Require Import ssreflect ssrbool ssrfun.

Set Default Proof Using "Type".
Set Default Goal Selector "!".

Section SMX_facts.
Context {State Symbol : Set}.

Local Definition Config := @Config State Symbol.

Inductive reachable_n (M: SMX) : nat -> Config -> Config -> Prop :=
  | reach_refl (n: nat) (X: Config) : reachable_n M n X X
  | reach_step (n: nat) (X Y Z: Config) : step M X Y -> reachable_n M n Y Z -> reachable_n M (1+n) X Z.

Definition terminal (M: SMX) (X: Config) : Prop :=
  forall (Y: Config), not (step M X Y).

Definition maybe_reachable (M: SMX) (n: nat) (X Y: Config) : Prop :=
  reachable_n M n X Y \/ (exists Z, reachable_n M n X Z /\ terminal M Z).

Lemma reachable_n_maybe_reachable {M n X Y} : reachable_n M n X Y-> maybe_reachable M n X Y.
Proof. move=> ?. by left. Qed.

Lemma terminal_maybe_reachable {M n X Y} : terminal M X -> maybe_reachable M n X Y.
Proof. move=> ?. right. exists X. constructor; [by apply: reach_refl | done]. Qed.

Lemma reachable_n_step {M X Y} : step M X Y -> reachable_n M 1 X Y.
Proof. move=> ?. apply: reach_step; [by eassumption | by apply: reach_refl]. Qed.

Lemma reachable_n_mon {M n m X Y} :
  n <= m -> reachable_n M n X Y -> reachable_n M m X Y.
Proof.
  elim: n m X Y.
  { move=> m X Y ?. move Hn: (0) => n HXY.
    case: HXY Hn => *; [by apply: reach_refl | by lia]. }
  move=> n IH m X Y Hnm. move Hn': (S n) => n' HXY.
  case: HXY Hn' => [|{}n'] *; first by apply: reach_refl.
  have ->: m = S (m - 1) by lia.
  apply: reach_step; first by eassumption. apply: IH; first by lia.
  by (have ->: n = n' by lia).
Qed.

Lemma reachable_n_trans {M} n m X Y Z :
  reachable_n M n X Y -> reachable_n M m Y Z -> reachable_n M (n+m) X Z.
Proof.
  elim: n X Y.
  { move=> X Y /=. move Hn: (0) => n HXY. case: HXY Hn; [done | by lia]. }
  move=> n IH X Y /=. move Hn': (S n) => n' HXY. case: HXY Hn' => [| {}n' {}X Y1 Y2] *.
  { apply: reachable_n_mon; last by eassumption. by lia. }
  have ?: n' = n by lia. subst n'.
  apply: reach_step; first by eassumption. by apply: IH; eassumption.
Qed.

Lemma reachable_n_refl' {M n X X'} :
  X = X' -> reachable_n M n X X'.
Proof. move=> ->. by apply: reach_refl. Qed.

Lemma reachable_n_mon' {M n n' X X' Y Y'} :
  n <= n' -> (X, Y) = (X', Y') -> reachable_n M n X Y -> reachable_n M n' X' Y'.
Proof. move=> ? [? ?] ?. subst. by apply: reachable_n_mon; eassumption. Qed.

Lemma reachable_n_trans' {M} n {m k X X' Y Z} :
  m+n <= k -> X = X' -> reachable_n M n Y Z -> reachable_n M m X Y -> reachable_n M k X' Z.
Proof. move /reachable_n_mon => H *. subst. apply: H. by apply: reachable_n_trans; eassumption. Qed.

Lemma reachable_n_reachable {M T x y} :
  reachable_n M T x y -> reachable M x y.
Proof.
  elim: T x y.
  { move HT: (0) => T x y Hxy. case: Hxy HT => *; [by apply: rt_refl | by lia]. }
  move=> T IH x y. move HT': (S T) => T' Hxy.
  case: Hxy HT'; first by (move=> *; apply: rt_refl).
  move=> {}T' {}x z {}y /(@rt_step Config) Hxz + ?.
  have ->: T' = T by lia. move /IH. by apply: rt_trans.
Qed.

Lemma maybe_reachable_refl' {M n X Y} : X = Y -> maybe_reachable M n X Y.
Proof. move=> ->. left. by apply: reach_refl. Qed.

Lemma maybe_reachable_mon' {M n n' X X' Y Y'} :
  n <= n' -> (X, Y) = (X', Y') -> maybe_reachable M n X Y -> maybe_reachable M n' X' Y'.
Proof.
  move /reachable_n_mon => H [-> ->] [?|]; first by (left; apply: H).
  move=> [Z [HZ ?]]. right. exists Z. by constructor; [apply: H | ].
Qed.

Lemma maybe_reachable_trans' {M} n {m k X X' Y Z} :
  m + n <= k -> X = X' -> maybe_reachable M n Y Z -> maybe_reachable M m X Y -> maybe_reachable M k X' Z.
Proof.
  move /reachable_n_mon => H <- HYZ [?|]; first last.
  { move=> [Z' [HZ' ?]]. right. exists Z'. constructor; last done.
    apply: H. apply: reachable_n_mon; last by eassumption. by lia. }
  move: HYZ => [? | [Z' [HZ' ?]]].
  { left. apply: H. by apply: reachable_n_trans; eassumption. }
  right. exists Z'. constructor; last done.
  apply: H. by apply: reachable_n_trans; eassumption.
Qed.

Lemma first_step {M} (op : Instruction) (v w: list Symbol) {n X Z} :
  1 <= n -> In op M ->
  let '((r, s, x), (r', s', y), b) := op in
    X = (r ++ v, s ++ w, x) ->
    reachable_n M (n-1) (if b is true then (s' ++ w, r' ++ v, y) else (r' ++ v, s' ++ w, y)) Z ->
    reachable_n M n X Z.
Proof.
  move=> Hn. move: op=> [[[[r s] x] [[r' s'] y]] b].
  move /(transition M v w) /reachable_n_step => + ? ?. subst X.
  by (apply: (reachable_n_trans' (n-1)); first by lia).
Qed.

Lemma maybe_first_step {M} (op : Instruction) (v w: list Symbol) {n X Z} :
  1 <= n -> In op M ->
  let '((r, s, x), (r', s', y), b) := op in
    X = (r ++ v, s ++ w, x) ->
    maybe_reachable M (n-1) (if b is true then (s' ++ w, r' ++ v, y) else (r' ++ v, s' ++ w, y)) Z ->
    maybe_reachable M n X Z.
Proof.
  move=> Hn. move: op=> [[[[r s] x] [[r' s'] y]] b].
  move /(transition M v w) /reachable_n_step => HXY ? HYZ. subst X.
  move: HYZ => [? | [Z' [HZ' ?]]].
  - left. move: HXY. by (apply: (reachable_n_trans' (n-1)); first by lia).
  - right. exists Z'. constructor; last done.
    move: HXY. by (apply: (reachable_n_trans' (n-1)); first by lia).
Qed.

End SMX_facts.