Require Import Arith Lia Relation_Operators Operators_Properties List.
Import ListNotations.

From Undecidability.StackMachines.Util Require Import Nat_facts List_facts.
Require Import Undecidability.StackMachines.SMN.

Require Import ssreflect ssrbool ssrfun.

Set Default Goal Selector "!".

Local Definition rt_rt1n := @clos_rt_rt1n_iff Config.

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

Lemma stepI {M: SMN} {X Y: Config} v w l r l' r' x y : X = (l v, r w, x) Y = (l' v, r' w, y)
  In ((l, r, x), (l', r', y)) M step M X Y.
Proof. move /transition. by apply. Qed.

Lemma step_incl {M1 M2 X Y} : incl step X Y step X Y.
Proof. move HM1M2. case > /HM1M2. by apply: transition. Qed.

Lemma deterministic_confluent {M} : deterministic M confluent M.
Proof.
  move HM ? ? + /rt_rt1n . elim: .
  { move *. eexists. by constructor; last by apply: rt_refl. }
  move ? ? ? /rt_rt1n Hy1z1 IH ? /rt_rt1n . case: .
  - move ?. eexists. constructor; first by apply: rt_refl.
    apply: rt_trans; last by eassumption. apply: rt_step. by eassumption.
  - move > /rt_rt1n Hy2z2 . have ? := HM _ _ _ . subst.
    by apply: IH.
Qed.


Inductive reachable_n (M: SMN) : Config Config Prop :=
  | rn_refl n X : reachable_n M n X X
  | rn_step n X Y Z: step M X Y reachable_n M n Y Z reachable_n M (1+n) X Z.

Lemma reachable_0E {M X Y} : reachable_n M 0 X Y X = Y.
Proof.
  move Hn: (0) n HXY. case: HXY Hn; first done. by .
Qed.


Lemma reachable_SnE {M n X Z} : reachable_n M (1+n) X Z
  X = Z ( Y, step M X Y reachable_n M n Y Z).
Proof.
  move Hn': (1+n) n' HXY. case: HXY Hn'; first by (move *; left).
  move {}n' *. right. have : n = n' by . by firstorder done.
Qed.


Lemma reachable_n_incl {M1 M2 n X Y} : incl reachable_n n X Y reachable_n n X Y.
Proof.
  move H. elim: n X Y.
  { move > /reachable_0E . by apply: rn_refl. }
  move n IH > /reachable_SnE. case.
  - move . by apply: rn_refl.
  - move [?] [? ?]. apply: rn_step.
    + apply: step_incl; by eassumption.
    + by apply: IH.
Qed.


Lemma reachable_to_reachable_n {M X Y} : reachable M X Y n, reachable_n M n X Y.
Proof.
  move /rt_rt1n. elim; first by (move ?; exists 0; apply: rn_refl).
  move > ? _ [n ?]. exists (1+n). apply: rn_step; by eassumption.
Qed.


Lemma reachable_n_to_reachable {M n X Y} : reachable_n M n X Y reachable M X Y.
Proof.
  elim; first by (move *; apply: rt_refl).
  move *. apply: rt_trans; last by eassumption.
  by apply: rt_step.
Qed.


Lemma reachable_incl {M1 M2 X Y} : incl reachable X Y reachable X Y.
Proof.
  move /reachable_n_incl H /reachable_to_reachable_n [?] ?.
  apply: reachable_n_to_reachable. apply: H. by eassumption.
Qed.


Lemma confluent_incl {M1 M2} : incl incl confluent confluent .
Proof.
  move /reachable_incl /reachable_incl ? ? ? / / {} / / [? [? ?]].
  eexists. constructor; apply: ; by eassumption.
Qed.


Lemma reachable_n_monotone {M X Y m n} : m n reachable_n M m X Y reachable_n M n X Y.
Proof.
  elim: n m X Y.
  { move m > ?. have : m = 0 by . move /reachable_0E . by apply: rn_refl. }
  move n IH [|m] > ?.
  { move /reachable_0E . by apply: rn_refl. }
  move /reachable_SnE [ | [Z [? ?]]]; first by apply: rn_refl.
  apply: rn_step; first by eassumption.
  apply: IH; last by eassumption. by .
Qed.


Lemma step_app {M1 M2 x y} : step ( ) x y step x y step x y.
Proof. case >. rewrite in_app_iff. case /transition ?; [by left | by right]. Qed.

Lemma reachable_n_stack_app {M n l r x l' r' y v w} :
  reachable_n M n (l, r, x) (l', r', y) reachable_n M n (l v, r w, x) (l' v, r' w, y).
Proof.
  elim: n l r x l' r' y.
  { move > /reachable_0E [] . apply: rn_refl. }
  move n IH l r x l' r' y /reachable_SnE [[] | [z] [+]]; first by apply: rn_refl.
  move Hx': (l, r, x) x' . case: Hx'.
  move > H [] /IH {}IH. apply: rn_step; last by eassumption.
  rewrite -?app_assoc. by apply: transition.
