Ignore:
Timestamp:
Nov 7, 2012, 4:42:02 PM (8 years ago)
Author:
campbell
Message:

Get a proper reverse mapping of function blocks to identifiers by getting
rid of shadowing.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/common/PositiveMap.ma

    r2420 r2439  
    2525 ].
    2626
    27 let rec insert (A:Type[0]) (b:Pos) (a:A) (t:positive_map A) on b : positive_map A ≝
     27let rec pm_set (A:Type[0]) (b:Pos) (a:option A) (t:positive_map A) on b : positive_map A ≝
    2828match b with
    2929[ one ⇒
    3030    match t with
    31     [ pm_leaf ⇒ pm_node A (Some ? a) (pm_leaf A) (pm_leaf A)
    32     | pm_node _ l r ⇒ pm_node A (Some ? a) l r
     31    [ pm_leaf ⇒ pm_node A a (pm_leaf A) (pm_leaf A)
     32    | pm_node _ l r ⇒ pm_node A a l r
    3333    ]
    3434| p0 tl ⇒
    3535    match t with
    36     [ pm_leaf ⇒ pm_node A (None ?) (insert A tl a (pm_leaf A)) (pm_leaf A)
    37     | pm_node x l r ⇒ pm_node A x (insert A tl a l) r
     36    [ pm_leaf ⇒ pm_node A (None ?) (pm_set A tl a (pm_leaf A)) (pm_leaf A)
     37    | pm_node x l r ⇒ pm_node A x (pm_set A tl a l) r
    3838    ]
    3939| p1 tl ⇒
    4040    match t with
    41     [ pm_leaf ⇒ pm_node A (None ?) (pm_leaf A) (insert A tl a (pm_leaf A))
    42     | pm_node x l r ⇒ pm_node A x l (insert A tl a r)
    43     ]
    44 ].
     41    [ pm_leaf ⇒ pm_node A (None ?) (pm_leaf A) (pm_set A tl a (pm_leaf A))
     42    | pm_node x l r ⇒ pm_node A x l (pm_set A tl a r)
     43    ]
     44].
     45
     46definition insert : ∀A:Type[0]. Pos → A → positive_map A → positive_map A ≝
     47λA,p,a. pm_set A p (Some ? a).
    4548
    4649let rec update (A:Type[0]) (b:Pos) (a:A) (t:positive_map A) on b : option (positive_map A) ≝
     
    6265    ]
    6366].
     67
     68lemma lookup_opt_pm_set_hit :
     69 ∀A:Type[0].∀v:option A.∀b:Pos.∀t:positive_map A.
     70  lookup_opt … b (pm_set … b v t) = v.
     71#A #v #b elim b
     72[ * //
     73| #tl #IH *
     74  [ whd in ⊢ (??%%); @IH
     75  | #x #l #r @IH
     76  ]
     77| #tl #IH *
     78  [ whd in ⊢ (??%%); @IH
     79  | #x #l #r @IH
     80  ]
     81] qed.
    6482
    6583lemma lookup_opt_insert_hit :
     
    87105#A #v #b #t #d whd in ⊢ (??%?); >lookup_opt_insert_hit %
    88106qed.
     107
     108lemma lookup_opt_pm_set_miss:
     109 ∀A:Type[0].∀v:option A.∀b,c:Pos.∀t:positive_map A.
     110  b ≠ c → lookup_opt … b (pm_set … c v t) = lookup_opt … b t.
     111#A #v #b elim b
     112[ * [ #t * #H elim (H (refl …))
     113    | *: #c' #t #NE cases t //
     114    ]
     115| #b' #IH *
     116  [ * [ #NE @refl | #x #l #r #NE @refl ]
     117  | #c' * [ #NE whd in ⊢ (??%%); @IH /2/
     118          | #x #l #r #NE whd in ⊢ (??%%); @IH /2/
     119          ]
     120  | #c' * //
     121  ]
     122| #b' #IH *
     123  [ * [ #NE @refl | #x #l #r #NE @refl ]
     124  | #c' * //
     125  | #c' * [ #NE whd in ⊢ (??%%); @IH /2/
     126          | #x #l #r #NE whd in ⊢ (??%%); @IH /2/
     127          ]
     128  ]
     129] qed.
    89130
    90131lemma lookup_opt_insert_miss:
     
    856897] qed.
    857898
     899lemma pm_find_aux_none : ∀A,t,pre,p,q,a.
     900  pm_find_aux pre A t p = None ? →
     901  lookup_opt A q t = Some ? a →
     902  ¬ p (pre q) a.
     903#A #t elim t
     904[ #pre #p #q #a #_ normalize #E destruct
     905| #oa #l #r #IHl #IHr #pre #p *
     906  [ #a cases oa
     907    [ #_ normalize #E destruct
     908    | #a' #F whd in F:(??%?); whd in F:(??match % with [_⇒?|_⇒?]?);
     909      #E normalize in E; destruct
     910      cases (p (pre one) a) in F ⊢ %; //
     911      normalize #E destruct
     912    ]
     913  | #q #a #F #L @(IHr (λx. pre (p1 x)) p q a ? L)
     914    whd in F:(??%?); cases oa in F;
     915    [2: #a' normalize cases (p (pre one) a') [ normalize #E destruct ] ]
     916    normalize cases (pm_find_aux ?? l p) normalize //
     917    #x #E destruct
     918  | #q #a #F #L @(IHl (λx. pre (p0 x)) p q a ? L)
     919    whd in F:(??%?); cases oa in F;
     920    [2: #a' normalize cases (p (pre one) a') [ normalize #E destruct ] ]
     921    normalize cases (pm_find_aux ?? l p) normalize //
     922  ]
     923] qed.
     924
     925lemma pm_find_none : ∀A,t,p,q,a.
     926  pm_find A t p = None ? →
     927  lookup_opt A q t = Some ? a →
     928  ¬ p q a.
     929#A #t
     930@(pm_find_aux_none A t (λx.x))
     931qed.
     932
    858933lemma pm_find_predicate : ∀A,t,p,q,a.
    859934  pm_find A t p = Some ? 〈q,a〉 →
Note: See TracChangeset for help on using the changeset viewer.