Changeset 3411

Timestamp:

Dec 23, 2013, 6:46:07 PM (7 years ago)

Author:

piccolo

Message:

new statement of correctness theorem in place

File:

• LTS/Language.ma (modified) (6 diffs)

LTS/Language.ma

@@ -265 +265 @@
 
 
-definition is_synt_succ : ∀p.relation (state p) ≝ λp,s1,s2.True.
+definition is_synt_succ : ∀p.relation (state p) ≝ λp,s1,s2.cont … s1 = cont … s2.
 (* bisognerebbe confrontare la coda dell'istruzione corrente e la parte di stack fino alla prima label.
  match (code … s1) with
@@ -1366 +1366 @@
 ∀s1,s2,s1' : state p.∀abs_top,abs_tail.
 ∀t : raw_trace (operational_semantics … p' prog) s1 s2.
+pre_measurable_trace … t → 
 state_rel … m keep abs_top abs_tail s1 s1' → 
 ∃abs_top',abs_tail'.∃s2'.∃t' : raw_trace (operational_semantics … p' t_prog) s1' s2'.
@@ -1373 +1374 @@
  len … t = len … t'.
 #p #p' #prog #no_dup @pair_elim * #t_prog #m #keep #EQtrans
-#s1 #s2 #s1' #abs_top #abs_tail #t lapply abs_top -abs_top lapply abs_tail
--abs_tail lapply s1' -s1' elim t
-[ #st #s1' #abs_tail #abs_top #H %{abs_top} %{abs_tail} %{s1'} %{(t_base …)} 
+#s1 #s2 #s1' #abs_top #abs_tail #t #Hpre lapply abs_top -abs_top lapply abs_tail
+-abs_tail lapply s1' -s1' elim Hpre
+[ #st #_ #s1' #abs_tail #abs_top #H %{abs_top} %{abs_tail} %{s1'} %{(t_base …)} 
   % [2: %] %{H} whd in match (get_costlabels_of_trace ????); >append_nil
   @is_permutation_eq
-]
-#st1 #st2 #st3 #lab whd in ⊢ (% → ?); #H inversion H in ⊢ ?; #st11 #st12
-[ * #lab1 #new_code #new_cont #EQcode11 #EQcont11 #EQcode12 #EQcont12 #EQstore
-  #Hio11 #EQio12 #Hl1 #EQ1 #EQ2 #EQ3 #EQ4 destruct #tl #IH #s1' #abs_tail #abs_top
-  whd in match state_rel in ⊢ (% → ?); normalize nodelta >EQcont11 in ⊢ (% → ?);
-  whd in match check_continuations; normalize nodelta whd in match (foldr2 ???????);
-  inversion (cont ? s1') [ #_ *] * #l1' #new_code' #new_cont' #_ #EQconts1'
-  normalize nodelta change with (check_continuations ?????) in match (foldr2 ???????); 
-  inversion(check_continuations ?????) [ #_ *] ** #H1 #l2 #ll2 #EQHl2 
-  >m_return_bind normalize nodelta inversion (call_post_clean ?????) [ #_ ***** ]
-  * #l3 #code_c_st12 #EQcode_c_st12 normalize nodelta
-  cases l1' in EQconts1'; (*in Hio11 Hl1 EQcont11 H;*) normalize nodelta
-  [1,4: [ #x #y ] #_ (*#_ #_ #_ #H*) *****
-  | #x #_ cases (ret_costed_abs ??) normalize nodelta [|#c] ******[|*] #EQ @⊥ >EQ in Hl1;
-    normalize * /2/ ] *
-  [ #EQconts1' normalize nodelta ****** #EQ destruct(EQ)
-    #HH1 #EQ destruct(EQ) >EQcode11 in ⊢ (% → ?); inversion(code … s1')
-    [
-    | #x 
-    | #seq #lbl #i #_ 
-    | #cond #ltrue #i1 #lfalse #i2 #i3 #_ #_ #_
-    | #cond #ltrue #i1 #lfalse #i2 #_ #_
-    | #f #act_p #ret_post #i #_
-    | #l_in #io #l_out #i #_
+| #st1 #st2 #st3 #lab whd in ⊢ (% → ?); #H inversion H in ⊢ ?; #st11 #st12
+  [ * #lab1 #new_code #new_cont #EQcode11 #EQcont11 #EQcode12 #EQcont12 #EQstore
+    #Hio11 #EQio12 #Hl1 #EQ1 #EQ2 #EQ3 #EQ4 destruct #tl #_ * #opt_l #EQ destruct(EQ) 
+    #pre_tl #IH #s1' #abs_tail #abs_top whd in match state_rel in ⊢ (% → ?); normalize nodelta >EQcont11 in ⊢ (% → ?);
+    whd in match check_continuations; normalize nodelta whd in match (foldr2 ???????);
+    inversion (cont ? s1') [ #_ *] * #l1' #new_code' #new_cont' #_ #EQconts1'
+    normalize nodelta change with (check_continuations ?????) in match (foldr2 ???????); 
+    inversion(check_continuations ?????) [ #_ *] ** #H1 #l2 #ll2 #EQHl2 
+    >m_return_bind normalize nodelta inversion (call_post_clean ?????) [ #_ ***** ]
+    * #l3 #code_c_st12 #EQcode_c_st12 normalize nodelta
+    cases l1' in EQconts1'; (*in Hio11 Hl1 EQcont11 H;*) normalize nodelta
+    [1,4: [ #x #y ] #_ (*#_ #_ #_ #H*) *****
+    | #x #_ cases (ret_costed_abs ??) normalize nodelta [|#c] ******[|*] #EQ @⊥ >EQ in Hl1;
+      normalize * /2/ ] *
+    [ #EQconts1' normalize nodelta ****** #EQ destruct(EQ)
+      #HH1 #EQ destruct(EQ) >EQcode11 in ⊢ (% → ?); inversion(code … s1')
+      [
+      | #x 
+      | #seq #lbl #i #_ 
+      | #cond #ltrue #i1 #lfalse #i2 #i3 #_ #_ #_
+      | #cond #ltrue #i1 #lfalse #i2 #_ #_
+      | #f #act_p #ret_post #i #_
+      | #l_in #io #l_out #i #_
+      ]
+      [|*: #_ whd in ⊢ (??%% → ?); [ #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ)]
+           cases(call_post_clean ?????) normalize nodelta
+           [1,3,5,7,9: #EQ destruct(EQ)] cases daemon (* da fare assurdi!!!*) ]
+      #EQcodes1' whd in ⊢ (??%% → ?); #EQ destruct(EQ) #EQstore11 #EQio11 #EQ destruct(EQ)
+      cases(IH (mk_state ? new_code' new_cont' (store … s1') false) ll2 abs_top …)
+      [2: whd whd in match check_continuations; normalize nodelta 
+         change with (check_continuations ?????) in match (foldr2 ???????); >EQHl2
+         normalize nodelta % // % // % // % // @EQcode_c_st12 ]
+      #abs_top' * #abs_tail' * #st3' * #t' ** #Hst3st3' #EQcosts #EQlen 
+      %{abs_top'} %{abs_tail'} %{st3'} %{(t_ind … (cost_act (None ?)) …  t')}
+      [ @hide_prf whd @(empty ????? 〈(cost_act (None ?)),?〉)
+        [3: assumption |4: assumption |*:] /3 by nmk/ ]
+      %   [2: whd in ⊢ (??%%); >EQlen % ] %{Hst3st3'} @EQcosts
+    | #lbl #EQconts1' normalize nodelta ******* #EQ destruct(EQ)
+      #HH1 #EQ destruct(EQ) #EQget_el >EQcode11 in ⊢ (% → ?); 
+      inversion(code … s1')
+      [
+      | #x 
+      | #seq #lbl #i #_ 
+      | #cond #ltrue #i1 #lfalse #i2 #i3 #_ #_ #_
+      | #cond #ltrue #i1 #lfalse #i2 #_ #_
+      | #f #act_p #ret_post #i #_
+      | #l_in #io #l_out #i #_
+      ]
+      [|*: #_ whd in ⊢ (??%% → ?); #EQ cases daemon (* da fare assurdi !!!*) ]
+      #EQcodes1' whd in ⊢ (??%% → ?); #EQ destruct(EQ) #EQstore #EQio #EQ destruct(EQ)
+      cases(IH (mk_state ? new_code' new_cont' (store … s1') false) ll2 l3 …)
+      [2: whd whd in match check_continuations; normalize nodelta
+         change with (check_continuations ?????) in match (foldr2 ???????); 
+         >EQHl2 in ⊢ (match % with [ _⇒ ? | _ ⇒ ?]);
+         normalize nodelta % // % // % // % // @EQcode_c_st12 ]
+      #abs_top' * #abs_tail' * #st3' * #t' ** #Hst3st3' #EQcost #EQlen 
+      %{abs_top'} %{abs_tail'} %{st3'}
+      %{(t_ind … (cost_act (Some ? lbl)) … t')}
+      [ @hide_prf whd @(empty ????? 〈(cost_act (Some ? lbl)),?〉)
+        [3: assumption |4: assumption |*:] /3 by nmk/ ]
+      % [2: whd in ⊢ (??%%); >EQlen % ] %{Hst3st3'} >map_labels_on_trace_append
+      whd in match (map_labels_on_trace ? [lbl]); >append_nil >EQget_el
+      @is_permutation_cons assumption
     ]
-    [|*: #_ whd in ⊢ (??%% → ?); [ #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ)]
-         cases(call_post_clean ?????) normalize nodelta
-         [1,3,5,7,9: #EQ destruct(EQ)] cases daemon (* da fare assurdi!!!*) ]
-    #EQcodes1' whd in ⊢ (??%% → ?); #EQ destruct(EQ) #EQstore11 #EQio11 #EQ destruct(EQ)
-    cases(IH (mk_state ? new_code' new_cont' (store … s1') false) ll2 abs_top …)
-    [2: whd whd in match check_continuations; normalize nodelta 
-       change with (check_continuations ?????) in match (foldr2 ???????); >EQHl2
-        normalize nodelta % // % // % // % // @EQcode_c_st12 ]
-    #abs_top' * #abs_tail' * #st3' * #t' ** #Hst3st3' #EQcosts #EQlen 
-    %{abs_top'} %{abs_tail'} %{st3'} %{(t_ind … (cost_act (None ?)) …  t')}
-    [ @hide_prf whd @(empty ????? 〈(cost_act (None ?)),?〉)
-      [3: assumption |4: assumption |*:] /3 by nmk/ ]
-    % [2: whd in ⊢ (??%%); >EQlen % ] %{Hst3st3'} @EQcosts
-  | #lbl #EQconts1' normalize nodelta ******* #EQ destruct(EQ)
-    #HH1 #EQ destruct(EQ) #EQget_el >EQcode11 in ⊢ (% → ?); 
-    inversion(code … s1')
-    [
-    | #x 
-    | #seq #lbl #i #_ 
-    | #cond #ltrue #i1 #lfalse #i2 #i3 #_ #_ #_
-    | #cond #ltrue #i1 #lfalse #i2 #_ #_
-    | #f #act_p #ret_post #i #_
-    | #l_in #io #l_out #i #_
-    ]
-    [|*: #_ whd in ⊢ (??%% → ?); #EQ cases daemon (* da fare assurdi !!!*) ]
-    #EQcodes1' whd in ⊢ (??%% → ?); #EQ destruct(EQ) #EQstore #EQio #EQ destruct(EQ)
-    cases(IH (mk_state ? new_code' new_cont' (store … s1') false) ll2 l3 …)
-    [2: whd whd in match check_continuations; normalize nodelta
-       change with (check_continuations ?????) in match (foldr2 ???????); 
-       >EQHl2 in ⊢ (match % with [ _⇒ ? | _ ⇒ ?]);
-        normalize nodelta % // % // % // % // @EQcode_c_st12 ]
-    #abs_top' * #abs_tail' * #st3' * #t' ** #Hst3st3' #EQcost #EQlen 
-    %{abs_top'} %{abs_tail'} %{st3'}
-    %{(t_ind … (cost_act (Some ? lbl)) … t')}
-    [ @hide_prf whd @(empty ????? 〈(cost_act (Some ? lbl)),?〉)
-      [3: assumption |4: assumption |*:] /3 by nmk/ ]
-    % [2: whd in ⊢ (??%%); >EQlen % ] %{Hst3st3'} >map_labels_on_trace_append
-    whd in match (map_labels_on_trace ? [lbl]); >append_nil >EQget_el
-    @is_permutation_cons assumption
-  ]
+  |  cases daemon (*TODO*)
 (*      
-| #seq #i #store * [| #lbl] #EQcode11 #EQstore #EQ destruct(EQ) #EQcont 
+|
+  #st1 #st2 #st3 #lab whd in ⊢ (% → ?); #H inversion H in ⊢ ?; #st11 #st12
+  #seq #i #store * [| #lbl] #EQcode11 #EQstore #EQ destruct(EQ) #EQcont 
   #EQ destruct(EQ) #Hio_st11 #Hio_st12 #EQ destruct(EQ) #EQ1 #EQ2 destruct(EQ1 EQ2)
   #EQ destruct(EQ) #tl #IH #st3 #l1 whd in ⊢ (% → ?); 
@@ -1454 +1457 @@
   #seq1 #opt_l #i1 #_ #EQcode_st3 change with (m_bind ?????) in ⊢ (??%? → ?);
   cases daemon *)
-|8: #f #act_p #opt_l #i #mem #env_it #EQcode11 #EQenv_it #EQmem
+  | cases daemon (*TODO*)
+  | cases daemon (*TODO*)
+  | cases daemon (*TODO*)
+  | cases daemon (*TODO*)
+  | cases daemon (*TODO*)
+  | #f #act_p #r_lb #cd #mem #env_it #EQ1 #EQ2 #EQ3 #EQ4 #EQ5 #EQ6 #EQ7 #EQ8 #EQ9 #EQ10
+    #EQ11 #EQ12 destruct #tl #_ * #x #EQ destruct(EQ)
+  | cases daemon (*TODO absurd as above*)
+  ]
+| cases daemon (*TODO*)
+| #st1 #st2 #st3 #lab #H inversion H in ⊢ ?; #st11 #st12
+  [1,2,3,4,5,6,7,9: cases daemon (*absurd!*)
+  | #f #act_p #opt_l #i #mem #env_it #EQcode11 #EQenv_it #EQmem
+    #EQ destruct(EQ) #EQcode12 #EQcont12 #EQio11 #EQio12 #EQ1 #EQ2 #EQ3 
+    destruct(EQ1 EQ2 EQ3) #EQ destruct(EQ) #tl #_ #_ whd in ⊢ (?% → ?); >EQcode11 in ⊢ (% → ?);
+    normalize nodelta cases opt_l in EQcode11 EQcont12; normalize nodelta [ #x #y *]
+    #lbl #EQcode11 #EQcont12 * #pre_tl #IH #st1' #abs_top #abs_tail
+    whd in ⊢ (% → ?); inversion(check_continuations ????) [ #_ *] ** #H1 
+    #abs_top_cont #abs_tail_cont #EQcheck
+    normalize nodelta **** #HH1 >EQcode11 in ⊢ (% → ?); inversion(code … st1')
+    [1,2,3,4,5,7: (*assurdi da fare*) cases daemon] #f' #act_p' #opt_l' #i' #_
+    #EQcode_st1' #EQclean #EQstore #EQio #EQ destruct(EQ)
+    lapply(trans_env_ok … no_dup) >EQtrans normalize nodelta #H
+    cases(H … EQenv_it) -H #env_it' * #fresh' * #EQenv_it' ***** #EQtrans 
+    #EQgen_labels #EQsignature #EQlab_env_it #same_map #same_keep
+    change with (m_bind ?????) in EQclean : (??%?); inversion(call_post_clean ?????) in EQclean;
+    [ #_ whd in ⊢ (??%% → ?); #EQ destruct] * #abs_top'' #i'' #EQi' >m_return_bind
+    inversion opt_l' in EQcode_st1'; [| #lbl'] #EQopt_l' #EQcode_st1' normalize nodelta
+    [2: inversion(memb ???) normalize nodelta #Hlbl_keep
+        [  inversion (get_element ????) normalize nodelta [ #_ whd in ⊢ (??%% → ?); #EQ destruct]
+           #lbl'' #l3' #_ #EQget_el whd in match (eqb ???); inversion (eqb ???) normalize nodelta
+          [2: #_ whd in ⊢ (??%% → ?); #EQ destruct] #H cases(eqb_true ? lbl'' lbl') #H1 #_
+          lapply(H1 H) -H -H1 #EQ destruct(EQ) inversion(eqb_list ???) normalize nodelta
+          [2: #_ whd in ⊢ (??%% → ?); #EQ destruct] #H cases(eqb_true (DeqSet_List ?) l3' abs_top'')
+          #H1 #_ lapply(H1 H) -H -H1 #EQ destruct(EQ) whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ
+          #EQ destruct(EQ)
+          cases(IH (mk_state ? (f_body … env_it') (〈ret_act opt_l',i'〉 :: (cont … st1')) (store ? st12) false) (abs_tail_cont) (gen_labels … (call_post_trans … (f_body … env_it) fresh' (nil ?))))
+          [2: whd >EQcont12
+            change with (m_bind ??? (check_continuations ?????) ?) in match (check_continuations ?????);
+            >EQcheck >m_return_bind normalize nodelta >EQi' normalize nodelta >EQopt_l'
+            whd in match ret_costed_abs; normalize nodelta >Hlbl_keep normalize nodelta
+            % // % // % // % [/5 by conj/] >EQgen_labels >EQcode12 <EQtrans
+            @(inverse_call_post_trans … fresh') 
+            [2: % |*: [2,3: /2 by / ] 
+                cases(lookup_ok_append … EQenv_it) #env1 * #env2 * #EQ1 #EQ2
+                whd in no_dup; destruct >EQ1 in no_dup; >foldr_map_append >foldr_map_append
+                #no_dup lapply(no_duplicates_append_r … no_dup) #H1 
+                lapply(no_duplicates_append_l … H1) whd in match (foldr ?????); -H1
+                change with ([?]@?) in match (?::?); #H1 
+                lapply(no_duplicates_append_r … H1) >append_nil //
+            ]
+          ]
+          #abs_top''' * #abs_tail''' * #st3' * #t' ** #Hst3st3' #EQcosts #EQlen %{abs_top'''}
+          %{abs_tail'''} %{st3'} %{(t_ind … (call_act f (f_lab … env_it')) …  t')}
+          [ @hide_prf @call /2 width=10 by jmeq_to_eq/ ] % [2: whd in ⊢ (??%%); >EQlen %]
+          %{Hst3st3'} >map_labels_on_trace_append whd in match (get_costlabels_of_trace ????) in ⊢ (???%);
+          >EQlab_env_it >associative_append whd in match (append ???); >associative_append
+          >associative_append in ⊢ (???%); >(associative_append … [?]) in ⊢ (???%);
+          whd in match (map_labels_on_trace ??); >EQgen_labels @is_permutation_cons
+          >append_nil whd in match (append ???) in ⊢ (???%); //
+        | whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ)
+        ]
+    | whd in ⊢ (??%% → ?); #EQ destruct(EQ)
+    ]
+  ]
+|        
+
+8:
+    #st1 #st2 #st3 #lab whd in ⊢ (% → ?); #H inversion H in ⊢ ?; #st11 #st12
+    #f #act_p #opt_l #i #mem #env_it #EQcode11 #EQenv_it #EQmem
     #EQ destruct(EQ) #EQcode12 #EQcont12 #EQio11 #EQio12 #EQ1 #EQ2 #EQ3 
     destruct(EQ1 EQ2 EQ3) #EQ destruct(EQ) #tl #IH #st1' #abs_top #abs_tail
@@ -1518 +1590 @@
           ]
           #abs_top''' * #abs_tail''' * #st3' * #t' ** #Hst3st3' #EQcosts #EQlen 
-          %{([a_return_post lbl'] @ abs_top''')}
+          %{abs_top'''}
           %{abs_tail'''} %{st3'} %{(t_ind … (call_act f (f_lab … env_it')) …  t')}
           [ @hide_prf @call /2 width=10 by jmeq_to_eq/ ] % [2: whd in ⊢ (??%%); >EQlen %]
@@ -1524 +1596 @@
           >EQlab_env_it >associative_append >associative_append
           >associative_append in ⊢ (???%); >(associative_append … [?]) in ⊢ (???%);
+          >EQopt_l' in t'; #t'
           whd in match (map_labels_on_trace ??); >EQgen_labels
           whd in match (foldr ?????); >append_nil
+          whd in match (get_costlabels_of_trace ????);
            @is_permutation_cons
           >append_nil whd in match (append ???) in ⊢ (???%); //