Require Import List Lia.
Import ListNotations.
Require Import Relation_Operators Operators_Properties.

Require Import Undecidability.StackMachines.SMN.
Require Undecidability.StackMachines.SSM.

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

Require Import Undecidability.StackMachines.Util.SMN_transform.

Require Import ssreflect ssrbool ssrfun.

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

Module Argument.
Section Reduction.
  Variable M : SMN.
  Variable confluent_M : confluent M.
  Variable basic_M : Forall basic M.

  Definition encode_Instruction (op: Instruction) : SSM.instruction :=
    match op with
    | (([], [a], x), ([b], [], y)) => (x, y, a, b, false)
    | (([a], [], x), ([], [b], y)) => (x, y, a, b, true)
    | _ => (0, 0, true, true, true)
    end.

  Definition M' : SSM.ssm := map encode_Instruction M.

  Lemma basic_instructions : forall op, In op M -> basic op.
  Proof using basic_M. by apply /Forall_forall. Qed.

  Lemma simulation_step {x y} : step M x y -> SSM.step M' x y.
  Proof using basic_M.
    case=> v w l r l' r' {}x {}y Hop. move: Hop (Hop) => /basic_instructions.
    move H1op: (l, r, x, (l', r', y)) => op H2op. case: H2op H1op.
    - move=> > [] *. subst. apply: SSM.step_r. rewrite /M' in_map_iff. eexists. by constructor; last by eassumption.
    - move=> > [] *. subst. apply: SSM.step_l. rewrite /M' in_map_iff. eexists. by constructor; last by eassumption.
  Qed.

  Lemma simulation {x y} : reachable M x y -> SSM.reachable M' x y.
  Proof using basic_M.
    elim.
    - move=> ? ? /simulation_step ?. by apply: rt_step.
    - move=> *. by apply: rt_refl.
    - move=> *. apply: rt_trans; by eassumption.
  Qed.

  Lemma inverse_simulation_step {x y} : SSM.step M' x y -> step M x y.
  Proof using basic_M.
    case=> >.
    - rewrite /M' in_map_iff. move=> [[[[l r] {}x] [[l' r'] {}y]]] [] + HM.
      move: HM (HM) => /basic_instructions.
      move H1op: (l, r, x, (l', r', y)) => op H2op. case: H2op H1op.
      + move=> > /=. by congruence.
      + move=> > [] /= ? ? ? ? ? ? + [] *. subst. move /transition. by apply.
    - rewrite /M' in_map_iff. move=> [[[[l r] {}x] [[l' r'] {}y]]] [] + HM.
      move: HM (HM) => /basic_instructions.
      move H1op: (l, r, x, (l', r', y)) => op H2op. case: H2op H1op.
      + move=> > [] /= ? ? ? ? ? ? + [] *. subst. move /transition. by apply.
      + move=> > /=. by congruence.
  Qed.

  Lemma inverse_simulation {x y} : SSM.reachable M' x y -> reachable M x y.
  Proof using basic_M.
    elim.
    - move=> ? ? /inverse_simulation_step ?. by apply: rt_step.
    - move=> *. by apply: rt_refl.
    - move=> *. apply: rt_trans; by eassumption.
  Qed.

  Lemma confluent_M' : SSM.confluent M'.
  Proof using basic_M confluent_M.
    move=> ? ? ? /inverse_simulation /= H1 /inverse_simulation /= H2.
    have [? []] := confluent_M _ _ _ H1 H2.
    move=> /simulation /= ? /simulation /= ?.
    eexists. constructor; by eassumption.
  Qed.

  Lemma boundedness : (exists NM, bounded M NM) <-> (exists NM', SSM.bounded M' NM').
  Proof using basic_M.
    constructor.
    - move=> [NM bounded_M]. exists NM.
      move=> X. have [L [HL ?]] := bounded_M X.
      exists L. constructor; last done.
      by move=> ? /inverse_simulation /= /HL ?.
    - move=> [NM' bounded_M']. exists NM'.
      move=> X. have [L [HL ?]] := bounded_M' X.
      exists L. constructor; last done.
      by move=> ? /simulation /= /HL ?.
  Qed.

End Reduction.
End Argument.

Require Import Undecidability.Synthetic.Definitions.

Local Definition SMNdl_to_cssm : { M : SMN | deterministic M /\ length_preserving M } -> SSM.cssm.
Proof.
  move=> [M [/deterministic_confluent H1M H2M]].
  exists (Argument.M' (sval (construct_basic_SMN M H1M H2M))).
  apply: Argument.confluent_M'.
  - exact (fst (snd (svalP (construct_basic_SMN M H1M H2M)))).
  - exact (fst ((svalP (construct_basic_SMN M H1M H2M)))).
Defined.

Theorem reduction : SMNdl_UB ⪯ SSM.CSSM_UB.
Proof.
  exists SMNdl_to_cssm. move=> [M [H1M H2M]]. constructor.
  - move=> [nMN] /=.
    set M1 := (construct_basic_SMN M (deterministic_confluent H1M) H2M).
    move=> HM. have [? [?]] := svalP M1.
    move /iffLR => /(_ ltac:(by eexists)) => /Argument.boundedness. by apply.
  - move /Argument.boundedness. set M1 := (construct_basic_SMN M (deterministic_confluent H1M) H2M).
    have [? [? <-]] := svalP M1. by apply.
Qed.