(**************************************************************************) (* ___ *) (* ||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 "arithmetics/nat.ma". include "basics/types.ma". include "basics/deqsets.ma". include "../src/ASM/Util.ma". inductive FunctionName : Type[0] ≝ | a_function_id : ℕ → FunctionName. inductive CallCostLabel : Type[0] ≝ | a_call_label : ℕ → CallCostLabel. inductive ReturnPostCostLabel : Type[0] ≝ | a_return_cost_label : ℕ → ReturnPostCostLabel. inductive NonFunctionalLabel : Type[0] ≝ | a_non_functional_label : ℕ → NonFunctionalLabel. inductive CostLabel : Type[0] ≝ | a_call : CallCostLabel → CostLabel | a_return_post : ReturnPostCostLabel → CostLabel | a_non_functional_label : NonFunctionalLabel → CostLabel | i_act : CostLabel. coercion a_call. coercion a_return_post. coercion a_non_functional_label. (* definition ret_act_label_to_cost_label : (ReturnPostCostLabel + NonFunctionalLabel) → CostLabel ≝ λx.match x with [inl a ⇒ a_return_post a | inr b ⇒ a_non_functional_label b]. coercion ret_act_label_to_cost_label. definition call_act_label_to_cost_label : (CallCostLabel + NonFunctionalLabel) → CostLabel ≝ λx.match x with [inl a ⇒ a_call a | inr b ⇒ a_non_functional_label b]. coercion call_act_label_to_cost_label. *) definition eq_nf_label : NonFunctionalLabel → NonFunctionalLabel → bool ≝ λx,y.match x with [ a_non_functional_label n ⇒ match y with [a_non_functional_label m ⇒ eqb n m ] ]. lemma eq_fn_label_elim : ∀P : bool → Prop.∀l1,l2 : NonFunctionalLabel. (l1 = l2 → P true) → (l1 ≠ l2 → P false) → P (eq_nf_label l1 l2). #P * #l1 * #l2 #H1 #H2 normalize @eqb_elim /3/ * #H3 @H2 % #EQ destruct @H3 % qed. definition DEQNonFunctionalLabel ≝ mk_DeqSet NonFunctionalLabel eq_nf_label ?. #x #y @eq_fn_label_elim [ #EQ destruct /2/] * #H % [ #EQ destruct] #H1 @⊥ @H assumption qed. unification hint 0 ≔ ; X ≟ DEQNonFunctionalLabel (* ---------------------------------------- *) ⊢ NonFunctionalLabel ≡ carr X. unification hint 0 ≔ p1,p2; X ≟ DEQNonFunctionalLabel (* ---------------------------------------- *) ⊢ eq_nf_label p1 p2 ≡ eqb X p1 p2. definition eq_function_name : FunctionName → FunctionName → bool ≝ λf1,f2.match f1 with [ a_function_id n ⇒ match f2 with [a_function_id m ⇒ eqb n m ] ]. lemma eq_function_name_elim : ∀P : bool → Prop.∀f1,f2. (f1 = f2 → P true) → (f1 ≠ f2 → P false) → P (eq_function_name f1 f2). #P * #f1 * #f2 #H1 #H2 normalize @eqb_elim /2/ * #H3 @H2 % #EQ destruct @H3 % qed. definition DEQFunctionName ≝ mk_DeqSet FunctionName eq_function_name ?. #x #y @eq_function_name_elim [ #EQ destruct /2/] * #H % [ #EQ destruct] #H1 @⊥ @H assumption qed. unification hint 0 ≔ ; X ≟ DEQFunctionName (* ---------------------------------------- *) ⊢ FunctionName ≡ carr X. unification hint 0 ≔ p1,p2; X ≟ DEQFunctionName (* ---------------------------------------- *) ⊢ eq_function_name p1 p2 ≡ eqb X p1 p2. definition eq_return_cost_lab : ReturnPostCostLabel → ReturnPostCostLabel → bool ≝ λc1,c2.match c1 with [a_return_cost_label n ⇒ match c2 with [ a_return_cost_label m ⇒ eqb n m]]. lemma eq_return_cost_lab_elim : ∀P : bool → Prop.∀c1,c2.(c1 = c2 → P true) → (c1 ≠ c2 → P false) → P (eq_return_cost_lab c1 c2). #P * #c1 * #c2 #H1 #H2 normalize @eqb_elim /2/ * #H @H2 % #EQ destruct @H % qed. definition DEQReturnPostCostLabel ≝ mk_DeqSet ReturnPostCostLabel eq_return_cost_lab ?. #x #y @eq_return_cost_lab_elim [ #EQ destruct /2/] * #H % [ #EQ destruct] #H1 @⊥ @H assumption qed. unification hint 0 ≔ ; X ≟ DEQReturnPostCostLabel (* ---------------------------------------- *) ⊢ ReturnPostCostLabel ≡ carr X. unification hint 0 ≔ p1,p2; X ≟ DEQReturnPostCostLabel (* ---------------------------------------- *) ⊢ eq_return_cost_lab p1 p2 ≡ eqb X p1 p2. definition eq_call_cost_lab : CallCostLabel → CallCostLabel → bool ≝ λc1,c2.match c1 with [a_call_label x ⇒ match c2 with [a_call_label y ⇒ eqb x y ]]. lemma eq_call_cost_lab_elim : ∀P : bool → Prop.∀c1,c2.(c1 = c2 → P true) → (c1 ≠ c2 → P false) → P (eq_call_cost_lab c1 c2). #P * #c1 * #c2 #H1 #H2 normalize @eqb_elim /2/ * #H @H2 % #EQ destruct @H % qed. definition DEQCallCostLabel ≝ mk_DeqSet CallCostLabel eq_call_cost_lab ?. #x #y @eq_call_cost_lab_elim [ #EQ destruct /2/] * #H % [ #EQ destruct] #H1 @⊥ @H assumption qed. unification hint 0 ≔ ; X ≟ DEQCallCostLabel (* ---------------------------------------- *) ⊢ CallCostLabel ≡ carr X. unification hint 0 ≔ p1,p2; X ≟ DEQCallCostLabel (* ---------------------------------------- *) ⊢ eq_call_cost_lab p1 p2 ≡ eqb X p1 p2. definition eq_costlabel : CostLabel → CostLabel → bool ≝ λc1.match c1 with [ a_call x1 ⇒ λc2.match c2 with [a_call y1 ⇒ x1 == y1 | _ ⇒ false ] | a_return_post x1 ⇒ λc2.match c2 with [ a_return_post y1 ⇒ x1 == y1 | _ ⇒ false ] | a_non_functional_label x1 ⇒ λc2.match c2 with [a_non_functional_label y1 ⇒ x1 == y1 | _ ⇒ false ] | i_act ⇒ λc2.match c2 with [i_act ⇒ true | _ ⇒ false ] ]. lemma eq_costlabel_elim : ∀P : bool → Prop.∀c1,c2.(c1 = c2 → P true) → (c1 ≠ c2 → P false) → P (eq_costlabel c1 c2). #P * [1,2,3: #c1 |] * [1,2,3,5,6,7,9,10,11,13,14,15: #c2 |*:] #H1 #H2 whd in match (eq_costlabel ??); try (@H2 % #EQ destruct) [ change with (eq_call_cost_lab ??) in ⊢ (?%); @eq_call_cost_lab_elim [ #EQ destruct @H1 % | * #H @H2 % #EQ destruct @H % ] | change with (eq_return_cost_lab ??) in ⊢ (?%); @eq_return_cost_lab_elim [ #EQ destruct @H1 % | * #H @H2 % #EQ destruct @H % ] | change with (eq_nf_label ??) in ⊢ (?%); @eq_fn_label_elim [ #EQ destruct @H1 % | * #H @H2 % #EQ destruct @H % ] | @H1 % ] qed. definition DEQCostLabel ≝ mk_DeqSet CostLabel eq_costlabel ?. #x #y @eq_costlabel_elim [ #EQ destruct /2/] * #H % [ #EQ destruct] #H1 @⊥ @H assumption qed. unification hint 0 ≔ ; X ≟ DEQCostLabel (* ---------------------------------------- *) ⊢ CostLabel ≡ carr X. unification hint 0 ≔ p1,p2; X ≟ DEQCostLabel (* ---------------------------------------- *) ⊢ eq_costlabel p1 p2 ≡ eqb X p1 p2. inductive ActionLabel : Type[0] ≝ | call_act : FunctionName → CallCostLabel → ActionLabel | ret_act : option(ReturnPostCostLabel) → ActionLabel | cost_act : option NonFunctionalLabel → ActionLabel. definition is_cost_label : ActionLabel → Prop ≝ λact.match act with [ cost_act nf ⇒ True | _ ⇒ False ]. inductive status_class : Type[0] ≝ | cl_jump : status_class | cl_io : status_class | cl_other : status_class. definition is_non_silent_cost_act : ActionLabel → Prop ≝ λact. ∃l. act = cost_act (Some ? l). record abstract_status : Type[2] ≝ { as_status :> Type[0] ; as_execute : ActionLabel → relation as_status ; as_syntactical_succ : relation as_status ; as_classify : as_status → status_class ; is_call_post_label : as_status → bool ; as_initial : as_status → bool ; as_final : as_status → bool ; jump_emits : ∀s1,s2,l. as_classify … s1 = cl_jump → as_execute l s1 s2 → is_non_silent_cost_act l ; io_entering : ∀s1,s2,l.as_classify … s2 = cl_io → as_execute l s1 s2 → is_non_silent_cost_act l ; io_exiting : ∀s1,s2,l.as_classify … s1 = cl_io → as_execute l s1 s2 → is_non_silent_cost_act l }. (* definition is_act_io_entering : abstract_status → ActionLabel → bool ≝ λS,l.match l with [ call_act f c ⇒ match c with [ inl _ ⇒ false | inr c' ⇒ is_io_entering S c' ] | ret_act x ⇒ match x with [ Some c ⇒ match c with [inl _ ⇒ false | inr c' ⇒ is_io_entering S c'] | None ⇒ false ] | cost_act x ⇒ match x with [ Some c ⇒ is_io_entering S c | None ⇒ false ] | init_act ⇒ false ]. definition is_act_io_exiting : abstract_status → ActionLabel → bool ≝ λS,l.match l with [ call_act f c ⇒ match c with [ inl _ ⇒ false | inr c' ⇒ is_io_exiting S c' ] | ret_act x ⇒ match x with [ Some c ⇒ match c with [inl _ ⇒ false | inr c' ⇒ is_io_exiting S c'] | None ⇒ false ] | cost_act x ⇒ match x with [ Some c ⇒ is_io_exiting S c | None ⇒ false ] | init_act ⇒ false ]. *) inductive raw_trace (S : abstract_status) : S → S → Type[0] ≝ | t_base : ∀st : S.raw_trace S st st | t_ind : ∀st1,st2,st3 : S.∀l : ActionLabel. as_execute S l st1 st2 → raw_trace S st2 st3 → raw_trace S st1 st3. definition is_cost_act : ActionLabel → Prop ≝ λact.∃l.act = cost_act l. definition is_call_act : ActionLabel → Prop ≝ λact.∃f,l.act = call_act f l. definition is_labelled_ret_act : ActionLabel → Prop ≝ λact.∃l.act = ret_act (Some ? l). definition is_unlabelled_ret_act : ActionLabel → Prop ≝ λact.act = ret_act (None ?). definition is_costlabelled_act : ActionLabel → Prop ≝ λact.match act with [ call_act _ _ ⇒ True | ret_act x ⇒ match x with [ Some _ ⇒ True | None ⇒ False ] | cost_act x ⇒ match x with [ Some _ ⇒ True | None ⇒ False ] ]. (* lemma well_formed_trace_inv : ∀S : abstract_status.∀st1,st2 : S.∀t : raw_trace S st1 st2. well_formed_trace … t → (st1 = st2 ∧ t ≃ t_base S st1) ∨ (∃st1'.∃l.∃prf : as_execute S l st1 st1'.∃tl : raw_trace S st1' st2. well_formed_trace … tl ∧ as_classify … st1 ≠ cl_jump ∧ t ≃ t_ind … prf … tl) ∨ (∃st1'.∃l.∃ prf : as_execute S l st1 st1'.∃ tl : raw_trace S st1' st2. well_formed_trace … tl ∧ is_non_silent_cost_act l ∧ t ≃ t_ind … prf … tl). (* ∨ (∃st1'.∃l.∃prf : as_execute S l st1 st1'.∃tl : raw_trace S st1' st2. well_formed_trace … tl ∧ as_classify … st1 = cl_io ∧ is_non_silent_cost_act l ∧ t ≃ t_ind … prf … tl).*) #S #st1 #st2 #t #H inversion H [ #st #EQ1 #EQ2 destruct(EQ1 EQ2) #EQ destruct(EQ) #_ /5 by refl_jmeq, or_introl, conj/ | #st1' #st2' #st3' #l #prf' #tl' #Htl #Hclass #_ #EQ2 #EQ3 #EQ4 destruct #_ % %2 %{st2'} %{l} %{prf'} %{tl'} /4 by conj/ | #st1' #st2' #st3' #l #prf #tl #Htl #Hl #_ #EQ2 #EQ3 #EQ4 destruct #_ %2 %{st2'} %{l} %{prf} %{tl} % // % // (*| #st1' #st2' #st3' #l #prf #tl #Htl #Hclass #is_non_silent #_ #EQ1 #EQ2 #EQ3 destruct #_ %2 %{st2'} %{l} %{prf} %{tl} /5 by conj/ *) ] qed. *) let rec append_on_trace (S : abstract_status) (st1 : S) (st2 : S) (st3 : S) (t1 : raw_trace S st1 st2) on t1 : raw_trace S st2 st3 → raw_trace S st1 st3 ≝ match t1 return λst1,st2,tr.raw_trace S st2 st3 → raw_trace S st1 st3 with [ t_base st ⇒ λt2.t2 | t_ind st1' st2' st3' l prf tl ⇒ λt2.t_ind … prf … (append_on_trace … tl t2) ]. interpretation "trace_append" 'append t1 t2 = (append_on_trace ???? t1 t2). lemma append_associative : ∀S,st1,st2,st3,st4. ∀t1 : raw_trace S st1 st2.∀t2 : raw_trace S st2 st3. ∀t3 : raw_trace S st3 st4.(t1 @ t2) @ t3 = t1 @ (t2 @ t3). #S #st1 #st2 #st3 #st4 #t1 elim t1 -t1 [ #st #t2 #t3 %] #st1' #st2' #st3' #l #prf #tl #IH #t2 #t3 whd in ⊢ (??%%); >IH % qed. definition trace_prefix: ∀S : abstract_status.∀st1,st2,st3 : S.raw_trace … st1 st2 → raw_trace … st1 st3 → Prop≝ λS,st1,st2,st3,t1,t2.∃t3 : raw_trace … st2 st3.t2 = t1 @ t3. definition trace_suffix : ∀S : abstract_status.∀st1,st2,st3 : S.raw_trace … st2 st3 → raw_trace … st1 st3 → Prop≝ λS,st1,st2,st3,t1,t2.∃t3 : raw_trace … st1 st2.t2 = t3 @ t1. inductive pre_silent_trace (S : abstract_status) : ∀st1,st2 : S.raw_trace S st1 st2 → Prop ≝ | silent_empty : ∀st : S.as_classify … st ≠ cl_io → pre_silent_trace … (t_base S st) | silent_cons : ∀st1,st2,st3 : S.∀prf : as_execute S (cost_act (None ?)) st1 st2. ∀tl : raw_trace S st2 st3. as_classify … st1 ≠ cl_io → pre_silent_trace … tl → pre_silent_trace … (t_ind … prf … tl). definition is_trace_non_empty : ∀S : abstract_status.∀st1,st2. raw_trace S st1 st2 → bool ≝ λS,st1,st2,t.match t with [ t_base _ ⇒ false | _ ⇒ true ]. definition silent_trace : ∀S:abstract_status.∀s1,s2 : S. raw_trace S s1 s2 → Prop ≝ λS,s1,s2,t.pre_silent_trace … t ∨ ¬ (bool_to_Prop (is_trace_non_empty … t)). lemma pre_silent_io : ∀S : abstract_status. ∀s1,s2 : S. ∀t : raw_trace … s1 s2. pre_silent_trace … t → as_classify … s2 ≠ cl_io. #S #s1 #s2 #t elim t [ #st #H inversion H // #st1 #st2 #st3 #prf #tl #H1 #sil_tl #_ #EQ1 #EQ2 #EQ3 destruct] #st1 #st2 #st3 #l #prf #tl #IH #H inversion H // #st1' #st2' #st3' #prf' #tl' #Hclass #silent_tl' #_ #EQ1 #EQ2 destruct #EQ destruct #_ @IH assumption qed. (* definition silent_trace : ∀S : abstract_status.∀st1,st2 : S. raw_trace S st1 st2 → Prop ≝ λS,st1,st2,t.pre_silent_trace … t ∧ well_formed_trace … t. lemma silent_is_well_formed : ∀S : abstract_status.∀st1,st2 : S. ∀t : raw_trace S st1 st2. silent_trace … t → well_formed_trace … t. #S #st1 #st2 #t * // qed. *) (* elim t -t [ #st #_ %] #st1' #st2' #st3' #l #prf #tl #IH * #H #cl %2 [2: >cl % #EQ destruct] @IH inversion H in ⊢ ?; [ #st #EQ1 #EQ2 #EQ3 destruct] #st1'' #st2'' #st3'' #prf' #tl' #H1 #Htl' #_ #EQ1 #EQ2 #EQ3 destruct #_ % [ assumption | #_ assumption] qed.*) inductive pre_measurable_trace (S : abstract_status) : ∀st1,st2 : S.raw_trace ? st1 st2 → Prop ≝ | pm_empty : ∀st : S. as_classify … st ≠ cl_io → pre_measurable_trace … (t_base ? st) | pm_cons_cost_act : ∀st1,st2,st3 : S.∀l : ActionLabel. ∀prf : as_execute S l st1 st2.∀tl : raw_trace S st2 st3. as_classify … st1 ≠ cl_io → is_cost_act l → pre_measurable_trace … tl → pre_measurable_trace … (t_ind … prf … tl) | pm_cons_lab_ret : ∀st1,st2,st3 : S.∀l : ActionLabel. as_classify … st1 ≠ cl_io → ∀prf : as_execute S l st1 st2.∀tl : raw_trace S st2 st3. is_labelled_ret_act l → pre_measurable_trace … tl → pre_measurable_trace … (t_ind … prf … tl) | pm_cons_post_call : ∀st1,st2,st3 : S.∀l : ActionLabel. ∀prf : as_execute S l st1 st2.∀tl : raw_trace S st2 st3. as_classify … st1 ≠ cl_io → is_call_act l → is_call_post_label … st1 → pre_measurable_trace … tl → pre_measurable_trace … (t_ind … prf … tl) | pm_balanced_call : ∀st1,st2,st3,st4,st5.∀l1,l2. ∀prf : as_execute S l1 st1 st2.∀t1 : raw_trace S st2 st3. ∀t2 : raw_trace S st4 st5.∀prf' : as_execute S l2 st3 st4. as_classify … st1 ≠ cl_io → as_classify … st3 ≠ cl_io → is_call_act l1 → ¬ is_call_post_label … st1 → pre_measurable_trace … t1 → pre_measurable_trace … t2 → as_syntactical_succ S st1 st4 → is_unlabelled_ret_act l2 → pre_measurable_trace … (t_ind … prf … (t1 @ (t_ind … prf' … t2))). lemma pre_measurable_trace_inv : ∀S : abstract_status. ∀st1,st2 : S.∀t : raw_trace … st1 st2. pre_measurable_trace … t → (st1 = st2 ∧ as_classify … st1 ≠ cl_io ∧ t ≃ t_base … st1) ∨ (∃st1' : S.∃l.∃prf : as_execute S l st1 st1'.∃tl. t = t_ind … prf … tl ∧ as_classify … st1 ≠ cl_io ∧ is_cost_act l ∧ pre_measurable_trace … tl) ∨ (∃st1' : S.∃l.∃prf : as_execute S l st1 st1'.∃tl. t = t_ind … prf … tl ∧ as_classify … st1 ≠ cl_io ∧ is_labelled_ret_act l ∧ pre_measurable_trace … tl) ∨ (∃st1' : S .∃l.∃prf : as_execute S l st1 st1'.∃tl. t = t_ind … prf … tl ∧ as_classify … st1 ≠ cl_io ∧ is_call_act l ∧ (bool_to_Prop (is_call_post_label … st1)) ∧ pre_measurable_trace … tl) ∨ (∃st1',st1'',st1''' : S.∃l1,l2.∃prf : as_execute S l1 st1 st1'. ∃t1 : raw_trace S st1' st1''.∃t2 : raw_trace S st1''' st2. ∃prf' : as_execute S l2 st1'' st1'''. t = t_ind … prf … (t1 @ (t_ind … prf' … t2)) ∧ as_classify … st1 ≠cl_io ∧ as_classify … st1'' ≠ cl_io ∧ is_call_act l1 ∧ bool_to_Prop (¬ is_call_post_label … st1) ∧ pre_measurable_trace … t1 ∧ pre_measurable_trace … t2 ∧ as_syntactical_succ S st1 st1''' ∧ is_unlabelled_ret_act l2). #S #st1 #st2 #t #H inversion H [ #st #Hclass #EQ1 #EQ2 destruct #EQ destruct #_ %%%%% // % // | #st1' #st2' #st3' #l #prf #tl #Hst1' #Hl #Htl #_ #EQ1 #EQ2 #EQ3 destruct #_ %%%%2 %{st2'} %{l} %{prf} %{tl} % // % // % // | #st1' #st2' #st3' #l #Hst1 #prf #tl #Hl #Htl #_ #EQ1 #EQ2 #EQ3 destruct #_ %%%2 %{st2'} %{l} %{prf} %{tl} % // % // % // | #st1' #st2' #st3' #l #prf #tl #Hst1 #Hl #H1st1 #Htl #_ #EQ1 #EQ2 #EQ3 destruct #_ % %2 %{st2'} %{l} %{prf} %{tl} % // % // % // % // | #st1' #st2' #st3' #st4' #st5' #l1 #l2 #prf #t1 #t2 #prf' #Hst1' #Hst3' #Hl1 #H1st1' #Ht1 #Ht2 #succ #Hl2 #_ #_ #EQ1 #EQ2 #EQ3 destruct #_ %2 %{st2'} %{st3'} %{st4'} %{l1} %{(ret_act (None ?))} %{prf} %{t1} %{t2} %{prf'} /12 by conj/ ] qed.