(**************************************************************)
(*   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 Bool.

Require Import utils pos vec. 
Require Import subcode sss.
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).

(** * Binary Stack Machines
   Binary stack machines have n stacks and there are just two instructions
  
   1/ POP s p q : pops the value on stack s and
                  if Empty then jumps to q 
                  if Zero then jumps to p
                  if One then jumps to next instruction,
   2/ PUSH s b : pushes the value b on stack s and jumps to next instructions 

 *)

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.


(** ** Semantics for BSM *)

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.      
  
  (* bsm_sss is a functional relation *)
      
  Fact bsm_sss_fun i s t1 t2 : i // s -1> t1 -> i // s -1> t2 -> t1 = t2.
(* Goal: forall (_ : bsm_sss i s t1) (_ : bsm_sss i s t2), @eq bsm_state t1 t2 *)
  Proof. intros []; subst; inversion 1; subst; auto; try mydiscr; myinj. Qed.

  (* bsm_sss is an informativelly total relation *) 
  
  Fact bsm_sss_total ii s : { t | ii // s -1> t }.
  Proof.
(* Goal: @sig bsm_state (fun t : bsm_state => bsm_sss ii s t) *)
    destruct s as (i,v).
(* Goal: @sig bsm_state (fun t : bsm_state => bsm_sss ii (@pair nat (vec (list bool) n) i v) t) *)
    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.
(* Goal: @ex bsm_state (fun t : bsm_state => bsm_sss ii s t) *)
    destruct (bsm_sss_total ii s); firstorder.
  Qed.
  
  (* Hence computations can only stop at instructions which lie outside the code 
     Stalling means no instruction can be executed anymore. It DOES NOT mean
     that the state cannot change anymore (this is a strictly lesser requirement).
  *)
  
  Fact bsm_sss_stall : forall P s, sss_step_stall bsm_sss P s -> out_code (fst s) P.
  Proof.
(* Goal: forall (P : prod nat (list (bsm_instr n))) (s : prod nat (vec (list bool) n)) (_ : @sss_step_stall (bsm_instr n) (vec (list bool) n) bsm_sss P s), @out_code (bsm_instr n) (@fst nat (vec (list bool) n) s) P *)
    intros (i,P) (q,v) H; unfold fst.
(* Goal: @out_code (bsm_instr n) q (@pair nat (list (bsm_instr n)) i P) *)
    red in H.
(* Goal: @out_code (bsm_instr n) q (@pair nat (list (bsm_instr n)) i P) *)
    destruct (in_out_code_dec q (i,P)) as [ H1 | ]; auto; exfalso.
(* Goal: False *)
    apply in_code_subcode in H1.
(* Goal: False *)
    destruct H1 as (ii & l & r & H1 & H2).
(* Goal: False *)
    simpl in H1.
(* Goal: False *)
    destruct (bsm_sss_total ii (q,v)) as (t & Ht).
(* Goal: False *)
    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.
(* Goal: forall (_ : @subcode (bsm_instr n) (@pair nat (list (bsm_instr n)) i (@cons (bsm_instr n) (@bsm_pop n x p q) (@nil (bsm_instr n)))) P) (_ : @eq (list bool) (@vec_pos (list bool) n v x) (@cons bool true ll)) (_ : @sss_compute (bsm_instr n) (vec (list bool) n) bsm_sss P (@pair nat (vec (list bool) n) (Init.Nat.add (S O) i) (@vec_change (list bool) n v x ll)) st), @sss_compute (bsm_instr n) (vec (list bool) n) bsm_sss P (@pair nat (vec (list bool) n) i v) st *)
    intros H1 H2.
(* Goal: forall _ : @sss_compute (bsm_instr n) (vec (list bool) n) bsm_sss P (@pair nat (vec (list bool) n) (Init.Nat.add (S O) i) (@vec_change (list bool) n v x (@cons bool b (@vec_pos (list bool) n v x)))) st, @sss_compute (bsm_instr n) (vec (list bool) n) bsm_sss P (@pair nat (vec (list bool) n) i v) st *)
    apply subcode_sss_compute_trans with (1 := H1).
(* Goal: @sss_compute (bsm_instr n) (vec (list bool) n) bsm_sss (@pair nat (list (bsm_instr n)) i (@cons (bsm_instr n) (@bsm_push n x b) (@nil (bsm_instr n)))) (@pair nat (vec (list bool) n) i v) (@pair nat (vec (list bool) n) (Init.Nat.add (S O) i) (@vec_change (list bool) n v x (@cons bool b (@vec_pos (list bool) n v x)))) *)
    exists 1; apply sss_steps_1.
(* Goal: @sss_step (bsm_instr n) (vec (list bool) n) bsm_sss (@pair nat (list (bsm_instr n)) i (@cons (bsm_instr n) (@bsm_push n x b) (@nil (bsm_instr n)))) (@pair nat (vec (list bool) n) i v) (@pair nat (vec (list bool) n) (Init.Nat.add (S O) i) (@vec_change (list bool) n v x (@cons bool b (@vec_pos (list bool) n v x)))) *)
    apply in_sss_step with (l := nil).
(* Goal: @eq nat (@fst nat (vec (list bool) n) (@pair nat (vec (list bool) n) i v)) (Init.Nat.add i (@length (bsm_instr n) (@nil (bsm_instr n)))) *)
(* Goal: bsm_sss (@bsm_push n x b) (@pair nat (vec (list bool) n) i v) (@pair nat (vec (list bool) n) (Init.Nat.add (S O) i) (@vec_change (list bool) n v x (@cons bool b (@vec_pos (list bool) n v x)))) *)
    simpl; omega.
(* Goal: bsm_sss (@bsm_push n x b) (@pair nat (vec (list bool) n) i v) (@pair nat (vec (list bool) n) (Init.Nat.add (S O) i) (@vec_change (list bool) n v x (@cons bool b (@vec_pos (list bool) n v x)))) *)
    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.
(* Goal: forall (_ : @subcode (bsm_instr n) (@pair nat (list (bsm_instr n)) i (@cons (bsm_instr n) (@bsm_pop n x p q) (@nil (bsm_instr n)))) P) (_ : @eq (list bool) (@vec_pos (list bool) n v x) (@cons bool true ll)) (_ : @sss_compute (bsm_instr n) (vec (list bool) n) bsm_sss P (@pair nat (vec (list bool) n) (Init.Nat.add (S O) i) (@vec_change (list bool) n v x ll)) st), @sss_compute (bsm_instr n) (vec (list bool) n) bsm_sss P (@pair nat (vec (list bool) n) i v) st *)
    intros H1 H2.
(* Goal: forall _ : @sss_compute (bsm_instr n) (vec (list bool) n) bsm_sss P (@pair nat (vec (list bool) n) (Init.Nat.add (S O) i) (@vec_change (list bool) n v x (@cons bool b (@vec_pos (list bool) n v x)))) st, @sss_compute (bsm_instr n) (vec (list bool) n) bsm_sss P (@pair nat (vec (list bool) n) i v) st *)
    apply subcode_sss_compute_trans with (1 := H1).
(* Goal: @sss_compute (bsm_instr n) (vec (list bool) n) bsm_sss (@pair nat (list (bsm_instr n)) i (@cons (bsm_instr n) (@bsm_push n x b) (@nil (bsm_instr n)))) (@pair nat (vec (list bool) n) i v) (@pair nat (vec (list bool) n) (Init.Nat.add (S O) i) (@vec_change (list bool) n v x (@cons bool b (@vec_pos (list bool) n v x)))) *)
    exists 1; apply sss_steps_1.
(* Goal: @sss_step (bsm_instr n) (vec (list bool) n) bsm_sss (@pair nat (list (bsm_instr n)) i (@cons (bsm_instr n) (@bsm_push n x b) (@nil (bsm_instr n)))) (@pair nat (vec (list bool) n) i v) (@pair nat (vec (list bool) n) (Init.Nat.add (S O) i) (@vec_change (list bool) n v x (@cons bool b (@vec_pos (list bool) n v x)))) *)
    apply in_sss_step with (l := nil).
(* Goal: @eq nat (@fst nat (vec (list bool) n) (@pair nat (vec (list bool) n) i v)) (Init.Nat.add i (@length (bsm_instr n) (@nil (bsm_instr n)))) *)
(* Goal: bsm_sss (@bsm_push n x b) (@pair nat (vec (list bool) n) i v) (@pair nat (vec (list bool) n) (Init.Nat.add (S O) i) (@vec_change (list bool) n v x (@cons bool b (@vec_pos (list bool) n v x)))) *)
    simpl; omega.
(* Goal: bsm_sss (@bsm_push n x b) (@pair nat (vec (list bool) n) i v) (@pair nat (vec (list bool) n) (Init.Nat.add (S O) i) (@vec_change (list bool) n v x (@cons bool b (@vec_pos (list bool) n v x)))) *)
    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.
(* Goal: forall (_ : @subcode (bsm_instr n) (@pair nat (list (bsm_instr n)) i (@cons (bsm_instr n) (@bsm_pop n x p q) (@nil (bsm_instr n)))) P) (_ : @eq (list bool) (@vec_pos (list bool) n v x) (@cons bool true ll)) (_ : @sss_compute (bsm_instr n) (vec (list bool) n) bsm_sss P (@pair nat (vec (list bool) n) (Init.Nat.add (S O) i) (@vec_change (list bool) n v x ll)) st), @sss_compute (bsm_instr n) (vec (list bool) n) bsm_sss P (@pair nat (vec (list bool) n) i v) st *)
    intros H1 H2.
(* Goal: forall _ : @sss_compute (bsm_instr n) (vec (list bool) n) bsm_sss P (@pair nat (vec (list bool) n) (Init.Nat.add (S O) i) (@vec_change (list bool) n v x (@cons bool b (@vec_pos (list bool) n v x)))) st, @sss_compute (bsm_instr n) (vec (list bool) n) bsm_sss P (@pair nat (vec (list bool) n) i v) st *)
    apply subcode_sss_compute_trans with (1 := H1).
(* Goal: @sss_compute (bsm_instr n) (vec (list bool) n) bsm_sss (@pair nat (list (bsm_instr n)) i (@cons (bsm_instr n) (@bsm_push n x b) (@nil (bsm_instr n)))) (@pair nat (vec (list bool) n) i v) (@pair nat (vec (list bool) n) (Init.Nat.add (S O) i) (@vec_change (list bool) n v x (@cons bool b (@vec_pos (list bool) n v x)))) *)
    exists 1; apply sss_steps_1.
(* Goal: @sss_step (bsm_instr n) (vec (list bool) n) bsm_sss (@pair nat (list (bsm_instr n)) i (@cons (bsm_instr n) (@bsm_push n x b) (@nil (bsm_instr n)))) (@pair nat (vec (list bool) n) i v) (@pair nat (vec (list bool) n) (Init.Nat.add (S O) i) (@vec_change (list bool) n v x (@cons bool b (@vec_pos (list bool) n v x)))) *)
    apply in_sss_step with (l := nil).
(* Goal: @eq nat (@fst nat (vec (list bool) n) (@pair nat (vec (list bool) n) i v)) (Init.Nat.add i (@length (bsm_instr n) (@nil (bsm_instr n)))) *)
(* Goal: bsm_sss (@bsm_push n x b) (@pair nat (vec (list bool) n) i v) (@pair nat (vec (list bool) n) (Init.Nat.add (S O) i) (@vec_change (list bool) n v x (@cons bool b (@vec_pos (list bool) n v x)))) *)
    simpl; omega.
(* Goal: bsm_sss (@bsm_push n x b) (@pair nat (vec (list bool) n) i v) (@pair nat (vec (list bool) n) (Init.Nat.add (S O) i) (@vec_change (list bool) n v x (@cons bool b (@vec_pos (list bool) n v x)))) *)
    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.
(* Goal: forall (_ : @subcode (bsm_instr n) (@pair nat (list (bsm_instr n)) i (@cons (bsm_instr n) (@bsm_pop n x p q) (@nil (bsm_instr n)))) P) (_ : @eq (list bool) (@vec_pos (list bool) n v x) (@cons bool b ll)) (_ : @eq nat p (Init.Nat.add (S O) i)) (_ : @sss_compute (bsm_instr n) (vec (list bool) n) bsm_sss P (@pair nat (vec (list bool) n) (Init.Nat.add (S O) i) (@vec_change (list bool) n v x ll)) st), @sss_compute (bsm_instr n) (vec (list bool) n) bsm_sss P (@pair nat (vec (list bool) n) i v) st *)
    destruct b; intros H1 H2 H3.
(* Goal: forall _ : @sss_compute (bsm_instr n) (vec (list bool) n) bsm_sss P (@pair nat (vec (list bool) n) (Init.Nat.add (S O) i) (@vec_change (list bool) n v x ll)) st, @sss_compute (bsm_instr n) (vec (list bool) n) bsm_sss P (@pair nat (vec (list bool) n) i v) st *)
(* Goal: forall _ : @sss_compute (bsm_instr n) (vec (list bool) n) bsm_sss P (@pair nat (vec (list bool) n) (Init.Nat.add (S O) i) (@vec_change (list bool) n v x ll)) st, @sss_compute (bsm_instr n) (vec (list bool) n) bsm_sss P (@pair nat (vec (list bool) n) i v) st *)
    apply bsm_compute_POP_1 with p q; auto.
(* Goal: forall _ : @sss_compute (bsm_instr n) (vec (list bool) n) bsm_sss P (@pair nat (vec (list bool) n) (Init.Nat.add (S O) i) (@vec_change (list bool) n v x ll)) st, @sss_compute (bsm_instr n) (vec (list bool) n) bsm_sss P (@pair nat (vec (list bool) n) i v) st *)
    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.
(* Goal: forall (_ : @subcode (bsm_instr n) (@pair nat (list (bsm_instr n)) i (@cons (bsm_instr n) (@bsm_push n x b) (@nil (bsm_instr n)))) P) (_ : @sss_compute (bsm_instr n) (vec (list bool) n) bsm_sss P (@pair nat (vec (list bool) n) (Init.Nat.add (S O) i) (@vec_change (list bool) n v x (@cons bool b (@vec_pos (list bool) n v x)))) st), @sss_compute (bsm_instr n) (vec (list bool) n) bsm_sss P (@pair nat (vec (list bool) n) i v) st *)
    intros H1.
(* Goal: forall _ : @sss_compute (bsm_instr n) (vec (list bool) n) bsm_sss P (@pair nat (vec (list bool) n) (Init.Nat.add (S O) i) (@vec_change (list bool) n v x (@cons bool b (@vec_pos (list bool) n v x)))) st, @sss_compute (bsm_instr n) (vec (list bool) n) bsm_sss P (@pair nat (vec (list bool) n) i v) st *)
    apply subcode_sss_compute_trans with (1 := H1).
(* Goal: @sss_compute (bsm_instr n) (vec (list bool) n) bsm_sss (@pair nat (list (bsm_instr n)) i (@cons (bsm_instr n) (@bsm_push n x b) (@nil (bsm_instr n)))) (@pair nat (vec (list bool) n) i v) (@pair nat (vec (list bool) n) (Init.Nat.add (S O) i) (@vec_change (list bool) n v x (@cons bool b (@vec_pos (list bool) n v x)))) *)
    exists 1; apply sss_steps_1.
(* Goal: @sss_step (bsm_instr n) (vec (list bool) n) bsm_sss (@pair nat (list (bsm_instr n)) i (@cons (bsm_instr n) (@bsm_push n x b) (@nil (bsm_instr n)))) (@pair nat (vec (list bool) n) i v) (@pair nat (vec (list bool) n) (Init.Nat.add (S O) i) (@vec_change (list bool) n v x (@cons bool b (@vec_pos (list bool) n v x)))) *)
    apply in_sss_step with (l := nil).
(* Goal: @eq nat (@fst nat (vec (list bool) n) (@pair nat (vec (list bool) n) i v)) (Init.Nat.add i (@length (bsm_instr n) (@nil (bsm_instr n)))) *)
(* Goal: bsm_sss (@bsm_push n x b) (@pair nat (vec (list bool) n) i v) (@pair nat (vec (list bool) n) (Init.Nat.add (S O) i) (@vec_change (list bool) n v x (@cons bool b (@vec_pos (list bool) n v x)))) *)
    simpl; omega.
(* Goal: bsm_sss (@bsm_push n x b) (@pair nat (vec (list bool) n) i v) (@pair nat (vec (list bool) n) (Init.Nat.add (S O) i) (@vec_change (list bool) n v x (@cons bool b (@vec_pos (list bool) n v x)))) *)
    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.
(* Goal: forall (_ : @subcode (bsm_instr n) (@pair nat (list (bsm_instr n)) i (@cons (bsm_instr n) (@bsm_pop n x p q) (@nil (bsm_instr n)))) P) (_ : @eq (list bool) (@vec_pos (list bool) n v x) (@nil bool)) (_ : not (@eq (prod nat (vec (list bool) n)) st (@pair nat (vec (list bool) n) i v))) (_ : @sss_steps (bsm_instr n) (vec (list bool) n) bsm_sss P a (@pair nat (vec (list bool) n) i v) st), @sig nat (fun b : nat => and (lt b a) (@sss_steps (bsm_instr n) (vec (list bool) n) bsm_sss P b (@pair nat (vec (list bool) n) q v) st)) *)
    intros H1 H2 H3 H4.
(* Goal: @sig nat (fun a : nat => and (lt a k) (@sss_steps (bsm_instr n) (vec (list bool) n) bsm_sss P a (@pair nat (vec (list bool) n) (Init.Nat.add (S O) i) (@vec_change (list bool) n v x (@cons bool b (@vec_pos (list bool) n v x)))) st)) *)
    apply sss_steps_inv in H4.
(* Goal: @sig nat (fun b : nat => and (lt b a) (@sss_steps (bsm_instr n) (vec (list bool) n) bsm_sss P b (@pair nat (vec (list bool) n) (Init.Nat.add (S O) i) (@vec_change (list bool) n v x ll)) st)) *)
    destruct H4 as [ (_ & ?) | (b & H4) ]; subst.
(* Goal: @sig nat (fun b : nat => and (lt b O) (@sss_steps (bsm_instr n) (vec (list bool) n) bsm_sss P b (@pair nat (vec (list bool) n) q v) (@pair nat (vec (list bool) n) i v))) *)
(* Goal: @sig nat (fun b : nat => and (lt b a) (@sss_steps (bsm_instr n) (vec (list bool) n) bsm_sss P b (@pair nat (vec (list bool) n) q v) st)) *)
    destruct H3; auto.
(* Goal: @sig nat (fun b : nat => and (lt b a) (@sss_steps (bsm_instr n) (vec (list bool) n) bsm_sss P b (@pair nat (vec (list bool) n) q v) st)) *)
    exists b.
(* Goal: and (lt a k) (@sss_steps (bsm_instr n) (vec (list bool) n) bsm_sss P a (@pair nat (vec (list bool) n) (Init.Nat.add (S O) i) (@vec_change (list bool) n v x (@cons bool b (@vec_pos (list bool) n v x)))) st) *)
    destruct H4 as (st2 & ? & H4 & H5); subst.
(* Goal: and (lt a (S a)) (@sss_steps (bsm_instr n) (vec (list bool) n) bsm_sss P a (@pair nat (vec (list bool) n) (Init.Nat.add (S O) i) (@vec_change (list bool) n v x (@cons bool b (@vec_pos (list bool) n v x)))) st) *)
    split.
(* Goal: lt a (S a) *)
(* Goal: @sss_steps (bsm_instr n) (vec (list bool) n) bsm_sss P a (@pair nat (vec (list bool) n) (Init.Nat.add (S O) i) (@vec_change (list bool) n v x (@cons bool b (@vec_pos (list bool) n v x)))) st *)
    omega.
(* Goal: @sss_steps (bsm_instr n) (vec (list bool) n) bsm_sss P a (@pair nat (vec (list bool) n) (Init.Nat.add (S O) i) (@vec_change (list bool) n v x (@cons bool b (@vec_pos (list bool) n v x)))) st *)
    apply sss_step_subcode_inv with (1 := H1) in H4.
(* Goal: @sss_steps (bsm_instr n) (vec (list bool) n) bsm_sss P b (@pair nat (vec (list bool) n) q v) st *)
    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.
(* Goal: forall (_ : @subcode (bsm_instr n) (@pair nat (list (bsm_instr n)) i (@cons (bsm_instr n) (@bsm_pop n x p q) (@nil (bsm_instr n)))) P) (_ : @eq (list bool) (@vec_pos (list bool) n v x) (@nil bool)) (_ : not (@eq (prod nat (vec (list bool) n)) st (@pair nat (vec (list bool) n) i v))) (_ : @sss_steps (bsm_instr n) (vec (list bool) n) bsm_sss P a (@pair nat (vec (list bool) n) i v) st), @sig nat (fun b : nat => and (lt b a) (@sss_steps (bsm_instr n) (vec (list bool) n) bsm_sss P b (@pair nat (vec (list bool) n) q v) st)) *)
    intros H1 H2 H3 H4.
(* Goal: @sig nat (fun a : nat => and (lt a k) (@sss_steps (bsm_instr n) (vec (list bool) n) bsm_sss P a (@pair nat (vec (list bool) n) (Init.Nat.add (S O) i) (@vec_change (list bool) n v x (@cons bool b (@vec_pos (list bool) n v x)))) st)) *)
    apply sss_steps_inv in H4.
(* Goal: @sig nat (fun b : nat => and (lt b a) (@sss_steps (bsm_instr n) (vec (list bool) n) bsm_sss P b (@pair nat (vec (list bool) n) (Init.Nat.add (S O) i) (@vec_change (list bool) n v x ll)) st)) *)
    destruct H4 as [ (_ & ?) | (b & H4) ]; subst.
(* Goal: @sig nat (fun b : nat => and (lt b O) (@sss_steps (bsm_instr n) (vec (list bool) n) bsm_sss P b (@pair nat (vec (list bool) n) q v) (@pair nat (vec (list bool) n) i v))) *)
(* Goal: @sig nat (fun b : nat => and (lt b a) (@sss_steps (bsm_instr n) (vec (list bool) n) bsm_sss P b (@pair nat (vec (list bool) n) q v) st)) *)
    destruct H3; auto.
(* Goal: @sig nat (fun b : nat => and (lt b a) (@sss_steps (bsm_instr n) (vec (list bool) n) bsm_sss P b (@pair nat (vec (list bool) n) q v) st)) *)
    exists b.
(* Goal: and (lt a k) (@sss_steps (bsm_instr n) (vec (list bool) n) bsm_sss P a (@pair nat (vec (list bool) n) (Init.Nat.add (S O) i) (@vec_change (list bool) n v x (@cons bool b (@vec_pos (list bool) n v x)))) st) *)
    destruct H4 as (st2 & ? & H4 & H5); subst.
(* Goal: and (lt a (S a)) (@sss_steps (bsm_instr n) (vec (list bool) n) bsm_sss P a (@pair nat (vec (list bool) n) (Init.Nat.add (S O) i) (@vec_change (list bool) n v x (@cons bool b (@vec_pos (list bool) n v x)))) st) *)
    split.
(* Goal: lt a (S a) *)
(* Goal: @sss_steps (bsm_instr n) (vec (list bool) n) bsm_sss P a (@pair nat (vec (list bool) n) (Init.Nat.add (S O) i) (@vec_change (list bool) n v x (@cons bool b (@vec_pos (list bool) n v x)))) st *)
    omega.
(* Goal: @sss_steps (bsm_instr n) (vec (list bool) n) bsm_sss P a (@pair nat (vec (list bool) n) (Init.Nat.add (S O) i) (@vec_change (list bool) n v x (@cons bool b (@vec_pos (list bool) n v x)))) st *)
    apply sss_step_subcode_inv with (1 := H1) in H4.
(* Goal: @sss_steps (bsm_instr n) (vec (list bool) n) bsm_sss P b (@pair nat (vec (list bool) n) q v) st *)
    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.
(* Goal: forall (_ : @subcode (bsm_instr n) (@pair nat (list (bsm_instr n)) i (@cons (bsm_instr n) (@bsm_pop n x p q) (@nil (bsm_instr n)))) P) (_ : @eq (list bool) (@vec_pos (list bool) n v x) (@cons bool b ll)) (_ : @eq nat p (Init.Nat.add (S O) i)) (_ : not (@eq (prod nat (vec (list bool) n)) st (@pair nat (vec (list bool) n) i v))) (_ : @sss_steps (bsm_instr n) (vec (list bool) n) bsm_sss P a (@pair nat (vec (list bool) n) i v) st), @sig nat (fun b : nat => and (lt b a) (@sss_steps (bsm_instr n) (vec (list bool) n) bsm_sss P b (@pair nat (vec (list bool) n) (Init.Nat.add (S O) i) (@vec_change (list bool) n v x ll)) st)) *)
    intros.
(* Goal: @sig nat (fun b : nat => and (lt b a) (@sss_steps (bsm_instr n) (vec (list bool) n) bsm_sss P b (@pair nat (vec (list bool) n) (Init.Nat.add (S O) i) (@vec_change (list bool) n v x ll)) st)) *)
    destruct b.
(* Goal: @sig nat (fun b : nat => and (lt b a) (@sss_steps (bsm_instr n) (vec (list bool) n) bsm_sss P b (@pair nat (vec (list bool) n) (Init.Nat.add (S O) i) (@vec_change (list bool) n v x ll)) st)) *)
(* Goal: @sig nat (fun b : nat => and (lt b a) (@sss_steps (bsm_instr n) (vec (list bool) n) bsm_sss P b (@pair nat (vec (list bool) n) (Init.Nat.add (S O) i) (@vec_change (list bool) n v x ll)) st)) *)
    apply bsm_steps_POP_1_inv with p q; auto.
(* Goal: @sig nat (fun b : nat => and (lt b a) (@sss_steps (bsm_instr n) (vec (list bool) n) bsm_sss P b (@pair nat (vec (list bool) n) (Init.Nat.add (S O) i) (@vec_change (list bool) n v x ll)) st)) *)
    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.
(* Goal: forall (_ : @subcode (bsm_instr n) (@pair nat (list (bsm_instr n)) i (@cons (bsm_instr n) (@bsm_pop n x p q) (@nil (bsm_instr n)))) P) (_ : @eq (list bool) (@vec_pos (list bool) n v x) (@nil bool)) (_ : not (@eq (prod nat (vec (list bool) n)) st (@pair nat (vec (list bool) n) i v))) (_ : @sss_steps (bsm_instr n) (vec (list bool) n) bsm_sss P a (@pair nat (vec (list bool) n) i v) st), @sig nat (fun b : nat => and (lt b a) (@sss_steps (bsm_instr n) (vec (list bool) n) bsm_sss P b (@pair nat (vec (list bool) n) q v) st)) *)
    intros H1 H2 H3 H4.
(* Goal: @sig nat (fun a : nat => and (lt a k) (@sss_steps (bsm_instr n) (vec (list bool) n) bsm_sss P a (@pair nat (vec (list bool) n) (Init.Nat.add (S O) i) (@vec_change (list bool) n v x (@cons bool b (@vec_pos (list bool) n v x)))) st)) *)
    apply sss_steps_inv in H4.
(* Goal: @sig nat (fun b : nat => and (lt b a) (@sss_steps (bsm_instr n) (vec (list bool) n) bsm_sss P b (@pair nat (vec (list bool) n) q v) st)) *)
    destruct H4 as [ (? & ?) | (b & H4) ]; subst; auto.
(* Goal: @sig nat (fun b : nat => and (lt b O) (@sss_steps (bsm_instr n) (vec (list bool) n) bsm_sss P b (@pair nat (vec (list bool) n) q v) (@pair nat (vec (list bool) n) i v))) *)
(* Goal: @sig nat (fun b : nat => and (lt b a) (@sss_steps (bsm_instr n) (vec (list bool) n) bsm_sss P b (@pair nat (vec (list bool) n) q v) st)) *)
    destruct H3; auto.
(* Goal: @sig nat (fun b : nat => and (lt b a) (@sss_steps (bsm_instr n) (vec (list bool) n) bsm_sss P b (@pair nat (vec (list bool) n) q v) st)) *)
    exists b.
(* Goal: and (lt a k) (@sss_steps (bsm_instr n) (vec (list bool) n) bsm_sss P a (@pair nat (vec (list bool) n) (Init.Nat.add (S O) i) (@vec_change (list bool) n v x (@cons bool b (@vec_pos (list bool) n v x)))) st) *)
    destruct H4 as (st2 & ? & H4 & H5); subst.
(* Goal: and (lt a (S a)) (@sss_steps (bsm_instr n) (vec (list bool) n) bsm_sss P a (@pair nat (vec (list bool) n) (Init.Nat.add (S O) i) (@vec_change (list bool) n v x (@cons bool b (@vec_pos (list bool) n v x)))) st) *)
    split.
(* Goal: lt a (S a) *)
(* Goal: @sss_steps (bsm_instr n) (vec (list bool) n) bsm_sss P a (@pair nat (vec (list bool) n) (Init.Nat.add (S O) i) (@vec_change (list bool) n v x (@cons bool b (@vec_pos (list bool) n v x)))) st *)
    omega.
(* Goal: @sss_steps (bsm_instr n) (vec (list bool) n) bsm_sss P a (@pair nat (vec (list bool) n) (Init.Nat.add (S O) i) (@vec_change (list bool) n v x (@cons bool b (@vec_pos (list bool) n v x)))) st *)
    apply sss_step_subcode_inv with (1 := H1) in H4.
(* Goal: @sss_steps (bsm_instr n) (vec (list bool) n) bsm_sss P b (@pair nat (vec (list bool) n) q v) st *)
    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.
(* Goal: forall (_ : @subcode (bsm_instr n) (@pair nat (list (bsm_instr n)) i (@cons (bsm_instr n) (@bsm_push n x b) (@nil (bsm_instr n)))) P) (_ : not (@eq (prod nat (vec (list bool) n)) st (@pair nat (vec (list bool) n) i v))) (_ : @sss_steps (bsm_instr n) (vec (list bool) n) bsm_sss P k (@pair nat (vec (list bool) n) i v) st), @sig nat (fun a : nat => and (lt a k) (@sss_steps (bsm_instr n) (vec (list bool) n) bsm_sss P a (@pair nat (vec (list bool) n) (Init.Nat.add (S O) i) (@vec_change (list bool) n v x (@cons bool b (@vec_pos (list bool) n v x)))) st)) *)
    intros H1 H2 H4.
(* Goal: @sig nat (fun a : nat => and (lt a k) (@sss_steps (bsm_instr n) (vec (list bool) n) bsm_sss P a (@pair nat (vec (list bool) n) (Init.Nat.add (S O) i) (@vec_change (list bool) n v x (@cons bool b (@vec_pos (list bool) n v x)))) st)) *)
    apply sss_steps_inv in H4.
(* Goal: @sig nat (fun a : nat => and (lt a k) (@sss_steps (bsm_instr n) (vec (list bool) n) bsm_sss P a (@pair nat (vec (list bool) n) (Init.Nat.add (S O) i) (@vec_change (list bool) n v x (@cons bool b (@vec_pos (list bool) n v x)))) st)) *)
    destruct H4 as [ (? & ?) | (a & H4) ]; subst; auto.
(* Goal: @sig nat (fun a : nat => and (lt a O) (@sss_steps (bsm_instr n) (vec (list bool) n) bsm_sss P a (@pair nat (vec (list bool) n) (Init.Nat.add (S O) i) (@vec_change (list bool) n v x (@cons bool b (@vec_pos (list bool) n v x)))) (@pair nat (vec (list bool) n) i v))) *)
(* Goal: @sig nat (fun a : nat => and (lt a k) (@sss_steps (bsm_instr n) (vec (list bool) n) bsm_sss P a (@pair nat (vec (list bool) n) (Init.Nat.add (S O) i) (@vec_change (list bool) n v x (@cons bool b (@vec_pos (list bool) n v x)))) st)) *)
    destruct H2; auto.
(* Goal: @sig nat (fun a : nat => and (lt a k) (@sss_steps (bsm_instr n) (vec (list bool) n) bsm_sss P a (@pair nat (vec (list bool) n) (Init.Nat.add (S O) i) (@vec_change (list bool) n v x (@cons bool b (@vec_pos (list bool) n v x)))) st)) *)
    exists a.
(* Goal: and (lt a k) (@sss_steps (bsm_instr n) (vec (list bool) n) bsm_sss P a (@pair nat (vec (list bool) n) (Init.Nat.add (S O) i) (@vec_change (list bool) n v x (@cons bool b (@vec_pos (list bool) n v x)))) st) *)
    destruct H4 as (st2 & ? & H4 & H5); subst.
(* Goal: and (lt a (S a)) (@sss_steps (bsm_instr n) (vec (list bool) n) bsm_sss P a (@pair nat (vec (list bool) n) (Init.Nat.add (S O) i) (@vec_change (list bool) n v x (@cons bool b (@vec_pos (list bool) n v x)))) st) *)
    split.
(* Goal: lt a (S a) *)
(* Goal: @sss_steps (bsm_instr n) (vec (list bool) n) bsm_sss P a (@pair nat (vec (list bool) n) (Init.Nat.add (S O) i) (@vec_change (list bool) n v x (@cons bool b (@vec_pos (list bool) n v x)))) st *)
    omega.
(* Goal: @sss_steps (bsm_instr n) (vec (list bool) n) bsm_sss P a (@pair nat (vec (list bool) n) (Init.Nat.add (S O) i) (@vec_change (list bool) n v x (@cons bool b (@vec_pos (list bool) n v x)))) st *)
    apply sss_step_subcode_inv with (1 := H1) in H4.
(* Goal: @sss_steps (bsm_instr n) (vec (list bool) n) bsm_sss P a (@pair nat (vec (list bool) n) (Init.Nat.add (S O) i) (@vec_change (list bool) n v x (@cons bool b (@vec_pos (list bool) n v x)))) st *)
    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.

(* The Halting problem for BSM *)
  
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.


     
