Changeset 2439 for src/common


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

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

Location:
src/common
Files:
5 edited

Legend:

Unmodified
Added
Removed
  • src/common/AST.ma

    r2319 r2439  
    674674let rec match_funct_entry_inv (M:matching)
    675675  (P:∀vs,id,f,id',f'. Prop)
    676   (H:∀vs,id,f,id',f'. match_fundef M vs f f' → P vs id f id' f')
     676  (H:∀vs,id,f,f'. match_fundef M vs f f' → P vs id f id f')
    677677  vs id f id' f'
    678678  (MFE:match_funct_entry M vs vs 〈id,f〉 〈id',f'〉) on MFE : P vs id f id' f' ≝
  • src/common/Errors.ma

    r1954 r2439  
    253253notation > "vbox('do' ident v 'as' ident E ← e; break e')" with precedence 48 for @{ bind_eq ?? ${e} (λ${ident v}.λ${ident E}.${e'})}.
    254254
     255lemma bind_as_inversion:
     256  ∀A,B: Type[0]. ∀f: res A. ∀g: ∀a:A. f = OK A a → res B. ∀y: B.
     257  (do x as E ← f; g x E = return y) →
     258  ∃x. ∃E:f = return x. g x E = return y.
     259#A #B #f cases f normalize
     260[ #a #g #y #e %{a} /2/
     261| #m #g #y #H destruct (H)
     262] qed.
     263
    255264definition bind2_eq ≝ λA,B,C:Type[0]. λf: res (A×B). λg: ∀a:A.∀b:B. f = OK ? 〈a,b〉 → res C.
    256265  match f return λx. f = x → ? with
  • src/common/Globalenvs.ma

    r2415 r2439  
    4545  functions: positive_map F;
    4646  nextfunction: Pos;
    47   symbols: identifier_map SymbolTag block
     47  symbols: identifier_map SymbolTag block;
     48  functions_inv: ∀b. lookup_opt ? b functions ≠ None ? →
     49                 ∃id. lookup … symbols id = Some ? (mk_block Code (neg b))
    4850}.
     51
     52(* We deal with shadowed names by overwriting their global environment entry
     53   and getting rid of any function mapping (the latter is necessary so that we
     54   get a reverse mapping).  In fact, the parser will prevent these anyway, but
     55   adding the uniqueness of these names throughout would be more trouble than
     56   it's worth. *)
     57   
     58definition drop_fn : ∀F:Type[0]. ident → genv_t F → genv_t F ≝
     59λF,id,g.
     60let fns ≝
     61  match lookup ?? (symbols … g) id with
     62  [ None ⇒ functions … g
     63  | Some b' ⇒
     64      match b' with
     65      [ mk_block r x ⇒
     66        match r with
     67        [ Code ⇒
     68          match x with
     69          [ neg p ⇒ pm_set … p (None ?) (functions … g)
     70          | _ ⇒ functions … g
     71          ]
     72        | _ ⇒ functions … g
     73        ]
     74      | _ ⇒ functions … g
     75      ]
     76  ]
     77in mk_genv_t F fns (nextfunction … g) (remove … (symbols … g) id) ?.
     78whd in match fns; -fns
     79#b #L
     80cases (functions_inv ? g b ?)
     81[ #id' #L'
     82  cases (identifier_eq … id id')
     83  [ #E destruct >L' in L; normalize >lookup_opt_pm_set_hit * #H cases (H (refl ??))
     84  | #NE %{id'} >lookup_remove_miss /2/
     85  ]
     86| cases (lookup ?? (symbols F g) id) in L;
     87  [ normalize //
     88  | * * * [ 2,3,5,6: #b' ] normalize //
     89    #H cut (b ≠ b')
     90    [ % #E destruct >lookup_opt_pm_set_hit in H; * /2/ ]
     91    #NE >lookup_opt_pm_set_miss in H; //
     92  ]
     93] qed.
     94
     95lemma drop_fn_id : ∀F,id,ge.
     96  lookup ?? (symbols … (drop_fn F id ge)) id = None ?.
     97#F #id * #fns #next #syms #inv
     98whd in match (drop_fn ???);
     99@lookup_remove_hit
     100qed.
     101
     102lemma drop_fn_lfn : ∀F,id,ge,b,f.
     103  lookup_opt ? b (functions … (drop_fn F id ge)) = Some ? f →
     104  lookup_opt ? b (functions … ge) = Some ? f.
     105#F #id #ge #b #f
     106whd in match (drop_fn ???);
     107cases (lookup ??? id)
     108[ normalize //
     109| * * * [2,3,5,6: #b' ] normalize //
     110  cases (decidable_eq_pos b b')
     111  [ #E destruct >lookup_opt_pm_set_hit #E destruct
     112  | #NE >lookup_opt_pm_set_miss //
     113  ]
     114] qed.
    49115
    50116definition add_funct : ∀F:Type[0]. (ident × F) → genv_t F → genv_t F ≝
     
    52118  let blk_id ≝ nextfunction ? g in
    53119  let b ≝ mk_block Code (neg blk_id) in
    54   mk_genv_t F (insert ? blk_id (\snd name_fun) (functions … g))
     120  let g' ≝ drop_fn F (\fst name_fun) g in
     121  mk_genv_t F (insert ? blk_id (\snd name_fun) (functions … g'))
    55122              (succ blk_id)
    56               (add ?? (symbols … g) (\fst name_fun) b).
     123              (add ?? (symbols … g') (\fst name_fun) b) ?.
     124#b' #L whd in match b;
     125cases (decidable_eq_pos blk_id b')
     126[ #E destruct
     127  %{(\fst name_fun)} @lookup_add_hit
     128| #NE
     129  cases (functions_inv ? g' b' ?)
     130  [ #id #L' %{id} >lookup_add_miss
     131    [ @L'
     132    | % #E destruct
     133      >drop_fn_id in L'; #E destruct
     134    ]
     135  | >lookup_opt_insert_miss in L; /2/
     136  ]
     137] qed.
    57138
    58139definition add_symbol : ∀F:Type[0]. ident → block → genv_t F → genv_t F ≝
    59140λF,name,b,g.
    60   mk_genv_t F (functions … g)
    61               (nextfunction … g)
    62               (add ?? (symbols … g) name b).
     141  let g' ≝ drop_fn F name g in
     142  mk_genv_t F (functions … g')
     143              (nextfunction … g')
     144              (add ?? (symbols … g') name b)
     145              ?.
     146#b' #L
     147cases (functions_inv ? g' b' ?)
     148[ #id #L' %{id} >lookup_add_miss
     149  [ @L'
     150  | % #E destruct
     151    >drop_fn_id in L'; #E destruct
     152  ]
     153| @L
     154] qed.
    63155
    64156(* Construct environment and initial memory store *)
    65157definition empty_mem ≝ empty. (* XXX*)
    66158definition empty : ∀F. genv_t F ≝
    67   λF. mk_genv_t F (pm_leaf ?) (succ_pos_of_nat … 2) (empty_map ??).
     159  λF. mk_genv_t F (pm_leaf ?) (succ_pos_of_nat … 2) (empty_map ??) ?.
     160#b #L normalize in L; cases L #L cases (L (refl ??))
     161qed.
    68162
    69163definition add_functs : ∀F:Type[0]. genv_t F → list (ident × F) → genv_t F ≝
     
    247341  (*%{pty}*) %{b} (*%{c}*) % // @E
    248342] qed.
    249 
    250 
    251 lemma vars_irrelevant_to_find_funct_ptr : ∀F,V,init,b,vars,ge,m.
    252   find_funct_ptr F (\fst (add_globals F V init 〈ge,m〉 vars)) b = find_funct_ptr F ge b.
    253 #F #V #init * * // * // #blk
    254 whd in ⊢ (? → ? → ? → ??%%);
    255 #vars elim vars
    256 [ #ge #m %
    257 | * * #id #r #v #tl #IH #ge #m
    258   whd in match (add_globals ?????);
    259   whd in ⊢ (??(???(??(???(????%?))))?);
    260   cases (alloc ????) #m' #b
    261   whd in ⊢ (??(???(??(???(????%?))))?);
    262   >IH cases ge #fnmap #nextblock #symmap
    263   whd in ⊢ (??(???%)?);
    264   %
    265 ] qed.
    266 
     343 
    267344lemma add_globals_match : ∀A,B,V,W,initV,initW.
    268345  ∀P:(ident × region × V) → (ident × region × W) → Prop.
     
    285362  destruct >E2 cases (alloc ????) #m' #b
    286363  @IH /2/
    287   whd in match (add_symbol ????);
    288   whd in match (add_symbol ????);
     364  whd in match (add_symbol ????); whd in match (drop_fn ???);
     365  whd in match (add_symbol ????); whd in match (drop_fn ???);
    289366  >E %
    290367] qed.
     368
    291369
    292370lemma pre_matching_fns_get_same_blocks : ∀A,B,P.
     
    306384  change with (add_functs ???) in match (foldr (ident × B) ????);
    307385  cases (IH tl' H) #E1 #E2
    308   % [ >E1 % | >E1 >E2 % ]
     386  % [ >E1 %
     387    | whd in match (drop_fn ???);
     388      whd in match (drop_fn ???);
     389      >E1 >E2 % ]
    309390] qed.
    310391
     
    334415  ]
    335416] qed.
     417
     418(* The mapping of blocks to symbols is total for functions. *)
     419
     420definition symbol_of_function_block : ∀F,ge,b. find_funct_ptr F ge b ≠ None ? → ident ≝
     421λF,ge,b,FFP.
     422match symbol_for_block F ge b return λx. symbol_for_block ??? = x → ? with
     423[ None ⇒ λH. ⊥
     424| Some id ⇒ λ_. id
     425] (refl ? (symbol_for_block F ge b)).
     426whd in H:(??%?);
     427cases b in FFP H ⊢ %; * * -b [2,3,5,6: #b ] normalize in ⊢ (% → ?); [4: #FFP | *: * #H cases (H (refl ??)) ]
     428cases (functions_inv … ge b FFP)
     429#id #L lapply (find_lookup ?? (symbols F ge) (λid',b'. eq_block (mk_block Code (neg b)) b') id (mk_block Code (neg b)))
     430lapply (find_none … (symbols F ge) (λid',b'. eq_block (mk_block Code (neg b)) b') id (mk_block Code (neg b)))
     431cases (find ????)
     432[ #H #_ #_ lapply (H (refl ??) L) @eq_block_elim [ #_ * | * #H' cases (H' (refl ??)) ]
     433| * #id' #b' #_ normalize #_ #E destruct
     434] qed.
     435
    336436
    337437(*
     
    524624qed.
    525625
     626lemma alloc_pair : ∀m,m',l,h,l',h',r. ∀P:mem×(Σb:block. block_region b = r) → mem×(Σb:block. block_region b = r) → Type[0].
     627  nextblock m = nextblock m' →
     628  (∀m1,m2,b. nextblock m1 = nextblock m2 → P 〈m1,b〉 〈m2,b〉) →
     629  P (alloc m l h r) (alloc m' l' h' r).
     630* #ct #nx #NX * #ct' #nx' #NX' #l #h #l' #h' #r #P #N destruct #H @H %
     631qed.
     632
     633lemma vars_irrelevant_to_find_funct_ptr :
     634  ∀F,G,V,W.
     635  ∀P:F → G → Prop.
     636  ∀init,init',b,vars,vars',ge,ge',m,m',f.
     637  (find_funct_ptr F ge b = Some ? f → ∃f'. find_funct_ptr G ge' b = Some ? f' ∧ P f f') →
     638  symbols F ge = symbols G ge' →
     639  nextblock m = nextblock m' →
     640  All2 … (λx,y. \fst x = \fst y) vars vars' →
     641  find_funct_ptr F (\fst (add_globals F V init 〈ge,m〉 vars)) b = Some ? f →
     642  ∃f'.find_funct_ptr G (\fst (add_globals G W init' 〈ge',m'〉 vars')) b = Some ? f' ∧ P f f'.
     643#F #G #V #W #P #init #init'
     644* * * [ 2,3,5,6: #blk ] [ 4: | *: #vars #vars' #ge #ge' #m #m' #f #H1 #H2 #H3 #H4 #H5 normalize in H5; destruct ]
     645#vars elim vars
     646[ * [ #ge #ge' #m #m' #f #H #_ #_ #_ @H
     647    | #x #tl #ge #ge' #m #m' #f #_ #_ #_ *
     648    ]
     649| * * #id #r #v #tl #IH *
     650  [ #ge #ge' #m #m' #f #_ #_ #_ *
     651  | * * #id' #r' #v' #tl'
     652    #ge #ge' #m #m' #f #FFP1 #Esym #Enext * #E destruct #MATCH
     653    whd in match (add_globals ?????); whd in match (add_globals G ????);
     654    whd in ⊢ (??(??(???(????%?))?)? → ??(λ_.?(??(??(???(????%?))?)?)?));
     655    @(alloc_pair … Enext) #m1 #m2 #b #Enext'
     656    whd in ⊢ (??(??(???(????%?))?)? → ??(λ_.?(??(??(???(????%?))?)?)?));
     657    #FFP
     658    @(IH … MATCH FFP)
     659    [ whd in ⊢ (??%? → ??(λ_.?(??%?)?));
     660      whd in ⊢ (??(???%)? → ??(λ_.?(??(???%)?)?));
     661      >Esym
     662      cases (lookup … id')
     663      [ @FFP1
     664      | * * * try @FFP1 #p try @FFP1
     665        normalize
     666        cases (decidable_eq_pos blk p)
     667        [ #E destruct >lookup_opt_pm_set_hit #E destruct
     668        | #NE >(lookup_opt_pm_set_miss … NE) >(lookup_opt_pm_set_miss … NE)
     669          @FFP1
     670        ]
     671      ]
     672    | whd in match (add_symbol ????); whd in match (drop_fn ???);
     673      whd in match (add_symbol ????); whd in match (drop_fn ???);
     674      >Esym %
     675    | assumption
     676    ]
     677  ]
     678] qed.
     679
    526680(* Now link functions in related programs, but without dealing with the type
    527681   casts yet. *)
    528682
     683lemma symbols_drop_fn_eq : ∀A,B,ge,ge',id.
     684  symbols A ge = symbols B ge' →
     685  symbols A (drop_fn A id ge) = symbols B (drop_fn B id ge').
     686#A #B #ge #ge' #id #E
     687whd in ⊢ (??(??%)(??%));
     688>E %
     689qed.
     690
     691lemma ge_add_functs : ∀A,B,fns,fns'.
     692  All2 ?? (λx,y. \fst x = \fst y) fns fns' →
     693  symbols A (add_functs A (empty ?) fns) = symbols B (add_functs B (empty ?) fns') ∧
     694  nextfunction A (add_functs A (empty ?) fns) = nextfunction B (add_functs B (empty ?) fns').
     695#A #B
     696#fns elim fns
     697[ * [ #_ % % | #h #t * ]
     698| * #id #a #tl #IH * * #id' #b #tl' * #E destruct #TL
     699  whd in match (add_functs ???); whd in match (add_functs B ??);
     700  cases (IH ? TL) #S #N >N % [2: % ]
     701  >(symbols_drop_fn_eq A B (foldr ??? (empty A) tl) (foldr ?? (add_funct B) (empty B) tl'))
     702  [ %
     703  | @S
     704  ]
     705] qed.
     706
     707lemma lookup_drop_fn_different : ∀F,ge,id,b,f.
     708  lookup_opt ? b (functions ? (drop_fn F id ge)) = Some ? f →
     709  lookup … (symbols ? ge) id ≠ Some ? (mk_block Code (neg b)).
     710#F #ge #id #b #f
     711whd in match (drop_fn F id ge);
     712cases (lookup … id)
     713[ #_ % #E destruct
     714| * * * [2,3,5,6: #b'] normalize
     715  [4: cases (decidable_eq_pos b b')
     716    [ #E destruct >lookup_opt_pm_set_hit #E destruct
     717    | #NE #_ @(not_to_not … NE) #E destruct //
     718    ]
     719  | *: #_ % #E destruct
     720  ]
     721] qed.
     722
     723lemma lookup_drop_fn_irrelevant : ∀F,ge,id,b.
     724  lookup … (symbols ? ge) id ≠ Some ? (mk_block Code (neg b)) →
     725  lookup_opt ? b (functions ? (drop_fn F id ge)) = lookup_opt ? b (functions ? ge).
     726#F #ge #id #b
     727whd in match (drop_fn F id ge);
     728cases (lookup … id)
     729[ //
     730| * * * //
     731  #b' normalize #NE
     732  @lookup_opt_pm_set_miss
     733  @(not_to_not … NE)
     734  #E destruct %
     735] qed.
     736
    529737lemma find_funct_ptr_All2 : ∀A,B,V,W,b,p,f,initV,initW,p',P.
     738  All2 ?? (λx,y. \fst x = \fst y ∧ P (\snd x) (\snd y)) (prog_funct ?? p) (prog_funct … p') →
     739  All2 … (λx,y. \fst x = \fst y) (prog_vars ?? p) (prog_vars ?? p') →
    530740  find_funct_ptr … (globalenv A V initV p) b = Some ? f →
    531   All2 ?? (λx,y. P (\snd x) (\snd y)) (prog_funct ?? p) (prog_funct … p') →
    532741  ∃f'. find_funct_ptr … (globalenv B W initW p') b = Some ? f' ∧ P f f'.
    533742#A #B #V #W #b * #vars #fns #main #f #initV #initW * #vars' #fns' #main' #P
     743#Mfns
    534744cases b * * [ 2,3,5,6(*,8,9,11,12,14,15,17,18*): #bp ]
    535 [ 4: (*12:*) | *: #F whd in F:(??%?); destruct ]
    536 >vars_irrelevant_to_find_funct_ptr
    537 >vars_irrelevant_to_find_funct_ptr
    538 letin varnames ≝ (map ??? vars)
    539 cut (lookup_opt (A varnames) bp (functions ? (add_functs ? (empty ?) [ ])) = None ?)
    540 //
    541 cut (nextfunction (A varnames) (empty ?) = nextfunction (B (map … (λx.\fst (\fst x)) vars')) (empty ?))
    542 //
    543 generalize in match (empty ?);
    544 generalize in match (empty ?);
    545 generalize in match fns';
    546 elim fns
    547 [ #fns' #ge' #ge #_ #F1 #FFP @⊥ normalize in FFP; >F1 in FFP; #E destruct
    548 | * #id #fn #tl #IH #fns' #ge' #ge #NF #F1 whd in ⊢ (??%? → ?);
    549   whd in match (functions ??);
    550   change with (add_functs ???) in match (foldr ?????);
    551   cases (decidable_eq_pos bp (nextfunction … (add_functs ? ge tl)))
    552   [ #E destruct  >lookup_opt_insert_hit #E destruct
    553     cases fns' [ * ]
    554     * #id' #fn' #tl' * #M #Mtl
    555     %{fn'} % // whd in ⊢ (??%?);
     745[ 4: (*12:*) | *: #_ #F whd in F:(??%?); destruct ]
     746whd in match (globalenv ????); whd in match (globalenv_allocmem ????);
     747whd in match (globalenv ????); whd in match (globalenv_allocmem ????);
     748@vars_irrelevant_to_find_funct_ptr
     749[ letin varnames ≝ (map ??? vars)
     750  generalize in match fns' in Mfns ⊢ %;
     751  elim fns
     752  [ #fns' #Mfns whd in ⊢ (??%? → ?); #E destruct
     753  | * #id #fn #tl #IH * * #id' #fn' #tl' * * #E #Phd destruct #Mtl
     754    whd in ⊢ (??%? → ?);
    556755    whd in match (functions ??);
    557     change with (add_functs ???) in match (foldr ???? tl');
    558     >nextfunction_length >nextfunction_length <NF >(All2_length  … Mtl)
    559     >lookup_opt_insert_hit @refl
    560   | #NE >lookup_opt_insert_miss //
    561     #FFP cases fns' [ * ] * #id' #fn' #tl' * #M #Mtl
    562     cases (IH ?????? Mtl)
    563     [ #fn'' * #FFP' #P' %{fn''} % [ whd in ⊢ (??%?); >lookup_opt_insert_miss [2: >nextfunction_length <NF <(All2_length … Mtl) <nextfunction_length @NE ] @FFP' | @P' ]
    564     | skip
    565     | 4: @NF
    566     | skip
    567     | //
    568     | @FFP
     756    change with (add_functs ???) in match (foldr ?????);
     757    cases (ge_add_functs ?? tl tl' ?) [2: @(All2_mp … Mtl) * #idA #a * #idB #b * // ]
     758    #SYMS #NEXT
     759    cases (decidable_eq_pos bp (nextfunction … (add_functs ? (empty ?) tl)))
     760    [ #E destruct >lookup_opt_insert_hit #E destruct
     761      %{fn'} % // whd in ⊢ (??%?);
     762      whd in match (functions ??);
     763      change with (add_functs ???) in match (foldr ???? tl');
     764      >NEXT >lookup_opt_insert_hit @refl
     765    | #NE >lookup_opt_insert_miss //
     766      #FFP cases (IH tl' Mtl ?)
     767      [ #fn'' * #FFP' #P' %{fn''} %
     768        [ whd in ⊢ (??%?);
     769          >lookup_opt_insert_miss [2: <NEXT // ]
     770          lapply (lookup_drop_fn_different ????? FFP)
     771          >SYMS
     772          #L >lookup_drop_fn_irrelevant // @FFP'
     773        | @P'
     774        ]
     775      | @(drop_fn_lfn … FFP)
     776      ]
    569777    ]
    570778  ]
     779| cases (ge_add_functs ?? fns fns' ?) [2: @(All2_mp … Mfns) * #idA #a * #idB #b * // ]
     780  #S #_ @S
     781| @refl
    571782] qed.
    572783
     
    577788  P f.
    578789#A #V #b #p #f #initV #P #FFP #ALL
    579 cut (All2 ?? (λx,y. P (\snd x)) (prog_funct ?? p) (prog_funct ?? p))
     790cut (All2 ?? (λx,y. \fst x = \fst y ∧ P (\snd x)) (prog_funct ?? p) (prog_funct ?? p))
    580791[ elim (prog_funct … p) in ALL ⊢ %;
    581792  [ // | #h #t #IH * #Hh #Ht % /2/ ] ]
    582 #ALL2
    583 cases (find_funct_ptr_All2 A A V V b p f initV initV p ? FFP ALL2)
     793cut (All2 ?? (λx,y. \fst x = \fst y) (prog_vars ?? p) (prog_vars ?? p))
     794[ elim (prog_vars … p) [ // | * #x #x' #tl #TL /2/ ] ]
     795#VARS2 #FNS2
     796cases (find_funct_ptr_All2 A A V V b p f initV initV p ? FNS2 VARS2 FFP)
    584797#x * //
    585798qed.
     
    602815#p #p' * #Mvars #Mfn #Mmain
    603816#b #f #FFP
    604 @(find_funct_ptr_All2 A B V W ??????? FFP)
    605 lapply (matching_vars … (mk_matching A B V W match_fn match_var) … Mvars)
    606 #E
    607 @(All2_mp … Mfn)
    608 * #id #f * #id' #f'
    609 <E in f' ⊢ %; #f' -Mmain -b -Mfn -Mvars -initV -initW -E
    610 normalize #H @(match_funct_entry_inv … H) //
     817@(find_funct_ptr_All2 A B V W ????????? FFP)
     818[ lapply (matching_vars … (mk_matching A B V W match_fn match_var) … Mvars)
     819  #E
     820  @(All2_mp … Mfn)
     821  * #id #f * #id' #f'
     822  <E in f' ⊢ %; #f' -Mmain -b -Mfn -Mvars -initV -initW -E
     823  normalize #H @(match_funct_entry_inv … H)
     824  #vs #id1 #f1 #f2 #M % //
     825| @(All2_mp … Mvars)
     826  * #x #x' * #y #y' #M inversion M #id #r #v1 #v2 #M' #E1 #E2 #_ destruct //
    611827qed.
    612828
  • src/common/Identifiers.ma

    r2420 r2439  
    326326  ].
    327327
     328(* Remove an entry from a map (and leave it equivalent, otherwise) *)
     329definition remove : ∀tag,A. identifier_map tag A → identifier tag → identifier_map tag A ≝
     330λtag,A,m,id. an_id_map tag A (pm_set A (match id with [ an_identifier p ⇒ p ]) (None ?)
     331                                       (match m with [ an_id_map m ⇒ m ])).
     332
     333lemma lookup_remove_hit : ∀tag,A,m,id.
     334  lookup tag A (remove tag A m id) id = None ?.
     335#tag #A * #m * #id @lookup_opt_pm_set_hit
     336qed.
     337
     338lemma lookup_remove_miss : ∀tag,A,m,id,id'.
     339  id ≠ id' →
     340  lookup tag A (remove tag A m id') id = lookup tag A m id.
     341#tag #A * #m * #id * #id' #NE
     342@lookup_opt_pm_set_miss
     343/2/
     344qed.
     345
    328346(* Fold over the entries in a map.  There are some lemmas to help reason about
    329347   this near the bottom of the file (they require sets). *)
     
    365383| * #id' #a' normalize #E destruct %
    366384] qed.
     385
     386lemma find_none : ∀tag,A,m,p,id,a.
     387  find tag A m p = None ? →
     388  lookup … m id = Some ? a →
     389  ¬ p id a.
     390#tag #A * #m #p * #id #a #FIND
     391@(pm_find_none A m (λid. p (an_identifier tag id)))
     392whd in FIND:(??%?); cases (pm_find ???) in FIND ⊢ %;
     393[ normalize #E destruct %
     394| * #id' #a' normalize #E destruct
     395] qed.
     396
    367397
    368398lemma find_predicate : ∀tag,A,m,p,id,a.
  • 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.