Qed.


Lemma reachable_stack_app {M l r x l' r' y v w} :
  reachable M (l, r, x) (l', r', y) reachable M (l v, r w, x) (l' v, r' w, y).
Proof.
  move /reachable_to_reachable_n [?] /reachable_n_stack_app ?. by apply: reachable_n_to_reachable.
Qed.


Lemma length_preserving_incl {M1 M2} : incl length_preserving length_preserving .
Proof. by move > / /. Qed.

Lemma length_preservingP {M l r x l' r' y} :
  length_preserving M reachable M (l, r, x) (l', r', y)
  (l, r, x) = (l', r', y) (length (l r) = length (l' r') 1 length (l r)).
Proof.
  move HM /reachable_to_reachable_n [n]. elim: n l r x l' r' y.
  { move > /reachable_0E ?. by left. }
  move n IH l r x l' r' y /reachable_SnE [? | [Z] []]; first by left.
  move HX: (l, r, x) X HXZ. case: HXZ HX.
  move > /HM []. rewrite ?app_length. move ? ? [] ? ? ?. subst.
  move /IH. case.
  - move [] *. subst. rewrite ?app_length. right. by .
  - rewrite ?app_length. move [] ? ?. right. by .
Qed.


Lemma next_configs M (X: Config) : L, ( Y, step M X Y In Y L) length L length M.
Proof.
  elim: M.
  { exists []. constructor > /=; [by case | by ]. }
  move: X [[lx rx] x] [[[l r] y] [[l' r'] z]] M [L [HL ?]].
  have [[] * | Hy] : (firstn (length l) lx, firstn (length r) rx, x) = (l, r, y)
    (firstn (length l) lx, firstn (length r) rx, x) (l, r, y) by do 4 decide equality.
  - exists ((l' skipn (length l) lx, r' skipn (length r) rx, z) :: L).
    constructor; last by (move /=; ).
    move HX: (lx, rx, x) X Z HXZ. case: HXZ HX v w > /=. case.
    + move + [] [[]] *. subst. left.
      by rewrite ?skipn_app ?skipn_all ?Nat.sub_diag /=.
    + move /transition /(_ v w) ? ?. right. apply: HL. by congruence.
  - exists L. constructor; last by (move /=; ).
    move HX: (lx, rx, x) X Z HXZ. case: HXZ HX v w > /=. case.
    + move + [] [[]] *. subst. exfalso. apply: Hy.
      by rewrite ?firstn_app ?firstn_all ?Nat.sub_diag ?app_nil_r.
    + move /transition /(_ v w) ? ?. apply: HL. by congruence.
Qed.


Lemma next_n_configs M (n: ) (Xs: list Config) :
   L, ( X Y, In X Xs reachable_n M n X Y In Y L) (length L (Nat.pow (1 + length M) n) * length Xs * (1+n)).
Proof.
  elim: n Xs.
  - move Xs. exists Xs. constructor; last by (move /=; ).
    by move X Y ? /reachable_0E .
  - move n IH Xs.
    have [Ys [HYs ?]]: L, ( X Y, In X Xs step M X Y In Y L) length L (1 + length M) * length Xs.
    {
      clear. elim: Xs.
      { exists []. constructor; [done | by move /=; ]. }
      move X Xs [L [HL ?]]. have [LX [HLX ?]] := next_configs M X.
      exists (LX L). constructor; first last.
      - rewrite app_length /length -?/(length _). by .
      - move > /=. rewrite in_app_iff. move [ /HLX ? | * ]; first by left.
        right. apply: HL; by eassumption. }
    have [L [HL ?]] := IH Ys. exists (Xs L). constructor.
    { move X Y HX /reachable_SnE. case.
      - move . apply /in_app_iff. by left.
      - move [Z] [/HYs] /(_ HX) /HL H /H ?. apply /in_app_iff. by right. }
    rewrite app_length.
    suff: length L (1 + length M) ^ S n * length Xs * (1 + n).
    { have := Nat.pow_nonzero (1 + length M) (S n) ltac:(). by nia. }
    rewrite /Nat.pow -/Nat.pow.
    have ? := Nat.pow_nonzero (1 + length M) n ltac:().
    suff: (1 + length M) ^ n * length Ys (1 + length M) * (1 + length M) ^ n * length Xs by nia.
    by nia.
Qed.


Lemma concat_reachable {M} {NM: } (xs : list Config) : bounded M NM
   L, ( x y, In x xs reachable M x y In y L) length L NM * length xs.
Proof.
  move bounded_M. elim: xs.
  { exists []. constructor; [done | by (move /=; ) ]. }
  move x xs [Lxs [HLxs ?]]. have [Lx [HLx ?]] := bounded_M x.
  exists (Lx Lxs). constructor; last by (rewrite app_length /=; ).
  move ? ? /=. rewrite in_app_iff. case.
  - move /HLx *. by left.
  - move *. right. apply: HLxs; by eassumption.
Qed.