Require Import List Arith Lia.

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

From Undecidability.MinskyMachines
  Require Import env mme_defs mme_utils.

From Undecidability.MuRec
  Require Import recalg.

Set Implicit Arguments.

Set Default Proof Using "Type".

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

Local Notation "P // s > t" := (sss_compute (mm_sss_env eq_nat_dec) P s t).
Local Notation "P // s -+> t" := (sss_progress (mm_sss_env eq_nat_dec) P s t).
Local Notation "P // s -[ k ] t" := (sss_steps (mm_sss_env eq_nat_dec) P k s t).
Local Notation "P // s ↓" := (sss_terminates (mm_sss_env eq_nat_dec ) P s).

Local Notation " e ⇢ x " := (@get_env _ _ e x).
Local Notation " e ⦃ x ⇠ v ⦄ " := (@set_env _ _ eq_nat_dec e x v).
Local Notation "x '⋈' y" := ( i : , xi = yi :> ) (at level 70, no associativity).

Local Notation "'⟦' f '⟧'" := (@ra_rel _ f) (at level 0).

Section ra_compiler.

  Ltac dest x y := destruct (eq_nat_dec x y) as [ | ]; [ subst x | ]; rew env.


  Definition ra_compiled n (f : recalg n) i p o m (P : list (mm_instr )) :=
        v e, ( i, m i ei = 0)
                 ( q, e⇢(pos2nat q+p) = vec_pos v q)
                 ( x, f v x
                    e', e' eox
                               (i,P) // (i,e) ->> (length P + i,e'))
                 ((i,P) // (i,e) x, f v x).

  Definition ra_compiler_spec n f i p o m := sig (@ra_compiled n f i p o m).

  Definition ra_compiler_stm n f :=
     i p o m, o < m
                  p o < n+p
                  n+p m
                  @ra_compiler_spec n f i p o m.

  Hint Resolve sss_progress_compute : core.

  Fact ra_compiler_cst c : ra_compiler_stm (ra_cst c).
  Proof.
    red; simpl; intros i p o m .
    exists (mm_set o m c i); intros v e _; split.
    2: exists c; cbv; auto.
    revert ; vec nil v; clear v.
    intros x E; simpl in E; subst x.
    rewrite mm_set_length.
    destruct mm_set_progress
      with (dst := o) (zero := m) (n := c) (i := i) (e := e)
      as (e' & & ); auto; try .
    exists e'; split; auto.
  Qed.


  Fact ra_compiler_zero : ra_compiler_stm ra_zero.
  Proof.
    red; simpl; intros i p o m .
    exists (mm_set o m 0 i); intros v e ; split.
    2: exists 0; cbv; auto.
    intros x; revert .
    vec split v with a; vec nil v; clear v.
    intros E; cbv in E; subst x.
    rewrite mm_set_length.
    destruct mm_set_progress
      with (dst := o) (zero := m) (n := 0) (i := i) (e := e)
      as (e' & & ); auto; try .
    exists e'; split; auto.
  Qed.


  Fact ra_compiler_succ : ra_compiler_stm ra_succ.
  Proof.
    red; simpl; intros i p o m .
    exists (mm_copy p o m (m+1) i INC o :: nil);
      intros v e ; split.
    2: exists (S (vec_head v)); cbv; auto.
    intros x; revert ; vec split v with a; vec nil v; clear v.
    intros H; simpl in H; subst x.
    specialize ( pos0); rewrite pos2nat_fst in ; simpl in .
    destruct mm_copy_progress
      with (src := p) (dst := o) (tmp := m) (zero := m+1) (i := i) (e := e)
      as (e' & & ); try ; try (apply ; ).
    exists (e'oS a); split.
    * intros j; dest j o; rewrite ; rew env.
    * rew length.
      apply sss_compute_trans with (9+i, e').
      - apply sss_progress_compute.
        revert ; apply subcode_sss_progress; auto.
      - mm env INC with o.
        mm env stop.
        rewrite , ; rew env.
  Qed.


  Fact ra_compiler_proj n q : ra_compiler_stm (@ra_proj n q).
  Proof.
    red; simpl; intros i p o m .
    exists (mm_copy (pos2nat q+p) o m (m+1) i);
      intros v e ; split.
    2: exists (vec_pos v q); cbv; auto.
    intros x E; simpl in E; subst x.
    destruct mm_copy_progress
      with (src := pos2nat q+p) (dst := o) (tmp := m) (zero := m+1) (i := i) (e := e)
      as (e' & & ); try ; try (apply ; );
        try (generalize (pos2nat_prop q); ).
    exists e'; split.
    * intros j; rewrite ; dest j o.
    * rew length; apply sss_progress_compute; auto.
  Qed.


  Section ra_compiler_comp.

    Variable (n : ).

    Local Fact ra_compiler_vec k (g : vec (recalg n) k) :
           ( p, ra_compiler_stm (vec_pos g p))
         i p o m,
                    o+k m
                  n+p o
                  { P : list (mm_instr ) |
       ( v w e, ( q, vec_pos g q v (vec_pos w q))
                    ( i, m i ei = 0)
                    ( j, e⇢(pos2nat j+p) = vec_pos v j)
                    e', ( j, o j < o+k e'j = ej)
                               ( q, e'⇢(pos2nat q+o) = vec_pos w q)
                               (i,P) // (i,e) ->> (length P + i,e'))
       ( v e, (i,P) // (i,e)
                    ( i, m i ei = 0)
                    ( q, e⇢(pos2nat q+p) = vec_pos v q)
                    ( q, x, vec_pos g q v x)) }.
    Proof.
      induction g as [ | k f g IHg ]; intros Hg i p o m .
      + exists nil; split.
        2: intros v e q; analyse pos q.
        intros v w e; vec nil w; clear w.
        intros _ .
        exists e; split; [ | split ]; auto.
        * intros q; analyse pos q.
        * simpl; mm env stop.
      + destruct (Hg pos0) with (i := i) (p := p) (o := o) (m := m)
          as (P & HP); try .
        destruct IHg with (i := length P+i) (p := p) (o := S o) (m := m)
          as (Q & & ); try .
        { intros q; apply (Hg (pos_nxt q)). }
        exists (PQ); split.
        * intros v w e; vec split w with a.
          intros .
          generalize ( pos0) ( q (pos_nxt q)); clear ; intros .
          simpl in , .
          destruct (proj1 (HP v e ) a) as ( & & ); auto.
          destruct ( v w ) as ( & & & ); auto.
          { intros j Hj; rewrite ; dest j o; . }
          { intros q; rewrite .
            assert (pos2nat q+p o); try rew env.
            generalize (pos2nat_prop q); . }
          exists ; split; [ | split ].
          - intros j Hj.
            rewrite , ; try .
            dest j o; .
          - intros q; analyse pos q; simpl.
            ++ rewrite pos2nat_fst, , ; try .
               simpl; rew env.
            ++ rewrite pos2nat_nxt, ; f_equal; .
          - apply sss_compute_trans with (length P+i,).
            ++ revert ; apply subcode_sss_compute; auto.
            ++ rew length.
               revert ; rewrite plus_assoc, (plus_comm _ (length _)).
               apply subcode_sss_compute.
               subcode_tac; rewrite app_nil_end; auto.
        * intros v e .
          assert ((i,P) // (i,e) ) as .
          { apply subcode_sss_terminates with (2 := ); auto. }
          destruct (proj2 (HP v _ )) with (1 := ) as (a & Ha); auto.
          simpl in Ha.
          destruct (proj1 (HP _ _ ) _ Ha) as ( & & ); auto.
          intros q; analyse pos q; simpl.
          1: exists a; auto.
          apply with .
          - assert ((i,PQ) // (length P+i,) ) as .
            { apply subcode_sss_terminates_inv
               with (2 := ) (P := (i,P)) ( := (length P+i,)); auto.
             * apply mm_sss_env_fun.
             * split; simpl; auto; . }
            destruct as (st & & ).
            assert ( (length P+i,Q) <sc (i,PQ) ) as .
            { subcode_tac; rewrite app_nil_end; auto. }
            destruct subcode_sss_compute_inv
              with (P := (length P+i,Q)) (3 := )
              as ( & & _ & ); auto.
            { revert ; apply subcode_out_code; auto. }
            exists ; split; auto.
          - intros j Hj; rewrite ; dest j o; .
          - clear q; intros q; rewrite .
            assert (pos2nat q+p o); try rew env.
            generalize (pos2nat_prop q); .
    Qed.


    Variable (k : ) (f : recalg k) (g : vec (recalg n) k)
             (Hf : ra_compiler_stm f)
             (Hg : q, ra_compiler_stm (vec_pos g q)).


    Fact ra_compiler_comp : ra_compiler_stm (ra_comp f g).
    Proof using Hf Hg.
      red; simpl; intros i p o m .
      destruct ra_compiler_vec with (1 := Hg) (i := i) (p := p) (o := m) (m := m+k)
        as (P & & ); auto.
      destruct Hf with (i := length P+i) (p := m) (o := o) (m := m+k)
        as (Q & HQ); try ; auto.
      exists (PQmm_multi_erase m (k+m) k (length P+length Q+i));
        intros v e ; split.
      + intros x; simpl; intros (w & & ).
        assert ( q, vec_pos g q v (vec_pos w q)) as .
        { intros q; generalize ( q); rewrite vec_pos_set; auto. }
        clear .
        destruct ( v w e) as ( & & & ); auto.
        { intros; apply ; . }
        destruct (HQ w ) as [ _ ]; auto.
        { intros j Hj; rewrite , ; . }
        destruct ( x) as ( & & ); auto.
        destruct mm_multi_erase_compute
          with (zero := k+m) (dst := m) (k := k) (i := length P+length Q+i) (e := )
          as ( & & & ); try ; auto.
        { rewrite , get_set_env_neq, , ; . }
        exists ; split.
        * intros j.
          destruct (interval_dec m (k+m) j) as [ H | H ].
          - rewrite , get_set_env_neq, ; .
          - rewrite , ; try ; dest j o.
            apply ; .
        * rew length.
          apply sss_compute_trans with (length P+i,).
          { revert ; apply subcode_sss_compute; auto. }
          apply sss_compute_trans with (length P+length Q+i,).
          { revert ; rewrite plus_assoc, (plus_comm _ (length _)).
            apply subcode_sss_compute; auto. }
          replace (length P+(length Q+2*k)+i)
            with (2*k+(length P+length Q+i)) by .
          revert ; apply subcode_sss_compute; auto.
    + intros .
      assert ((i,P) // (i,e) ) as .
      { revert ; apply subcode_sss_terminates; auto. }
      assert ( q, ex (vec_pos g q v)) as .
      { apply with (1 := ) (3 := ).
        intros; apply ; . }
      apply vec_reif in ; destruct as (w & Hw).
      destruct ( v w e) as ( & & & ); auto.
      { intros; apply ; . }
      destruct (HQ w ) as [ _ (x & Hx) ]; auto.
        { intros j Hj; rewrite , ; . }
      - apply subcode_sss_terminates
          with (Q := (i,PQmm_multi_erase m (k + m) k (length P+length Q+i))); auto.
        apply subcode_sss_terminates_inv with (2 := ) (P := (i,P)); auto.
        { apply mm_sss_env_fun. }
        split; simpl; auto; .
      - exists x, w; split; auto.
        intros q; rewrite vec_pos_set; auto.
    Qed.


  End ra_compiler_comp.

  Section ra_compiler_rec.

    Variables (n : ) (f : recalg n) (g : recalg (S (S n)))
              (Hf : ra_compiler_stm f)
              (Hg : ra_compiler_stm g).


    Variables (i p o m : )
              ( : o < m)
              ( : p o < S (n + p))
              ( : S (n + p) m).

    Notation v0 := (2+n+m).
    Notation zero := (3+n+m).
    Notation tmp := (4+n+m).

    Local Definition rec_Q1 :=
              mm_multi_copy tmp zero n (1+p) (2+m) i
            mm_copy p v0 tmp zero (9*n+i)
            mm_erase m zero (9+9*n+i).

    Notation Q1 := rec_Q1.

    Local Fact rec_Q1_length : length Q1 = 11+9*n.
    Proof using . unfold ; rew length; . Qed.

    Local Fact rec_F_full : ra_compiler_spec f (11+9*n+i) (2+m) o zero.
    Proof using Hf . apply Hf; . Qed.

    Notation F := (proj1_sig rec_F_full).
    Local Definition rec_HF1 x v e H1 H2 := proj1 (proj2_sig rec_F_full v e ) x.
    Local Definition rec_HF2 v e H1 H2 := proj2 (proj2_sig rec_F_full v e ).

    Local Fact rec_G_full : ra_compiler_spec g (21+length F+9*n+i) m o zero.
    Proof using Hg . apply Hg; . Qed.

    Notation G := (proj1_sig rec_G_full).
    Local Definition rec_HG1 x v e H1 H2 := proj1 (proj2_sig rec_G_full v e ) x.
    Local Definition rec_HG2 v e H1 H2 := proj2 (proj2_sig rec_G_full v e ).

    Local Definition rec_s2 := 11+length F+9*n+i.

    Notation s2 := rec_s2.

    Local Definition rec_Q2 :=
              DEC v0 (23+length F+length G+9*n+i)
           :: mm_copy o (1+m) tmp zero (12+length F+9*n+i)
            G
            INC m :: DEC zero rec_s2 :: nil.

    Notation Q2 := rec_Q2.

    Local Fact rec_Q2_progress_O e :
               ev0 = 0
             (s2,Q2) // (s2,e) -+> (length Q2+s2,e).
    Proof.
      intros .
      unfold .
      mm env DEC zero with v0 (23+length F+length G+9*n+i).
      mm env stop; f_equal; rew length.
      unfold ; .
    Qed.


    Local Fact rec_Q2_progress_S x y v e :
              ( j, zero j ej = 0)
            ( j, vec_pos v j = e⇢(pos2nat j+2+m))
            ev0 = S x
            g (em##eo##v) y
            e', ( j, j o j v0 j m j 1+m e'j = ej)
                       e'o = y
                       e'v0 = x
                       e'm = S (em)
                       e'⇢(1+m) = eo
                       (s2,Q2) // (s2,e) -+> (s2,e').
    Proof.
      generalize rec_Q1_length; intros Q1_length.
      intros .
      set ( := ev0x).
      destruct (@mm_copy_progress o (1+m) tmp zero)
        with (i := 12+length F+9*n+i) (e := )
        as ( & & ); try .
      1,2: unfold ; rewrite get_set_env_neq, ; .
      destruct rec_HG1 with (e := ) (3 := )
        as ( & & ).
      { intros j Hj; rewrite ; unfold .
        dest j (1+m); try .
        dest j (2+n+m); try . }
      { intros j.
        rewrite ; unfold .
        analyse pos j.
        * rewrite pos2nat_fst; simpl.
          do 2 (rewrite get_set_env_neq; try ).
        * rewrite pos2nat_nxt, pos2nat_fst; rew env.
          rewrite get_set_env_neq; auto; .
        * do 2 rewrite pos2nat_nxt.
          generalize (pos2nat_prop j); intro Hj.
          do 2 (rewrite get_set_env_neq; try ).
          simpl; rewrite ; f_equal; . }
      exists (mS(em)); msplit 5.
      * intros j ; rew env.
        rewrite ; rew env.
        rewrite ; unfold ; rew env.
      * rewrite get_set_env_neq, ; try ; rew env.
      * rewrite get_set_env_neq, ; try .
        rewrite get_set_env_neq, ; try .
        unfold ; rewrite get_set_env_neq; try .
        rew env.
      * rew env.
      * rewrite get_set_env_neq, ; try .
        rewrite get_set_env_neq, ; try .
        rew env; unfold .
        rewrite get_set_env_neq; .
      * unfold .
        mm env DEC S with v0 (23 + length F + length G + 9 * n + i) x.
        apply sss_compute_trans with (21+length F+9*n+i,).
        { apply sss_progress_compute.
          unfold , ; revert ; apply subcode_sss_progress; auto. }
        apply sss_compute_trans with (length G+(21+length F+9*n+i), ).
        { unfold , ; revert ; apply subcode_sss_compute; auto. }
        mm env INC with m.
        { unfold ; subcode_tac. }
        mm env DEC zero with zero s2.
        { unfold ; subcode_tac. }
        { rewrite get_set_env_neq; try .
          rewrite , get_set_env_neq; try .
          rewrite , get_set_env_neq; try .
          unfold ; rewrite get_set_env_neq; try .
          apply ; . }
        mm env stop; do 3 f_equal.
        rewrite , get_set_env_neq; try .
        rewrite , get_set_env_neq; try .
        unfold ; rewrite get_set_env_neq; .
    Qed.


    Local Fact rec_Q2_progress_S_inv x v e :
              ( j, zero j ej = 0)
            ( j, vec_pos v j = e⇢(pos2nat j+2+m))
            ev0 = S x
            (s2,Q2) // (s2,e)
            y, g (em##eo##v) y.
    Proof.
      intros ((s & e') & (k & ) & ).
      unfold fst in .
      assert ( : e1, ev0x⦄⦃1+m⇠(eo)⦄
                            (s2,Q2) // (s2,e) -+> (10+s2,)).
      { destruct mm_copy_progress
          with (src := o) (dst := 1+m) (tmp := tmp) (zero := zero)
               (i := 12+length F+9*n+i) (e := ev0x)
          as ( & & ); try .
        1,2: rewrite get_set_env_neq, ; .
        exists ; split.
        + intros j; rewrite ; auto.
          rewrite get_set_env_neq with (q := o); auto; .
        + unfold .
          mm env DEC S with v0 (23+length F+length G+9*n+i) x.
          replace (1+s2) with (12+length F+9*n+i) by (unfold ; ).
          replace (10+s2) with (9+(12+length F+9*n+i)) by (unfold ; ).
          apply sss_progress_compute.
          revert ; apply subcode_sss_progress; auto.
          unfold ; subcode_tac. }
      destruct as ( & & ).
      destruct subcode_sss_progress_inv with (4 := ) (5 := )
        as (k' & & ); auto.
      { apply mm_sss_env_fun. }
      { apply subcode_refl. }
      apply rec_HG2 with (e := ).
      * intros j Hj; rewrite , get_set_env_neq, get_set_env_neq; auto; .
      * intros j; rewrite ; analyse pos j.
        + rewrite pos2nat_fst; simpl.
          do 2 (rewrite get_set_env_neq; try ).
        + rewrite pos2nat_nxt, pos2nat_fst; rew env.
        + do 2 rewrite pos2nat_nxt; simpl.
          generalize (pos2nat_prop j); intros .
          do 2 (rewrite get_set_env_neq; try ).
          rewrite ; f_equal; .
      * apply subcode_sss_terminates with (Q := (s2,Q2)).
        + unfold , ; auto.
        + exists (s,e'); split; auto.
          exists k'; apply .
    Qed.


    Local Fact rec_Q2_compute_rec (v : vec n) e s k :
              ( j, zero j ej = 0)
            ( j, vec_pos v j = e⇢(pos2nat j+2+m))
            eo = s 0
            ev0 = k
            ( i, i < k g (i+(em)##s i##v) (s (S i)))
   e', ( j, j o j v0 j m j 1+m e'j = ej)
              e'o = s k
              e'v0 = 0
              e'm = (ev0)+(em)
              (s2,Q2) // (s2,e) -+> (length Q2+s2,e').
    Proof.
      revert e s; induction k as [ | k IHk ]; intros e s .
      + exists e; msplit 4; auto.
        * rewrite ; auto.
        * apply rec_Q2_progress_O; auto.
      + generalize ( 0); intros ; spec in ; try .
        rewrite in ; simpl in .
        destruct rec_Q2_progress_S with (3 := ) (4 := )
          as ( & & & & & & ); auto.
        destruct IHk with (s := i s (S i)) (e := )
          as ( & & & & & ); auto.
        * intros; rewrite , ; .
        * intros j; generalize (pos2nat_prop j); intro.
          rewrite , ; auto; .
        * intros j Hj.
          rewrite .
          replace (j+S(em)) with ((S j)+(em)) by .
          apply ; .
        * exists ; msplit 4; auto.
          - intros j ? ? ? ?; rewrite ; auto.
          - rewrite , , , ; .
          - apply sss_progress_trans with (1 := ); auto.
    Qed.


    Local Fact rec_Q2_compute_rev (v : vec n) e :
              ( j, zero j ej = 0)
            ( j, vec_pos v j = e⇢(pos2nat j+2+m))
            (s2,Q2) // (s2,e)
            s, s 0 = eo i, i < ev0 g (i+(em)##s i##v) (s (S i)).
    Proof.
      intros ((u & e') & (k & ) & ).
      unfold fst in .
      revert e e' .
      induction on k as IHk with measure k.
      intros e e' .
      case_eq (ev0).
      + intros ?; exists ( _ eo); split; auto; intros; .
      + intros x Hx.
        destruct rec_Q2_progress_S_inv
          with (1 := ) (2 := ) (3 := Hx)
          as (y & Hy).
        { exists (u,e'); split; auto; exists k; auto. }
        destruct rec_Q2_progress_S with (3 := Hx) (4 := Hy)
          as ( & & & & & & ); auto.
        destruct subcode_sss_progress_inv with (4 := ) (5 := )
          as (k' & & ); auto.
        { apply mm_sss_env_fun. }
        { apply subcode_refl. }
        apply IHk in ; auto.
        * destruct as (s & & ).
          exists ( i match i with 0 eo | S i s i end); split; auto.
          intros [ | j ] Hj; simpl.
          - rewrite , ; auto.
          - specialize ( j).
            rewrite in .
            replace (S (j+(em))) with (j+S(em)) by .
            apply ; .
        * intros j Hj; rewrite , ; .
        * intros j; rewrite , ; try .
          generalize (pos2nat_prop j); intro; .
    Qed.


    Local Fact rec_Q2_length : length Q2 = 12+length G.
    Proof. unfold ; rew length; ring. Qed.

    Local Definition rec_Q3 := mm_multi_erase m zero (2+n) (23+length F+length G+9*n+i).

    Notation Q3 := rec_Q3.

    Local Fact rec_Q3_length : length Q3 = 4+2*n.
    Proof. unfold ; rew length; ring. Qed.

    Local Fact rec_Q1_progress e :
                ( j, zero j ej = 0)
   e', ( j, j < n e'⇢(j+2+m) = e⇢(j+1+p))
              e'v0 = ep
              e'm = 0
              ( j, j m 2+m j v0 e'j = ej)
              (i,Q1) // (i,e) -+> (length Q1+i,e').
    Proof using .
      intros .
      destruct (@mm_multi_copy_compute tmp zero n (1+p) (2+m))
        with (i := i) (e := e)
        as ( & & & ); try .
      1,2: apply ; .
      destruct (@mm_copy_progress p v0 tmp zero)
        with (i := 9*n+i) (e := )
        as ( & & ); try .
      1,2: rewrite , ; .
      destruct (@mm_erase_progress m zero)
        with (i := 9+9*n+i) (e := )
        as ( & & ); try .
      1: rewrite , get_set_env_neq, , ; .
      exists ; msplit 4.
      * intros j Hj.
        rewrite , get_set_env_neq,
                , get_set_env_neq,
                 plus_assoc, ; try .
        f_equal; .
      * rewrite , get_set_env_neq, ; rew env; try .
        rewrite ; .
      * rewrite ; rew env.
      * intros j .
        rewrite ; rew env.
        rewrite , get_set_env_neq, ; .
      * rewrite rec_Q1_length; unfold .
        apply sss_compute_progress_trans with (9*n+i,).
        { revert ; apply subcode_sss_compute; auto. }
        apply sss_progress_trans with (9+(9*n+i), ).
        { revert ; apply subcode_sss_progress; auto. }
        { rewrite plus_assoc; revert .
          apply subcode_sss_progress; auto. }
    Qed.


    Notation Q4 := (Q1FQ2Q3).

    Local Fact rec_Q4_progress (v : vec (S n)) x e :
                 ( j, m j ej = 0)
               ( j, vec_pos v j = e⇢(pos2nat j+p))
               s_rec f g v x
   e', ( j, j o e'j = ej)
               e'o = x
               (i,Q4) // (i,e) -+> (length Q4+i,e').
    Proof.
      generalize rec_Q1_length rec_Q2_length rec_Q3_length.
      intros Q1_length Q2_length Q3_length.
      vec split v with k.
      intros .
      rewrite s_rec_eq in .
      destruct as (s & & & ); simpl vec_head in *; simpl vec_tail in *.
      generalize ( pos0); rewrite pos2nat_fst; intros ; simpl in .
      generalize ( j (pos_nxt j)); clear ; intros ; simpl in .
      destruct rec_Q1_progress with (e := e) as ( & & & & & ).
      { intros; apply ; . }
      assert ( j, pos2nat j + (2 + m) = vec_pos v j) as .
      { intros j; rewrite , pos2nat_nxt.
        replace (S (pos2nat j)+p) with (pos2nat j+1+p) by .
        generalize (pos2nat_prop j); intros H.
        rewrite ; auto; f_equal; . }
      destruct rec_HF1 with (3 := ) (e := ) as ( & & ); auto.
      { intros j Hj; rewrite , ; . }
      destruct rec_Q2_compute_rec with (e := ) (v := v) (s := s) (k := k)
        as ( & & & & _ & ).
      { intros j Hj; rewrite , get_set_env_neq, , ; . }
      { intros j; rewrite , , get_set_env_neq; try .
        f_equal; . }
      { rewrite ; rew env. }
      { rewrite , get_set_env_neq, ; . }
      { intros j Hj.
        rewrite , get_set_env_neq, , plus_comm; try .
        simpl; apply ; auto. }
      destruct mm_multi_erase_compute
        with (zero := zero) (dst := m) (k := 2+n) (e := )
             (i := 23+length F+length G+9*n+i)
        as ( & & & ); try .
      { rewrite , , get_set_env_neq, , ; . }
      exists ; msplit 2.
      * intros j Hj.
        dest j (2+n+m).
        { rewrite , , ; . }
        destruct (interval_dec m v0 j).
        - rewrite , ; .
        - rewrite , , , get_set_env_neq, ; try .
      * rewrite ; try .
      * rew length.
        apply sss_progress_trans with (length Q1+i,).
        { revert ; apply subcode_sss_progress; auto. }
        apply sss_compute_progress_trans with (length F+length Q1+i,).
        { rewrite Q1_length.
          replace (length F+(11+9*n)+i) with (length F+(11+9*n+i)) by .
          revert ; apply subcode_sss_compute; auto. }
        apply sss_progress_compute_trans with (length Q2+s2,).
        { replace (length F+length Q1+i) with s2.
          revert ; apply subcode_sss_progress; unfold ; auto.
          unfold ; rewrite Q1_length; . }
        { replace (length Q2+s2) with (23+length F+length G+9*n+i).
          replace (length Q1+(length F+(length Q2+length Q3))+i)
             with (2*(2+n)+(23+length F+length G+9*n+i)).
          revert ; apply subcode_sss_compute; auto.
          unfold ; subcode_tac; rewrite app_nil_end; auto.
          rewrite Q1_length, Q2_length, Q3_length; .
          rewrite Q2_length; unfold ; . }
    Qed.


    Local Fact rec_Q4_compute_rev (v : vec (S n)) e :
                 ( j, m j ej = 0)
               ( j, vec_pos v j = e⇢(pos2nat j+p))
               (i,Q4) // (i,e)
               x, s_rec f g v x.
    Proof.
      generalize rec_Q1_length rec_Q2_length rec_Q3_length.
      intros Q1_length Q2_length Q3_length.
      vec split v with k.
      intros .
      destruct rec_Q1_progress with (e := e)
        as ( & & & & & ); auto.
      { intros; apply ; . }
      generalize ; intros .
      apply subcode_sss_terminates_inv
        with (P := (i,Q1)) ( := (length Q1+i,)) in ; auto.
      2: apply mm_sss_env_fun.
      2: { split.
           + apply sss_progress_compute; auto.
           + unfold out_code, code_end, fst, snd; . }
      assert ( : q : pos n, pos2nat q + (2 + m) = vec_pos v q).
      { intros j; specialize ( (pos_nxt j)); simpl in .
        rewrite , pos2nat_nxt, plus_assoc, .
        + f_equal; .
        + apply pos2nat_prop. }
      destruct rec_HF2 with (v := v) (e := )
        as (x & Hx); auto.
      { intros j Hj; rewrite , ; . }
      { rewrite Q1_length in .
        revert ; apply subcode_sss_terminates; auto. }
      destruct rec_HF1 with (3 := Hx) (e := )
        as ( & & ); auto.
      { intros j Hj; rewrite , ; . }
      destruct rec_Q2_compute_rev with (v := v) (e := )
        as (s & & ).
      { intros j Hj; rewrite , get_set_env_neq, , ; . }
      { intros j; rewrite , , get_set_env_neq.
        + f_equal; .
        + . }
      { apply subcode_sss_terminates with (i, Q4).
        1: unfold ; auto.
        apply subcode_sss_terminates_inv with (P := (i,Q1F)) (2 := ); auto.
        1: apply mm_sss_env_fun.
        1: rewrite app_ass; apply subcode_left; auto.
        split.
        + rewrite Q1_length.
          replace s2 with (length F+(11+9*n+i)).
          revert ; apply subcode_sss_compute; auto.
          unfold ; .
        + unfold out_code, code_end, fst, snd.
          rew length; rewrite Q1_length; unfold ; . }
      assert (k = v0) as Hk.
      { rewrite , get_set_env_neq; try .
        rewrite ; apply ( pos0). }
      exists (s k).
      apply s_rec_eq; exists s; msplit 2; auto.
      * simpl; rewrite , ; rew env.
      * simpl; rewrite Hk; intros j Hj.
        specialize ( j Hj).
        rewrite , get_set_env_neq, , plus_comm in ; auto; .
    Qed.


    Fact ra_compiler_rec : ra_compiler_spec (ra_rec f g) i p o m.
    Proof using Hf Hg .
      exists Q4; intros v e ; split.
      + intros x; simpl ra_rel; intros .
        destruct rec_Q4_progress with (3 := ) (e := e)
          as (e' & & & ); auto.
        exists e'; split.
        * intros j; dest j o.
        * apply sss_progress_compute; auto.
      + intros .
        apply rec_Q4_compute_rev with (e := e); auto.
    Qed.


  End ra_compiler_rec.

  Section ra_compiler_min.

    Variables (n : ) (f : recalg (S n)) (Hf : ra_compiler_stm f).


    Variables (i p o m : )
              ( : o < m)
              ( : p o < n + p)
              ( : n + p m).

    Notation zero := (1+n+m).
    Notation tmp := (2+n+m).

    Local Definition min_Q1 :=
              mm_multi_copy tmp zero n p (1+m) i
            mm_erase m zero (9*n+i).

    Notation Q1 := min_Q1.

    Local Fact min_Q1_length : length Q1 = 2+9*n.
    Proof using . unfold ; rew length; . Qed.

    Local Definition min_s1 := length Q1 + i.

    Notation s1 := min_s1.

    Local Fact min_F_full : ra_compiler_spec f s1 m o zero.
    Proof using Hf . apply Hf; . Qed.

    Notation F := (proj1_sig min_F_full).
    Local Definition min_HF1 x v e H1 H2 H3 := proj1 (proj2_sig min_F_full v e ) x .
    Local Definition min_HF2 v e H1 H2 H3 := proj2 (proj2_sig min_F_full v e ) .

    Local Definition min_Q2 :=
              F
            DEC o (3+length F+s1)
           :: INC m
           :: DEC zero s1
           :: nil.

    Notation Q2 := min_Q2.

    Local Fact min_Q2_length : length Q2 = 3+length F.
    Proof. unfold ; rew length; . Qed.

    Local Fact min_Q1_progress e :
                ( j, zero j ej = 0)
   e', ( j, j < n e'⇢(j+1+m) = e⇢(j+p))
              e'm = 0
              ( j, m j n+m e'j = ej)
              (i,Q1) // (i,e) -+> (length Q1+i,e').
    Proof using .
      intros .
      destruct (@mm_multi_copy_compute tmp zero n p (1+m))
        with (i := i) (e := e)
        as ( & & & ); try .
      1,2: apply ; .
      destruct (@mm_erase_progress m zero)
        with (i := 9*n+i) (e := )
        as ( & & ); try .
      1: rewrite , ; .
      exists ; msplit 3.
      * intros; rewrite , get_set_env_neq, plus_assoc, ; auto; .
      * rewrite ; rew env.
      * intros; rewrite , get_set_env_neq, ; auto; .
      * rewrite min_Q1_length; unfold .
        apply sss_compute_progress_trans with (9*n+i,).
        { revert ; apply subcode_sss_compute; auto. }
        { replace (2+9*n+i) with (2+(9*n+i)) by .
          revert ; apply subcode_sss_progress; auto. }
    Qed.


    Local Fact min_Q2_0_progress v e :
                ( j, zero j ej = 0)
              ( j, vec_pos v j = e⇢(pos2nat j+1+m))
              f (em##v) 0
   e', ( j, j o e'j = ej)
              e'o = 0
              (s1,Q2) // (s1,e) -+> (length Q2+s1,e').
    Proof.
      intros .
      destruct min_HF1 with (1 := ) (e := e) as ( & & ); auto.
      { intros j; analyse pos j; simpl.
        * rewrite pos2nat_fst; auto.
        * rewrite pos2nat_nxt, ; f_equal; . }
      exists ; msplit 2.
      1,2: intros; rewrite ; rew env.
      apply sss_compute_progress_trans with (length F+s1,).
      * unfold ; revert ; apply subcode_sss_compute; auto.
      * rewrite min_Q2_length; unfold .
        mm env DEC zero with o (3+length F+s1).
        1: rewrite ; rew env.
        mm env stop.
    Qed.


    Local Fact min_Q2_S_progress x v e :
                ( j, zero j ej = 0)
              ( j, vec_pos v j = e⇢(pos2nat j+1+m))
              f (em##v) (S x)
   e', ( j, j o j m e'j = ej)
              e'o = x
              e'm = S (em)
              (s1,Q2) // (s1,e) -+> (s1,e').
    Proof.
      intros .
      destruct min_HF1 with (1 := ) (e := e) as ( & & ); auto.
      { intros j; analyse pos j; simpl.
        * rewrite pos2nat_fst; auto.
        * rewrite pos2nat_nxt, ; f_equal; . }
      exists (ox⦄⦃mS (em)); msplit 3.
      1,3: intros; rew env; rewrite ; rew env.
      1: clear ; dest o m; .
      apply sss_compute_progress_trans with (length F+s1,).
      { unfold ; revert ; apply subcode_sss_compute; auto. }
      unfold .
      mm env DEC S with o (3 + length F + s1) x.
      { rewrite ; rew env. }
      mm env INC with m.
      mm env DEC zero with zero s1.
      { do 2 (rewrite get_set_env_neq; try ).
        rewrite , get_set_env_neq, ; . }
      mm env stop; f_equal.
      clear .
      dest o m; try .
      rewrite ; rew env.
    Qed.


    Local Fact min_Q2_progress_rec v e k :
                ( j, zero j ej = 0)
              ( j, vec_pos v j = e⇢(pos2nat j+1+m))
              ( i, i < k x, f (i+(em)##v) (S x))
   e', ( j, j o j m e'j = ej)
              e'm = k+(em)
              (s1,Q2) // (s1,e) ->> (s1,e').
    Proof.
      revert e; induction k as [ | k IHk ]; intros e .
      + exists e; msplit 2; auto; mm env stop.
      + destruct ( 0) as (x & Hx); try ; simpl in Hx.
        destruct min_Q2_S_progress
          with (v := v) (e := e) (x := x)
          as ( & & _ & & ); auto.
        destruct IHk with (e := )
          as ( & & & ).
        { intros; rewrite , ; . }
        { intros j; rewrite , ; auto; . }
        { intros j Hj; rewrite .
          replace (j+S(em)) with ((S j)+(em)) by .
          apply ; . }
        exists ; msplit 2.
        * intros; rewrite , ; auto.
        * rewrite , ; .
        * apply sss_compute_trans with (2 := ).
          apply sss_progress_compute; auto.
    Qed.


    Local Fact min_Q2_compute_rev v e :
              ( j, zero j ej = 0)
            ( j, vec_pos v j = e⇢(pos2nat j+1+m))
            (s1,Q2) // (s1,e)
            k, f (k+(em)##v) 0 j, j < k x, f (j+(em)##v) (S x).
    Proof.
      intros ((,e') & (q & ) & ); simpl fst in .
      revert e .
      induction on q as IHq with measure q.
      intros e .
      destruct min_HF2 with (e := e) (v := (em)##v)
        as ([ | x ] & Hx); auto.
      { apply subcode_sss_terminates with (Q := (s1,Q2)).
        + unfold ; auto.
        + exists (,e'); split; auto; exists q; auto. }
      { intros j; analyse pos j.
        + rewrite pos2nat_fst; auto.
        + rewrite pos2nat_nxt; simpl.
          rewrite ; f_equal; . }
      * exists 0; split; auto; intros; .
      * destruct min_Q2_S_progress with (v := v) (e := e) (x := x)
          as ( & & & & ); auto.
        destruct subcode_sss_progress_inv with (4 := ) (5 := )
          as (q' & & ); auto.
        { apply mm_sss_env_fun. }
        { apply subcode_refl. }
        destruct IHq with (4 := )
          as (k & & ); try .
        { intros; rewrite , ; . }
        { intros; rewrite , ; auto; . }
        exists (S k); split.
        + rewrite in .
          eq goal ; do 2 f_equal; .
        + intros [ | j ] Hj.
          - simpl; exists x; auto.
          - replace (S j + (em)) with (j+(m)).
            apply ; .
            rewrite ; .
    Qed.


    Local Fact min_Q2_progress v e k :
                ( j, zero j ej = 0)
              ( j, vec_pos v j = e⇢(pos2nat j+1+m))
              em = 0
              s_min f v k
   e', ( j, j o j m e'j = ej)
              e'm = k
              (s1,Q2) // (s1,e) -+> (length Q2+s1,e').
    Proof.
      intros ( & ).
      destruct min_Q2_progress_rec with (e := e) (k := k) (v := v)
        as ( & & & ); auto.
      { intros; rewrite , plus_comm; auto. }
      destruct min_Q2_0_progress with (v := v) (e := )
        as ( & & _ & ).
      { intros; rewrite , ; . }
      { intros j; rewrite , ; . }
      { rewrite , , plus_comm; auto. }
      exists ; msplit 2.
      * intros; rewrite , ; auto.
      * rewrite , , ; .
      * apply sss_compute_progress_trans with (s1,); auto.
    Qed.


    Local Definition min_s4 := length Q1+length Q2+i.

    Notation s4 := min_s4.

    Local Definition min_Q4 :=
              Q1 Q2
            mm_copy m o tmp zero s4
            mm_multi_erase m zero (1+n) (9+s4).

    Notation Q4 := min_Q4.

    Local Fact min_Q4_progress v e x :
                 ( j, m j ej = 0)
               ( j, vec_pos v j = e⇢(pos2nat j+p))
               s_min f v x
   e', ( j, j o e'j = ej)
               e'o = x
               (i,Q4) // (i,e) -+> (length Q4+i,e').
    Proof.
      intros .
      destruct min_Q1_progress with (e := e)
        as ( & & & & ).
      { intros j Hj; apply ; . }
      destruct min_Q2_progress with (v := v) (e := ) (k := x)
        as ( & & & ); auto.
      { intros j Hj; rewrite , ; . }
      { intros j; rewrite , ; auto; apply pos2nat_prop. }
      destruct mm_copy_progress
        with (src := m) (dst := o) (tmp := tmp) (zero := zero)
             (i := s4) (e := )
        as ( & & ); try .
      1,2: rewrite , , ; .
      destruct mm_multi_erase_compute
        with (dst := m) (zero := zero) (k := 1+n)
             (i := 9+s4) (e := )
        as ( & & & ); try .
      { rewrite , get_set_env_neq, , , ; . }
      exists ; msplit 2.
      * intros j Hj.
        destruct (interval_dec m zero j).
        + rewrite , ; .
        + rewrite , ; rew env; try .
          rewrite , ; .
      * rewrite , , ; rew env; .
      * apply sss_progress_trans with (length Q1+i,).
        { unfold ; revert ; apply subcode_sss_progress; auto. }
        apply sss_progress_trans with (length Q2+s1,).
        { unfold at 1 in ; revert ; unfold ; apply subcode_sss_progress; auto. }
        apply sss_progress_compute_trans with (9+s4,).
        { replace (length Q2+s1) with s4.
          unfold ; revert ; apply subcode_sss_progress; unfold ; auto.
          unfold , ; . }
        { replace (length Q4+i) with (2*(1+n)+(9+s4)).
          unfold ; revert ; apply subcode_sss_compute; auto.
          unfold ; subcode_tac; rewrite app_nil_end; auto.
          unfold , ; rew length; . }
    Qed.


    Local Fact min_Q4_terminates v e :
                 ( j, m j ej = 0)
               ( j, vec_pos v j = e⇢(pos2nat j+p))
               (i,Q4) // (i,e)
               x, s_min f v x.
    Proof.
      intros .
       destruct min_Q1_progress with (e := e)
        as ( & & & & ).
      { intros j Hj; apply ; . }
      apply subcode_sss_terminates_inv
        with (P := (i,Q1)) ( := (s1,)) in .
      * apply subcode_sss_terminates with (P := (s1,Q2)) in .
        + apply min_Q2_compute_rev with (v := v) in .
          - destruct as (x & & ).
            rewrite , plus_comm in .
            exists x; split; auto.
            intros j Hj; specialize ( _ Hj).
            rewrite , plus_comm in ; auto.
          - intros; rewrite , ; .
          - intros; rewrite , ; auto; apply pos2nat_prop.
        + unfold , ; auto.
      * apply mm_sss_env_fun.
      * unfold ; auto.
      * unfold ; split.
        + apply sss_progress_compute; auto.
        + unfold out_code, code_end, fst, snd; .
    Qed.


    Fact ra_compiler_min : ra_compiler_spec (ra_min f) i p o m.
    Proof using Hf .
      exists Q4; intros v e ; split.
      + intros x; simpl ra_rel; intros .
        destruct min_Q4_progress with (3 := ) (e := e)
          as (e' & & & ); auto.
        exists e'; split.
        * intros j; dest j o.
        * apply sss_progress_compute; auto.
      + intro; apply min_Q4_terminates with (e := e); auto.
    Qed.


  End ra_compiler_min.

  Theorem ra_compiler n f : @ra_compiler_stm n f.
  Proof.
    induction f as [ c | | | n q | n k f g Hf Hg | | ].
    + apply ra_compiler_cst.
    + apply ra_compiler_zero.
    + apply ra_compiler_succ.
    + apply ra_compiler_proj.
    + apply ra_compiler_comp; trivial.
    + intros i p o m ? ? ?; apply ra_compiler_rec; auto.
    + intros i p o m ? ? ?; apply ra_compiler_min; auto.
  Qed.


  Corollary ra_mm_env_simulator n (f : recalg n) :
              { P | v e, ( p, e⇢(pos2nat p) = vec_pos v p)
                                ( j, n < j ej = 0)
                                ( x, f v x
                                      e', e' enx
                                                (1,P) // (1,e) ->> (1+length P,e'))
                                ((1,P) // (1,e) ex (f v)) }.
  Proof.
    destruct (ra_compiler f) with (i := 1) (p := 0) (o := n) (m := S n)
      as (P & HP); try .
    exists P; intros v e ; split.
    + intros x .
      rewrite plus_comm; apply HP with (v := v); auto.
      intros; rewrite plus_comm; simpl; auto.
    + intros .
      apply (HP v e); auto.
      intros; rewrite plus_comm; simpl; auto.
  Qed.


End ra_compiler.