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) : Config Config Prop :=
  | reach_refl (n: ) (X: Config) : reachable_n M n X X
  | reach_step (n: ) (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 :=
   (Y: Config), not (step M X Y).

Definition maybe_reachable (M: SMX) (n: ) (X Y: Config) : Prop :=
  reachable_n M n X Y ( 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 ]. }
  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 .
  apply: reach_step; first by eassumption. apply: IH; first by .
  by (have : n = n' by ).
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 ]. }
  move n IH X Y /=. move Hn': (S n) n' HXY. case: HXY Hn' [| {}n' {}X ] *.
  { apply: reachable_n_mon; last by eassumption. by . }
  have ?: n' = n by . 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 ]. }
  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 . 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 . }
  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 ).
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 ).
  - right. exists Z'. constructor; last done.
    move: HXY. by (apply: (reachable_n_trans' (n-1)); first by ).
Qed.


End SMX_facts.