Changeset 1134 for Deliverables/D3.3/id-lookup-branch

Timestamp:

Aug 29, 2011, 5:45:03 PM (10 years ago)

Author:

campbell

Message:

Extra results for non-failing map updates.

Location:

Deliverables/D3.3/id-lookup-branch

Files:

• ASM/BitVectorTrie.ma (modified) (1 diff)
• common/Identifiers.ma (modified) (3 diffs)
• utilities/option.ma (modified) (1 diff)

Deliverables/D3.3/id-lookup-branch/ASM/BitVectorTrie.ma

@@ -524 +524 @@
  ]
 qed.    
+
+lemma update_fail : ∀A,n,b,a,t.
+  update A n b a t = None ? →
+  lookup_opt A n b t = None ?.
+#A #n elim n
+[ #b @(vector_inv_n … b) #a #t cases (BitVectorTrie_O … t)
+  [ * #x #E >E normalize #NE destruct
+  | #E >E normalize //
+  ]
+| #m #IH #b @(vector_inv_n … b) #hd #tl #a #t cases (BitVectorTrie_Sn … t)
+  [ * #t1 * #t2 #E >E cases hd whd in ⊢ (??%? → ??%?)
+    #X lapply (option_map_none … X) @IH
+  | #E >E normalize //
+  ]
+] qed.
+
+lemma update_lookup_opt_same : ∀A,n,b,a,t,t'.
+  update A n b a t = Some ? t' →
+  lookup_opt A n b t' = Some ? a.
+#A #n elim n
+[ #b #a #t #t' @(vector_inv_n … b)
+  cases (BitVectorTrie_O … t)
+  [ * #x #E >E normalize #E' destruct @refl
+  | #E >E normalize #E' destruct
+  ]
+| #m #IH #b #a #t #t'
+  @(vector_inv_n … b) #bhd #btl
+  cases (BitVectorTrie_Sn … t)
+  [ * #t1 * #t2 #E' >E'
+    whd in ⊢ (??%? → ??%?) cases bhd #U
+    cases (option_map_some ????? U)
+    #tn' * #U' #E'' <E''
+    whd in ⊢ (??%?) whd in ⊢ (??(???%%)?)
+    @(IH … U')
+  | #E >E normalize #E' destruct
+  ]
+] qed.
+
+lemma update_lookup_opt_other : ∀A,n,b,a,t,t'.
+  update A n b a t = Some ? t' →
+  ∀b'. b ≠ b' →
+  lookup_opt A n b' t = lookup_opt A n b' t'.
+#A #n elim n
+[ #b #a #t #t' #E #b'
+  @(vector_inv_n … b) @(vector_inv_n … b')
+  * #NE cases (NE (refl ??))
+| #m #IH #b #a #t #t'
+  @(vector_inv_n … b) #bhd #btl
+  cases (BitVectorTrie_Sn … t)
+  [ * #t1 * #t2 #E >E whd in ⊢ (??%? → ?) cases bhd
+    #U cases (option_map_some ????? U) #tn' * #U' #E' <E'
+    #b' @(vector_inv_n … b') #bhd' #btl'
+    cases bhd'
+    [ 2,3: #_ @refl
+    | *: #NE whd in ⊢ (??%%) whd in ⊢ (??(???%%)(???%%))
+         @(IH … U') % #E'' >E'' in NE * #H @H @refl
+    ]
+  | #E >E whd in ⊢ (??%? → ?) #NE destruct
+  ]
+] qed.
+

Deliverables/D3.3/id-lookup-branch/common/Identifiers.ma

@@ -3 +3 @@
 include "ASM/Arithmetic.ma".
 include "common/Errors.ma".
+include "utilities/option.ma".
 
 (* identifiers and their generators are tagged to differentiate them, and to
@@ -157 +158 @@
 
 (* A predicate that an identifier is in a map, and a failure-avoiding lookup
-   using it. *)
+   and update using it. *)
 
 definition present : ∀tag,A. identifier_map tag A → identifier tag → Prop ≝
@@ -166 +167 @@
 cases H #H'  cases (H' (refl ??)) qed.
 
+definition update_present : ∀tag,A. ∀m:identifier_map tag A. ∀id. present ?? m id → A → identifier_map tag A ≝
+λtag,A,m,l,p,a.
+  let l' ≝ match l with [ an_identifier l' ⇒ l' ] in
+  let m' ≝ match m with [ an_id_map m' ⇒ m' ] in
+  let u' ≝ update A 16 l' a m' in
+  match u' return λx. update ????? = x → ? with
+  [ None ⇒ λE.⊥
+  | Some m' ⇒ λ_. an_id_map tag A m'
+  ] (refl ? u').
+whd in p; whd in p:(?(??%?)) E:(??(???%?%)?);
+cases l in p E; cases m; -l' -m' #m' #l' whd in ⊢ (?(??(???%%)?) → ??(???%?%)? → ?)
+#NL #U cases NL #H @H @(update_fail … U)
+qed.
+
+lemma update_still_present : ∀tag,A,m,id,a,id'.
+  ∀H:present tag A m id.
+  ∀H':present tag A m id'.
+  present tag A (update_present tag A m id' H' a) id.
+#tag #A * #m * #id #a * #id' #H #H'
+whd whd in ⊢ (?(??(???(%??????)?)?)) normalize nodelta
+cases (identifier_eq ? (an_identifier tag id) (an_identifier tag id'))
+[ #E >E @refute_none_by_refl #m' #U whd in ⊢ (?(??%?)) >(update_lookup_opt_same ?????? U)
+  % #E' destruct
+| #NE @refute_none_by_refl #m' #U whd in ⊢ (?(??%?)) whd in ⊢ (?(??(???%%)?))
+  <(update_lookup_opt_other ?????? U id) [ @H | % #E cases NE >E #H @H @refl ]
+] qed.
 
 (* Sets *)

Deliverables/D3.3/id-lookup-branch/utilities/option.ma

@@ -3 +3 @@
 definition option_map : ∀A,B:Type[0]. (A → B) → option A → option B ≝
 λA,B,f,o. match o with [ None ⇒ None B | Some a ⇒ Some B (f a) ].
+
+lemma option_map_none : ∀A,B,f,x.
+  option_map A B f x = None B → x = None A.
+#A #B #f * [ // | #a #E whd in E:(??%?); destruct ]
+qed.
+
+lemma option_map_some : ∀A,B,f,x,v.
+  option_map A B f x = Some B v → ∃y. x = Some ? y ∧ f y = v.
+#A #B #f *
+[ #v normalize #E destruct
+| #y #v normalize #E %{y} destruct % //
+] qed.
+
+lemma refute_none_by_refl : ∀A,B:Type[0]. ∀P:A → B. ∀Q:B → Type[0]. ∀x:option A. ∀H:x = None ? → False.
+  (∀v. x = Some ? v → Q (P v)) →
+  Q (match x return λy.x = y → ? with [ Some v ⇒ λ_. P v | None ⇒ λE. match H E in False with [ ] ] (refl ? x)).
+#A #B #P #Q *
+[ #H cases (H (refl ??))
+| #a #H #p normalize @p @refl
+] qed.
+