Ignore:
Timestamp:
Oct 23, 2012, 3:57:02 PM (7 years ago)
Author:
campbell
Message:

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

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/common/PositiveMap.ma

    r2335 r2415  
    590590  λA,B,t,f,b. pm_fold_inf_aux A B t f t (λx.x) b (λp. refl ??).
    591591
     592(* Find an entry in the map matching the given predicate *)
     593
     594let rec pm_find_aux (pre: Pos → Pos) (A:Type[0]) (t: positive_map A) (p:Pos → A → bool) on t : option (Pos × A) ≝
     595match t with
     596[ pm_leaf ⇒ None ?
     597| pm_node a l r ⇒
     598  let x ≝ match a with
     599  [ Some a ⇒ if p (pre one) a then Some ? 〈pre one, a〉 else None ?
     600  | None ⇒ None ?
     601  ] in
     602  match x with
     603  [ Some x ⇒ Some ? x
     604  | None ⇒
     605    match pm_find_aux (λx. pre (p0 x)) A l p with
     606    [ None ⇒ pm_find_aux (λx. pre (p1 x)) A r p
     607    | Some y ⇒ Some ? y
     608    ]
     609  ]
     610].
     611
     612definition pm_find : ∀A:Type[0]. positive_map A → (Pos → A → bool) → option (Pos × A) ≝
     613  pm_find_aux (λx.x).
     614
     615lemma pm_find_aux_pre : ∀A,t,pre,p,q,a.
     616  pm_find_aux pre A t p = Some ? 〈q,a〉 →
     617  ∃q'. q = pre q'.
     618#A #t elim t
     619[ normalize #pre #p #q #a #E destruct
     620| * [2:#a] #l #r #IHl #IHr #pre #p #q #a' normalize
     621  [ cases (p (pre one) a) normalize [ #E destruct /2/ ] ]
     622  lapply (IHl (λx. pre (p0 x)) p)
     623  cases (pm_find_aux ?? l ?)
     624  [ 1,3: #_ normalize
     625    lapply (IHr (λx. pre (p1 x)) p)
     626    cases (pm_find_aux ?? r ?)
     627    [ 1,3: #_ #E destruct
     628    | *: * #q' #a'' #H #E destruct cases (H ?? (refl ??)) #q'' #E destruct /2/
     629    ]
     630  | *: * #q' #a'' #H normalize #E destruct cases (H ?? (refl ??)) #q'' #E destruct /2/
     631  ]
     632] qed.
     633
     634(* XXX: Hmm... destruct doesn't work properly with this, not sure why *)
     635lemma option_pair_f_eq : ∀A,B:Type[0].∀a,a',b,b'. ∀f:A → A.
     636  (∀a,a'. f a = f a' → a = a') →
     637  Some (A×B) 〈f a,b〉 = Some ? 〈f a',b'〉 →
     638  a = a' ∧ b = b'.
     639#A #B #a #a' #b #b' #f #EXT #E
     640cut (f a = f a') [ destruct (E) destruct (e0) @e2 (* WTF? *) ]
     641#E' >(EXT … E') in E ⊢ %; #E destruct /2/
     642qed.
     643
     644lemma pm_find_lookup : ∀A,p,q,a,t.
     645  pm_find A t p = Some ? 〈q,a〉 →
     646  lookup_opt A q t = Some ? a.
     647#A #p #q #a normalize #t
     648change with ((λx.x) q) in match q in ⊢ (% → ?);
     649cut (∀y,z:Pos. (λx.x) y = (λx.x) z → y = z) //
     650generalize in match q; -q generalize in match (λx.x);
     651elim t
     652[ #pre #q #_  normalize #E destruct
     653| * [2:#a'] #l #r #IHl #IHr #pre #q #PRE
     654  normalize [ cases (p (pre one) a') normalize [ #E cases (option_pair_f_eq … pre PRE E) #E1 #E2 destruct normalize % ] ]
     655  lapply (IHl (λx.pre (p0 x)))
     656  lapply (pm_find_aux_pre A l (λx.pre (p0 x)) p)
     657  cases (pm_find_aux ?? l ?)
     658  [ 1,3: #_ #_ normalize
     659    lapply (IHr (λx.pre (p1 x)))
     660    lapply (pm_find_aux_pre A r (λx.pre (p1 x)) p)
     661    cases (pm_find_aux ?? r ?)
     662    [ 1,3: #_ #_ #E destruct
     663    | *: * #q' #a' #H1 #H2 #E destruct cases (H1 ?? (refl ??)) #q'' #E lapply (PRE … E) #E' destruct
     664         whd in ⊢ (??%?); @H2 //
     665         #y #z #E lapply (PRE … E) #E' destruct //
     666    ]
     667  | *: * #q' #a' #H1 #H2 normalize #E destruct cases (H1 ?? (refl ??)) #q'' #E lapply (PRE … E) #E' destruct
     668         whd in ⊢ (??%?); @H2 //
     669         #y #z #E lapply (PRE … E) #E' destruct //
     670  ]
     671] qed.
     672
     673lemma pm_find_predicate : ∀A,t,p,q,a.
     674  pm_find A t p = Some ? 〈q,a〉 →
     675  p q a.
     676#A #t #p normalize #q
     677change with ((λx.x) q) in match q; generalize in match q; -q generalize in match (λx.x);
     678elim t
     679[ normalize #pre #q #a #E destruct
     680| * [2:#a'] #l #r #IHl #IHr #pre #q #a normalize
     681  [ lapply (refl ? (p (pre one) a')) cases (p (pre one) a') in ⊢ (???% → %);
     682    [ #E normalize #E'
     683      cut (pre one = pre q) [ destruct (E') destruct (e0) @e2 (* XXX ! *) ]
     684      #E'' <E'' in E' ⊢ %; #E' destruct >E %
     685    | #_ normalize
     686    ]
     687  ]
     688  lapply (IHl (λx.pre (p0 x)))
     689  lapply (pm_find_aux_pre A l (λx.pre (p0 x)) p)
     690  cases (pm_find_aux ?? l ?)
     691  [ 1,3: #_ #_ normalize
     692    lapply (IHr (λx.pre (p1 x)))
     693    lapply (pm_find_aux_pre A r (λx.pre (p1 x)) p)
     694    cases (pm_find_aux ?? r ?)
     695    [ 1,3: #_ #_ #E destruct
     696    | *: * #q' #a' #H1 #H2 #E destruct cases (H1 … (refl ??)) #q'' #E >E @H2 >E %
     697    ]
     698  | *: * #q' #a' #H1 #H2 normalize #E destruct cases (H1 … (refl ??)) #q'' #E >E @H2 >E %
     699  ]
     700] qed.
Note: See TracChangeset for help on using the changeset viewer.