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

Set Implicit Arguments.

Reserved Notation "i '//' r '-1>' s" (at level 70, no associativity).
Reserved Notation "P '//' r ':1>' s" (at level 70, no associativity).
Reserved Notation "P '//' r '-[' n ']->' s" (at level 70, no associativity).
Reserved Notation "P '//' r '-+>' s" (at level 70, no associativity).
Reserved Notation "P '//' r '->>' s" (at level 70, no associativity).
Reserved Notation "P '//' r '-]]' s" (at level 70, no associativity).
Reserved Notation "P '//' r '~~>' s" (at level 70, no associativity).
Reserved Notation "P '//' r ↓" (at level 70, no associativity).

Section Small_Step_Semantics.

  (** * Code
      A generic library to implement Small Step Semantics on programs described
      by lists of instructions that modify a state and a Program Counter (PC) 
     
      An important part of the library is devoted to show locality lemmas
      that related computation inside sub-programs to outer programs
      
      This is ESSENTIAL to be able to show properties compositionally,
      ie to derive properties of program from properties of sub-programs
   *)

  (** ** Syntax *)


  Variable (instr : Set) (data : Type).

  (* A state contain the PC (current instruction) and data *)
  
  Notation state := (nat * data)%type.
  
  Variable one_step : instr -> state -> state -> Prop.
  
  Notation "i // s -1> t" := (one_step i s t) (at level 70, no associativity).
  Notation "s ⟬ i ⦒  t" := (one_step i s t) (at level 70, no associativity).
 
  Hypothesis (sss_fun : forall i s t1 t2, i // s -1> t1 -> i // s -1> t2 -> t1 = t2).
  Hypothesis (sss_dec : forall i st1 st2, { i // st1 -1> st2 } + { ~ i // st1 -1> st2 }).
  
  (* A code is a contiguous list of instructions starting at some position *)
  
  Notation code := (nat * list instr)%type.
  
  (** ** Semantics *)
  
  (* This a one step computation *) 

  Definition sss_step P st1 st2 := exists k l i r d, P = (k,l++i::r)
                                                  /\ st1 = (k+length l,d)
                                                  /\ i // st1 -1> st2.
                                                        
  Notation "P // r :1> s" := (sss_step P r s)  (at level 70, no associativity).
  
  (* Functionality of one step computations *)

  Fact sss_step_fun P s t1 t2 : P // s :1> t1 -> P // s :1> t2 -> t1 = t2.
  Proof.
    intros (k1 & l1 & i1 & r1 & d1 & ? & ? & H1)
           (k2 & l2 & i2 & r2 & d2 & ? & ? & H2).
(* Goal: @eq (prod nat data) t1 t2 *)
    subst.
(* Goal: @eq (prod nat data) t1 t2 *)
    inversion H3.
(* Goal: @eq (prod nat data) t1 t2 *)
    inversion H4.
(* Goal: @eq (prod nat data) t1 t2 *)
    subst k2.
(* Goal: @eq (prod nat data) t1 t2 *)
    apply list_app_inj in H5; try omega.
(* Goal: @eq (prod nat data) t1 t2 *)
    destruct H5 as (? & H5); inversion H5.
(* Goal: @eq (prod nat data) t1 t2 *)
    subst.
(* Goal: @eq (prod nat data) t1 t2 *)
    revert H1 H2; apply sss_fun.
  Qed.
 
  (* A "more general/usable" constructor *)
  
  Fact in_sss_step k l i r st1 st2 : fst st1 = k+length l        
                               ->       i     // st1  -1>  st2 
                               -> (k,l++i::r) // st1  :1>  st2.
  Proof. destruct st1 as (j,d); simpl; intro; subst; exists k,l,i,r,d; auto. Qed.

  (* A destructor *)

  Fact sss_step_subcode_inv P ii st st' : 
        (fst st, ii::nil) <sc P -> P // st :1> st' -> ii // st -1> st'.
  Proof.
(* Goal: forall (_ : @subcode instr (@pair nat (list instr) (@fst nat data st) (@cons instr ii (@nil instr))) P) (_ : sss_step P st st'), one_step ii st st' *)
    intros H1 (k & l2 & jj & r2 & d1 & H3 & H4 & H5); subst P st.
(* Goal: one_step ii (@pair nat data (Init.Nat.add k (@length instr l2)) d1) st' *)
    destruct H1 as (l1 & r1 & H1 & H2).
(* Goal: one_step ii (@pair nat data (Init.Nat.add k (@length instr l2)) d1) st' *)
    simpl in H1, H2.
(* Goal: one_step ii (@pair nat data (Init.Nat.add k (@length instr l2)) d1) st' *)
    apply list_app_inj in H1; try omega.
(* Goal: one_step ii (@pair nat data (Init.Nat.add k (@length instr l2)) d1) st' *)
    destruct H1 as (? & H1); subst l2.
(* Goal: one_step ii (@pair nat data (Init.Nat.add k (@length instr l1)) d1) st' *)
    inversion H1; subst jj r2; auto.
  Qed.

  Fact sss_step_supcode P Q st st' :
       P <sc Q -> in_code (fst st) P -> Q // st :1> st' -> P // st :1> st'.
  Proof.
(* Goal: @eq (prod nat data) t1 t2 *)
    intros H1 H2 (k & l & ii & r & d & ? & ? & H3); subst.
    destruct P as (iP,cP). 
    destruct H1 as (ll & rr & H1 & H4).
    simpl in H2.
    symmetry in H1.
    apply list_app_cons_eq_inv in H1.
    destruct H1 as [ (m & G1 & G2) | (m & G1 & G2) ].
    2: apply f_equal with (f := @length _) in G1;
(* Goal: lt q k *)
(* Goal: @subcode instr P P *)
       exfalso; revert G1; rew length; intro; omega.
    apply list_app_cons_eq_inv in G2.
    destruct G2 as [ (p & G3 & G4) | (p & G3 & G4) ].
    subst; exfalso; revert H2; rew length; intro; omega.
(* Goal: @eq (prod nat data) t1 t2 *)
    subst.
    apply in_sss_step; auto.
    revert H2; rew length; simpl; intro; omega.
  Qed.
  
  (* sss_step is decidable *)
  
  Fact sss_step_dec P st1 st2 : { P // st1 :1> st2 } + { ~ P // st1 :1> st2 }.
  Proof.
(* Goal: sumbool (sss_step P st1 st2) (not (sss_step P st1 st2)) *)
    destruct st1 as (j,d).
(* Goal: sumbool (sss_step P (@pair nat data j d) st2) (not (sss_step P (@pair nat data j d) st2)) *)
    destruct P as (k,ll).
(* Goal: sumbool (sss_step (@pair nat (list instr) k ll) (@pair nat data j d) st2) (not (sss_step (@pair nat (list instr) k ll) (@pair nat data j d) st2)) *)
    destruct (le_lt_dec k j) as [ H1 | H1 ].
(* Goal: sumbool (sss_step (@pair nat (list instr) k ll) (@pair nat data j d) st2) (not (sss_step (@pair nat (list instr) k ll) (@pair nat data j d) st2)) *)
(* Goal: sumbool (sss_step (@pair nat (list instr) k ll) (@pair nat data j d) st2) (not (sss_step (@pair nat (list instr) k ll) (@pair nat data j d) st2)) *)
    destruct (le_lt_dec (S j) (k+length ll)) as [ H2 | H2 ].
(* Goal: sumbool (sss_step (@pair nat (list instr) k ll) (@pair nat data j d) st2) (not (sss_step (@pair nat (list instr) k ll) (@pair nat data j d) st2)) *)
(* Goal: sumbool (sss_step (@pair nat (list instr) k ll) (@pair nat data j d) st2) (not (sss_step (@pair nat (list instr) k ll) (@pair nat data j d) st2)) *)
(* Goal: sumbool (sss_step (@pair nat (list instr) k ll) (@pair nat data j d) st2) (not (sss_step (@pair nat (list instr) k ll) (@pair nat data j d) st2)) *)
    destruct (@list_pick _ ll (j-k)) as (i & l & r & ? & ?).
(* Goal: lt q k *)
(* Goal: @subcode instr P P *)
    omega.
(* Goal: @eq (prod nat data) t1 t2 *)
    assert (j = k+length l) by omega; subst.
(* Goal: sumbool (sss_step (@pair nat (list instr) k (@app instr l (@cons instr i r))) (@pair nat data (Init.Nat.add k (@length instr l)) d) st2) (not (sss_step (@pair nat (list instr) k (@app instr l (@cons instr i r))) (@pair nat data (Init.Nat.add k (@length instr l)) d) st2)) *)
(* Goal: sumbool (sss_step (@pair nat (list instr) k ll) (@pair nat data j d) st2) (not (sss_step (@pair nat (list instr) k ll) (@pair nat data j d) st2)) *)
(* Goal: sumbool (sss_step (@pair nat (list instr) k ll) (@pair nat data j d) st2) (not (sss_step (@pair nat (list instr) k ll) (@pair nat data j d) st2)) *)
    destruct (sss_dec i (k+length l,d) st2) as [ | C ].
    left; apply in_sss_step; auto.
(* Goal: sumbool (sss_step (@pair nat (list instr) k (@app instr l (@cons instr i r))) (@pair nat data (Init.Nat.add k (@length instr l)) d) st2) (not (sss_step (@pair nat (list instr) k (@app instr l (@cons instr i r))) (@pair nat data (Init.Nat.add k (@length instr l)) d) st2)) *)
(* Goal: sumbool (sss_step (@pair nat (list instr) k ll) (@pair nat data j d) st2) (not (sss_step (@pair nat (list instr) k ll) (@pair nat data j d) st2)) *)
(* Goal: sumbool (sss_step (@pair nat (list instr) k ll) (@pair nat data j d) st2) (not (sss_step (@pair nat (list instr) k ll) (@pair nat data j d) st2)) *)
    right; contradict C.
(* Goal: one_step i (@pair nat data (Init.Nat.add k (@length instr l)) d) st2 *)
(* Goal: sumbool (sss_step (@pair nat (list instr) k ll) (@pair nat data j d) st2) (not (sss_step (@pair nat (list instr) k ll) (@pair nat data j d) st2)) *)
(* Goal: sumbool (sss_step (@pair nat (list instr) k ll) (@pair nat data j d) st2) (not (sss_step (@pair nat (list instr) k ll) (@pair nat data j d) st2)) *)
    destruct C as (k1 & l1 & i1 & r1 & d1 & ? & ? & ?).
(* Goal: @eq (prod nat data) t1 t2 *)
    inversion H3; subst.
(* Goal: @eq (prod nat data) t1 t2 *)
    inversion H; subst.
(* Goal: lt q k *)
(* Goal: @subcode instr P P *)
    apply list_app_inj in H8; try omega.
(* Goal: one_step i (@pair nat data (Init.Nat.add k1 (@length instr l)) d1) st2 *)
(* Goal: sumbool (sss_step (@pair nat (list instr) k ll) (@pair nat data j d) st2) (not (sss_step (@pair nat (list instr) k ll) (@pair nat data j d) st2)) *)
(* Goal: sumbool (sss_step (@pair nat (list instr) k ll) (@pair nat data j d) st2) (not (sss_step (@pair nat (list instr) k ll) (@pair nat data j d) st2)) *)
    destruct H8 as (? & H8); inversion H8; subst; auto.
    
(* Goal: sumbool (sss_step (@pair nat (list instr) k ll) (@pair nat data j d) st2) (not (sss_step (@pair nat (list instr) k ll) (@pair nat data j d) st2)) *)
    right; intros (k1 & l1 & i1 & r1 & d1 & ? & ? & ?).
(* Goal: @eq (prod nat data) t1 t2 *)
    inversion H; subst.
(* Goal: @eq (prod nat data) t1 t2 *)
    inversion H0; subst.
(* Goal: lt q k *)
(* Goal: @subcode instr P P *)
    rewrite app_length in H2; simpl in H2; omega.
    
(* Goal: sumbool (sss_step (@pair nat (list instr) k ll) (@pair nat data j d) st2) (not (sss_step (@pair nat (list instr) k ll) (@pair nat data j d) st2)) *)
    right; intros (k1 & l1 & i1 & r1 & d1 & ? & ? & ?).
(* Goal: @eq (prod nat data) t1 t2 *)
    inversion H; subst.
(* Goal: @eq (prod nat data) t1 t2 *)
    inversion H0; subst.
(* Goal: lt q k *)
(* Goal: @subcode instr P P *)
    omega.
  Qed.

  (* This is a n steps computation *)
  
  Inductive sss_steps (P : code) : nat -> state -> state -> Prop :=
    | in_sss_steps_0 : forall st,                  P // st   -[0]->    st
    | in_sss_steps_S : forall n st1 st2 st3,       P // st1   :1>      st2
                                              ->   P // st2  -[n]->    st3
                                              ->   P // st1  -[S n]->  st3
  where "P // r -[ n ]-> s" := (sss_steps P n r s).
  
  (* More usable constructors *)
  
  Fact sss_steps_0 P st1 st2 : st1 = st2 -> P // st1 -[0]-> st2.
  Proof. intros []; constructor. Qed.

  Fact sss_steps_1 P st1 st2 : P // st1 :1> st2 -> P // st1 -[1]-> st2.
  Proof.
(* Goal: sss_steps Q (S k) st1 st3 *)
    constructor 2 with st2; auto.
(* Goal: sss_steps P O st2 st2 *)
    constructor 1.
  Qed.
  
  Fact sss_steps_trans P n m st1 st2 st3 :
         P // st1 -[n]-> st2 -> P // st2 -[m]-> st3 -> P // st1 -[n+m]-> st3 .
  Proof.
(* Goal: forall (_ : sss_steps P n st1 st2) (_ : sss_steps P m st2 st3), sss_steps P (Init.Nat.add n m) st1 st3 *)
    intros H; revert H st3.
(* Goal: forall (_ : sss_steps P n st1 st2) (st3 : prod nat data) (_ : sss_steps P m st2 st3), sss_steps P (Init.Nat.add n m) st1 st3 *)
    induction 1 as [ | ? ? st2 ]; simpl; intros; auto.
(* Goal: sss_steps Q (S k) st1 st3 *)
    constructor 2 with st2; auto.
  Qed.
  
  (* Inversion lemma *)
 
  Fact sss_steps_0_inv P st1 st2 : P // st1 -[0]-> st2 -> st1 = st2.
  Proof. inversion 1; auto. Qed.
  
  Fact sss_steps_S_inv P st1 st3 k : 
                        st1 <> st3 
      ->                P // st1 -[k]-> st3 
      -> exists k' st2, k = S k' 
                     /\ P // st1 :1> st2
                     /\ P // st2 -[k']-> st3.
  Proof.
(* Goal: forall _ : sss_steps P (S k) st1 st3, @ex (prod nat data) (fun st2 : prod nat data => and (sss_step P st1 st2) (sss_steps P k st2 st3)) *)
    intros H.
(* Goal: @eq (prod nat data) t1 t2 *)
    inversion 1; subst.
(* Goal: @ex nat (fun k' : nat => @ex (prod nat data) (fun st2 : prod nat data => and (@eq nat O (S k')) (and (sss_step P st3 st2) (sss_steps P k' st2 st3)))) *)
(* Goal: @ex nat (fun k' : nat => @ex (prod nat data) (fun st2 : prod nat data => and (@eq nat (S n) (S k')) (and (sss_step P st1 st2) (sss_steps P k' st2 st3)))) *)
    destruct H; auto.
(* Goal: @ex nat (fun k' : nat => @ex (prod nat data) (fun st2 : prod nat data => and (@eq nat (S n) (S k')) (and (sss_step P st1 st2) (sss_steps P k' st2 st3)))) *)
    exists n, st2; auto.
  Qed.

  Fact sss_steps_inv P k st1 st3 : 
          P // st1 -[k]-> st3 
       -> (k = 0 /\ st1 = st3)
        + { k' | exists st2, k = S k' 
                       /\ P // st1 :1> st2
                       /\ P // st2 -[k']-> st3 }%type.
  Proof.
(* Goal: forall _ : sss_steps P (S k) st1 st3, @ex (prod nat data) (fun st2 : prod nat data => and (sss_step P st1 st2) (sss_steps P k st2 st3)) *)
    intros H.
(* Goal: sum (and (@eq nat k O) (@eq (prod nat data) st1 st3)) (@sig nat (fun k' : nat => @ex (prod nat data) (fun st2 : prod nat data => and (@eq nat k (S k')) (and (sss_step P st1 st2) (sss_steps P k' st2 st3))))) *)
    destruct k as [ | k ]; [ left | right ].
(* Goal: and (@eq nat O O) (@eq (prod nat data) st1 st3) *)
(* Goal: @sig nat (fun k' : nat => @ex (prod nat data) (fun st2 : prod nat data => and (@eq nat (S k) (S k')) (and (sss_step P st1 st2) (sss_steps P k' st2 st3)))) *)
    apply sss_steps_0_inv in H; auto.
(* Goal: @sig nat (fun k' : nat => @ex (prod nat data) (fun st2 : prod nat data => and (@eq nat (S k) (S k')) (and (sss_step P st1 st2) (sss_steps P k' st2 st3)))) *)
    exists k.
(* Goal: @eq (prod nat data) t1 t2 *)
    inversion H; subst.
(* Goal: @ex (prod nat data) (fun st2 : prod nat data => and (sss_step P st1 st2) (sss_steps P k st2 st3)) *)
    exists st2; auto.
  Qed.
  
  Fact sss_steps_S_inv' P st1 st3 k :  
                        P // st1 -[S k]-> st3 
      -> exists st2,    P // st1 :1> st2
                     /\ P // st2 -[k]-> st3.
  Proof.
(* Goal: forall _ : sss_steps P (S k) st1 st3, @ex (prod nat data) (fun st2 : prod nat data => and (sss_step P st1 st2) (sss_steps P k st2 st3)) *)
    intros H.
(* Goal: @eq (prod nat data) t1 t2 *)
    inversion H; subst.
(* Goal: @ex (prod nat data) (fun st2 : prod nat data => and (sss_step P st1 st2) (sss_steps P k st2 st3)) *)
    exists st2; auto.
  Qed.
 
  Fact sss_steps_fun P k s t1 t2 :
         P // s -[k]-> t1 
      -> P // s -[k]-> t2 
      -> t1 = t2.
  Proof.
(* Goal: forall (_ : sss_steps P k s t1) (_ : sss_steps P k s t2), @eq (prod nat data) t1 t2 *)
    intros H; revert H t2; induction 1 as [ | ? ? st2 ? H1 H2 IH2 ]; simpl; intros t2 Ht2; auto.
(* Goal: @eq (prod nat data) st t2 *)
(* Goal: @eq (prod nat data) st3 t2 *)
    inversion Ht2; auto.
(* Goal: @eq (prod nat data) t1 t2 *)
    inversion Ht2; subst.
(* Goal: @eq (prod nat data) t1 t2 *)
    generalize (sss_step_fun H1 H0); intro; subst.
(* Goal: @eq (prod nat data) st3 t2 *)
    apply IH2 in H3; auto.
  Qed.
   
  Fact sss_steps_plus_inv P n m st1 st3 : 
         P // st1 -[n+m]-> st3 
      -> exists st2, P // st1 -[n]-> st2 
                  /\ P // st2 -[m]-> st3.
  Proof.
(* Goal: forall _ : sss_steps P (Init.Nat.add n m) st1 st3, @ex (prod nat data) (fun st2 : prod nat data => and (sss_steps P n st1 st2) (sss_steps P m st2 st3)) *)
    revert st1 st3; induction n as [ | n IHn ]; intros s t.
(* Goal: forall _ : sss_steps P (Init.Nat.add O m) s t, @ex (prod nat data) (fun st2 : prod nat data => and (sss_steps P O s st2) (sss_steps P m st2 t)) *)
(* Goal: forall _ : sss_steps P (Init.Nat.add (S n) m) s t, @ex (prod nat data) (fun st2 : prod nat data => and (sss_steps P (S n) s st2) (sss_steps P m st2 t)) *)
    exists s; split; auto; constructor.
(* Goal: @eq (prod nat data) t1 t2 *)
    inversion 1; subst.
(* Goal: @ex (prod nat data) (fun st2 : prod nat data => and (sss_steps P (S n) s st2) (sss_steps P m st2 t)) *)
    apply IHn in H2; destruct H2 as (st & ? & ?).
(* Goal: @ex (prod nat data) (fun st2 : prod nat data => and (sss_steps P (S n) s st2) (sss_steps P m st2 t)) *)
    exists st; split; auto.
(* Goal: sss_steps Q (S k) st1 st3 *)
    constructor 2 with st2; auto.
  Qed.
  
  Definition sss_progress P st1 st2 := exists k, 0 < k /\ P // st1 -[k]-> st2.
  Definition sss_compute  P st1 st2 := exists k, P // st1 -[k]-> st2.
  
  Notation "P // r -+> s" := (sss_progress P r s).
  Notation "P // r ->> s" := (sss_compute P r s).
  
  Fact sss_progress_compute P st1 st2 : P // st1 -+> st2 -> P // st1 ->> st2.
  Proof. intros (k & _ & ?); exists k; auto. Qed. 
  
  Fact sss_compute_trans P st1 st2 st3 : P // st1 ->> st2 -> P // st2 ->> st3 -> P // st1 ->> st3.
  Proof. intros (i & H1) (j & H2); exists (i+j); revert H1 H2; apply sss_steps_trans. Qed.
  
  Fact sss_progress_compute_trans P st1 st2 st3 : P // st1 -+> st2 -> P // st2 ->> st3 -> P // st1 -+> st3.
  Proof. intros (i & ? & H1) (j & H2); exists (i+j); split; try omega; revert H1 H2; apply sss_steps_trans. Qed.
  
  Fact sss_compute_progress_trans P st1 st2 st3 : P // st1 ->> st2 -> P // st2 -+> st3 -> P // st1 -+> st3.
  Proof. intros (i & H1) (j & ? & H2); exists (i+j); split; try omega; revert H1 H2; apply sss_steps_trans. Qed.
  
  Fact sss_progress_trans P st1 st2 st3 : P // st1 -+> st2 -> P // st2 -+> st3 -> P // st1 -+> st3.
  Proof. intro; apply sss_compute_progress_trans, sss_progress_compute; trivial. Qed.

  (* Computations must start inside code *) 
  
  Fact sss_step_in_code P st1 st2 : P // st1 :1> st2 -> in_code (fst st1) P.
  Proof.
(* Goal: forall _ : sss_step P st1 st2, @in_code instr (@fst nat data st1) P *)
    revert P st1 st2; intros (n,c) (i,d) st2 (q & l & ii & r & d1 & H1 & H2 & _).
(* Goal: @eq (prod nat data) t1 t2 *)
    inversion H1; subst.
(* Goal: @eq (prod nat data) t1 t2 *)
    inversion H2; subst.
(* Goal: lt q k *)
(* Goal: @subcode instr P P *)
    simpl; rew length; omega.
  Qed.

  Fact sss_steps_compute P n st1 st2 : P // st1 -[n]-> st2 -> P // st1 ->> st2.
  Proof. exists n; trivial. Qed.
  
  (** We propose a library of locality lemmas that link computations
      in subcode to computations in the code *)

  (** ** Compisitional Reasoning over Subcode *)

  (* First inclusions lemmas *)

  Fact subcode_sss_step P Q st1 st2: P <sc Q -> P // st1 :1> st2 -> Q // st1 :1> st2.
  Proof.
(* Goal: forall (_ : @subcode instr P Q) (_ : sss_step P st1 st2), sss_step Q st1 st2 *)
    destruct P as (n1,c1).
(* Goal: forall (_ : @subcode instr (@pair nat (list instr) n1 c1) Q) (_ : sss_step (@pair nat (list instr) n1 c1) st1 st2), sss_step Q st1 st2 *)
    destruct Q as (n2,c2).
(* Goal: forall (_ : @subcode instr (@pair nat (list instr) n1 c1) (@pair nat (list instr) n2 c2)) (_ : sss_step (@pair nat (list instr) n1 c1) st1 st2), sss_step (@pair nat (list instr) n2 c2) st1 st2 *)
    simpl.
(* Goal: forall (_ : @ex (list instr) (fun l : list instr => @ex (list instr) (fun r : list instr => and (@eq (list instr) c2 (@app instr l (@app instr c1 r))) (@eq nat n1 (Init.Nat.add n2 (@length instr l)))))) (_ : sss_step (@pair nat (list instr) n1 c1) st1 st2), sss_step (@pair nat (list instr) n2 c2) st1 st2 *)
    intros (l & r & H1 & H2) H3.
(* Goal: sss_step (@pair nat (list instr) n2 c2) st1 st2 *)
    destruct H3 as (q & ll & i & rr & d1 & H3 & H4 & H5).
(* Goal: @eq (prod nat data) t1 t2 *)
    inversion H3; subst.
(* Goal: sss_step (@pair nat (list instr) n2 (@app instr l (@app instr (@app instr ll (@cons instr i rr)) r))) (@pair nat data (Init.Nat.add (Init.Nat.add n2 (@length instr l)) (@length instr ll)) d1) st2 *)
    exists n2, (l++ll), i, (rr++r), d1; repeat split; auto.
(* Goal: @eq (prod nat (list instr)) (@pair nat (list instr) n2 (@app instr l (@app instr (@app instr ll (@cons instr i rr)) r))) (@pair nat (list instr) n2 (@app instr (@app instr l ll) (@cons instr i (@app instr rr r)))) *)
(* Goal: @eq (prod nat data) (@pair nat data (Init.Nat.add (Init.Nat.add n2 (@length instr l)) (@length instr ll)) d1) (@pair nat data (Init.Nat.add n2 (@length instr (@app instr l ll))) d1) *)
    f_equal; solve list eq.
(* Goal: lt q k *)
(* Goal: @subcode instr P P *)
    f_equal; rew length; omega.
  Qed.

  Fact subcode_sss_steps P Q k st1 st2: P <sc Q -> P // st1 -[k]-> st2 -> Q // st1 -[k]-> st2.
  Proof.
(* Goal: forall (_ : @subcode instr P Q) (_ : sss_steps P k st1 st2), sss_steps Q k st1 st2 *)
    induction 2 as [ | k st1 st2 st3 H3 H4 IH4 ].
(* Goal: sss_steps Q O st st *)
(* Goal: sss_steps Q (S k) st1 st3 *)
    constructor.
(* Goal: sss_steps Q (S k) st1 st3 *)
    constructor 2 with st2; auto.
(* Goal: sss_step Q st1 st2 *)
    revert H3; apply subcode_sss_step; auto.
  Qed.
  
  Fact subcode_sss_progress P Q st1 st2: P <sc Q -> P // st1 -+> st2 -> Q // st1 -+> st2.
  Proof.
(* Goal: forall (_ : @subcode instr P Q) (_ : sss_progress P st1 st2), sss_progress Q st1 st2 *)
    intros ? (k & ? & Hk); exists k; split; auto; revert Hk; apply subcode_sss_steps; auto.
  Qed.

  Fact subcode_sss_compute P Q st1 st2: P <sc Q -> P // st1 ->> st2 -> Q // st1 ->> st2.
  Proof.
(* Goal: forall (_ : @subcode instr P Q) (_ : sss_compute P st1 st2), sss_compute Q st1 st2 *)
    intros ? (k & Hk); exists k; revert Hk; apply subcode_sss_steps; auto.
  Qed.

  Fact subcode_sss_compute_trans P Q st1 st2 st3 :
       P <sc Q -> P // st1 ->> st2 -> Q // st2 ->> st3 -> Q // st1 ->> st3.
  Proof.
(* Goal: forall (_ : @subcode instr P Q) (_ : sss_compute P st1 st2) (_ : sss_compute Q st2 st3), sss_compute Q st1 st3 *)
    intros ? H.
(* Goal: forall _ : sss_compute Q st2 st3, sss_compute Q st1 st3 *)
    apply sss_compute_trans.
(* Goal: sss_compute Q st1 st2 *)
    revert H; apply subcode_sss_compute; auto.
  Qed.
  
  Fact subcode_sss_compute_linstr k li P st1 st2 st :
            (fst st1,li) // st1 -[k]-> st2
         -> (fst st1,li) <sc P
         -> P // st2 ->> st
         -> P // st1 ->> st.
  Proof.
(* Goal: forall (_ : @out_code instr (@fst nat data st1) P) (_ : sss_steps P k st1 st2), @eq (prod nat data) st1 st2 *)
    intros H1 H2.
(* Goal: forall _ : sss_compute P st2 st, sss_compute P st1 st *)
    apply subcode_sss_compute_trans with (1 := H2).
(* Goal: @ex nat (fun q : nat => and (@eq nat k (Init.Nat.add O q)) (sss_steps (@pair nat (list instr) j cj) q st (@pair nat data n d))) *)
(* Goal: @ex nat (fun q : nat => and (@eq nat k (Init.Nat.add (S p) q)) (sss_steps (@pair nat (list instr) j cj) q st3 (@pair nat data n d))) *)
    exists k; auto.
  Qed.
  
  Fact subcode_sss_compute_instr P i st1 st2 st3 : 
            i // st1 -1> st2
        ->  (fst st1,i::nil) <sc P
        ->  P // st2 ->> st3
        ->  P // st1 ->> st3.
  Proof.
(* Goal: forall (_ : one_step i st1 st2) (_ : @subcode instr (@pair nat (list instr) (@fst nat data st1) (@cons instr i (@nil instr))) P) (_ : sss_compute P st2 st3), sss_compute P st1 st3 *)
    intro H; apply subcode_sss_compute_linstr with (k := 1).
(* Goal: sss_steps (@pair nat (list instr) (@fst nat data st1) (@cons instr i (@nil instr))) (S O) st1 st2 *)
    apply sss_steps_1, in_sss_step with (l := nil); auto.
  Qed.
  
  (* Then are reverse inclusion lemmas *)

  Fact subcode_sss_step_inv P Q st1 st2 : 
         P <sc Q 
      -> in_code (fst st1) P
      -> Q // st1 :1> st2
      -> P // st1 :1> st2.
  Proof.
(* Goal: forall (_ : @subcode instr (@pair nat (list instr) n1 c1) (@pair nat (list instr) n2 c2)) (_ : sss_step (@pair nat (list instr) n1 c1) st1 st2), sss_step (@pair nat (list instr) n2 c2) st1 st2 *)
    revert P Q st1 st2; intros (nP,cP) (nQ,cQ) (i,d) st; simpl.
(* Goal: forall (_ : @ex (list instr) (fun l : list instr => @ex (list instr) (fun r : list instr => and (@eq (list instr) cQ (@app instr l (@app instr cP r))) (@eq nat nP (Init.Nat.add nQ (@length instr l)))))) (_ : and (le nP i) (lt i (Init.Nat.add nP (@length instr cP)))) (_ : sss_step (@pair nat (list instr) nQ cQ) (@pair nat data i d) st), sss_step (@pair nat (list instr) nP cP) (@pair nat data i d) st *)
    intros (l & r & H1 & H2) H3 (q & ll & ii & rr & d1 & H4 & H5 & H6).
(* Goal: @eq (prod nat data) t1 t2 *)
    inversion H4; subst.
(* Goal: @eq (prod nat data) t1 t2 *)
    inversion H5; subst.
(* Goal: sss_step (@pair nat (list instr) (Init.Nat.add q (@length instr l)) cP) (@pair nat data (Init.Nat.add q (@length instr ll)) d1) st *)
    clear H4 H5.
(* Goal: sss_step (@pair nat (list instr) (Init.Nat.add q (@length instr l)) cP) (@pair nat data (Init.Nat.add q (@length instr ll)) d1) st *)
    apply list_app_cons_eq_inv in H7. 
(* Goal: sss_step (@pair nat (list instr) (Init.Nat.add q (@length instr l)) cP) (@pair nat data (Init.Nat.add q (@length instr ll)) d1) st *)
    destruct H7 as [ (m & Hm1 & Hm2) | (m & Hm1 & Hm2) ].
(* Goal: sss_step (@pair nat (list instr) (Init.Nat.add q (@length instr l)) cP) (@pair nat data (Init.Nat.add q (@length instr ll)) d1) st *)
(* Goal: sss_step (@pair nat (list instr) (Init.Nat.add q (@length instr l)) cP) (@pair nat data (Init.Nat.add q (@length instr ll)) d1) st *)
    apply list_app_cons_eq_inv in Hm2.
(* Goal: sss_step (@pair nat (list instr) (Init.Nat.add q (@length instr l)) cP) (@pair nat data (Init.Nat.add q (@length instr ll)) d1) st *)
(* Goal: sss_step (@pair nat (list instr) (Init.Nat.add q (@length instr l)) cP) (@pair nat data (Init.Nat.add q (@length instr ll)) d1) st *)
    destruct Hm2 as [ (p & Hp1 & Hp2) | (p & Hp1 & Hp2) ].

(* Goal: sss_step (@pair nat (list instr) (Init.Nat.add q (@length instr l)) cP) (@pair nat data (Init.Nat.add q (@length instr ll)) d1) st *)
    apply f_equal with (f := @length _) in Hm1.
(* Goal: sss_step (@pair nat (list instr) (Init.Nat.add q (@length instr l)) cP) (@pair nat data (Init.Nat.add q (@length instr ll)) d1) st *)
(* Goal: sss_step (@pair nat (list instr) (Init.Nat.add q (@length instr l)) cP) (@pair nat data (Init.Nat.add q (@length instr ll)) d1) st *)
(* Goal: sss_step (@pair nat (list instr) (Init.Nat.add q (@length instr l)) cP) (@pair nat data (Init.Nat.add q (@length instr ll)) d1) st *)
    apply f_equal with (f := @length _) in Hp1.
(* Goal: lt q k *)
(* Goal: @subcode instr P P *)
    revert Hm1 Hp1; rew length; intros; omega.

    subst cP; apply in_sss_step; auto.
(* Goal: lt q k *)
(* Goal: @subcode instr P P *)
    simpl; subst; rew length; omega.
    
(* Goal: sss_step (@pair nat (list instr) (Init.Nat.add q (@length instr l)) cP) (@pair nat data (Init.Nat.add q (@length instr ll)) d1) st *)
    apply f_equal with (f := @length _) in Hm1.
(* Goal: sss_step (@pair nat (list instr) (Init.Nat.add q (@length instr l)) cP) (@pair nat data (Init.Nat.add q (@length instr ll)) d1) st *)
    apply f_equal with (f := @length _) in Hm2.
(* Goal: lt q k *)
(* Goal: @subcode instr P P *)
    revert Hm1 Hm2; rew length; intros; omega.
  Qed.

  Definition sss_output P st st' := P // st ->> st' /\ out_code (fst st') P.

  Notation "P // x ~~> y" := (sss_output P x y).

  Definition sss_terminates P st := exists st', P // st ~~> st'.

  Notation "P // x ↓" := (sss_terminates P x).

  Fact subcode_sss_terminates_instr P i st1 st2 : 
            i // st1 -1> st2
        ->  (fst st1,i::nil) <sc P
        ->  P // st2 ↓
        ->  P // st1 ↓.
  Proof.
(* Goal: forall (_ : one_step i st1 st2) (_ : @subcode instr (@pair nat (list instr) (@fst nat data st1) (@cons instr i (@nil instr))) P) (_ : sss_terminates P st2), sss_terminates P st1 *)
    intros H1 H2 (st3 & H3 & H4).
(* Goal: sss_terminates P st1 *)
    exists st3; split; auto.
(* Goal: sss_compute P st1 st3 *)
    revert H1 H2 H3; apply subcode_sss_compute_instr.
  Qed.

  (* No computation is possible *)
  
  Definition sss_stall ii st := forall st', ~ ii // st -1> st'.
  Definition sss_step_stall P st := forall st', ~ P // st :1> st'.

  Fact sss_steps_stall_inv P p s1 s2 : sss_step_stall P s1 -> P // s1 -[p]-> s2 -> p = 0 /\ s1 = s2.
  Proof.
(* Goal: forall (_ : sss_step_stall P s1) (_ : sss_steps P p s1 s2), and (@eq nat p O) (@eq (prod nat data) s1 s2) *)
    intros H; induction 1 as [ | p st1 st2 st3 H1 ]; auto.
(* Goal: and (@eq nat (S p) O) (@eq (prod nat data) st1 st3) *)
    apply H in H1; destruct H1.
  Qed.

  Fact sss_steps_stall_fun P p q s1 s2 :
         sss_step_stall P s2
      -> P // s1 -[p]-> s2 
      -> P // s1 -[q]-> s2
      -> p = q.
  Proof.
(* Goal: forall (_ : sss_step_stall P s2) (_ : sss_steps P p s1 s2) (_ : sss_steps P q s1 s2), @eq nat p q *)
    intros H1 H2; revert H2 q.
    induction 1 as [ s1 | p s1 s2 s3 H2 H3 IH3 ];
      intros q H5.
(* Goal: @eq nat O q *)
(* Goal: @eq nat (S p) q *)
    apply sss_steps_stall_inv, proj1 in H5; auto.
(* Goal: @eq nat (S p) q *)
    destruct q.
(* Goal: @eq (prod nat data) t1 t2 *)
    apply sss_steps_0_inv in H5; subst.
(* Goal: @eq nat (S p) O *)
(* Goal: @eq nat (S p) (S q) *)
    apply H1 in H2; destruct H2.
(* Goal: @eq nat (S p) (S q) *)
    specialize (IH3 H1).
(* Goal: @eq nat (S p) (S q) *)
    apply sss_steps_S_inv' in H5.
(* Goal: @eq nat (S p) (S q) *)
    destruct H5 as (st2' & H5 & H6).
(* Goal: @eq nat (S p) (S q) *)
    generalize (sss_step_fun H2 H5).
(* Goal: forall _ : @eq (prod nat data) s2 st2', @eq nat (S p) (S q) *)
    intros; subst st2'.
(* Goal: @eq nat (S p) (S q) *)
    apply IH3 in H6; subst; auto.
  Qed. 

  Definition sss_compute_max P s1 s2 := (P // s1 ->> s2 /\ sss_step_stall P s2).

  Notation " P // s1 -]] s2 " := (sss_compute_max P s1 s2).
  
  (* No computation outside the code *)

  Fact sss_out_step_stall P st : out_code (fst st) P -> sss_step_stall P st.
  Proof.
(* Goal: forall _ : @out_code instr (@fst nat data st) P, sss_step_stall P st *)
    revert P st; intros (n,code) (i,st).
(* Goal: forall _ : @out_code instr (@fst nat data (@pair nat data i st)) (@pair nat (list instr) n code), sss_step_stall (@pair nat (list instr) n code) (@pair nat data i st) *)
    intros H1 st' (k & l & ii & r & d1 & H2 & H3 & H4).
(* Goal: @eq (prod nat data) t1 t2 *)
    inversion H2; inversion H3; subst.
(* Goal: forall _ : sss_steps (@pair nat (list instr) j cj) k st1 (@pair nat data n d), @ex nat (fun q : nat => and (@eq nat k (Init.Nat.add p q)) (sss_steps (@pair nat (list instr) j cj) q st2 (@pair nat data n d))) *)
    simpl in H1.
(* Goal: lt q k *)
(* Goal: @subcode instr P P *)
    revert H1; rew length; intros []; omega.
  Qed.

  Fact sss_stall_step_stall ii P st :
          (fst st,ii::nil) <sc P
       -> sss_stall ii st
       -> sss_step_stall P st.
  Proof.
(* Goal: forall (_ : @subcode instr (@pair nat (list instr) (@fst nat data st) (@cons instr ii (@nil instr))) P) (_ : sss_stall ii st), sss_step_stall P st *)
    intros H1 H2 st' H.
    apply sss_step_subcode_inv  with (1 := H1) in H.
(* Goal: False *)
    revert H; apply H2.
  Qed.
  
  Fact sss_stall_step_0 ii P q st st' :
          (fst st,ii::nil) <sc P
       -> sss_stall ii st
       -> P // st -[q]-> st' -> q = 0 /\ st = st'.
  Proof.
(* Goal: forall (_ : @out_code instr (@fst nat data st1) P) (_ : sss_steps P k st1 st2), @eq (prod nat data) st1 st2 *)
    intros H1 H2.
(* Goal: forall _ : sss_steps P q st st', and (@eq nat q O) (@eq (prod nat data) st st') *)
    generalize (sss_stall_step_stall H1 H2).
(* Goal: forall (_ : sss_step_stall P st) (_ : sss_steps P q st st'), and (@eq nat q O) (@eq (prod nat data) st st') *)
    intros H3 H4.
(* Goal: @ex nat (fun k' : nat => and (@eq nat k (S k')) (sss_steps P k' st2 st3)) *)
    apply sss_steps_inv in H4.
(* Goal: and (@eq nat q O) (@eq (prod nat data) st st') *)
    destruct H4 as [ | (k & st2 & _ & H5 & _) ]; auto.
(* Goal: and (@eq nat q O) (@eq (prod nat data) st st') *)
    contradict H5; apply H3.
  Qed.

  Fact sss_step_stall_inv P st :
          sss_step_stall P st
(* Goal: not (@eq (prod nat data) (@pair nat data i x) (@pair nat data i (f x))) *)
(* Goal: and (@eq nat p q) (@ex nat (fun n : nat => and (C2 (@iter data f x n)) (spec (@iter data f x n) y))) *)
       -> { ii | (fst st,ii::nil) <sc P /\ sss_stall ii st }
        + { out_code (fst st) P }.
  Proof.
(* Goal: forall _ : sss_steps P (S k) st1 st3, @ex (prod nat data) (fun st2 : prod nat data => and (sss_step P st1 st2) (sss_steps P k st2 st3)) *)
    intros H.
    destruct (in_out_code_dec (fst st) P) as [ H1 | H1 ].
    2: tauto.
    destruct P as (iP,cP).
    destruct st as (j,d).
(* Goal: forall _ : sss_steps (@pair nat (list instr) j cj) k st1 (@pair nat data n d), @ex nat (fun q : nat => and (@eq nat k (Init.Nat.add p q)) (sss_steps (@pair nat (list instr) j cj) q st2 (@pair nat data n d))) *)
    simpl in H1.
    destruct (@list_pick _ cP (j-iP)) as (ii & l & r & H2 & H3).
(* Goal: lt q k *)
(* Goal: @subcode instr P P *)
    omega.
    left; exists ii; simpl; split.
(* Goal: lt q k *)
(* Goal: @subcode instr P P *)
    exists l, r; split; auto; omega.
    intros st' H4.
    apply (H st'). 
    subst; apply in_sss_step; auto.
(* Goal: lt q k *)
(* Goal: @subcode instr P P *)
    simpl; omega.
  Qed.

  Fact sss_steps_stall k P st st' : 
         out_code (fst st) P
      -> P // st -[k]-> st' 
      -> k = 0 /\ st = st'.
  Proof.
(* Goal: forall (_ : @subcode instr (@pair nat (list instr) n1 c1) (@pair nat (list instr) n2 c2)) (_ : sss_step (@pair nat (list instr) n1 c1) st1 st2), sss_step (@pair nat (list instr) n2 c2) st1 st2 *)
    destruct P; simpl.
(* Goal: forall (_ : @out_code instr (@fst nat data st1) P) (_ : sss_steps P k st1 st2), @eq (prod nat data) st1 st2 *)
    intros H1 H2.
(* Goal: @eq (prod nat data) st1 st2 *)
    apply sss_steps_inv in H2.
(* Goal: and (@eq nat k O) (@eq (prod nat data) st st') *)
    destruct H2 as [ (? & ?) | (m & st2 & ? & H2 & _) ]; auto.
(* Goal: and (@eq nat k O) (@eq (prod nat data) st st') *)
    apply sss_out_step_stall in H2; try red; tauto.
  Qed.
  
  (** This is a critical lemma about the locality of computations
  
      If P is subcode of Q and a computation in Q starts in P and ends outside of P,
      then it is decomposed in a first computation in P ending outside of P
      and a second computation in Q 
      
    *)
  
  Lemma subcode_sss_steps_inv P Q k st1 st3 :
       P <sc Q
    -> in_code  (fst st1) P
    -> out_code (fst st3) P
    -> Q // st1 -[k]-> st3
    -> exists k1 k2 st2, 
          P // st1 -[k1]-> st2
       /\ Q // st2 -[k2]-> st3
       /\ k = k1+k2 
       /\ out_code (fst st2) P.
  Proof.
(* Goal: forall (_ : @subcode instr P Q) (_ : @in_code instr (@fst nat data st1) P) (_ : @out_code instr (@fst nat data st3) P) (_ : sss_steps Q k st1 st3), @ex nat (fun k1 : nat => @ex nat (fun k2 : nat => @ex (prod nat data) (fun st2 : prod nat data => and (sss_steps P k1 st1 st2) (and (sss_steps Q k2 st2 st3) (and (@eq nat k (Init.Nat.add k1 k2)) (@out_code instr (@fst nat data st2) P)))))) *)
    intros H1 H2 H3 H4; revert H4 H2 H3.
(* Goal: forall (_ : sss_steps Q k st1 st3) (_ : @in_code instr (@fst nat data st1) P) (_ : @out_code instr (@fst nat data st3) P), @ex nat (fun k1 : nat => @ex nat (fun k2 : nat => @ex (prod nat data) (fun st2 : prod nat data => and (sss_steps P k1 st1 st2) (and (sss_steps Q k2 st2 st3) (and (@eq nat k (Init.Nat.add k1 k2)) (@out_code instr (@fst nat data st2) P)))))) *)
    induction 1 as [ st1 | k st1 st2 st3 H4 H5 IH5 ]; intros H2 H3.
    
(* Goal: sss_steps Q O st st *)
(* Goal: sss_steps Q (S k) st1 st3 *)
    exists 0, 0, st1; repeat split; auto; constructor.
    
(* Goal: @ex nat (fun k1 : nat => @ex nat (fun k2 : nat => @ex (prod nat data) (fun st2 : prod nat data => and (sss_steps P k1 st1 st2) (and (sss_steps Q k2 st2 st3) (and (@eq nat (S k) (Init.Nat.add k1 k2)) (@out_code instr (@fst nat data st2) P)))))) *)
    apply subcode_sss_step_inv with (1 := H1) in H4; auto.
(* Goal: @ex nat (fun k1 : nat => @ex nat (fun k2 : nat => @ex (prod nat data) (fun st2 : prod nat data => and (sss_steps P k1 st1 st2) (and (sss_steps Q k2 st2 st3) (and (@eq nat (S k) (Init.Nat.add k1 k2)) (@out_code instr (@fst nat data st2) P)))))) *)
    destruct (in_out_code_dec (fst st2) P) as [ H6 | H6 ].
    
(* Goal: @ex nat (fun k1 : nat => @ex nat (fun k2 : nat => @ex (prod nat data) (fun st2 : prod nat data => and (sss_steps P k1 st1 st2) (and (sss_steps Q k2 st2 st3) (and (@eq nat (S k) (Init.Nat.add k1 k2)) (@out_code instr (@fst nat data st2) P)))))) *)
(* Goal: @ex nat (fun k1 : nat => @ex nat (fun k2 : nat => @ex (prod nat data) (fun st2 : prod nat data => and (sss_steps P k1 st1 st2) (and (sss_steps Q k2 st2 st3) (and (@eq nat (S k) (Init.Nat.add k1 k2)) (@out_code instr (@fst nat data st2) P)))))) *)
    destruct (IH5 H6 H3) as (k1 & k2 & st & ? & ? & ? & ?).
(* Goal: @ex nat (fun k1 : nat => @ex nat (fun k2 : nat => @ex (prod nat data) (fun st2 : prod nat data => and (sss_steps P k1 st1 st2) (and (sss_steps Q k2 st2 st3) (and (@eq nat (S k) (Init.Nat.add k1 k2)) (@out_code instr (@fst nat data st2) P)))))) *)
(* Goal: @ex nat (fun k1 : nat => @ex nat (fun k2 : nat => @ex (prod nat data) (fun st2 : prod nat data => and (sss_steps P k1 st1 st2) (and (sss_steps Q k2 st2 st3) (and (@eq nat (S k) (Init.Nat.add k1 k2)) (@out_code instr (@fst nat data st2) P)))))) *)
    exists (S k1), k2, st; repeat split; auto.
(* Goal: sss_steps P (S k1) st1 st *)
(* Goal: @eq nat (S k) (Init.Nat.add (S k1) k2) *)
(* Goal: @ex nat (fun k1 : nat => @ex nat (fun k2 : nat => @ex (prod nat data) (fun st2 : prod nat data => and (sss_steps P k1 st1 st2) (and (sss_steps Q k2 st2 st3) (and (@eq nat (S k) (Init.Nat.add k1 k2)) (@out_code instr (@fst nat data st2) P)))))) *)
    constructor 2 with (1 := H4); auto.
(* Goal: lt q k *)
(* Goal: @subcode instr P P *)
    omega.
    
(* Goal: @ex nat (fun k1 : nat => @ex nat (fun k2 : nat => @ex (prod nat data) (fun st2 : prod nat data => and (sss_steps P k1 st1 st2) (and (sss_steps Q k2 st2 st3) (and (@eq nat (S k) (Init.Nat.add k1 k2)) (@out_code instr (@fst nat data st2) P)))))) *)
    exists 1, k, st2; repeat split; auto.
(* Goal: sss_steps P (S O) st1 st2 *)
    apply sss_steps_1; auto.
  Qed.

  Lemma subcode_sss_compute_inv P Q st1 st3 :
       P <sc Q
    -> out_code (fst st3) P
    -> Q // st1 ->> st3
    -> exists st2, 
          P // st1 ->> st2
       /\ Q // st2 ->> st3
       /\ out_code (fst st2) P.
  Proof.
(* Goal: forall (_ : @subcode instr P Q) (_ : @out_code instr (@fst nat data st3) P) (_ : sss_compute Q st1 st3), @ex (prod nat data) (fun st2 : prod nat data => and (sss_compute P st1 st2) (and (sss_compute Q st2 st3) (@out_code instr (@fst nat data st2) P))) *)
    intros H1 H3 (k & Hk).
(* Goal: @ex (prod nat data) (fun st2 : prod nat data => and (sss_compute P st1 st2) (and (sss_compute Q st2 st3) (@out_code instr (@fst nat data st2) P))) *)
    destruct (in_out_code_dec (fst st1) P) as [ H2 | H2 ].
    + apply subcode_sss_steps_inv with (1 := H1) in Hk; auto.
(* Goal: @ex (prod nat data) (fun st2 : prod nat data => and (sss_compute P st1 st2) (and (sss_compute Q st2 st3) (@out_code instr (@fst nat data st2) P))) *)
      destruct Hk as (k1 & k2 & st2 & H4 & H5 & H6 & H7).
(* Goal: @ex (prod nat data) (fun st2 : prod nat data => and (sss_compute P st1 st2) (and (sss_compute Q st2 st3) (@out_code instr (@fst nat data st2) P))) *)
      exists st2; repeat split; auto; red; firstorder.
    + exists st1; repeat split; auto.
(* Goal: sss_steps Q O st st *)
(* Goal: sss_steps Q (S k) st1 st3 *)
      * exists 0; constructor.
      * red; firstorder.
  Qed.

  (* Inversion lemma *)

  Fact subcode_sss_step_inv_1 P i st1 st2 : (fst st1,i::nil) <sc P -> P // st1 :1> st2 -> i // st1 -1> st2.
  Proof.
    revert P st1; intros (j,cj) (n,d) H1 H2.
    apply subcode_sss_step_inv with (1 := H1) in H2.
(* Goal: lt q k *)
(* Goal: @subcode instr P P *)
    2: simpl; omega.
    destruct H2 as (q & l & ii & r & d1 & H2 & H3 & H4).
    inversion H3; subst n d1; auto.
    eq goal H4; f_equal.
    inversion H2.
    destruct l as [ | ? [ | ] ]; try discriminate.
    inversion H5; subst; auto.
  Qed.

  (* Starting a computation in subcode ending outside of it
     can be cut in half *)

  Fact subcode_sss_subcode_inv P Q p k st1 st2 st3 :
           out_code (fst st3) P 
        -> P <sc Q
        -> P // st1 -[p]-> st2
        -> Q // st1 -[k]-> st3
        -> exists q, k = p+q /\ Q // st2 -[q]-> st3.
  Proof.
(* Goal: forall (_ : @out_code instr (@fst nat data st3) P) (_ : @subcode instr P Q) (_ : sss_steps P p st1 st2) (_ : sss_steps Q k st1 st3), @ex nat (fun q : nat => and (@eq nat k (Init.Nat.add p q)) (sss_steps Q q st2 st3)) *)
    revert P Q st3; intros P (j,cj) (n,d) H1 H2 H3.
(* Goal: forall _ : sss_steps (@pair nat (list instr) j cj) k st1 (@pair nat data n d), @ex nat (fun q : nat => and (@eq nat k (Init.Nat.add p q)) (sss_steps (@pair nat (list instr) j cj) q st2 (@pair nat data n d))) *)
    simpl in H1.
(* Goal: forall _ : sss_steps (@pair nat (list instr) j cj) k st1 (@pair nat data n d), @ex nat (fun q : nat => and (@eq nat k (Init.Nat.add p q)) (sss_steps (@pair nat (list instr) j cj) q st2 (@pair nat data n d))) *)
    revert k.
    induction H3 as [ st | p st1 st2 st3 H4 H5 IH5 ];
      intros k Hk.
(* Goal: @ex nat (fun q : nat => and (@eq nat k (Init.Nat.add O q)) (sss_steps (@pair nat (list instr) j cj) q st (@pair nat data n d))) *)
(* Goal: @ex nat (fun q : nat => and (@eq nat k (Init.Nat.add (S p) q)) (sss_steps (@pair nat (list instr) j cj) q st3 (@pair nat data n d))) *)
    exists k; auto.
(* Goal: @ex nat (fun q : nat => and (@eq nat k (Init.Nat.add (S p) q)) (sss_steps (@pair nat (list instr) j cj) q st3 (@pair nat data n d))) *)
    apply sss_steps_inv in Hk.
(* Goal: @ex nat (fun q : nat => and (@eq nat k (Init.Nat.add (S p) q)) (sss_steps (@pair nat (list instr) j cj) q st3 (@pair nat data n d))) *)
    destruct Hk as [ (? & Hk) | (m & st4 & ? & Hk & H3) ].
(* Goal: lt q k *)
(* Goal: @subcode instr P P *)
    1: subst st1; apply sss_step_in_code in H4; simpl in H4; omega.
(* Goal: @ex nat (fun q : nat => and (@eq nat k (Init.Nat.add (S p) q)) (sss_steps (@pair nat (list instr) j cj) q st3 (@pair nat data n d))) *)
    apply subcode_sss_step with (1 := H2) in H4.
(* Goal: @ex nat (fun q : nat => and (@eq nat k (Init.Nat.add (S p) q)) (sss_steps (@pair nat (list instr) j cj) q st3 (@pair nat data n d))) *)
    rewrite (sss_step_fun Hk H4) in H3.
(* Goal: @ex nat (fun q : nat => and (@eq nat k (Init.Nat.add (S p) q)) (sss_steps (@pair nat (list instr) j cj) q st3 (@pair nat data n d))) *)
    apply IH5 in H3; auto.
(* Goal: @ex nat (fun q : nat => and (@eq nat k (Init.Nat.add (S p) q)) (sss_steps (@pair nat (list instr) j cj) q st3 (@pair nat data n d))) *)
    destruct H3 as (q & ? & H3).
(* Goal: lt q k *)
(* Goal: @subcode instr P P *)
    exists q; split; auto; omega.
  Qed.

  Fact subcode_sss_terminates_inv P Q st st1 :
           Q // st ↓
        -> P <sc Q
        -> P // st ~~> st1
        -> Q // st1 ↓.
  Proof.
(* Goal: forall (_ : sss_terminates Q st) (_ : @subcode instr P Q) (_ : sss_output P st st1), sss_terminates Q st1 *)
    intros (st3 & (k & H1) & H2) H3 ((p & H4) & H5).
    destruct subcode_sss_subcode_inv with (2 := H3) (3 := H4) (4 := H1)
      as (q & _ & H6).
(* Goal: @out_code instr (@fst nat data st3) P *)
(* Goal: sss_terminates Q st1 *)
    1: revert H2; apply subcode_out_code; auto.
(* Goal: sss_terminates Q st1 *)
    exists st3; split; auto; exists q; auto.
  Qed.

  Fact subcode_sss_progress_inv P Q p st1 st2 st3 :
           out_code (fst st3) P 
        -> P <sc Q
        -> P // st1 -+> st2
        -> Q // st1 -[p]-> st3
        -> exists q, q < p /\ Q // st2 -[q]-> st3.
  Proof.
(* Goal: forall (_ : @out_code instr (@fst nat data st3) P) (_ : @subcode instr P Q) (_ : sss_progress P st1 st2) (_ : sss_steps Q p st1 st3), @ex nat (fun q : nat => and (lt q p) (sss_steps Q q st2 st3)) *)
    intros H1 H2 (k & ? & H3) H4.
(* Goal: @ex nat (fun q : nat => and (lt q k) (sss_steps P q st2 st3)) *)
    apply subcode_sss_subcode_inv with (3 := H3) in H4; auto.
(* Goal: lt q k *)
(* Goal: @subcode instr P P *)
    destruct H4 as (q & ? & ?); exists q; split; auto; omega.
  Qed.

  Section sss_terminates_ind.

    Variable (P : code) (R : state -> Prop).

    Hypothesis (HR0 : forall st, out_code (fst st) P -> R st)
               (HR1 : forall st1, (forall Q st2, Q <sc P -> Q // st1 -+> st2 -> P // st2 ↓ -> R st2) -> R st1).

    Theorem sss_terminates_ind st : P // st ↓ -> R st.
    Proof.
(* Goal: forall _ : sss_terminates P st, R st *)
      intros (st2 & (k & H1) & H2); revert st st2 H1 H2.
(* Goal: forall (st1 : prod nat data) (_ : sss_steps P k st1 st3), R st1 st3 *)
      induction k as [ k IH ] using (well_founded_induction_type lt_wf).
(* Goal: forall (st st2 : prod nat data) (_ : sss_steps P k st st2) (_ : @out_code instr (@fst nat data st2) P), R st *)
      intros st1 st2 H1 H2.
(* Goal: R st1 st3 *)
      destruct k as [ | k ].
      + apply sss_steps_0_inv in H1.
(* Goal: R st1 *)
        subst; apply HR0; auto.
      + apply HR1.
(* Goal: forall (Q : subcode.code instr) (st2 : prod nat data) (_ : @subcode instr Q P) (_ : sss_progress Q st1 st2) (_ : sss_terminates P st2), R st2 *)
        intros Q st2' HQ H5 (st3 & H6 & H7).
(* Goal: R st2' *)
        apply subcode_sss_progress_inv with (3 := H5) in H1; auto.
(* Goal: R st2' *)
(* Goal: @out_code instr (@fst nat data st2) Q *)
        destruct H1 as (q & G1 & G2).
(* Goal: R st2' *)
(* Goal: @out_code instr (@fst nat data st2) Q *)
        apply IH with (2 := G2); auto.
(* Goal: @out_code instr (@fst nat data st') P *)
        revert H2; apply subcode_out_code; auto.
    Qed.

  End sss_terminates_ind. 
 
  Section sss_compute_max_ind.

    Variable (P : code) (R : state -> state -> Prop).

    Hypothesis (HQ0 : forall st, sss_step_stall P st -> R st st)
               (HQ1 : forall st1 st3, (forall Q st2, Q <sc P -> Q // st1 -+> st2 -> P // st2 -]] st3 -> R st2 st3) -> R st1 st3).

    Theorem sss_compute_max_ind st1 st3 : P // st1 -]] st3 -> R st1 st3.
    Proof.
(* Goal: forall _ : sss_compute_max P st1 st3, R st1 st3 *)
      intros ((k & H1) & H2); revert st1 H1.
(* Goal: forall (st1 : prod nat data) (_ : sss_steps P k st1 st3), R st1 st3 *)
      induction k as [ k IH ] using (well_founded_induction_type lt_wf).
(* Goal: forall (st1 : prod nat data) (_ : sss_steps P k st1 st3), R st1 st3 *)
      intros st1 H1.
(* Goal: R st1 st3 *)
      destruct k as [ | k ].
(* Goal: R st1 st3 *)
(* Goal: R st1 st3 *)
      apply sss_steps_0_inv in H1.
(* Goal: R st1 st3 *)
(* Goal: R st1 st3 *)
      subst; apply HQ0; auto.
(* Goal: R st1 st3 *)
      apply HQ1.
(* Goal: forall (Q : subcode.code instr) (st2 : prod nat data) (_ : @subcode instr Q P) (_ : sss_progress Q st1 st2) (_ : sss_compute_max P st2 st3), R st2 st3 *)
      intros Q st2' HQ H5 ((q & H6) & _).
(* Goal: R st2' st3 *)
      apply subcode_sss_progress with (1 := HQ) in H5.
(* Goal: R st2' st3 *)
      destruct H5 as (l & Hl & H5).
(* Goal: R st2' st3 *)
      generalize (sss_steps_trans H5 H6); intro H7.
(* Goal: R st2' st3 *)
      generalize (sss_steps_stall_fun H2 H1 H7); intros H8.
(* Goal: lt q k *)
(* Goal: @subcode instr P P *)
      apply IH with q; auto; omega.
    Qed.

  End sss_compute_max_ind. 
 
  Fact sss_compute_inv P st1 st2 st3 :
             out_code (fst st3) P
          -> P // st1 ->> st2
          -> P // st1 ->> st3
          -> P // st2 ->> st3.
  Proof.
(* Goal: forall (_ : @out_code instr (@fst nat data st3) P) (_ : sss_compute P st1 st2) (_ : sss_compute P st1 st3), sss_compute P st2 st3 *)
    intros H2 (p & H3) (k & H4).
(* Goal: @ex nat (fun q : nat => and (lt q k) (sss_steps P q st2 st3)) *)
    apply subcode_sss_subcode_inv with (3 := H3) in H4; auto.
(* Goal: sss_compute P st2 st3 *)
(* Goal: @subcode instr P P *)
    destruct H4 as (q & _ & ?); exists q; auto.
(* Goal: @subcode instr P P *)
(* Goal: @eq (prod nat data) st2 st3 *)
    apply subcode_refl.
  Qed.

  Fact sss_compute_step_out_inv P k st1 st2 st3 :
           st1 <> st2
        -> out_code (fst st3) P
        -> P // st1 ->> st2
        -> P // st1 -[k]-> st3
        -> exists q, q < k /\ P // st2 -[q]-> st3.
  Proof.
(* Goal: forall (_ : not (@eq (prod nat data) st1 st2)) (_ : @out_code instr (@fst nat data st3) P) (_ : sss_compute P st1 st2) (_ : sss_steps P k st1 st3), @ex nat (fun q : nat => and (lt q k) (sss_steps P q st2 st3)) *)
    intros H1 H2 (p & H3) H4.
(* Goal: @ex nat (fun q : nat => and (lt q k) (sss_steps P q st2 st3)) *)
    apply subcode_sss_subcode_inv with (3 := H3) in H4; auto.
(* Goal: @ex nat (fun q : nat => and (lt q k) (sss_steps P q st2 st3)) *)
(* Goal: @subcode instr P P *)
    destruct H4 as (q & H4 & H5).
(* Goal: @ex nat (fun q : nat => and (lt q k) (sss_steps Q q st2 st3)) *)
    exists q; split; auto.
(* Goal: lt q k *)
(* Goal: @subcode instr P P *)
    destruct p.   
(* Goal: lt q k *)
(* Goal: lt q k *)
(* Goal: @subcode instr P P *)
    apply sss_steps_0_inv in H3.
(* Goal: lt q k *)
(* Goal: lt q k *)
(* Goal: @subcode instr P P *)
    destruct H1; auto.
(* Goal: lt q k *)
(* Goal: @subcode instr P P *)
    omega.
(* Goal: @subcode instr P P *)
(* Goal: @eq (prod nat data) st2 st3 *)
    apply subcode_refl.
  Qed.
  
  Fact subcode_sss_subcode_compute_inv P Q k st1 st2 st3 :
           in_code (fst st1) P
        -> out_code (fst st2) P
        -> out_code (fst st3) P 
        -> P <sc Q
        -> P // st1 ->> st2
        -> Q // st1 -[k]-> st3
        -> exists q, q < k /\ Q // st2 -[q]-> st3.
  Proof.
(* Goal: forall (_ : @in_code instr (@fst nat data st1) P) (_ : @out_code instr (@fst nat data st2) P) (_ : @out_code instr (@fst nat data st3) P) (_ : @subcode instr P Q) (_ : sss_compute P st1 st2) (_ : sss_steps Q k st1 st3), @ex nat (fun q : nat => and (lt q k) (sss_steps Q q st2 st3)) *)
    intros H H0 H1 H2 (p & H3) H4.
(* Goal: @ex nat (fun q : nat => and (lt q k) (sss_steps Q q st2 st3)) *)
    apply subcode_sss_subcode_inv with (2 := H2) (3 := H3) in H4; auto.
(* Goal: @ex nat (fun q : nat => and (lt q k) (sss_steps Q q st2 st3)) *)
    destruct H4 as (q & Hq & H4).
(* Goal: @ex nat (fun q : nat => and (lt q k) (sss_steps Q q st2 st3)) *)
    exists q; split; auto.
(* Goal: lt q k *)
(* Goal: @subcode instr P P *)
    destruct p; try omega.
(* Goal: lt q k *)
    apply sss_steps_0_inv in H3; subst st2.
(* Goal: lt q k *)
(* Goal: @subcode instr P P *)
    red in H, H0; omega.
  Qed.

  Fact subcode_sss_steps_inv_1 P i k st1 st2 st3 :
        st1 <> st3
     -> i // st1 -1> st2
     -> (fst st1,i::nil) <sc P
     -> P // st1 -[k]-> st3
     -> exists k', k = S k' /\ P // st2 -[k']-> st3.
  Proof.
(* Goal: forall (_ : @out_code instr (@fst nat data st2) P) (_ : @out_code instr (@fst nat data st3) P) (_ : sss_compute P st1 st2) (_ : sss_compute P st1 st3), @eq (prod nat data) st2 st3 *)
    intros H1 H2 H3 H4.
(* Goal: @ex nat (fun k' : nat => and (@eq nat k (S k')) (sss_steps P k' st2 st3)) *)
    apply sss_steps_inv in H4.
(* Goal: @ex nat (fun k' : nat => and (@eq nat k (S k')) (sss_steps P k' st2 st3)) *)
    destruct H4 as [ (_ & H4) | (k' & st & ? & H4 & ?) ].
(* Goal: @ex nat (fun k' : nat => and (@eq nat k (S k')) (sss_steps P k' st2 st3)) *)
(* Goal: @ex nat (fun k' : nat => and (@eq nat k (S k')) (sss_steps P k' st2 st3)) *)
    contradict H1; auto.
(* Goal: @ex nat (fun k' : nat => and (@eq nat k (S k')) (sss_steps P k' st2 st3)) *)
    exists k'; split; auto.
(* Goal: sss_steps P k' st2 st3 *)
    apply subcode_sss_step_inv_1 with (1 := H3) in H4.
(* Goal: sss_steps P k' st2 st3 *)
    rewrite (sss_fun H2 H4); auto.
  Qed.
  
  Fact subcode_sss_steps_stop P i k st1 st2 : 
            (forall st, ~ i // st1 -1> st)
        ->  (fst st1,i::nil) <sc P
        ->  P // st1 -[k]-> st2 -> k = 0 /\ st1 = st2.
  Proof.
(* Goal: forall (_ : forall st : prod nat data, not (one_step i st1 st)) (_ : @subcode instr (@pair nat (list instr) (@fst nat data st1) (@cons instr i (@nil instr))) P) (_ : sss_steps P k st1 st2), and (@eq nat k O) (@eq (prod nat data) st1 st2) *)
    intros H1 H2 H3.
(* Goal: and (@eq nat k O) (@eq (prod nat data) st1 st2) *)
    apply sss_steps_inv in H3.
(* Goal: and (@eq nat k O) (@eq (prod nat data) st1 st2) *)
    destruct H3 as [ | (k' & st & ? & H3 & H4) ]; auto; exfalso.
(* Goal: False *)
    apply (H1 st), subcode_sss_step_inv_1 with (1 := H2); auto.
  Qed.
  
  Fact sss_steps_stop P k st1 st2 :
             out_code (fst st1) P
          -> P // st1 -[k]-> st2
          -> st1 = st2.
  Proof.
(* Goal: forall (_ : @out_code instr (@fst nat data st1) P) (_ : sss_steps P k st1 st2), @eq (prod nat data) st1 st2 *)
    intros H1 H2.
(* Goal: @eq (prod nat data) st1 st2 *)
    apply sss_steps_inv in H2.
(* Goal: @eq (prod nat data) st1 st2 *)
    destruct H2 as [ [ _ ? ] | (k' & st3 & H2 & H3 & H4) ]; auto.
(* Goal: @eq (prod nat data) st1 st2 *)
    destruct (sss_out_step_stall H1 H3).
  Qed.

  Fact sss_compute_stop P st1 st2 :
             out_code (fst st1) P
          -> P // st1 ->> st2
          -> st1 = st2.
  Proof.
(* Goal: forall (_ : @out_code instr (@fst nat data st1) P) (_ : sss_compute P st1 st2), @eq (prod nat data) st1 st2 *)
    intros H1 (k & H2); revert H2; apply sss_steps_stop; auto.
  Qed.
  
  Fact sss_compute_fun P st1 st2 st3 :
             out_code (fst st2) P
          -> out_code (fst st3) P 
          -> P // st1 ->> st2
          -> P // st1 ->> st3 
          -> st2 = st3.
  Proof.
(* Goal: forall (_ : @out_code instr (@fst nat data st2) P) (_ : @out_code instr (@fst nat data st3) P) (_ : sss_compute P st1 st2) (_ : sss_compute P st1 st3), @eq (prod nat data) st2 st3 *)
    intros H1 H2 H3 H4.
(* Goal: @eq (prod nat data) st2 st3 *)
    destruct (in_out_code_dec (fst st1) P) as [ H5 | H5 ].
(* Goal: @eq (prod nat data) st2 st3 *)
(* Goal: @eq (prod nat data) st2 st3 *)
    destruct H4 as (k & H4).
(* Goal: @eq (prod nat data) st2 st3 *)
(* Goal: @eq (prod nat data) st2 st3 *)
    apply subcode_sss_subcode_compute_inv with (5 := H3) in H4; auto.
(* Goal: @eq (prod nat data) st2 st3 *)
(* Goal: @subcode instr P P *)
(* Goal: @eq (prod nat data) st2 st3 *)
    destruct H4 as (q & _ & H4).
(* Goal: @eq (prod nat data) st2 st3 *)
(* Goal: @subcode instr P P *)
(* Goal: @eq (prod nat data) st2 st3 *)
    apply sss_steps_stop in H4; auto.
(* Goal: @subcode instr P P *)
(* Goal: @eq (prod nat data) st2 st3 *)
    apply subcode_refl.
(* Goal: @eq (prod nat data) st2 st3 *)
    apply sss_compute_stop in H3; auto.
(* Goal: @eq (prod nat data) st2 st3 *)
    apply sss_compute_stop in H4; auto.
(* Goal: @eq (prod nat data) st2 st3 *)
    subst; auto.
  Qed.

  Fact sss_output_fun P st st1 st2 : P // st ~~> st1 -> P // st ~~> st2 -> st1 = st2.
  Proof.
(* Goal: forall (_ : sss_output P st st1) (_ : sss_output P st st2), @eq (prod nat data) st1 st2 *)
    intros (H1 & H2) (H3 & H4); revert H2 H4 H1 H3; apply sss_compute_fun.
  Qed.

  Fact subcode_sss_terminates P Q st : P <sc Q -> Q // st ↓ -> P // st ↓.
  Proof.
(* Goal: forall (_ : @subcode instr P Q) (_ : sss_terminates Q st), sss_terminates P st *)
    intros H (st' & H1 & H2).
(* Goal: sss_terminates P st *)
    apply subcode_sss_compute_inv with (1 := H) in H1; auto.
    + destruct H1 as (st2 & H1 & H3 & H4).
(* Goal: sss_terminates P st *)
      exists st2; split; auto.
    + revert H2; apply subcode_out_code; auto.
  Qed.

  Section sss_loop.

    (* P contains a loop that modifies the data (in a way computable by f)
       when condition C1 is satisfied and otherwise stops somewhere outside
       of P when condition C2 is satisfied.

       Then P stops iff exists n, C2 (iter f x n) *)

    Variable (P : code) (pre : data -> Prop) (spec : data -> data -> Prop)
             (f : data -> data) (Hf : forall x, x <> f x)
             (C1 C2 : data -> Prop) (HC : forall x, pre x -> { C1 x } + { C2 x }) 
             (i : nat) (p : nat) (Hp : out_code p P)
             (HP1 : forall x, pre x -> C1 x -> P // (i,x) ->> (i,f x) /\ pre (f x))
             (HP2 : forall x, pre x -> C2 x -> exists y, P // (i,x) ->> (p,y) /\ spec x y).

    Theorem sss_loop_sound x : pre x 
                            -> (exists n, C2 (iter f x n)) 
                            -> exists n y, P // (i,x) ->> (p,y) /\ spec (iter f x n) y.
    Proof.
(* Goal: forall (_ : pre x) (_ : @ex nat (fun n : nat => C2 (@iter data f x n))), @ex nat (fun n : nat => @ex data (fun y : data => and (sss_compute P (@pair nat data i x) (@pair nat data p y)) (spec (@iter data f x n) y))) *)
      intros H (n & Hn); revert x H Hn.
(* Goal: forall (x : data) (_ : pre x) (_ : C2 (@iter data f x n)), @ex nat (fun n : nat => @ex data (fun y : data => and (sss_compute P (@pair nat data i x) (@pair nat data p y)) (spec (@iter data f x n) y))) *)
      induction n as [ | n IHn ]; intros x Hx Hn.
(* Goal: @ex nat (fun n : nat => @ex data (fun y : data => and (sss_compute P (@pair nat data i x) (@pair nat data p y)) (spec (@iter data f x n) y))) *)
(* Goal: @ex nat (fun n : nat => @ex data (fun y : data => and (sss_compute P (@pair nat data i x) (@pair nat data p y)) (spec (@iter data f x n) y))) *)
      simpl; exists 0; apply HP2; auto.
(* Goal: and (@eq nat p q) (@ex nat (fun n : nat => and (C2 (@iter data f x n)) (spec (@iter data f x n) y))) *)
      destruct (HC Hx) as [ H | H ]. 
(* Goal: @ex nat (fun n : nat => @ex data (fun y : data => and (sss_compute P (@pair nat data i x) (@pair nat data p y)) (spec (@iter data f x n) y))) *)
(* Goal: @ex nat (fun n : nat => @ex data (fun y : data => and (sss_compute P (@pair nat data i x) (@pair nat data p y)) (spec (@iter data f x n) y))) *)
      apply IHn in Hn.
(* Goal: @ex nat (fun n : nat => @ex data (fun y : data => and (sss_compute P (@pair nat data i x) (@pair nat data p y)) (spec (@iter data f x n) y))) *)
(* Goal: pre (f x) *)
(* Goal: @ex nat (fun n : nat => @ex data (fun y : data => and (sss_compute P (@pair nat data i x) (@pair nat data p y)) (spec (@iter data f x n) y))) *)
      destruct Hn as (m & y & H1 & H2).
(* Goal: @ex nat (fun n : nat => @ex data (fun y : data => and (sss_compute P (@pair nat data i x) (@pair nat data p y)) (spec (@iter data f x n) y))) *)
(* Goal: pre (f x) *)
(* Goal: @ex nat (fun n : nat => @ex data (fun y : data => and (sss_compute P (@pair nat data i x) (@pair nat data p y)) (spec (@iter data f x n) y))) *)
      exists (S m), y; split; auto.
(* Goal: forall _ : sss_compute Q st2 st3, sss_compute Q st1 st3 *)
      generalize H1; apply sss_compute_trans.
(* Goal: pre (f x) *)
(* Goal: @ex nat (fun n : nat => @ex data (fun y : data => and (sss_compute P (@pair nat data i x) (@pair nat data p y)) (spec (@iter data f x n) y))) *)
      apply HP1; auto.
(* Goal: pre (f x) *)
(* Goal: @ex nat (fun n : nat => @ex data (fun y : data => and (sss_compute P (@pair nat data i x) (@pair nat data p y)) (spec (@iter data f x n) y))) *)
      apply HP1; auto.
(* Goal: @ex nat (fun n : nat => @ex data (fun y : data => and (sss_compute P (@pair nat data i x) (@pair nat data p y)) (spec (@iter data f x n) y))) *)
      destruct (HP2 Hx) as (y & H1 & H2); auto.
(* Goal: @ex nat (fun n : nat => @ex data (fun y : data => and (sss_compute P (@pair nat data i x) (@pair nat data p y)) (spec (@iter data f x n) y))) *)
      exists 0, y; auto.
    Qed.

    Theorem sss_loop_complete x y q : pre x 
                                   -> out_code q P 
                                   -> P // (i,x) ->> (q,y) 
                                   -> p = q /\ exists n, C2 (iter f x n) /\ spec (iter f x n) y.
    Proof.
(* Goal: forall (_ : pre x) (_ : @out_code instr q P) (_ : sss_compute P (@pair nat data i x) (@pair nat data q y)), and (@eq nat p q) (@ex nat (fun n : nat => and (C2 (@iter data f x n)) (spec (@iter data f x n) y))) *)
      intros Hx Hq (k & Hk); revert x Hx y q Hq Hk.
(* Goal: forall (x : data) (_ : pre x) (y : data) (q : nat) (_ : @out_code instr q P) (_ : sss_steps P k (@pair nat data i x) (@pair nat data q y)), and (@eq nat p q) (@ex nat (fun n : nat => and (C2 (@iter data f x n)) (spec (@iter data f x n) y))) *)
      induction k as [ k IHk ] using (well_founded_induction lt_wf); intros x Hx y q Hq Hk.
(* Goal: and (@eq nat p q) (@ex nat (fun n : nat => and (C2 (@iter data f x n)) (spec (@iter data f x n) y))) *)
      destruct (HC Hx) as [ H | H ].
      * apply HP1 in H; auto; destruct H as [ H1 H2 ].
        destruct (@sss_compute_step_out_inv P k (i,x) (i,f x) (q,y))
          as (k' & H3 & H4); auto.
(* Goal: not (@eq (prod nat data) (@pair nat data i x) (@pair nat data i (f x))) *)
(* Goal: and (@eq nat p q) (@ex nat (fun n : nat => and (C2 (@iter data f x n)) (spec (@iter data f x n) y))) *)
        { inversion 1 as [ H3 ]; revert H3; apply Hf. } 
(* Goal: and (@eq nat p q) (@ex nat (fun n : nat => and (C2 (@iter data f x n)) (spec (@iter data f x n) y))) *)
        destruct IHk with (2 := H2) (4 := H4) as (E & n & Hn); auto.
(* Goal: and (@eq nat p q) (@ex nat (fun n : nat => and (C2 (@iter data f x n)) (spec (@iter data f x n) y))) *)
        split; auto; exists (S n); auto.
      * destruct HP2 with (2 := H) as (z & Hz & Hy); auto.
(* Goal: and (@eq nat p q) (@ex nat (fun n : nat => and (C2 (@iter data f x n)) (spec (@iter data f x n) y))) *)
        apply ex_intro with (x := k) in Hk.
(* Goal: and (@eq nat p q) (@ex nat (fun n : nat => and (C2 (@iter data f x n)) (spec (@iter data f x n) y))) *)
        generalize (@sss_compute_fun _ _ (p,z) (q,y) Hp Hq Hz Hk).
(* Goal: @eq (prod nat data) st2 st3 *)
        inversion 1; subst; auto.
(* Goal: and (@eq nat q q) (@ex nat (fun n : nat => and (C2 (@iter data f x n)) (spec (@iter data f x n) y))) *)
        split; auto.
(* Goal: @ex nat (fun n : nat => and (C2 (@iter data f x n)) (spec (@iter data f x n) y)) *)
        exists 0; simpl; auto.
    Qed.

  End sss_loop.

End Small_Step_Semantics.

(*
Notation " P '//' r ':1>' s " := (sss_step _ P r s)  (at level 70, no associativity).
Notation " P '//' r '-[' n ']->' s " := (sss_steps _ P n r s) (at level 70, no associativity).
Notation " P '//' r '->>' s " := (sss_compute _ P r s) (at level 70, no associativity).
*)


