Changeset 2415 for src/common/PositiveMap.ma

Timestamp:

Oct 23, 2012, 3:57:02 PM (8 years ago)

Author:

campbell

Message:

Add the ability to map blocks to symbols in preparation for stack space.

File:

• src/common/PositiveMap.ma (modified) (1 diff)

src/common/PositiveMap.ma

@@ -590 +590 @@
   λA,B,t,f,b. pm_fold_inf_aux A B t f t (λx.x) b (λp. refl ??).
 
+(* Find an entry in the map matching the given predicate *)
+
+let rec pm_find_aux (pre: Pos → Pos) (A:Type[0]) (t: positive_map A) (p:Pos → A → bool) on t : option (Pos × A) ≝
+match t with
+[ pm_leaf ⇒ None ?
+| pm_node a l r ⇒
+  let x ≝ match a with
+  [ Some a ⇒ if p (pre one) a then Some ? 〈pre one, a〉 else None ?
+  | None ⇒ None ?
+  ] in
+  match x with
+  [ Some x ⇒ Some ? x
+  | None ⇒ 
+    match pm_find_aux (λx. pre (p0 x)) A l p with
+    [ None ⇒ pm_find_aux (λx. pre (p1 x)) A r p
+    | Some y ⇒ Some ? y
+    ]
+  ]
+].
+
+definition pm_find : ∀A:Type[0]. positive_map A → (Pos → A → bool) → option (Pos × A) ≝
+  pm_find_aux (λx.x).
+
+lemma pm_find_aux_pre : ∀A,t,pre,p,q,a.
+  pm_find_aux pre A t p = Some ? 〈q,a〉 →
+  ∃q'. q = pre q'.
+#A #t elim t
+[ normalize #pre #p #q #a #E destruct
+| * [2:#a] #l #r #IHl #IHr #pre #p #q #a' normalize
+  [ cases (p (pre one) a) normalize [ #E destruct /2/ ] ]
+  lapply (IHl (λx. pre (p0 x)) p)
+  cases (pm_find_aux ?? l ?)
+  [ 1,3: #_ normalize
+    lapply (IHr (λx. pre (p1 x)) p)
+    cases (pm_find_aux ?? r ?)
+    [ 1,3: #_ #E destruct
+    | *: * #q' #a'' #H #E destruct cases (H ?? (refl ??)) #q'' #E destruct /2/
+    ]
+  | *: * #q' #a'' #H normalize #E destruct cases (H ?? (refl ??)) #q'' #E destruct /2/
+  ]
+] qed.
+
+(* XXX: Hmm... destruct doesn't work properly with this, not sure why *)
+lemma option_pair_f_eq : ∀A,B:Type[0].∀a,a',b,b'. ∀f:A → A.
+  (∀a,a'. f a = f a' → a = a') →
+  Some (A×B) 〈f a,b〉 = Some ? 〈f a',b'〉 →
+  a = a' ∧ b = b'.
+#A #B #a #a' #b #b' #f #EXT #E
+cut (f a = f a') [ destruct (E) destruct (e0) @e2 (* WTF? *) ]
+#E' >(EXT … E') in E ⊢ %; #E destruct /2/
+qed.
+
+lemma pm_find_lookup : ∀A,p,q,a,t.
+  pm_find A t p = Some ? 〈q,a〉 →
+  lookup_opt A q t = Some ? a.
+#A #p #q #a normalize #t
+change with ((λx.x) q) in match q in ⊢ (% → ?);
+cut (∀y,z:Pos. (λx.x) y = (λx.x) z → y = z) //
+generalize in match q; -q generalize in match (λx.x);
+elim t
+[ #pre #q #_  normalize #E destruct
+| * [2:#a'] #l #r #IHl #IHr #pre #q #PRE
+  normalize [ cases (p (pre one) a') normalize [ #E cases (option_pair_f_eq … pre PRE E) #E1 #E2 destruct normalize % ] ]
+  lapply (IHl (λx.pre (p0 x)))
+  lapply (pm_find_aux_pre A l (λx.pre (p0 x)) p)
+  cases (pm_find_aux ?? l ?)
+  [ 1,3: #_ #_ normalize
+    lapply (IHr (λx.pre (p1 x)))
+    lapply (pm_find_aux_pre A r (λx.pre (p1 x)) p)
+    cases (pm_find_aux ?? r ?)
+    [ 1,3: #_ #_ #E destruct
+    | *: * #q' #a' #H1 #H2 #E destruct cases (H1 ?? (refl ??)) #q'' #E lapply (PRE … E) #E' destruct
+         whd in ⊢ (??%?); @H2 //
+         #y #z #E lapply (PRE … E) #E' destruct //
+    ]
+  | *: * #q' #a' #H1 #H2 normalize #E destruct cases (H1 ?? (refl ??)) #q'' #E lapply (PRE … E) #E' destruct
+         whd in ⊢ (??%?); @H2 //
+         #y #z #E lapply (PRE … E) #E' destruct //
+  ]
+] qed.
+
+lemma pm_find_predicate : ∀A,t,p,q,a.
+  pm_find A t p = Some ? 〈q,a〉 →
+  p q a.
+#A #t #p normalize #q
+change with ((λx.x) q) in match q; generalize in match q; -q generalize in match (λx.x);
+elim t
+[ normalize #pre #q #a #E destruct
+| * [2:#a'] #l #r #IHl #IHr #pre #q #a normalize
+  [ lapply (refl ? (p (pre one) a')) cases (p (pre one) a') in ⊢ (???% → %);
+    [ #E normalize #E'
+      cut (pre one = pre q) [ destruct (E') destruct (e0) @e2 (* XXX ! *) ]
+      #E'' <E'' in E' ⊢ %; #E' destruct >E %
+    | #_ normalize
+    ]
+  ]
+  lapply (IHl (λx.pre (p0 x)))
+  lapply (pm_find_aux_pre A l (λx.pre (p0 x)) p)
+  cases (pm_find_aux ?? l ?)
+  [ 1,3: #_ #_ normalize
+    lapply (IHr (λx.pre (p1 x)))
+    lapply (pm_find_aux_pre A r (λx.pre (p1 x)) p)
+    cases (pm_find_aux ?? r ?)
+    [ 1,3: #_ #_ #E destruct
+    | *: * #q' #a' #H1 #H2 #E destruct cases (H1 … (refl ??)) #q'' #E >E @H2 >E %
+    ]
+  | *: * #q' #a' #H1 #H2 normalize #E destruct cases (H1 … (refl ??)) #q'' #E >E @H2 >E %
+  ]
+] qed.