(**************************************************************************)
(*       ___                                                              *)
(*      ||M||                                                             *)
(*      ||A||       A project by Andrea Asperti                           *)
(*      ||T||                                                             *)
(*      ||I||       Developers:                                           *)
(*      ||T||         The HELM team.                                      *)
(*      ||A||         http://helm.cs.unibo.it                             *)
(*      \   /                                                             *)
(*       \ /        This file is distributed under the terms of the       *)
(*        v         GNU General Public License Version 2                  *)
(*                                                                        *)
(**************************************************************************)

include "mono_stack.ma".
include "Simulation.ma".

let rec mono_env_store_rel (s1 : list (list ℕ)) (s2 : list ℕ) (fp : ℕ) on s1 : Prop ≝ 
match s1 with
[ nil ⇒ s2 = nil ?
| cons x xs ⇒ ∃old_fp,s21,s22.s2 = s21 @ [old_fp] @ s22 ∧
              x= s21 @ [O] ∧
              mono_env_store_rel xs s22 old_fp ∧ |s22| = fp
].

definition mono_store_rel : frame_store_t → mono_stack_store_t → Prop ≝ 
λst1,st2.mono_env_store_rel (\fst st1) (\fst st2) (\fst (\snd st2)) ∧ (\snd (\snd st1)) = (\snd (\snd st2)).

definition mono_stack_relations : 
∀prog : Program stack_env_params stack_instr_params flat_labels.∀bound.
relations flat_labels
(operational_semantics stack_state_params (stack_sem_state_params bound) prog)
(operational_semantics mono_stack_state_params (mono_stack_sem_state_params bound) prog) ≝ 
λprog.λbound.
mk_relations … (λs1,s2.mono_store_rel … (store … s1) (store … s2) ∧ code … s1 = code … s2 ∧ cont … s1 = cont … s2) 
  (λ_.λ_.True).

lemma minus_right_cancellable : ∀n,m,p : ℕ.n = m → n-p = m -p. //
qed.


lemma read_frame_ok : 
∀st1,st2,fp,env,x,n.
mono_env_store_rel st1 st2 fp → option_hd … st1 = return env → 
to_shift + x < |env| →
read_frame env (to_shift+x) O = return n → 
read_frame st2 (to_shift+x) fp = return n.
#st1 elim st1 [ #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9 normalize in H7; destruct]
#env #tl #IH #st2 #fp #env' #x #n * #old_fp * #s21 * #s22 *** #EQ1 #EQ2 destruct #H #EQ destruct 
whd in ⊢ (??%% → ?); #EQ destruct #H1
change with (nth_opt ???) in ⊢ (??%? → ?);  <minus_n_O >length_append normalize in ⊢ (??(??%?)? → ?);
>nth_first 
[2: normalize >minus_minus_comm >commutative_plus <(plus_minus … 1) // normalize <(minus_Sn_m … (S (S x)))
   [2: >length_append in H1; normalize >(commutative_plus) normalize  /2/]
   normalize /2/
]
#H2 change with (nth_opt ???) in ⊢ (??%?); >nth_first 
[2: >length_append >length_append normalize <plus_n_Sm normalize <(minus_minus_comm ? (|s22|)) 
    >commutative_plus <(plus_minus … (|s22|)) [2: //] <minus_n_n normalize >minus_plus <(minus_Sn_m … (S x +1))
    [2: normalize >commutative_plus normalize normalize in H1; >length_append in H1; normalize >commutative_plus
        normalize /2/ ]
    <commutative_plus normalize /2/
] 
>length_append >length_append 
cut((|s21|+(|[old_fp]|+|s22|)-(to_shift+x)-|s22|-1) = (|s21|+1-S (S x)-1))
[ normalize @minus_right_cancellable  >minus_minus_comm >commutative_plus <(plus_minus … (|s22|)) [2: //]
  <(minus_Sn_n … (|s22|)) >commutative_plus %
] #EQ >EQ assumption
qed.

definition stack_mono_stack_simulation : ∀prog : Program stack_env_params stack_instr_params flat_labels.∀bound.
simulation_conditions … (mono_stack_relations prog bound) ≝λprog.λbound.mk_simulation_conditions ….
(*[4: #s1 #s2 #s1' #H inversion H
   [ #st1 #st2 * #lab #instr #tl #EQcode_st1 #EQcond_st1 #EQ1 #EQ2 destruct #EQstore *)
cases daemon
qed.