(**************************************************************)
(*   Copyright Dominique Larchey-Wendling [*]                 *)
(*                                                            *)
(*                             [*] Affiliation LORIA -- CNRS  *)
(**************************************************************)
(*      This file is distributed under the terms of the       *)
(*         CeCILL v2 FREE SOFTWARE LICENSE AGREEMENT          *)
(**************************************************************)

Require Import List Arith Omega.

Require Import utils pos vec. 
Require Import subcode sss.

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

(** * Minsky Machines

    A Minsky machine has n registers and there are just two instructions
 
    1/ INC x   : increment register x by 1
    2/ DEC x k : decrement register x by 1 if x > 0
                 or jump to k if x = 0

  *)

Inductive mm_instr n : Set :=
  | mm_inc : pos n -> mm_instr n
  | mm_dec : pos n -> nat -> mm_instr n
  .

Notation INC := mm_inc.
Notation DEC := mm_dec.

(** ** Semantics for MM *)

Section Minsky_Machine.

  Variable (n : nat).

  Definition mm_state := (nat*vec nat n)%type.

  (* Minsky machine small step semantics *)

  Inductive mm_sss : mm_instr n -> mm_state -> mm_state -> Prop :=
    | in_mm_sss_inc   : forall i x v,                   INC x   // (i,v) -1> (1+i,v[(S (v#>x))/x])
    | in_mm_sss_dec_0 : forall i x k v,   v#>x = O   -> DEC x k // (i,v) -1> (k,v)
    | in_mm_sss_dec_1 : forall i x k v u, v#>x = S u -> DEC x k // (i,v) -1> (1+i,v[u/x])
  where "i // s -1> t" := (mm_sss i s t).

  Fact mm_sss_fun i s t1 t2 : i // s -1> t1 -> i // s -1> t2 -> t1 = t2.
  Proof.
(* Goal: forall (_ : mm_sss i s t1) (_ : mm_sss i s t2), @eq mm_state t1 t2 *)
    intros []; subst.
(* Goal: forall _ : mm_sss (@mm_inc n x) (@pair nat (vec nat n) i v) (@pair nat (vec nat n) j w), and (@eq nat j (Init.Nat.add (S O) i)) (@eq (vec nat n) w (@vec_change nat n v x (S (@vec_pos nat n v x)))) *)
    inversion 1; subst; auto.
(* Goal: forall _ : mm_sss (@mm_inc n x) (@pair nat (vec nat n) i v) (@pair nat (vec nat n) j w), and (@eq nat j (Init.Nat.add (S O) i)) (@eq (vec nat n) w (@vec_change nat n v x (S (@vec_pos nat n v x)))) *)
    inversion 1; subst; auto.
(* Goal: @eq mm_state (@pair nat (vec nat n) (Init.Nat.add (S O) i0) (@vec_change nat n v x u)) (@pair nat (vec nat n) k v) *)
(* Goal: @eq mm_state (@pair nat (vec nat n) (Init.Nat.add (S O) i0) (@vec_change nat n v x u)) (@pair nat (vec nat n) (Init.Nat.add (S O) i0) (@vec_change nat n v x u0)) *)
    rewrite H in H6; discriminate.
(* Goal: forall _ : mm_sss (@mm_inc n x) (@pair nat (vec nat n) i v) (@pair nat (vec nat n) j w), and (@eq nat j (Init.Nat.add (S O) i)) (@eq (vec nat n) w (@vec_change nat n v x (S (@vec_pos nat n v x)))) *)
    inversion 1; subst; auto.
(* Goal: @eq mm_state (@pair nat (vec nat n) (Init.Nat.add (S O) i0) (@vec_change nat n v x u)) (@pair nat (vec nat n) k v) *)
(* Goal: @eq mm_state (@pair nat (vec nat n) (Init.Nat.add (S O) i0) (@vec_change nat n v x u)) (@pair nat (vec nat n) (Init.Nat.add (S O) i0) (@vec_change nat n v x u0)) *)
    rewrite H in H6; discriminate.
