Changeset 1516 for src/common
- Timestamp:
- Nov 19, 2011, 12:38:20 AM (9 years ago)
- Location:
- src/common
- Files:
-
- 9 edited
-
AST.ma (modified) (5 diffs)
-
Events.ma (modified) (1 diff)
-
FrontEndOps.ma (modified) (1 diff)
-
GenMem.ma (modified) (1 diff)
-
Identifiers.ma (modified) (4 diffs)
-
Integers.ma (modified) (1 diff)
-
Mem.ma (modified) (9 diffs)
-
Pointers.ma (modified) (3 diffs)
-
PositiveMap.ma (modified) (6 diffs)
Legend:
- Unmodified
- Added
- Removed
-
src/common/AST.ma
r1465 r1516 145 145 lemma eq_intsize_elim : ∀sz1,sz2. ∀P:bool → Type[0]. 146 146 (sz1 ≠ sz2 → P false) → (sz1 = sz2 → P true) → P (eq_intsize sz1 sz2). 147 * * #P #Hne #Heq whd in ⊢ (?%) try (@Heq @refl) @Hne % #E destruct147 * * #P #Hne #Heq whd in ⊢ (?%); try (@Heq @refl) @Hne % #E destruct 148 148 qed. 149 149 … … 175 175 (sz1 ≠ sz2 → Q d) → (∀E:sz1 = sz2. match sym_eq ??? E return λx.λ_.P x → Type[0] with [ refl ⇒ λp. Q (f p) ] p ) → Q (intsize_eq_elim A sz1 sz2 P p f d). 176 176 #A * * #P #p #f #d #Q #Hne #Heq 177 [ 1,5,9: whd in ⊢ (?%) @(Heq (refl ??))178 | *: whd in ⊢ (?%) @Hne % #E destruct177 [ 1,5,9: whd in ⊢ (?%); @(Heq (refl ??)) 178 | *: whd in ⊢ (?%); @Hne % #E destruct 179 179 ] qed. 180 180 … … 351 351 #A #B #C #f #l elim l 352 352 [ #l' #E normalize in E; destruct % 353 | * #a #b #tl #IH #l' normalize in ⊢ (??%? → ?) cases (f b) normalize in ⊢ (? → ??%? → ?)353 | * #a #b #tl #IH #l' normalize in ⊢ (??%? → ?); cases (f b) normalize in ⊢ (? → ??%? → ?); 354 354 [2: #err #E destruct 355 355 | #c change with (match map_partial … f tl with [ OK x ⇒ ? | Error y ⇒ ?] = ? → ?) 356 cases (map_partial … f tl) in IH ⊢ % 357 #x #IH normalize in ⊢ (??%? → ?) #ABS destruct normalize356 cases (map_partial … f tl) in IH ⊢ %; 357 #x #IH normalize in ⊢ (??%? → ?); #ABS destruct normalize 358 358 >(IH x) // ]] 359 359 qed. … … 487 487 [ #l' elim l' // #he #tl #IH #ABS normalize in ABS; destruct 488 488 | #he1 #tl1 #IH #l' cases l' [ #ABS normalize in ABS; destruct ] 489 #he2 #tl2 #EQ whd in EQ:(??%%) ⊢ (??%%) >(IH tl2) destruct normalize in e1 ⊢ %>e0 //489 #he2 #tl2 #EQ whd in EQ:(??%%) ⊢ (??%%); >(IH tl2) destruct normalize in e1 ⊢ %; >e0 // 490 490 >e0 in e1; normalize #H @H ] 491 491 qed. … … 498 498 do fl ← map_partial … (*prefix_funct_name*) transf_partial_function (prog_funct ?? p); ?. 499 499 (*CSC: interactive mode because of dependent types *) 500 generalize in match (map_partial_preserves_first … transf_partial_variable (prog_vars … p)) 500 generalize in match (map_partial_preserves_first … transf_partial_variable (prog_vars … p)); 501 501 cases (map_partial … transf_partial_variable (prog_vars … p)) 502 502 [ #vl #EQ -
src/common/Events.ma
r961 r1516 155 155 ]. 156 156 [ *; #NE @False_rect_Type0 @NE @refl 157 | % #E' >E' in E #E whd in E:(??%%); destruct (E);157 | % #E' >E' in E; #E whd in E:(??%%); destruct (E); 158 158 ] qed. 159 159 -
src/common/FrontEndOps.ma
r1410 r1516 139 139 val_typ v' t'. 140 140 #t #t' #op elim op 141 [ #sz #sg #sz' #sg' #v #v' #H @(elim_val_typ … H) #i whd in ⊢ (??%? → ?) 142 cases sg whd in ⊢ (??%? → ?) #E' destruct %143 | #sz #sg #v #v' #H @(elim_val_typ … H) #i whd in ⊢ (??%? → ?) #E' destruct %141 [ #sz #sg #sz' #sg' #v #v' #H @(elim_val_typ … H) #i whd in ⊢ (??%? → ?); 142 cases sg whd in ⊢ (??%? → ?); #E' destruct % 143 | #sz #sg #v #v' #H @(elim_val_typ … H) #i whd in ⊢ (??%? → ?); #E' destruct % 144 144 | #t'' #sz #sg cases t'' 145 [ #sz' #sg' #H #v #v' #H1 @(elim_val_typ … H1) #i whd in ⊢ (??%? → ?) #E' destruct cases (eq_bv ???) whd in ⊢ (?%?)%145 [ #sz' #sg' #H #v #v' #H1 @(elim_val_typ … H1) #i whd in ⊢ (??%? → ?); #E' destruct cases (eq_bv ???) whd in ⊢ (?%?); % 146 146 | #r #H #v #v' #H1 @(elim_val_typ … H1) whd % 147 [ whd in ⊢ (??%? → ?) #E' destruct; %148 | #b #c #o whd in ⊢ (??%? → ?) #E' destruct %147 [ whd in ⊢ (??%? → ?); #E' destruct; % 148 | #b #c #o whd in ⊢ (??%? → ?); #E' destruct % 149 149 ] 150 150 | #f * 151 151 ] 152 | #sz #sg #v #v' #H @(elim_val_typ … H) #i whd in ⊢ (??%? → ?) #E destruct %153 | #sz #v #v' #H @(elim_val_typ … H) #f whd in ⊢ (??%? → ?) #E destruct %2154 | #sz #v #v' #H @(elim_val_typ … H) #f whd in ⊢ (??%? → ?) #E destruct %2155 | #v #v' #H @(elim_val_typ … H) #f whd in ⊢ (??%? → ?) #E destruct %2156 | #fsz #sz #v #v' #H @(elim_val_typ … H) #f whd in ⊢ (??%? → ?) #E destruct %157 | #fsz #sz #v #v' #H @(elim_val_typ … H) #f whd in ⊢ (??%? → ?) #E destruct %158 | #fsz #sz #v #v' #H @(elim_val_typ … H) #i whd in ⊢ (??%? → ?) #E destruct %2159 | #fsz #sz #v #v' #H @(elim_val_typ … H) #i whd in ⊢ (??%? → ?) #E destruct %2160 | #t'' #v #v' #H whd in ⊢ (??%? → ?) #E destruct @H161 | #sz #sg #r #v #v' #H @(elim_val_typ … H) #i whd in ⊢ (??%? → ?) cases (eq_bv ???)162 whd in ⊢ (??%? → ?) #E destruct //152 | #sz #sg #v #v' #H @(elim_val_typ … H) #i whd in ⊢ (??%? → ?); #E destruct % 153 | #sz #v #v' #H @(elim_val_typ … H) #f whd in ⊢ (??%? → ?); #E destruct %2 154 | #sz #v #v' #H @(elim_val_typ … H) #f whd in ⊢ (??%? → ?); #E destruct %2 155 | #v #v' #H @(elim_val_typ … H) #f whd in ⊢ (??%? → ?); #E destruct %2 156 | #fsz #sz #v #v' #H @(elim_val_typ … H) #f whd in ⊢ (??%? → ?); #E destruct % 157 | #fsz #sz #v #v' #H @(elim_val_typ … H) #f whd in ⊢ (??%? → ?); #E destruct % 158 | #fsz #sz #v #v' #H @(elim_val_typ … H) #i whd in ⊢ (??%? → ?); #E destruct %2 159 | #fsz #sz #v #v' #H @(elim_val_typ … H) #i whd in ⊢ (??%? → ?); #E destruct %2 160 | #t'' #v #v' #H whd in ⊢ (??%? → ?); #E destruct @H 161 | #sz #sg #r #v #v' #H @(elim_val_typ … H) #i whd in ⊢ (??%? → ?); cases (eq_bv ???) 162 whd in ⊢ (??%? → ?); #E destruct // 163 163 | #sz #sg #r #v #v' #H @(elim_val_typ … H) % 164 [ whd in ⊢ (??%? → ?) #E destruct %165 | #b #c #o whd in ⊢ (??%? → ?) #E destruct164 [ whd in ⊢ (??%? → ?); #E destruct % 165 | #b #c #o whd in ⊢ (??%? → ?); #E destruct 166 166 ] 167 167 ] qed. -
src/common/GenMem.ma
r1395 r1516 53 53 ∀A: Type[0]. ∀x: block. ∀v: A. ∀f: block -> A. 54 54 update_block … x v f x = v. 55 #A * * #ix #v #f whd in ⊢ (??%?) 55 #A * * #ix #v #f whd in ⊢ (??%?); 56 56 >eq_block_b_b // 57 57 qed. -
src/common/Identifiers.ma
r1515 r1516 56 56 57 57 lemma eq_identifier_refl : ∀tag,id. eq_identifier tag id id = true. 58 #tag * #id whd in ⊢ (??%?) >eqb_n_n @refl58 #tag * #id whd in ⊢ (??%?); >eqb_n_n @refl 59 59 qed. 60 60 … … 64 64 65 65 definition identifier_eq : ∀tag:String. ∀x,y:identifier tag. (x=y) + (x≠y). 66 #tag * #x * #y lapply (refl ? (eqb x y)) cases (eqb x y) in ⊢ (???% → %) 66 #tag * #x * #y lapply (refl ? (eqb x y)) cases (eqb x y) in ⊢ (???% → %); 67 67 #E [ % | %2 ] 68 68 lapply E @eqb_elim … … 184 184 ] (refl ? u'). 185 185 cases l in p E; cases m; -l' -m' #m' #l' 186 whd in ⊢ (% → ?) 187 whd in ⊢ (?(??(???%%)?) → ??(??%?%)? → ?) 186 whd in ⊢ (% → ?); 187 whd in ⊢ (?(??(???%%)?) → ??(??%?%)? → ?); 188 188 #NL #U cases NL #H @H @(update_fail … U) 189 189 qed. … … 194 194 present tag A (update_present tag A m id' H' a) id. 195 195 #tag #A * #m * #id #a * #id' #H #H' 196 whd whd in ⊢ (?(??(???(%??????)?)?)) normalize nodelta196 whd whd in ⊢ (?(??(???(%??????)?)?)); normalize nodelta 197 197 cases (identifier_eq ? (an_identifier tag id) (an_identifier tag id')) 198 [ #E >E @refute_none_by_refl #m' #U whd in ⊢ (?(??%?)) >(update_lookup_opt_same ????? U)198 [ #E >E @refute_none_by_refl #m' #U whd in ⊢ (?(??%?)); >(update_lookup_opt_same ????? U) 199 199 % #E' destruct 200 | #NE @refute_none_by_refl #m' #U whd in ⊢ (?(??%?)) whd in ⊢ (?(??(??%%)?))200 | #NE @refute_none_by_refl #m' #U whd in ⊢ (?(??%?)); whd in ⊢ (?(??(??%%)?)); 201 201 <(update_lookup_opt_other ????? U id) [ @H | % #E cases NE >E #H @H @refl ] 202 202 ] qed. -
src/common/Integers.ma
r1512 r1516 124 124 125 125 lemma eq_dec: ∀x,y: int. (x = y) + (x ≠ y). 126 #x #y lapply (refl ? (eq_bv ? x y)) cases (eq_bv ? x y) in ⊢ (???% → ?) #E126 #x #y lapply (refl ? (eq_bv ? x y)) cases (eq_bv ? x y) in ⊢ (???% → ?); #E 127 127 [ %1 lapply E @(eq_bv_elim … x y) [ // | #_ #X destruct ] 128 128 | %2 lapply E @(eq_bv_elim … x y) [ #_ #X destruct | /2/ ] -
src/common/Mem.ma
r891 r1516 66 66 ∀A: Type[0]. ∀x: block. ∀v: A. ∀f: block -> A. 67 67 update_block … x v f x = v. 68 #A * * #ix #v #f whd in ⊢ (??%?) 68 #A * * #ix #v #f whd in ⊢ (??%?); 69 69 >eq_block_b_b // 70 70 qed. … … 192 192 lemma align_size_chunk_divides: 193 193 ∀chunk. (align_chunk chunk ∣ size_chunk chunk). 194 #chunk cases chunk;[8:#r cases r ]normalize;/3 /;194 #chunk cases chunk;[8:#r cases r ]normalize;/3 by witness/; 195 195 qed. 196 196 … … 735 735 lemma valid_not_valid_diff: 736 736 ∀m,b,b'. valid_block m b → ¬(valid_block m b') → b ≠ b'. 737 #m #b #b' #H #H' @nmk #e >e in H #H737 #m #b #b' #H #H' @nmk #e >e in H; #H 738 738 @(absurd ? H H') 739 739 qed. … … 759 759 #m #chunk #chunk2 #r #b #ofs #H1 #H2 760 760 elim H2;#H3 #H4 #H5 #H6 #H7 761 >H1 in H5 #H5761 >H1 in H5; #H5 762 762 % //; 763 763 <(align_chunk_compat … H1) //; … … 807 807 #b' cases (store_inv … STORE) 808 808 #H1 #H2 >H2 809 whd in ⊢ (??(?%?)?) whd in ⊢ (??%?)810 whd in ⊢ (??(?%)?) @eq_block_elim #E809 whd in ⊢ (??(?%?)?); whd in ⊢ (??%?); 810 whd in ⊢ (??(?%)?); @eq_block_elim #E 811 811 normalize // 812 812 qed. … … 864 864 #chunk #m1 #r #b #ofs #v #m2 #STORE 865 865 #chunk' #r' #b' #ofs' 866 * Hv;866 * as Hv 867 867 #Hvb #Hl #Hr #Halign #Hptr 868 868 % //; … … 878 878 #chunk #m1 #r #b #ofs #v #m2 #STORE 879 879 #chunk' #r' #b' #ofs' 880 * Hv;880 * as Hv 881 881 #Hvb #Hl #Hr #Halign #Hcompat 882 882 % //; … … 3514 3514 ∀m,a,v. 3515 3515 storev Mint8signed m a v = storev Mint8unsigned m a v. 3516 #m #a #v whd in ⊢ (??%%) elim a //3517 #r #b #p #ofs whd in ⊢ (??%%) 3516 #m #a #v whd in ⊢ (??%%); elim a // 3517 #r #b #p #ofs whd in ⊢ (??%%); 3518 3518 >(in_bounds_equiv Mint8signed Mint8unsigned … (option mem) ???) // 3519 3519 qed. … … 3522 3522 ∀m,a,v. 3523 3523 storev Mint16signed m a v = storev Mint16unsigned m a v. 3524 #m #a #v whd in ⊢ (??%%) elim a //3525 #r #b #p #ofs whd in ⊢ (??%%) 3524 #m #a #v whd in ⊢ (??%%); elim a // 3525 #r #b #p #ofs whd in ⊢ (??%%); 3526 3526 >(in_bounds_equiv Mint16signed Mint16unsigned … (option mem) ???) // 3527 3527 qed. -
src/common/Pointers.ma
r1215 r1516 34 34 P (eq_block b1 b2). 35 35 #P * #r1 #i1 * #r2 #i2 #H1 #H2 36 whd in ⊢ (?%) @eq_region_elim #H337 [ whd in ⊢ (?%) @eqZb_elim [ /2/ | * #NE @H2 % #E @NE destruct % ]36 whd in ⊢ (?%); @eq_region_elim #H3 37 [ whd in ⊢ (?%); @eqZb_elim [ /2/ | * #NE @H2 % #E @NE destruct % ] 38 38 | @H2 % #E destruct elim H3 /2/ 39 39 ] qed. 40 40 41 41 lemma eq_block_b_b : ∀b. eq_block b b = true. 42 * * #z whd in ⊢ (??%?) >eqZb_z_z @refl42 * * #z whd in ⊢ (??%?); >eqZb_z_z @refl 43 43 qed. 44 44 … … 71 71 72 72 lemma reflexive_eq_offset: ∀x. eq_offset x x = true. 73 whd in match eq_offset /2/73 whd in match eq_offset; /2/ 74 74 qed. 75 75 … … 109 109 110 110 lemma reflexive_eq_pointer: ∀p. eq_pointer p p = true. 111 #p whd in ⊢ (??%?) >eq_block_b_b >reflexive_eq_region >reflexive_eq_offset //111 #p whd in ⊢ (??%?); >eq_block_b_b >reflexive_eq_region >reflexive_eq_offset // 112 112 qed. -
src/common/PositiveMap.ma
r1515 r1516 62 62 [ * // 63 63 | #tl #IH * 64 [ whd in ⊢ (??%%) @IH64 [ whd in ⊢ (??%%); @IH 65 65 | #x #l #r @IH 66 66 ] 67 67 | #tl #IH * 68 [ whd in ⊢ (??%%) @IH68 [ whd in ⊢ (??%%); @IH 69 69 | #x #l #r @IH 70 70 ] … … 80 80 | #b' #IH * 81 81 [ * [ #NE @refl | #x #l #r #NE @refl ] 82 | #c' * [ #NE whd in ⊢ (??%%) @IH /2/83 | #x #l #r #NE whd in ⊢ (??%%) @IH /2/82 | #c' * [ #NE whd in ⊢ (??%%); @IH /2/ 83 | #x #l #r #NE whd in ⊢ (??%%); @IH /2/ 84 84 ] 85 85 | #c' * // … … 88 88 [ * [ #NE @refl | #x #l #r #NE @refl ] 89 89 | #c' * // 90 | #c' * [ #NE whd in ⊢ (??%%) @IH /2/91 | #x #l #r #NE whd in ⊢ (??%%) @IH /2/90 | #c' * [ #NE whd in ⊢ (??%%); @IH /2/ 91 | #x #l #r #NE whd in ⊢ (??%%); @IH /2/ 92 92 ] 93 93 ] … … 110 110 [ * [ // | * // #x #l #r normalize #E destruct ] 111 111 | #b' #IH * [ // | #x #l #r #U @IH whd in U:(??%?); 112 cases (update A b' a r) in U ⊢ % 112 cases (update A b' a r) in U ⊢ %; 113 113 [ // | normalize #t #E destruct ] 114 114 ] 115 115 | #b' #IH * [ // | #x #l #r #U @IH whd in U:(??%?); 116 cases (update A b' a l) in U ⊢ % 116 cases (update A b' a l) in U ⊢ %; 117 117 [ // | normalize #t #E destruct ] 118 118 ] … … 124 124 #A #b #a elim b 125 125 [ * [ #t' normalize #E destruct 126 | * [ 2: #x ] #l #r #t' whd in ⊢ (??%? → ??%?) 126 | * [ 2: #x ] #l #r #t' whd in ⊢ (??%? → ??%?); 127 127 #E destruct // 128 128 ] 129 129 | #b' #IH * 130 130 [ #t' normalize #E destruct 131 | #x #l #r #t' whd in ⊢ (??%? → ??%?) 131 | #x #l #r #t' whd in ⊢ (??%? → ??%?); 132 132 lapply (IH r) 133 133 cases (update A b' a r) … … 138 138 | #b' #IH * 139 139 [ #t' normalize #E destruct 140 | #x #l #r #t' whd in ⊢ (??%? → ??%?) 140 | #x #l #r #t' whd in ⊢ (??%? → ??%?); 141 141 lapply (IH l) 142 142 cases (update A b' a l)
Note: See TracChangeset
for help on using the changeset viewer.
