Ignore:
Timestamp:
Jan 31, 2013, 5:15:49 PM (8 years ago)
Author:
tranquil
Message:
  • map_opt and map on positive maps are now clean (erase empty subtrees)
  • minor changes to blocks
File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/common/PositiveMap.ma

    r2590 r2599  
    422422include "utilities/option.ma".
    423423
     424definition is_none : ∀A.option A → bool ≝ λA,o.match o with [ None ⇒ true | _ ⇒ false ].
     425definition is_pm_leaf : ∀A.positive_map A → bool ≝ λA,m.match m with [ pm_leaf ⇒ true | _ ⇒ false ].
     426
    424427let rec map_opt A B (f : A → option B) (b : positive_map A) on b : positive_map B ≝
    425428match b with
    426429[ pm_leaf ⇒ pm_leaf ?
    427 | pm_node a l r ⇒ pm_node ? (!x ← a ; f x)
    428     (map_opt ?? f l)
    429     (map_opt ?? f r)
     430| pm_node a l r ⇒
     431  let a' ≝ !x ← a ; f x in
     432  let l' ≝ map_opt ?? f l in
     433  let r' ≝ map_opt ?? f r in
     434  if is_none … a' ∧ is_pm_leaf … l' ∧ is_pm_leaf … r' then
     435    pm_leaf ?
     436  else
     437    pm_node ? a' l' r'
    430438].
    431439
    432440definition map ≝ λA,B,f.map_opt A B (λx. Some ? (f x)).
     441
     442lemma andb_false_r : ∀b.(b∧false)=false. *% qed.
    433443
    434444lemma lookup_opt_map : ∀A,B,f,b,p.
    435445  lookup_opt … p (map_opt A B f b) = ! x ← lookup_opt … p b ; f x.
    436446#A#B#f#b elim b [//]
    437 #a #l #r #Hil #Hir * [//]
    438 #p
    439 whd in ⊢ (??(???%)(????%?));
    440 whd in ⊢ (??%?); //
    441 qed.
    442 
     447#a #l #r #IHl #IHr * [2,3: #p ]
     448whd in match (map_opt ????); whd in match (lookup_opt ???) in ⊢ (???%);
     449[3: cases (! x ← a ; f x) [2: #x] try % cases (?∧?) % ]
     450inversion (map_opt ??? l)
     451[2,4: #lo #ll #lr #_ #_ >andb_false_r normalize nodelta #EQl <EQl
     452  whd in ⊢ (??%?); // ]
     453#EQl
     454inversion (map_opt ??? r)
     455[2,4: #ro #rl #rr #_ #_ >andb_false_r normalize nodelta #EQr <EQr <EQl
     456  whd in ⊢ (??%?); // ]
     457#EQr
     458[ <IHr >EQr | <IHl >EQl ] cases (?∧?) %
     459qed.
     460
     461(*
    443462lemma map_opt_id_eq_ext : ∀A,m,f.(∀x.f x = Some ? x) → map_opt A A f m = m.
    444463#A #m #f #Hf elim m [//]
     
    449468#A #m @map_opt_id_eq_ext //
    450469qed.
     470*)
    451471
    452472let rec merge A B C (choice : option A → option B → option C)
     
    458478  [ pm_leaf ⇒ map_opt ?? (λx.choice (Some ? x) (None ?)) a
    459479  | pm_node o' l' r' ⇒
    460     match (choice o o') with 
    461     [None ⇒
    462       match (merge … choice l l') with
    463       [pm_leaf ⇒ match (merge … choice r r') with
    464           [pm_leaf ⇒ pm_leaf ?
    465           |_ ⇒ pm_node ? (None ?) (merge … choice l l') (merge … choice r r')
    466           ]
    467       |_ ⇒ pm_node ? (None ?) (merge … choice l l') (merge … choice r r')
    468       ]
    469    |Some x ⇒
    470     pm_node ? (Some ? x)
    471       (merge … choice l l')
    472       (merge … choice r r')
    473   ]
    474 ]].
     480    let o'' ≝ choice o o' in
     481    let l'' ≝ merge … choice l l' in
     482    let r'' ≝ merge … choice r r' in
     483    if is_none … o'' ∧ is_pm_leaf … l'' ∧ is_pm_leaf … r'' then
     484      pm_leaf ?
     485    else
     486      pm_node ? o'' l'' r''
     487  ]
     488].
    475489
    476490lemma lookup_opt_merge : ∀A,B,C,choice,a,b,p.
     
    478492  lookup_opt … p (merge A B C choice a b) =
    479493    choice (lookup_opt … p a) (lookup_opt … p b).
    480  #A#B#C#choice#a elim a
    481 [ normalize #b
     494 #A#B#C#choice#a elim a -a
     495[ #b
    482496| #o#l#r#Hil#Hir * [2: #o'#l'#r' * [2,3: #x] normalize cases(choice o o') normalize /2 by /
    483497  [3: cases (merge A B C choice l l') normalize /2 by / cases(merge A B C choice r r')
     
    490504elim (lookup_opt ???)
    491505normalize //
    492 qed. 
     506qed.
    493507
    494508let rec domain_size (A : Type[0]) (b : positive_map A) on b : ℕ ≝
     
    504518interpretation "positive map size" 'card p = (domain_size ? p).
    505519
     520(*
    506521lemma map_opt_size : ∀A,B,f,b.|map_opt A B f b| ≤ |b|.
    507522#A#B#f#b elim b [//]
     
    510525@le_plus assumption
    511526qed.
     527*)
    512528
    513529lemma map_size : ∀A,B,f,b.|map A B f b| = |b|.
    514530#A#B#f#b elim b [//]
    515 *[2:#x]#l#r#Hil#Hir normalize
    516 >Hil >Hir @refl
     531*[2:#x]#l#r#Hil#Hir
     532[ normalize >Hil >Hir @refl ]
     533whd in match (map ????);
     534inversion (map_opt ??? l)
     535[2: #lo #ll #lr #_ #_ >andb_false_r normalize nodelta #EQl <EQl
     536  whd in ⊢ (??%?); normalize nodelta >Hil >Hir % ]
     537#EQl
     538inversion (map_opt ??? r)
     539[2,4: #ro #rl #rr #_ #_ >andb_false_r normalize nodelta #EQr <EQr <EQl
     540  whd in ⊢ (??%?); normalize nodelta >Hil >Hir % ]
     541#EQr normalize nodelta normalize
     542<Hil <Hir whd in match map; normalize nodelta >EQl >EQr %
    517543qed.
    518544
Note: See TracChangeset for help on using the changeset viewer.