source: LTS/stack_monostack_pass.ma

Last change on this file was 3591, checked in by piccolo, 4 years ago

stared pass stack to monostack, closed the first three proof obbligations of simulation conditions

File size: 6.4 KB
Line 
1(**************************************************************************)
2(*       ___                                                              *)
3(*      ||M||                                                             *)
4(*      ||A||       A project by Andrea Asperti                           *)
5(*      ||T||                                                             *)
6(*      ||I||       Developers:                                           *)
7(*      ||T||         The HELM team.                                      *)
8(*      ||A||         http://helm.cs.unibo.it                             *)
9(*      \   /                                                             *)
10(*       \ /        This file is distributed under the terms of the       *)
11(*        v         GNU General Public License Version 2                  *)
12(*                                                                        *)
13(**************************************************************************)
14
15include "mono_stack.ma".
16include "Simulation.ma".
17
18let rec mono_env_store_rel (s1 : list (list ℕ)) (s2 : list ℕ) (fp : ℕ) on s1 : Prop ≝
19match s1 with
20[ nil ⇒ s2 = nil ?
21| cons x xs ⇒ ∃old_fp,s21,s22.s2 = s21 @ [old_fp] @ s22 ∧
22              x= s21 @ [O] ∧
23              mono_env_store_rel xs s22 old_fp ∧ |s22| = fp
24].
25
26definition mono_store_rel : frame_store_t → mono_stack_store_t → Prop ≝
27λst1,st2.mono_env_store_rel (\fst st1) (\fst st2) (\fst (\snd st2)) ∧ (\snd (\snd st1)) = (\snd (\snd st2)).
28
29definition mono_state_rel ≝
30λs1 : state stack_state_params.λs2 : state mono_stack_state_params.
31mono_store_rel … (store … s1) (store … s2) ∧ code … s1 = code … s2 ∧ cont … s1 = cont … s2
32∧ io_info … s1 = io_info … s2.
33
34definition mono_stack_relations :
35∀prog : Program stack_env_params stack_instr_params flat_labels.∀bound.
36relations flat_labels
37(operational_semantics stack_state_params (stack_sem_state_params bound) prog)
38(operational_semantics mono_stack_state_params (mono_stack_sem_state_params bound) prog) ≝
39λprog.λbound.
40mk_relations … mono_state_rel
41  (λ_.λ_.True).
42
43lemma minus_right_cancellable : ∀n,m,p : ℕ.n = m → n-p = m -p. //
44qed.
45
46
47lemma read_frame_ok :
48∀st1,st2,fp,env,x,n.
49mono_env_store_rel st1 st2 fp → option_hd … st1 = return env →
50to_shift + x < |env| →
51read_frame env (to_shift+x) O = return n →
52read_frame st2 (to_shift+x) fp = return n.
53#st1 elim st1 [ #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9 normalize in H7; destruct]
54#env #tl #IH #st2 #fp #env' #x #n * #old_fp * #s21 * #s22 *** #EQ1 #EQ2 destruct #H #EQ destruct
55whd in ⊢ (??%% → ?); #EQ destruct #H1
56change with (nth_opt ???) in ⊢ (??%? → ?);  <minus_n_O >length_append normalize in ⊢ (??(??%?)? → ?);
57>nth_first
58[2: normalize >minus_minus_comm >commutative_plus <(plus_minus … 1) // normalize <(minus_Sn_m … (S (S x)))
59   [2: >length_append in H1; normalize >(commutative_plus) normalize  /2/]
60   normalize /2/
61]
62#H2 change with (nth_opt ???) in ⊢ (??%?); >nth_first
63[2: >length_append >length_append normalize <plus_n_Sm normalize <(minus_minus_comm ? (|s22|))
64    >commutative_plus <(plus_minus … (|s22|)) [2: //] <minus_n_n normalize >minus_plus <(minus_Sn_m … (S x +1))
65    [2: normalize >commutative_plus normalize normalize in H1; >length_append in H1; normalize >commutative_plus
66        normalize /2/ ]
67    <commutative_plus normalize /2/
68]
69>length_append >length_append
70cut((|s21|+(|[old_fp]|+|s22|)-(to_shift+x)-|s22|-1) = (|s21|+1-S (S x)-1))
71[ normalize @minus_right_cancellable  >minus_minus_comm >commutative_plus <(plus_minus … (|s22|)) [2: //]
72  <(minus_Sn_n … (|s22|)) >commutative_plus %
73] #EQ >EQ assumption
74qed.
75
76lemma update_frame_ok :
77∀st1,st2,fp,env,x,val,new_env.
78mono_env_store_rel (env :: st1) st2 fp →
79assign_frame env (to_shift + x) O val = return new_env →
80∃new_st.
81assign_frame st2 (to_shift + x) fp val = return new_st ∧
82mono_env_store_rel (new_env :: st1) new_st fp.
83#st1 #st2 #fp #env #x #val #new_env * #old_fp * #s11 * #s22 *** #EQ1 #EQ2 destruct
84#Hrel #EQ destruct change with (update ????) in ⊢ (??%? → ?); #EQnew_env
85%{(new_env @ s22)} %
86[2: %{old_fp} %{(chop … new_env)} %{s22} % // % // % xxxxxx
87qed.
88
89lemma list_n_plus : ∀A,a,n,m.list_n A a (n +m) = list_n A a n @ list_n A a m.
90#A #a #n elim n // -n #m #IH #m whd in ⊢ (??%%); @eq_f @IH
91qed.
92
93lemma stack_initial_mono_initial : ∀prog,bound.
94∀s1.∀s2.
95bool_to_Prop (lang_initial ? (stack_sem_state_params bound) prog s1) →
96bool_to_Prop (lang_initial ? (mono_stack_sem_state_params bound) prog s2) →
97mono_state_rel s1 s2.
98#prog #bound #s1 #s2 whd in match lang_initial; normalize nodelta @eq_instructions_elim #EQcode_s1 [2: *]
99@eqb_list_elim #EQcont_s1 [2: *] inversion(?==?) normalize nodelta #EQstore_s1 [2: *] normalize nodelta
100whd in ⊢ (?% → ?); #Hio_s1 @eq_instructions_elim #EQcode_s2 [2: *] @eqb_list_elim #EQcont_s2 [2: *]
101inversion(?==?) #EQstore_s2 [2: *] whd in ⊢ (?% → ?); #Hio_s2 % [2: >Hio_s1 >Hio_s2 %]
102% [2: >EQcont_s1 >EQcont_s2 %] % [2: >EQcode_s1 >EQcode_s2 %] >(\P EQstore_s1) >(\P EQstore_s2)
103% // whd whd in match (init_store ??); %{O} %{(list_n … O (pred (to_shift + bound)))}
104%{[ ]} % // % // %
105[ >append_nil ] change with (list_n ? O 1) in match ([0]); <list_n_plus <(commutative_plus … 1) %
106qed.
107
108lemma stack_final_mono_final : ∀s1,s2.mono_state_rel s1 s2 →
109bool_to_Prop(lang_final … s1) → bool_to_Prop (lang_final … s2).
110#s1 #s2 #REL whd in match lang_final; normalize nodelta @eq_instructions_elim #EQcode_s1 [2: *]
111inversion(cont … s1) [2: #z #zs #_ #_ *] #EQcont_s1 * @andb_Prop
112cases REL ** #_ >EQcode_s1 #EQcode_s2 >EQcont_s1 #EQcont_s2 #_ [ <EQcode_s2 % | <EQcont_s2 %]
113qed.
114
115lemma var_io_is_stack_io :∀s1,s2.mono_state_rel s1 s2 → lang_classify ? s2 = cl_io → lang_classify ? s1 = cl_io.
116#s1 #s2 *** #_ #EQcode #_ #Hio whd in ⊢ (??%? → ??%?); >EQcode cases(code ??)
117[| #rt | #seq #opt_l #i | #cond #ltrue #i_true #lfalse #i_false #i | #cond #ltrue #i_true #lfalse #i | #f #act #opt_l #i |
118    #lin *]
119normalize nodelta #EQ destruct >Hio //
120qed.
121
122
123
124
125definition stack_mono_stack_simulation : ∀prog : Program stack_env_params stack_instr_params flat_labels.∀bound.
126simulation_conditions … (mono_stack_relations prog bound) ≝λprog.λbound.mk_simulation_conditions ….
127(*[4: #s1 #s2 #s1' #H inversion H
128   [ #st1 #st2 * #lab #instr #tl #EQcode_st1 #EQcond_st1 #EQ1 #EQ2 destruct #EQstore *)
129cases daemon
130qed.
Note: See TracBrowser for help on using the repository browser.