Require Import List Arith Lia.

From Undecidability.Shared.Libs.DLW
  Require Import utils pos vec subcode sss.

From Undecidability.MinskyMachines
  Require Export MM.

Set Implicit Arguments.

Set Default Proof Using "Type".

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).

Section Minsky_Machine.

  Variable (n : ).

  Notation "i // s -1> t" := (@mm_sss n i s t).
  Notation "P // s -[ k ] t" := (sss_steps (@mm_sss n) P k s t).
  Notation "P // s -+> t" := (sss_progress (@mm_sss n) P s t).
  Notation "P // s > t" := (sss_compute (@mm_sss n) P s t).

  Fact mm_sss_fun i s t1 t2 : i // s -1> i // s -1> = .
  Proof.
    intros []; subst.
    inversion 1; subst; auto.
    inversion 1; subst; auto.
    rewrite H in ; discriminate.
    inversion 1; subst; auto.
    rewrite H in ; discriminate.
    rewrite H in ; inversion ; subst; auto.
  Qed.


  Fact mm_sss_total ii s : { t | ii // s -1> t }.
  Proof.
    destruct s as (i,v).
    destruct ii as [ x | x j ]; [ | case_eq (v#>x); [ | intros k ]; intros E ].
    * exists (1+i,v[(S (v#>x))/x]); constructor.
    * exists (j,v); constructor; auto.
    * exists (1+i,v[k/x]); constructor; auto.
  Qed.


  Fact mm_sss_INC_inv x i v j w : INC x // (i,v) -1> (j,w) j=1+i w = v[(S (v#>x))/x].
  Proof. inversion 1; subst; auto. Qed.

  Fact mm_sss_DEC0_inv x k i v j w : v#>x = O DEC x k // (i,v) -1> (j,w) j = k w = v.
  Proof.
    intros H; inversion 1; subst; auto; rewrite H in ; try discriminate.
  Qed.


  Fact mm_sss_DEC1_inv x k u i v j w : v#>x = S u DEC x k // (i,v) -1> (j,w) j=1+i w = v[u/x].
  Proof.
    intros H; inversion 1; subst; auto; rewrite H in ; try discriminate.
    inversion ; subst; auto.
  Qed.


  Fact mm_progress_INC P i x v st :
         (i,INC x::nil) <sc P
       P // (1+i,v[(S (v#>x))/x]) ->> st
       P // (i,v) -+> st.
  Proof.
    intros .
    apply sss_progress_compute_trans with (2 := ).
    apply subcode_sss_progress with (1 := ).
    exists 1; split; auto; apply sss_steps_1.
    apply in_sss_step with (l := nil).
    simpl; .
    constructor; auto.
  Qed.


  Corollary mm_compute_INC P i x v st : (i,INC x::nil) <sc P P // (1+i,v[(S (v#>x))/x]) ->> st P // (i,v) ->> st.
  Proof. intros; apply sss_progress_compute; eapply mm_progress_INC; eauto. Qed.

  Fact mm_progress_DEC_0 P i x k v st :
         (i,DEC x k::nil) <sc P
       v#>x = O
       P // (k,v) ->> st
       P // (i,v) -+> st.
  Proof.
    intros .
    apply sss_progress_compute_trans with (2 := ).
    apply subcode_sss_progress with (1 := ).
    exists 1; split; auto; apply sss_steps_1.
    apply in_sss_step with (l := nil).
    simpl; .
    constructor; auto.
  Qed.


  Corollary mm_compute_DEC_0 P i x k v st : (i,DEC x k::nil) <sc P v#>x = O P // (k,v) ->> st P // (i,v) ->> st.
  Proof. intros; apply sss_progress_compute; eapply mm_progress_DEC_0; eauto. Qed.

  Fact mm_progress_DEC_S P i x k v u st :
         (i,DEC x k::nil) <sc P
       v#>x = S u
       P // (1+i,v[u/x]) ->> st
       P // (i,v) -+> st.
  Proof.
    intros .
    apply sss_progress_compute_trans with (2 := ).
    apply subcode_sss_progress with (1 := ).
    exists 1; split; auto; apply sss_steps_1.
    apply in_sss_step with (l := nil).
    simpl; .
    constructor; auto.
  Qed.


  Corollary mm_compute_DEC_S P i x k v u st : (i,DEC x k::nil) <sc P v#>x = S u P // (1+i,v[u/x]) ->> st P // (i,v) ->> st.
  Proof. intros; apply sss_progress_compute; eapply mm_progress_DEC_S; eauto. Qed.

  Fact mm_steps_INC_inv k P i x v st :
         (i,INC x::nil) <sc P
       k 0
       P // (i,v) -[k]-> st
       k', k' < k P // (1+i,v[(S (v#>x))/x]) -[k']-> st.
  Proof.
    intros .
    apply sss_steps_inv in .
    destruct as [ (? & ?) | (k' & & ? & & ) ]; subst; auto.
    destruct ; auto.
    apply sss_step_subcode_inv with (1 := ) in .
    exists k'; split.
    .
    inversion ; subst; auto.
  Qed.


  Fact mm_steps_DEC_0_inv k P i x p v st :
         (i,DEC x p::nil) <sc P
       k 0
       v#>x = 0
       P // (i,v) -[k]-> st
       k', k' < k P // (p,v) -[k']-> st.
  Proof.
    intros .
    apply sss_steps_inv in .
    destruct as [ (? & ?) | (k' & & ? & & ) ]; subst; auto.
    destruct ; auto.
    apply sss_step_subcode_inv with (1 := ) in .
    exists k'; split.
    .
    inversion ; subst; auto.
    rewrite in ; discriminate.
  Qed.


  Fact mm_steps_DEC_1_inv k P i x p v u st :
         (i,DEC x p::nil) <sc P
       k 0
       v#>x = S u
       P // (i,v) -[k]-> st
       k', k' < k P // (1+i,v[u/x]) -[k']-> st.
  Proof.
    intros .
    apply sss_steps_inv in .
    destruct as [ (? & ?) | (k' & & ? & & ) ]; subst; auto.
    destruct ; auto.
    apply sss_step_subcode_inv with (1 := ) in .
    exists k'; split.
    .
    inversion ; subst; auto; rewrite in .
    discriminate.
    inversion ; subst; auto.
  Qed.


End Minsky_Machine.

Local Notation "i // s -1> t" := (@mm_sss _ i s t).
Local Notation "P // s -[ k ] t" := (sss_steps (@mm_sss _) P k s t).
Local Notation "P // s -+> t" := (sss_progress (@mm_sss _) P s t).
Local Notation "P // s > t" := (sss_compute (@mm_sss _) P s t).
Local Notation "P // s ~~> t" := (sss_output (@mm_sss _) P s t).

Tactic Notation "mm" "sss" "INC" "with" uconstr(a) :=
  match goal with
    | |- _ // _ -+> _ apply mm_progress_INC with (x := a)
    | |- _ // _ ->> _ apply mm_compute_INC with (x := a)
  end; auto.

Tactic Notation "mm" "sss" "DEC" "0" "with" uconstr(a) uconstr(b) :=
  match goal with
    | |- _ // _ -+> _ apply mm_progress_DEC_0 with (x := a) (k := b)
    | |- _ // _ ->> _ apply mm_compute_DEC_0 with (x := a) (k := b)
  end; auto.

Tactic Notation "mm" "sss" "DEC" "S" "with" uconstr(a) uconstr(b) uconstr(c) :=
  match goal with
    | |- _ // _ -+> _ apply mm_progress_DEC_S with (x := a) (k := b) (u := c)
    | |- _ // _ ->> _ apply mm_compute_DEC_S with (x := a) (k := b) (u := c)
  end; auto.

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

Section mm_special_ind.

  Variables (n : ) (P : *list (mm_instr (pos n))) (se : * vec n)
            (Q : * vec n Prop).

  Hypothesis ( : Q se)
             ( : i ρ v j w, (i,ρ::nil) <sc P
                                      ρ // (i,v) -1> (j,w)
                                      P // (j,w) ->> se
                                      Q (j,w)
                                      Q (i,v)).

  Theorem mm_special_ind s : P // s ->> se Q s.
  Proof using .
    intros (q & ); revert s .
    induction q as [ | q IHq ]; intros s Hs.
    + apply sss_steps_0_inv in Hs; subst; apply .
    + apply sss_steps_S_inv' in Hs.
      destruct Hs as ((j,w) & (j' & l & ρ & r & u & & & ) & ); subst s P.
      apply with (i := j'+length l) (2 := ); auto.
      exists q; auto.
  Qed.


End mm_special_ind.

Section mm_term_ind.

  Variables (n : ) (P : *list (mm_instr (pos n))) (se : * vec n)
            (Q : * vec n Prop).

  Hypothesis ( : out_code (fst se) P Q se)
             ( : i ρ v j w, (i,ρ::nil) <sc P
                                      ρ // (i,v) -1> (j,w)
                                      P // (j,w) ~~> se
                                      Q (j,w)
                                      Q (i,v)).

  Theorem mm_term_ind s : P // s ~~> se Q s.
  Proof using .
    intros ( & ).
    revert s ; apply mm_special_ind; auto.
    intros i v j w' .
    apply with (1 := ); auto.
    split; auto.
  Qed.


End mm_term_ind.