(* Goal: @eq mm_state (@pair nat (vec nat n) (Init.Nat.add (S O) i0) (@vec_change nat n v x u)) (@pair nat (vec nat n) (Init.Nat.add (S O) i0) (@vec_change nat n v x u0)) *)
    rewrite H in H6; inversion H6; subst; auto.
  Qed.
  
  Fact mm_sss_total ii s : { t | ii // s -1> t }.
  Proof.
(* Goal: @sig mm_state (fun t : mm_state => mm_sss ii s t) *)
    destruct s as (i,v).
(* Goal: @sig mm_state (fun t : mm_state => mm_sss ii (@pair nat (vec nat n) i v) t) *)
    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].
(* Goal: forall _ : mm_sss (@mm_inc n x) (@pair nat (vec nat n) i v) (@pair nat (vec nat n) j w), and (@eq nat j (Init.Nat.add (S O) i)) (@eq (vec nat n) w (@vec_change nat n v x (S (@vec_pos nat n v 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. 
(* Goal: forall (_ : @eq nat (@vec_pos nat n v x) (S u)) (_ : mm_sss (@mm_dec n x k) (@pair nat (vec nat n) i v) (@pair nat (vec nat n) j w)), and (@eq nat j (Init.Nat.add (S O) i)) (@eq (vec nat n) w (@vec_change nat n v x u)) *)
    intros H; inversion 1; subst; auto; rewrite H in H2; 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. 
(* Goal: forall (_ : @eq nat (@vec_pos nat n v x) (S u)) (_ : mm_sss (@mm_dec n x k) (@pair nat (vec nat n) i v) (@pair nat (vec nat n) j w)), and (@eq nat j (Init.Nat.add (S O) i)) (@eq (vec nat n) w (@vec_change nat n v x u)) *)
    intros H; inversion 1; subst; auto; rewrite H in H2; try discriminate.
(* Goal: and (@eq nat (S i) (Init.Nat.add (S O) i)) (@eq (vec nat n) (@vec_change nat n v x u0) (@vec_change nat n v x u)) *)
    inversion H2; subst; auto.
  Qed.

(*
  Definition mm_step_stall := sss_step_stall mm_sss.
  Definition mm_program := (nat*list (mm_instr n))%type.
  Definition mm_steps := sss_steps mm_sss.
  Definition mm_compute := sss_compute mm_sss.
*)

  Notation "P // s -[ k ]-> t" := (sss_steps mm_sss P k s t).
  Notation "P // s -+> t" := (sss_progress mm_sss P s t).
  Notation "P // s ->> t" := (sss_compute mm_sss P s t).
  
  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.
(* Goal: forall (_ : @subcode (mm_instr n) (@pair nat (list (mm_instr n)) i (@cons (mm_instr n) (@mm_inc n x) (@nil (mm_instr n)))) P) (_ : @sss_compute (mm_instr n) (vec nat n) mm_sss P (@pair nat (vec nat n) (Init.Nat.add (S O) i) (@vec_change nat n v x (S (@vec_pos nat n v x)))) st), @sss_progress (mm_instr n) (vec nat n) mm_sss P (@pair nat (vec nat n) i v) st *)
    intros H1 H2.
(* Goal: @sss_progress (mm_instr n) (vec nat n) mm_sss P (@pair nat (vec nat n) i v) st *)
    apply sss_progress_compute_trans with (2 := H2).
(* Goal: @sss_progress (mm_instr n) (vec nat n) mm_sss P (@pair nat (vec nat n) i v) (@pair nat (vec nat n) (Init.Nat.add (S O) i) (@vec_change nat n v x u)) *)
    apply subcode_sss_progress with (1 := H1).
(* Goal: @sss_progress (mm_instr n) (vec nat n) mm_sss (@pair nat (list (mm_instr n)) i (@cons (mm_instr n) (@mm_dec n x k) (@nil (mm_instr n)))) (@pair nat (vec nat n) i v) (@pair nat (vec nat n) (Init.Nat.add (S O) i) (@vec_change nat n v x u)) *)
    exists 1; split; auto; apply sss_steps_1.
(* Goal: @sss_step (mm_instr n) (vec nat n) mm_sss (@pair nat (list (mm_instr n)) i (@cons (mm_instr n) (@mm_dec n x k) (@nil (mm_instr n)))) (@pair nat (vec nat n) i v) (@pair nat (vec nat n) (Init.Nat.add (S O) i) (@vec_change nat n v x u)) *)
    apply in_sss_step with (l := nil).
(* Goal: @eq nat (@fst nat (vec nat n) (@pair nat (vec nat n) i v)) (Init.Nat.add i (@length (mm_instr n) (@nil (mm_instr n)))) *)
(* Goal: mm_sss (@mm_dec n x k) (@pair nat (vec nat n) i v) (@pair nat (vec nat n) (Init.Nat.add (S O) i) (@vec_change nat n v x u)) *)
    simpl; omega.
(* Goal: mm_sss (@mm_dec n x k) (@pair nat (vec nat n) i v) (@pair nat (vec nat n) (Init.Nat.add (S O) i) (@vec_change nat n v x u)) *)
    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.
(* Goal: forall (_ : @subcode (mm_instr n) (@pair nat (list (mm_instr n)) i (@cons (mm_instr n) (@mm_dec n x k) (@nil (mm_instr n)))) P) (_ : @eq nat (@vec_pos nat n v x) (S u)) (_ : @sss_compute (mm_instr n) (vec nat n) mm_sss P (@pair nat (vec nat n) (Init.Nat.add (S O) i) (@vec_change nat n v x u)) st), @sss_progress (mm_instr n) (vec nat n) mm_sss P (@pair nat (vec nat n) i v) st *)
    intros H1 H2 H3.
(* Goal: @sss_progress (mm_instr n) (vec nat n) mm_sss P (@pair nat (vec nat n) i v) st *)
    apply sss_progress_compute_trans with (2 := H3).
(* Goal: @sss_progress (mm_instr n) (vec nat n) mm_sss P (@pair nat (vec nat n) i v) (@pair nat (vec nat n) (Init.Nat.add (S O) i) (@vec_change nat n v x u)) *)
    apply subcode_sss_progress with (1 := H1).
(* Goal: @sss_progress (mm_instr n) (vec nat n) mm_sss (@pair nat (list (mm_instr n)) i (@cons (mm_instr n) (@mm_dec n x k) (@nil (mm_instr n)))) (@pair nat (vec nat n) i v) (@pair nat (vec nat n) (Init.Nat.add (S O) i) (@vec_change nat n v x u)) *)
    exists 1; split; auto; apply sss_steps_1.
(* Goal: @sss_step (mm_instr n) (vec nat n) mm_sss (@pair nat (list (mm_instr n)) i (@cons (mm_instr n) (@mm_dec n x k) (@nil (mm_instr n)))) (@pair nat (vec nat n) i v) (@pair nat (vec nat n) (Init.Nat.add (S O) i) (@vec_change nat n v x u)) *)
    apply in_sss_step with (l := nil).
(* Goal: @eq nat (@fst nat (vec nat n) (@pair nat (vec nat n) i v)) (Init.Nat.add i (@length (mm_instr n) (@nil (mm_instr n)))) *)
(* Goal: mm_sss (@mm_dec n x k) (@pair nat (vec nat n) i v) (@pair nat (vec nat n) (Init.Nat.add (S O) i) (@vec_change nat n v x u)) *)
    simpl; omega.
(* Goal: mm_sss (@mm_dec n x k) (@pair nat (vec nat n) i v) (@pair nat (vec nat n) (Init.Nat.add (S O) i) (@vec_change nat n v x u)) *)
    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.
(* Goal: forall (_ : @subcode (mm_instr n) (@pair nat (list (mm_instr n)) i (@cons (mm_instr n) (@mm_dec n x k) (@nil (mm_instr n)))) P) (_ : @eq nat (@vec_pos nat n v x) (S u)) (_ : @sss_compute (mm_instr n) (vec nat n) mm_sss P (@pair nat (vec nat n) (Init.Nat.add (S O) i) (@vec_change nat n v x u)) st), @sss_progress (mm_instr n) (vec nat n) mm_sss P (@pair nat (vec nat n) i v) st *)
    intros H1 H2 H3.
(* Goal: @sss_progress (mm_instr n) (vec nat n) mm_sss P (@pair nat (vec nat n) i v) st *)
    apply sss_progress_compute_trans with (2 := H3).
(* Goal: @sss_progress (mm_instr n) (vec nat n) mm_sss P (@pair nat (vec nat n) i v) (@pair nat (vec nat n) (Init.Nat.add (S O) i) (@vec_change nat n v x u)) *)
    apply subcode_sss_progress with (1 := H1).
(* Goal: @sss_progress (mm_instr n) (vec nat n) mm_sss (@pair nat (list (mm_instr n)) i (@cons (mm_instr n) (@mm_dec n x k) (@nil (mm_instr n)))) (@pair nat (vec nat n) i v) (@pair nat (vec nat n) (Init.Nat.add (S O) i) (@vec_change nat n v x u)) *)
    exists 1; split; auto; apply sss_steps_1.
(* Goal: @sss_step (mm_instr n) (vec nat n) mm_sss (@pair nat (list (mm_instr n)) i (@cons (mm_instr n) (@mm_dec n x k) (@nil (mm_instr n)))) (@pair nat (vec nat n) i v) (@pair nat (vec nat n) (Init.Nat.add (S O) i) (@vec_change nat n v x u)) *)
    apply in_sss_step with (l := nil).
(* Goal: @eq nat (@fst nat (vec nat n) (@pair nat (vec nat n) i v)) (Init.Nat.add i (@length (mm_instr n) (@nil (mm_instr n)))) *)
(* Goal: mm_sss (@mm_dec n x k) (@pair nat (vec nat n) i v) (@pair nat (vec nat n) (Init.Nat.add (S O) i) (@vec_change nat n v x u)) *)
    simpl; omega.
(* Goal: mm_sss (@mm_dec n x k) (@pair nat (vec nat n) i v) (@pair nat (vec nat n) (Init.Nat.add (S O) i) (@vec_change nat n v x u)) *)
    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
      -> exists k', k' < k /\ P // (1+i,v[(S (v#>x))/x]) -[k']-> st.
  Proof.
(* Goal: forall (_ : @subcode (mm_instr n) (@pair nat (list (mm_instr n)) i (@cons (mm_instr n) (@mm_inc n x) (@nil (mm_instr n)))) P) (_ : not (@eq nat k O)) (_ : @sss_steps (mm_instr n) (vec nat n) mm_sss P k (@pair nat (vec nat n) i v) st), @ex nat (fun k' : nat => and (lt k' k) (@sss_steps (mm_instr n) (vec nat n) mm_sss P k' (@pair nat (vec nat n) (Init.Nat.add (S O) i) (@vec_change nat n v x (S (@vec_pos nat n v x)))) st)) *)
    intros H1 H2 H4.
(* Goal: @ex nat (fun k' : nat => and (lt k' k) (@sss_steps (mm_instr n) (vec nat n) mm_sss P k' (@pair nat (vec nat n) (Init.Nat.add (S O) i) (@vec_change nat n v x u)) st)) *)
    apply sss_steps_inv in H4.
(* Goal: @ex nat (fun k' : nat => and (lt k' k) (@sss_steps (mm_instr n) (vec nat n) mm_sss P k' (@pair nat (vec nat n) (Init.Nat.add (S O) i) (@vec_change nat n v x u)) st)) *)
    destruct H4 as [ (? & ?) | (k' & st2 & ? & H4 & H5) ]; subst; auto.
(* Goal: @ex nat (fun k' : nat => and (lt k' O) (@sss_steps (mm_instr n) (vec nat n) mm_sss P k' (@pair nat (vec nat n) (Init.Nat.add (S O) i) (@vec_change nat n v x u)) (@pair nat (vec nat n) i v))) *)
(* Goal: @ex nat (fun k'0 : nat => and (lt k'0 (S k')) (@sss_steps (mm_instr n) (vec nat n) mm_sss P k'0 (@pair nat (vec nat n) (Init.Nat.add (S O) i) (@vec_change nat n v x u)) st)) *)
    destruct H2; auto.
(* Goal: @ex nat (fun k'0 : nat => and (lt k'0 (S k')) (@sss_steps (mm_instr n) (vec nat n) mm_sss P k'0 (@pair nat (vec nat n) (Init.Nat.add (S O) i) (@vec_change nat n v x u)) st)) *)
    apply sss_step_subcode_inv with (1 := H1) in H4.
(* Goal: @ex nat (fun k'0 : nat => and (lt k'0 (S k')) (@sss_steps (mm_instr n) (vec nat n) mm_sss P k'0 (@pair nat (vec nat n) (Init.Nat.add (S O) i) (@vec_change nat n v x u)) st)) *)
    exists k'; split.
(* Goal: lt k' (S k') *)
(* Goal: @sss_steps (mm_instr n) (vec nat n) mm_sss P k' (@pair nat (vec nat n) (Init.Nat.add (S O) i) (@vec_change nat n v x u)) st *)
    omega.
(* Goal: @sss_steps (mm_instr n) (vec nat n) mm_sss P k' (@pair nat (vec nat n) p v) st *)
    inversion H4; 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
      -> exists k', k' < k /\ P // (p,v) -[k']-> st.
  Proof.
(* Goal: forall (_ : @subcode (mm_instr n) (@pair nat (list (mm_instr n)) i (@cons (mm_instr n) (@mm_dec n x p) (@nil (mm_instr n)))) P) (_ : not (@eq nat k O)) (_ : @eq nat (@vec_pos nat n v x) (S u)) (_ : @sss_steps (mm_instr n) (vec nat n) mm_sss P k (@pair nat (vec nat n) i v) st), @ex nat (fun k' : nat => and (lt k' k) (@sss_steps (mm_instr n) (vec nat n) mm_sss P k' (@pair nat (vec nat n) (Init.Nat.add (S O) i) (@vec_change nat n v x u)) st)) *)
    intros H1 H2 H3 H4.
(* Goal: @ex nat (fun k' : nat => and (lt k' k) (@sss_steps (mm_instr n) (vec nat n) mm_sss P k' (@pair nat (vec nat n) (Init.Nat.add (S O) i) (@vec_change nat n v x u)) st)) *)
    apply sss_steps_inv in H4.
(* Goal: @ex nat (fun k' : nat => and (lt k' k) (@sss_steps (mm_instr n) (vec nat n) mm_sss P k' (@pair nat (vec nat n) (Init.Nat.add (S O) i) (@vec_change nat n v x u)) st)) *)
    destruct H4 as [ (? & ?) | (k' & st2 & ? & H4 & H5) ]; subst; auto.
(* Goal: @ex nat (fun k' : nat => and (lt k' O) (@sss_steps (mm_instr n) (vec nat n) mm_sss P k' (@pair nat (vec nat n) (Init.Nat.add (S O) i) (@vec_change nat n v x u)) (@pair nat (vec nat n) i v))) *)
(* Goal: @ex nat (fun k'0 : nat => and (lt k'0 (S k')) (@sss_steps (mm_instr n) (vec nat n) mm_sss P k'0 (@pair nat (vec nat n) (Init.Nat.add (S O) i) (@vec_change nat n v x u)) st)) *)
    destruct H2; auto.
(* Goal: @ex nat (fun k'0 : nat => and (lt k'0 (S k')) (@sss_steps (mm_instr n) (vec nat n) mm_sss P k'0 (@pair nat (vec nat n) (Init.Nat.add (S O) i) (@vec_change nat n v x u)) st)) *)
    apply sss_step_subcode_inv with (1 := H1) in H4.
(* Goal: @ex nat (fun k'0 : nat => and (lt k'0 (S k')) (@sss_steps (mm_instr n) (vec nat n) mm_sss P k'0 (@pair nat (vec nat n) (Init.Nat.add (S O) i) (@vec_change nat n v x u)) st)) *)
    exists k'; split.
(* Goal: lt k' (S k') *)
(* Goal: @sss_steps (mm_instr n) (vec nat n) mm_sss P k' (@pair nat (vec nat n) (Init.Nat.add (S O) i) (@vec_change nat n v x u)) st *)
    omega.
(* Goal: @sss_steps (mm_instr n) (vec nat n) mm_sss P k' (@pair nat (vec nat n) p v) st *)
    inversion H4; subst; auto.
(* Goal: @sss_steps (mm_instr n) (vec nat n) mm_sss P k' (@pair nat (vec nat n) p v) st *)
    rewrite H3 in H9; 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
      -> exists k', k' < k /\ P // (1+i,v[u/x]) -[k']-> st.
  Proof.
(* Goal: forall (_ : @subcode (mm_instr n) (@pair nat (list (mm_instr n)) i (@cons (mm_instr n) (@mm_dec n x p) (@nil (mm_instr n)))) P) (_ : not (@eq nat k O)) (_ : @eq nat (@vec_pos nat n v x) (S u)) (_ : @sss_steps (mm_instr n) (vec nat n) mm_sss P k (@pair nat (vec nat n) i v) st), @ex nat (fun k' : nat => and (lt k' k) (@sss_steps (mm_instr n) (vec nat n) mm_sss P k' (@pair nat (vec nat n) (Init.Nat.add (S O) i) (@vec_change nat n v x u)) st)) *)
    intros H1 H2 H3 H4.
(* Goal: @ex nat (fun k' : nat => and (lt k' k) (@sss_steps (mm_instr n) (vec nat n) mm_sss P k' (@pair nat (vec nat n) (Init.Nat.add (S O) i) (@vec_change nat n v x u)) st)) *)
    apply sss_steps_inv in H4.
(* Goal: @ex nat (fun k' : nat => and (lt k' k) (@sss_steps (mm_instr n) (vec nat n) mm_sss P k' (@pair nat (vec nat n) (Init.Nat.add (S O) i) (@vec_change nat n v x u)) st)) *)
    destruct H4 as [ (? & ?) | (k' & st2 & ? & H4 & H5) ]; subst; auto.
(* Goal: @ex nat (fun k' : nat => and (lt k' O) (@sss_steps (mm_instr n) (vec nat n) mm_sss P k' (@pair nat (vec nat n) (Init.Nat.add (S O) i) (@vec_change nat n v x u)) (@pair nat (vec nat n) i v))) *)
(* Goal: @ex nat (fun k'0 : nat => and (lt k'0 (S k')) (@sss_steps (mm_instr n) (vec nat n) mm_sss P k'0 (@pair nat (vec nat n) (Init.Nat.add (S O) i) (@vec_change nat n v x u)) st)) *)
    destruct H2; auto.
(* Goal: @ex nat (fun k'0 : nat => and (lt k'0 (S k')) (@sss_steps (mm_instr n) (vec nat n) mm_sss P k'0 (@pair nat (vec nat n) (Init.Nat.add (S O) i) (@vec_change nat n v x u)) st)) *)
    apply sss_step_subcode_inv with (1 := H1) in H4.
(* Goal: @ex nat (fun k'0 : nat => and (lt k'0 (S k')) (@sss_steps (mm_instr n) (vec nat n) mm_sss P k'0 (@pair nat (vec nat n) (Init.Nat.add (S O) i) (@vec_change nat n v x u)) st)) *)
    exists k'; split.
(* Goal: lt k' (S k') *)
(* Goal: @sss_steps (mm_instr n) (vec nat n) mm_sss P k' (@pair nat (vec nat n) (Init.Nat.add (S O) i) (@vec_change nat n v x u)) st *)
    omega.
(* Goal: @sss_steps (mm_instr n) (vec nat n) mm_sss P k' (@pair nat (vec nat n) (Init.Nat.add (S O) i) (@vec_change nat n v x u)) st *)
    inversion H4; subst; auto; rewrite H3 in H9.
(* Goal: @sss_steps (mm_instr n) (vec nat n) mm_sss P k' (@pair nat (vec nat n) (Init.Nat.add (S O) i) (@vec_change nat n v x u)) st *)
(* Goal: @sss_steps (mm_instr n) (vec nat n) mm_sss P k' (@pair nat (vec nat n) (Init.Nat.add (S O) i) (@vec_change nat n v x u)) st *)
    discriminate.
(* Goal: @sss_steps (mm_instr n) (vec nat n) mm_sss P k' (@pair nat (vec nat n) (Init.Nat.add (S O) i) (@vec_change nat n v x u)) st *)
    inversion H9; subst; auto.
  Qed.
  
End Minsky_Machine.

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

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.

(* The Halting problem for MM, for linear logic encoding, we restrict
   to a very specific halting problem. Starting from (1,v), does the
   MM halt at state (0,vec_zero) *)

Definition MM_PROBLEM := { n : nat & { P : list (mm_instr n) & vec nat n } }.

Local Notation "i // s -1> t" := (@mm_sss _ i s t).
Local Notation "P // s ~~> t" := (sss_output (@mm_sss _) P s t).
Local Notation "P // s ↓" := (sss_terminates (@mm_sss _) P s). 

Definition MM_HALTS_ON_ZERO (P : MM_PROBLEM) := 
  match P with existT _ n (existT _ P v) => (1,P) // (1,v) ~~> (0,vec_zero) end.

Definition MM_HALTING (P : MM_PROBLEM) :=
  match P with existT _ n (existT _ P v) => (1, P) // (1, v) ↓ end.

Section mm_special_ind.

  Variables (n : nat) (P : nat*list (mm_instr n)) (se : nat * vec nat n)
            (Q : nat * vec nat n -> Prop).

  Hypothesis (HQ0 : Q se)
             (HQ1 : forall 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.
(* Goal: forall _ : @sss_compute (mm_instr n) (vec nat n) (@mm_sss n) P s se, Q s *)
    intros (q & H1); revert s H1.
(* Goal: forall (s : prod nat (vec nat n)) (_ : @sss_steps (mm_instr n) (vec nat n) (@mm_sss n) P q s se), Q s *)
    induction q as [ | q IHq ]; intros s Hs.
    + apply sss_steps_0_inv in Hs; subst; apply HQ0.
    + apply sss_steps_S_inv' in Hs.
(* Goal: Q s *)
      destruct Hs as ((j,w) & (j' & l & ρ & r & u & G1 & G2 & G3) & Hs2); subst s P.
      apply HQ1 with (i := j'+length l) (2 := G3); auto.
(* Goal: @sss_compute (mm_instr n) (vec nat n) (@mm_sss n) (@pair nat (list (mm_instr n)) j' (@app (mm_instr n) l (@cons (mm_instr n) ρ r))) (@pair nat (vec nat n) j w) se *)
      exists q; auto.
  Qed.

End mm_special_ind.

Section mm_term_ind.

  Variables (n : nat) (P : nat*list (mm_instr n)) (se : nat * vec nat n)
            (Q : nat * vec nat n -> Prop).

  Hypothesis (HQ0 : out_code (fst se) P -> Q se)
             (HQ1 : forall 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.
(* Goal: forall _ : @sss_output (mm_instr n) (vec nat n) (@mm_sss n) P s se, Q s *)
    intros (H1 & H2).
(* Goal: Q s *)
    revert s H1; apply mm_special_ind; auto.
(* Goal: forall (i : nat) (ρ : mm_instr n) (v : vec nat n) (j : nat) (w : vec nat n) (_ : @subcode (mm_instr n) (@pair nat (list (mm_instr n)) i (@cons (mm_instr n) ρ (@nil (mm_instr n)))) P) (_ : @mm_sss n ρ (@pair nat (vec nat n) i v) (@pair nat (vec nat n) j w)) (_ : @sss_compute (mm_instr n) (vec nat n) (@mm_sss n) P (@pair nat (vec nat n) j w) se) (_ : Q (@pair nat (vec nat n) j w)), Q (@pair nat (vec nat n) i v) *)
    intros i rho v j w' H1 H3 H4.
(* Goal: forall _ : Q (@pair nat (vec nat n) j w'), Q (@pair nat (vec nat n) i v) *)
    apply HQ1 with (1 := H1); auto.
(* Goal: @sss_output (mm_instr n) (vec nat n) (@mm_sss n) P (@pair nat (vec nat n) j w') se *)
    split; auto.
  Qed.

End mm_term_ind.




