Changeset 1134 for Deliverables/D3.3/id-lookup-branch
- Timestamp:
- Aug 29, 2011, 5:45:03 PM (10 years ago)
- Location:
- Deliverables/D3.3/id-lookup-branch
- Files:
-
- 3 edited
Legend:
- Unmodified
- Added
- Removed
-
Deliverables/D3.3/id-lookup-branch/ASM/BitVectorTrie.ma
r1074 r1134 524 524 ] 525 525 qed. 526 527 lemma update_fail : ∀A,n,b,a,t. 528 update A n b a t = None ? → 529 lookup_opt A n b t = None ?. 530 #A #n elim n 531 [ #b @(vector_inv_n … b) #a #t cases (BitVectorTrie_O … t) 532 [ * #x #E >E normalize #NE destruct 533 | #E >E normalize // 534 ] 535 | #m #IH #b @(vector_inv_n … b) #hd #tl #a #t cases (BitVectorTrie_Sn … t) 536 [ * #t1 * #t2 #E >E cases hd whd in ⊢ (??%? → ??%?) 537 #X lapply (option_map_none … X) @IH 538 | #E >E normalize // 539 ] 540 ] qed. 541 542 lemma update_lookup_opt_same : ∀A,n,b,a,t,t'. 543 update A n b a t = Some ? t' → 544 lookup_opt A n b t' = Some ? a. 545 #A #n elim n 546 [ #b #a #t #t' @(vector_inv_n … b) 547 cases (BitVectorTrie_O … t) 548 [ * #x #E >E normalize #E' destruct @refl 549 | #E >E normalize #E' destruct 550 ] 551 | #m #IH #b #a #t #t' 552 @(vector_inv_n … b) #bhd #btl 553 cases (BitVectorTrie_Sn … t) 554 [ * #t1 * #t2 #E' >E' 555 whd in ⊢ (??%? → ??%?) cases bhd #U 556 cases (option_map_some ????? U) 557 #tn' * #U' #E'' <E'' 558 whd in ⊢ (??%?) whd in ⊢ (??(???%%)?) 559 @(IH … U') 560 | #E >E normalize #E' destruct 561 ] 562 ] qed. 563 564 lemma update_lookup_opt_other : ∀A,n,b,a,t,t'. 565 update A n b a t = Some ? t' → 566 ∀b'. b ≠ b' → 567 lookup_opt A n b' t = lookup_opt A n b' t'. 568 #A #n elim n 569 [ #b #a #t #t' #E #b' 570 @(vector_inv_n … b) @(vector_inv_n … b') 571 * #NE cases (NE (refl ??)) 572 | #m #IH #b #a #t #t' 573 @(vector_inv_n … b) #bhd #btl 574 cases (BitVectorTrie_Sn … t) 575 [ * #t1 * #t2 #E >E whd in ⊢ (??%? → ?) cases bhd 576 #U cases (option_map_some ????? U) #tn' * #U' #E' <E' 577 #b' @(vector_inv_n … b') #bhd' #btl' 578 cases bhd' 579 [ 2,3: #_ @refl 580 | *: #NE whd in ⊢ (??%%) whd in ⊢ (??(???%%)(???%%)) 581 @(IH … U') % #E'' >E'' in NE * #H @H @refl 582 ] 583 | #E >E whd in ⊢ (??%? → ?) #NE destruct 584 ] 585 ] qed. 586 -
Deliverables/D3.3/id-lookup-branch/common/Identifiers.ma
r1105 r1134 3 3 include "ASM/Arithmetic.ma". 4 4 include "common/Errors.ma". 5 include "utilities/option.ma". 5 6 6 7 (* identifiers and their generators are tagged to differentiate them, and to … … 157 158 158 159 (* A predicate that an identifier is in a map, and a failure-avoiding lookup 159 using it. *)160 and update using it. *) 160 161 161 162 definition present : ∀tag,A. identifier_map tag A → identifier tag → Prop ≝ … … 166 167 cases H #H' cases (H' (refl ??)) qed. 167 168 169 definition update_present : ∀tag,A. ∀m:identifier_map tag A. ∀id. present ?? m id → A → identifier_map tag A ≝ 170 λtag,A,m,l,p,a. 171 let l' ≝ match l with [ an_identifier l' ⇒ l' ] in 172 let m' ≝ match m with [ an_id_map m' ⇒ m' ] in 173 let u' ≝ update A 16 l' a m' in 174 match u' return λx. update ????? = x → ? with 175 [ None ⇒ λE.⊥ 176 | Some m' ⇒ λ_. an_id_map tag A m' 177 ] (refl ? u'). 178 whd in p; whd in p:(?(??%?)) E:(??(???%?%)?); 179 cases l in p E; cases m; -l' -m' #m' #l' whd in ⊢ (?(??(???%%)?) → ??(???%?%)? → ?) 180 #NL #U cases NL #H @H @(update_fail … U) 181 qed. 182 183 lemma update_still_present : ∀tag,A,m,id,a,id'. 184 ∀H:present tag A m id. 185 ∀H':present tag A m id'. 186 present tag A (update_present tag A m id' H' a) id. 187 #tag #A * #m * #id #a * #id' #H #H' 188 whd whd in ⊢ (?(??(???(%??????)?)?)) normalize nodelta 189 cases (identifier_eq ? (an_identifier tag id) (an_identifier tag id')) 190 [ #E >E @refute_none_by_refl #m' #U whd in ⊢ (?(??%?)) >(update_lookup_opt_same ?????? U) 191 % #E' destruct 192 | #NE @refute_none_by_refl #m' #U whd in ⊢ (?(??%?)) whd in ⊢ (?(??(???%%)?)) 193 <(update_lookup_opt_other ?????? U id) [ @H | % #E cases NE >E #H @H @refl ] 194 ] qed. 168 195 169 196 (* Sets *) -
Deliverables/D3.3/id-lookup-branch/utilities/option.ma
r761 r1134 3 3 definition option_map : ∀A,B:Type[0]. (A → B) → option A → option B ≝ 4 4 λA,B,f,o. match o with [ None ⇒ None B | Some a ⇒ Some B (f a) ]. 5 6 lemma option_map_none : ∀A,B,f,x. 7 option_map A B f x = None B → x = None A. 8 #A #B #f * [ // | #a #E whd in E:(??%?); destruct ] 9 qed. 10 11 lemma option_map_some : ∀A,B,f,x,v. 12 option_map A B f x = Some B v → ∃y. x = Some ? y ∧ f y = v. 13 #A #B #f * 14 [ #v normalize #E destruct 15 | #y #v normalize #E %{y} destruct % // 16 ] qed. 17 18 lemma refute_none_by_refl : ∀A,B:Type[0]. ∀P:A → B. ∀Q:B → Type[0]. ∀x:option A. ∀H:x = None ? → False. 19 (∀v. x = Some ? v → Q (P v)) → 20 Q (match x return λy.x = y → ? with [ Some v ⇒ λ_. P v | None ⇒ λE. match H E in False with [ ] ] (refl ? x)). 21 #A #B #P #Q * 22 [ #H cases (H (refl ??)) 23 | #a #H #p normalize @p @refl 24 ] qed. 25
Note: See TracChangeset
for help on using the changeset viewer.