Changeset 3371 for src/joint/lineariseProof.ma
 Timestamp:
 Jun 26, 2013, 2:22:28 PM (7 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/joint/lineariseProof.ma
r2808 r3371 18 18 include "joint/semanticsUtils.ma". 19 19 include "common/ExtraMonads.ma". 20 (* 21 !!!SPOSTATO IN extraGlobalenvs.ma!!!! 22 23 include alias "common/PositiveMap.ma". 24 25 lemma add_functs_functions_miss : ∀F. ∀ge : genv_t F.∀ l.∀ id. 26 id < (nextfunction ? ge) → 27 lookup_opt … id (functions ? ge) = None ? → 28 lookup_opt … id (functions … (add_functs F ge l)) = None ?. 29 #F #ge #l #id whd in match add_functs; normalize nodelta 30 elim l l [ #_ normalize //] 31 * #id1 #f1 #tl #IND #H #H1 whd in match (foldr ?????); 32 >lookup_opt_insert_miss [ inversion(lookup_opt ? ? ?) [ #_ %] 33 #f1 #H3 <(drop_fn_lfn … f1 H3) @(IND H H1) 34  cut(nextfunction F ge ≤ nextfunction F (foldr … (add_funct F) ge tl)) 35 [elim tl [normalize //] 36 #x #tl2 whd in match (foldr ?????) in ⊢ (? → %); #H %2{H} ] 37 #H2 lapply(transitive_le … H H2) @lt_to_not_eq 38 qed. 39 40 lemma add_globals_functions_miss : ∀F,V,init. ∀gem : genv_t F × mem.∀ id,l. 41 lookup_opt … id (functions ? (\fst gem)) = None ? → 42 lookup_opt … id (functions … (\fst (add_globals F V init gem l))) = None ?. 43 #F #V #init * #ge #m #id #l lapply ge ge lapply m m elim l [ #ge #m #H @H] 44 ** #x1 #x2 #x3 #tl whd in match add_globals; 45 normalize nodelta #IND #m #ge #H whd in match (foldl ?????); normalize nodelta 46 cases(alloc m ? ? x2) #m1 #bl1 normalize nodelta @IND whd in match add_symbol; 47 normalize nodelta inversion(lookup_opt ? ? ?) [ #_ %] 48 #f1 #H3 <(drop_fn_lfn … f1 H3) assumption 49 qed. 50 51 52 lemma globalenv_no_minus_one : 53 ∀F,V,i,p. 54 find_funct_ptr … (globalenv F V i p) (mk_block Code (1)) = None ?. 55 #F #V #i #p 56 whd in match find_funct_ptr; normalize nodelta 57 whd in match globalenv; 58 whd in match globalenv_allocmem; normalize nodelta 59 @add_globals_functions_miss @add_functs_functions_miss normalize // 60 qed. 61 *) 62 63 (* !!!spostato in semantics.ma ed aggiunto un include a extraGlobalenvs.ma!!! 64 65 lemma fetch_internal_function_no_minus_one : 66 ∀F,V,i,p,bl. 67 block_id (pi1 … bl) = 1 → 68 fetch_internal_function … (globalenv (λvars.fundef (F vars)) V i p) 69 bl = Error … [MSG BadFunction]. 70 #F#V#i#p ** #r #id #EQ1 #EQ2 destruct 71 whd in match fetch_internal_function; 72 whd in match fetch_function; normalize nodelta 73 >globalenv_no_minus_one 74 cases (symbol_for_block ???) normalize // 75 qed. 76 77 *) 78 79 (*spostato in ExtraMonads.ma 80 81 lemma bind_option_inversion_star: 82 ∀A,B: Type[0].∀P : Prop.∀f: option A. ∀g: A → option B. ∀y: B. 83 (∀x.f = Some … x → g x = Some … y → P) → 84 (! x ← f ; g x = Some … y) → P. 85 #A #B #P #f #g #y #H #G elim (option_bind_inverse ????? G) #x * @H qed. 86 87 interpretation "option bind inversion" 'bind_inversion = 88 (bind_option_inversion_star ???????). 89 90 lemma bind_inversion_star : ∀X,Y.∀P : Prop. 91 ∀m : res X.∀f : X → res Y.∀v : Y. 92 (∀x. m = return x → f x = return v → P) → 93 ! x ← m ; f x = return v → P. 94 #X #Y #P #m #f #v #H #G 95 elim (bind_inversion ????? G) #x * @H qed. 96 97 interpretation "res bind inversion" 'bind_inversion = 98 (bind_inversion_star ???????). 99 100 lemma IO_bind_inversion: 101 ∀O,I,A,B.∀P : Prop.∀f: IO O I A. ∀g: A → IO O I B. ∀y: B. 102 (∀x.f = return x → g x = return y → P) → 103 (! x ← f ; g x = return y) → P. 104 #O #I #A #B #P #f #g #y cases f normalize 105 [ #o #f #_ #H destruct 106  #a #G #H @(G ? (refl …) H) 107  #e #_ #H destruct 108 ] qed. 109 110 interpretation "IO bind inversion" 'bind_inversion = 111 (IO_bind_inversion ?????????). 112 113 record MonadFunctRel (M1 : Monad) (M2 : Monad) : Type[1] ≝ 114 { m_frel :6> ∀X,Y.∀P : X → Prop.(∀x.P x → Y) → (M1 X → M2 Y → Prop) 115 ; mfr_return : ∀X,Y,P,F,x,prf.m_frel X Y P F (return x) (return (F x prf)) 116 ; mfr_bind : ∀X,Y,Z,W,P,Q,F,G,m,n. 117 m_frel X Y P F m n → ∀f,g.(∀x,prf.m_frel Z W Q G (f x) (g (F x prf))) → 118 m_frel ?? Q G (m_bind … m f) (m_bind … n g) 119 ; m_frel_ext : ∀X,Y,P,F,G.(∀x,prf1,prf2.F x prf1 = G x prf2) → ∀u,v.m_frel X Y P F u v → m_frel X Y P G u v 120 }. 121 122 *) 123 124 (*definition IO_preserve : ∀O,I.MonadFunctRel (IOMonad O I) (IOMonad O I) ≝ 125 λO,I.mk_MonadFunctRel ?? 126 (λX,Y,F,m,n.∀x.m = return x → n = return F x) 127 ???. 128 [ #X #Y #F #x #y whd in ⊢ (??%%→?); #EQ destruct(EQ) % 129  #X #Y #Z #W #F #G * 130 [ #o #f  #u  #e ] #n #H #f #g #K #x 131 whd in ⊢ (??%%→?); #EQ destruct(EQ) 132 >(H ? (refl …)) @K @EQ 133  #X #Y #P #Q #H #z #w #G #x #EQ >(G … EQ) >H % 134 ] 135 qed.*) 136 137 (* spostato in ExtraMonads.ma 138 definition res_preserve : MonadFunctRel Res Res ≝ 139 mk_MonadFunctRel ?? 140 (λX,Y,P,F,m,n.∀x.m = return x → ∃prf.n = return F x prf) 141 ???. 142 [ #X #Y #P #F #x #prf #x' whd in ⊢ (??%%→?); #EQ destruct(EQ) %{prf} % 143  #X #Y #Z #W #P #Q #F #G * 144 [ #u  #e ] #n #H #f #g #K #x 145 whd in ⊢ (??%%→?); #EQ destruct(EQ) 146 cases (H ? (refl …)) #prf #L >L @(K ? prf ? EQ) 147  #X #Y #P #F #G #H #u #v #K #x #EQ 148 cases (K … EQ) #prf #EQ' %{prf} >EQ' >H try % 149 ] 150 qed. 151 152 definition opt_preserve : MonadFunctRel Option Option ≝ 153 mk_MonadFunctRel ?? 154 (λX,Y,P,F,m,n.∀x.m = return x → ∃prf.n = return F x prf) 155 ???. 156 [ #X #Y #P #F #x #prf #x' whd in ⊢ (??%%→?); #EQ destruct(EQ) %{prf} % 157  #X #Y #Z #W #P #Q #F #G * 158 [  #u ] #n #H #f #g #K #x 159 whd in ⊢ (??%%→?); #EQ destruct(EQ) 160 cases (H ? (refl …)) #prf #L >L @(K ? prf ? EQ) 161  #X #Y #P #F #G #H #u #v #K #x #EQ 162 cases (K … EQ) #prf #EQ' %{prf} >EQ' >H try % 163 ] 164 qed. 165 166 definition io_preserve : ∀O,I.MonadFunctRel (IOMonad O I) (IOMonad O I) ≝ 167 λO,I.mk_MonadFunctRel ?? 168 (λX,Y,P,F,m,n.∀x.m = return x → ∃prf.n = return F x prf) 169 ???. 170 [ #X #Y #P #F #x #prf #x' whd in ⊢ (??%%→?); #EQ destruct(EQ) %{prf} % 171  #X #Y #Z #W #P #Q #F #G * 172 [ #o #f  #u  #e ] #n #H #f #g #K #x 173 whd in ⊢ (??%%→?); #EQ destruct(EQ) 174 cases (H ? (refl …)) #prf #L >L @(K ? prf ? EQ) 175  #X #Y #P #F #G #H #u #v #K #x #EQ 176 cases (K … EQ) #prf #EQ' %{prf} >EQ' >H try % 177 ] 178 qed. 179 180 definition preserving ≝ 181 λM1,M2.λFR : MonadFunctRel M1 M2. 182 λX,Y,A,B : Type[0]. 183 λP : X → Prop. 184 λQ : A → Prop. 185 λF : ∀x : X.P x → Y. 186 λG : ∀a : A.Q a → B. 187 λf : X → M1 A. 188 λg : Y → M2 B. 189 ∀x,prf. 190 FR … G 191 (f x) (g (F x prf)). 192 193 definition preserving2 ≝ 194 λM1,M2.λFR : MonadFunctRel M1 M2. 195 λX,Y,Z,W,A,B : Type[0]. 196 λP : X → Prop. 197 λQ : Y → Prop. 198 λR : A → Prop. 199 λF : ∀x : X.P x → Z. 200 λG : ∀y : Y.Q y → W. 201 λH : ∀a : A.R a → B. 202 λf : X → Y → M1 A. 203 λg : Z → W → M2 B. 204 ∀x,y,prf1,prf2. 205 FR … H 206 (f x y) (g (F x prf1) (G y prf2)). 207 *) 20 21 check mk_sem_graph_params 208 22 209 23 definition graph_prog_params ≝ 210 λp,p',prog,stack_sizes. 211 mk_prog_params (mk_sem_graph_params p p') prog stack_sizes. 24 λp,p',pre_main,prog,stack_sizes. 25 mk_prog_params (mk_sem_graph_params p p' pre_main) prog stack_sizes. 26 27 check mk_sem_graph_params 212 28 213 29 definition graph_abstract_status: 214 ∀p:uns erialized_params.30 ∀p:uns_params. 215 31 (∀F.sem_unserialized_params p F) → 32 (∀prog : joint_program (mk_graph_params p). 33 joint_closed_internal_function (mk_graph_params p) (prog_names … prog)) → 216 34 ∀prog : joint_program (mk_graph_params p). 217 35 (ident → option ℕ) → 218 36 abstract_status 219 ≝ 220 λp,p',pr og,stack_sizes.221 joint_abstract_status (graph_prog_params ? p' pr og stack_sizes).37 ≝ 38 λp,p',pre_main,prog,stack_sizes. 39 joint_abstract_status (graph_prog_params ? p' pre_main prog stack_sizes). 222 40 223 41 definition lin_prog_params ≝ 224 λp,p',pr og,stack_sizes.225 mk_prog_params (mk_sem_lin_params p p' ) prog stack_sizes.42 λp,p',pre_main,prog,stack_sizes. 43 mk_prog_params (mk_sem_lin_params p p' pre_main) prog stack_sizes. 226 44 227 45 definition lin_abstract_status: 228 ∀p:uns erialized_params.46 ∀p:uns_params. 229 47 (∀F.sem_unserialized_params p F) → 48 (∀prog : joint_program (mk_lin_params p). 49 joint_closed_internal_function (mk_lin_params p) (prog_names … prog)) → 230 50 ∀prog : joint_program (mk_lin_params p). 231 51 (ident → option ℕ) → 232 52 abstract_status 233 53 ≝ 234 λp,p',pr og,stack_sizes.235 joint_abstract_status (lin_prog_params ? p' pr og stack_sizes).54 λp,p',pre_main,prog,stack_sizes. 55 joint_abstract_status (lin_prog_params ? p' pre_main prog stack_sizes). 236 56 237 57 (*
Note: See TracChangeset
for help on using the changeset viewer.