Require Import List Arith Omega Bool.

From Undecidability.Shared.Libs.DLW Require Import Utils.utils Vec.pos Vec.vec.
From Undecidability.ILL.Code Require Import subcode sss.
From Undecidability.ILL.Bsm Require Import list_bool.

Set Implicit Arguments.

Tactic Notation "rew" "length" := autorewrite with length_db.

Local Notation "e #> x" := (vec_pos e x).
Local Notation "e [ v / x ]" := (vec_change e x v).

Inductive bsm_instr n : Set :=
  | bsm_pop : pos n -> nat -> nat -> bsm_instr n
  | bsm_push : pos n -> bool -> bsm_instr n
  .

Notation POP := bsm_pop.
Notation PUSH := bsm_push.

Section Binary_Stack_Machine.

  Variable (n : nat).

  Definition bsm_state := (nat*vec (list bool) n)%type.

  Inductive bsm_sss : bsm_instr n -> bsm_state -> bsm_state -> Prop :=
    | in_bsm_sss_pop_E : forall i x p q v, v#>x = nil -> POP x p q // (i,v) -1> ( q,v)
    | in_bsm_sss_pop_0 : forall i x p q v ll, v#>x = Zero::ll -> POP x p q // (i,v) -1> ( p,v[ll/x])
    | in_bsm_sss_pop_1 : forall i x p q v ll, v#>x = One ::ll -> POP x p q // (i,v) -1> (1+i,v[ll/x])
    | in_bsm_sss_push : forall i x b v, PUSH x b // (i,v) -1> (1+i,v[(b::v#>x)/x])
  where "i // s -1> t" := (bsm_sss i s t).

  Ltac mydiscr :=
      match goal with H: ?x = _, G : ?x = _ |- _ => rewrite H in G; discriminate end.

  Ltac myinj :=
      match goal with H: ?x = _, G : ?x = _ |- _ => rewrite H in G; inversion G; subst; auto end.


  Fact bsm_sss_fun i s t1 t2 : i // s -1> t1 -> i // s -1> t2 -> t1 = t2.
  Proof. intros []; subst; inversion 1; subst; auto; try mydiscr; myinj. Qed.


  Fact bsm_sss_total ii s : { t | ii // s -1> t }.
  Proof.
    destruct s as (i,v).
    destruct ii as [ x p q | x b ].
    + case_eq (v#>x); [ intros Hx | intros [] l Hx ].
      * exists (q,v); constructor; trivial.
      * exists (1+i,v[l/x]); constructor; trivial.
      * exists (p,v[l/x]); constructor; trivial.
    + exists (1+i,v[(b::v#>x)/x]); constructor.
  Qed.

  Fact bsm_sss_total' ii s : exists t, ii // s -1> t.
  Proof.
    destruct (bsm_sss_total ii s); firstorder.
  Qed.


  Fact bsm_sss_stall : forall P s, sss_step_stall bsm_sss P s -> out_code (fst s) P.
  Proof.
    intros (i,P) (q,v) H; unfold fst.
    red in H.
    destruct (in_out_code_dec q (i,P)) as [ H1 | ]; auto; exfalso.
    apply in_code_subcode in H1.
    destruct H1 as (ii & l & r & H1 & H2).
    simpl in H1.
    destruct (bsm_sss_total ii (q,v)) as (t & Ht).
    apply (H t); subst; apply in_sss_step; auto.
  Qed.

  Notation "P // s -[ k ]-> t" := (sss_steps bsm_sss P k s t).
  Notation "P // s ->> t" := (sss_compute bsm_sss P s t).

  Fact bsm_compute_POP_E P i x p q v st :
         (i,POP x p q::nil) <sc P
      -> v#>x = nil
      -> P // (q,v) ->> st
      -> P // (i,v) ->> st.
  Proof.
    intros H1 H2.
    apply subcode_sss_compute_trans with (1 := H1).
    exists 1; apply sss_steps_1.
    apply in_sss_step with (l := nil).
    simpl; omega.
    constructor; auto.
  Qed.

  Fact bsm_compute_POP_0 P i x p q ll v st :
         (i,POP x p q::nil) <sc P
      -> v#>x = Zero::ll
      -> P // (p,v[ll/x]) ->> st
      -> P // (i,v) ->> st.
  Proof.
    intros H1 H2.
    apply subcode_sss_compute_trans with (1 := H1).
    exists 1; apply sss_steps_1.
    apply in_sss_step with (l := nil).
    simpl; omega.
    constructor; auto.
  Qed.

  Fact bsm_compute_POP_1 P i x p q ll v st :
         (i,POP x p q::nil) <sc P
      -> v#>x = One::ll
      -> P // (1+i,v[ll/x]) ->> st
      -> P // (i,v) ->> st.
  Proof.
    intros H1 H2.
    apply subcode_sss_compute_trans with (1 := H1).
    exists 1; apply sss_steps_1.
    apply in_sss_step with (l := nil).
    simpl; omega.
    constructor; auto.
  Qed.

  Fact bsm_compute_POP_any P i x p q b ll v st :
         (i,POP x p q::nil) <sc P
      -> v#>x = b::ll
      -> p = 1+i
      -> P // (1+i,v[ll/x]) ->> st
      -> P // (i,v) ->> st.
  Proof.
    destruct b; intros H1 H2 H3.
    apply bsm_compute_POP_1 with p q; auto.
    apply bsm_compute_POP_0 with q; subst; auto.
  Qed.

  Fact bsm_compute_PUSH P i x b v st :
         (i,PUSH x b::nil) <sc P
      -> P // (1+i,v[(b::v#>x)/x]) ->> st
      -> P // (i,v) ->> st.
  Proof.
    intros H1.
    apply subcode_sss_compute_trans with (1 := H1).
    exists 1; apply sss_steps_1.
    apply in_sss_step with (l := nil).
    simpl; omega.
    constructor; auto.
  Qed.

  Fact bsm_steps_POP_0_inv a P i x p q ll v st :
         (i,POP x p q::nil) <sc P
      -> v#>x = Zero::ll
      -> st <> (i,v)
      -> P // (i,v) -[a]-> st
      -> { b | b < a /\ P // (p,v[ll/x]) -[b]-> st }.
  Proof.
    intros H1 H2 H3 H4.
    apply sss_steps_inv in H4.
    destruct H4 as [ (_ & ?) | (b & H4) ]; subst.
    destruct H3; auto.
    exists b.
    destruct H4 as (st2 & ? & H4 & H5); subst.
    split.
    omega.
    apply sss_step_subcode_inv with (1 := H1) in H4.
    inversion H4; subst; try mydiscr; myinj.
  Qed.

  Fact bsm_steps_POP_1_inv a P i x p q ll v st :
         (i,POP x p q::nil) <sc P
      -> v#>x = One::ll
      -> st <> (i,v)
      -> P // (i,v) -[a]-> st
      -> { b | b < a /\ P // (1+i,v[ll/x]) -[b]-> st }.
  Proof.
    intros H1 H2 H3 H4.
    apply sss_steps_inv in H4.
    destruct H4 as [ (_ & ?) | (b & H4) ]; subst.
    destruct H3; auto.
    exists b.
    destruct H4 as (st2 & ? & H4 & H5); subst.
    split.
    omega.
    apply sss_step_subcode_inv with (1 := H1) in H4.
    inversion H4; subst; try mydiscr; myinj.
  Qed.

  Fact bsm_steps_POP_any_inv a P i x p q b ll v st :
         (i,POP x p q::nil) <sc P
      -> v#>x = b::ll
      -> p = 1+i
      -> st <> (i,v)
      -> P // (i,v) -[a]-> st
      -> { b | b < a /\ P // (1+i,v[ll/x]) -[b]-> st }.
  Proof.
    intros.
    destruct b.
    apply bsm_steps_POP_1_inv with p q; auto.
    apply bsm_steps_POP_0_inv with i q; subst; auto.
  Qed.

  Fact bsm_steps_POP_E_inv a P i x p q v st :
         (i,POP x p q::nil) <sc P
      -> v#>x = nil
      -> st <> (i,v)
      -> P // (i,v) -[a]-> st
      -> { b | b < a /\ P // (q,v) -[b]-> st }.
  Proof.
    intros H1 H2 H3 H4.
    apply sss_steps_inv in H4.
    destruct H4 as [ (? & ?) | (b & H4) ]; subst; auto.
    destruct H3; auto.
    exists b.
    destruct H4 as (st2 & ? & H4 & H5); subst.
    split.
    omega.
    apply sss_step_subcode_inv with (1 := H1) in H4.
    inversion H4; subst; try mydiscr; myinj.
  Qed.

  Fact bsm_steps_PUSH_inv k P i x b v st :
         (i,PUSH x b::nil) <sc P
      -> st <> (i,v)
      -> P // (i,v) -[k]-> st
      -> { a | a < k /\ P // (1+i,v[(b::v#>x)/x]) -[a]-> st }.
  Proof.
    intros H1 H2 H4.
    apply sss_steps_inv in H4.
    destruct H4 as [ (? & ?) | (a & H4) ]; subst; auto.
    destruct H2; auto.
    exists a.
    destruct H4 as (st2 & ? & H4 & H5); subst.
    split.
    omega.
    apply sss_step_subcode_inv with (1 := H1) in H4.
    inversion H4; subst; auto.
  Qed.

End Binary_Stack_Machine.

Tactic Notation "bsm" "sss" "POP" "empty" "with" uconstr(a) constr(b) constr(c) :=
     apply bsm_compute_POP_E with (x := a) (p := b) (q := c); auto.

Tactic Notation "bsm" "sss" "POP" "0" "with" uconstr(a) constr(b) constr(c) uconstr(d) :=
     apply bsm_compute_POP_0 with (x := a) (p := b) (q := c) (ll := d); auto.

Tactic Notation "bsm" "sss" "POP" "1" "with" uconstr(a) constr(b) constr(c) uconstr(d) :=
     apply bsm_compute_POP_1 with (x := a) (p := b) (q := c) (ll := d); auto.

Tactic Notation "bsm" "sss" "POP" "any" "with" uconstr(a) constr(c) constr(d) constr(e) constr(f) :=
     apply bsm_compute_POP_any with (x := a) (p := c) (q := d) (b := e) (ll := f); auto.

Tactic Notation "bsm" "sss" "PUSH" "with" uconstr(a) constr(q) :=
     apply bsm_compute_PUSH with (x := a) (b := q); auto.

Tactic Notation "bsm" "sss" "stop" := exists 0; apply sss_steps_0; auto.

Tactic Notation "bsm" "inv" "POP" "empty" "with" hyp(H) constr(a) constr(b) constr(c) constr(d) :=
     apply bsm_steps_POP_E_inv with (x := a) (p := b) (q := c) (ll := d) in H; auto.

Tactic Notation "bsm" "inv" "POP" "0" "with" hyp(H) constr(a) constr(b) constr(c) constr(d) :=
     apply bsm_steps_POP_0_inv with (x := a) (p := b) (q := c) (ll := d) in H; auto.

Tactic Notation "bsm" "inv" "POP" "1" "with" hyp(H) constr(a) constr(b) constr(c) constr(d) :=
     apply bsm_steps_POP_1_inv with (x := a) (p := b) (q := c) (ll := d) in H; auto.

Tactic Notation "bsm" "inv" "POP" "any" "with" hyp(H) constr(a) constr(c) constr(d) constr(e) constr(f) :=
     apply bsm_steps_POP_any_inv with (x := a) (p := c) (q := d) (b := e) (ll := f) in H; auto.

Tactic Notation "bsm" "inv" "PUSH" "with" hyp(H) constr(a) constr(c) :=
     apply bsm_steps_PUSH_inv with (x := a) (b := c) in H; auto.

Hint Immediate bsm_sss_fun.


Definition BSM_PROBLEM := { n : nat & { i : nat & { P : list (bsm_instr n) & vec (list bool) n } } }.

Local Notation "P // s ↓" := (sss_terminates (@bsm_sss _) P s).

Definition BSM_HALTING (P : BSM_PROBLEM) :=
  match P with existT _ n (existT _ i (existT _ P v)) => (i,P) // (i,v) ↓ end.