source: src/common/PositiveMap.ma @ 2183

include "basics/types.ma".
include "utilities/binary/positive.ma".

inductive positive_map (A:Type[0]) : Type[0] ≝
| pm_leaf : positive_map A
| pm_node : option A → positive_map A → positive_map A → positive_map A.

let rec lookup_opt (A:Type[0]) (b:Pos) (t:positive_map A) on t : option A ≝
match t with
[ pm_leaf ⇒ None ?
| pm_node a l r ⇒
    match b with
    [ one ⇒ a
    | p0 tl ⇒ lookup_opt A tl l
    | p1 tl ⇒ lookup_opt A tl r
    ]
].

definition lookup: ∀A:Type[0].Pos → positive_map A → A → A ≝  
 λA.λb.λt.λx.
 match lookup_opt A b t with
 [ None ⇒ x
 | Some r ⇒ r
 ].

let rec insert (A:Type[0]) (b:Pos) (a:A) (t:positive_map A) on b : positive_map A ≝
match b with
[ one ⇒
    match t with
    [ pm_leaf ⇒ pm_node A (Some ? a) (pm_leaf A) (pm_leaf A)
    | pm_node _ l r ⇒ pm_node A (Some ? a) l r
    ]
| p0 tl ⇒
    match t with
    [ pm_leaf ⇒ pm_node A (None ?) (insert A tl a (pm_leaf A)) (pm_leaf A)
    | pm_node x l r ⇒ pm_node A x (insert A tl a l) r
    ]
| p1 tl ⇒
    match t with
    [ pm_leaf ⇒ pm_node A (None ?) (pm_leaf A) (insert A tl a (pm_leaf A))
    | pm_node x l r ⇒ pm_node A x l (insert A tl a r)
    ]
].

let rec update (A:Type[0]) (b:Pos) (a:A) (t:positive_map A) on b : option (positive_map A) ≝
match b with
[ one ⇒
    match t with
    [ pm_leaf ⇒ None ?
    | pm_node x l r ⇒ option_map ?? (λ_. pm_node A (Some ? a) l r) x
    ]
| p0 tl ⇒
    match t with
    [ pm_leaf ⇒ None ?
    | pm_node x l r ⇒ option_map ?? (λl. pm_node A x l r) (update A tl a l)
    ]
| p1 tl ⇒
    match t with
    [ pm_leaf ⇒ None ?
    | pm_node x l r ⇒ option_map ?? (λr. pm_node A x l r) (update A tl a r)
    ]
].

lemma lookup_opt_insert_hit : 
 ∀A:Type[0].∀v:A.∀b:Pos.∀t:positive_map A.
  lookup_opt … b (insert … b v t) = Some A v.
#A #v #b elim b
[ * //
| #tl #IH * 
  [ whd in ⊢ (??%%); @IH
  | #x #l #r @IH
  ]
| #tl #IH * 
  [ whd in ⊢ (??%%); @IH
  | #x #l #r @IH
  ]
] qed.

lemma lookup_insert_hit:
  ∀a: Type[0].
  ∀v: a.
  ∀b: Pos.
  ∀t: positive_map a.
  ∀d: a.
    lookup … b (insert … b v t) d = v.
#A #v #b #t #d whd in ⊢ (??%?); >lookup_opt_insert_hit %
qed.

lemma lookup_opt_insert_miss:
 ∀A:Type[0].∀v:A.∀b,c:Pos.∀t:positive_map A.
  b ≠ c → lookup_opt … b (insert … c v t) = lookup_opt … b t.
#A #v #b elim b
[ * [ #t * #H elim (H (refl …))
    | *: #c' #t #NE cases t //
    ]
| #b' #IH *
  [ * [ #NE @refl | #x #l #r #NE @refl ]
  | #c' * [ #NE whd in ⊢ (??%%); @IH /2/
          | #x #l #r #NE whd in ⊢ (??%%); @IH /2/
          ]
  | #c' * //
  ]
| #b' #IH *
  [ * [ #NE @refl | #x #l #r #NE @refl ]
  | #c' * //
  | #c' * [ #NE whd in ⊢ (??%%); @IH /2/
          | #x #l #r #NE whd in ⊢ (??%%); @IH /2/
          ]
  ]
] qed.

let rec fold (A, B: Type[0]) (f: Pos → A → B → B)
 (t: positive_map A) (b: B) on t: B ≝
match t with
[ pm_leaf ⇒ b
| pm_node a l r ⇒
    let b ≝ match a with [ None ⇒ b | Some a ⇒ f one a b ] in
    let b ≝ fold A B (λx.f (p0 x)) l b in
            fold A B (λx.f (p1 x)) r b
].    

lemma update_fail : ∀A,b,a,t.
  update A b a t = None ? →
  lookup_opt A b t = None ?.
#A #b #a elim b
[ * [ // | * // #x #l #r normalize #E destruct ]
| #b' #IH * [ // | #x #l #r #U @IH whd in U:(??%?);
                   cases (update A b' a r) in U ⊢ %;
                   [ // | normalize #t #E destruct ]
            ]
| #b' #IH * [ // | #x #l #r #U @IH whd in U:(??%?);
                   cases (update A b' a l) in U ⊢ %;
                   [ // | normalize #t #E destruct ]
            ]
] qed.

lemma update_lookup_opt_same : ∀A,b,a,t,t'.
  update A b a t = Some ? t' →
  lookup_opt A b t' = Some ? a.
#A #b #a elim b
[ * [ #t' normalize #E destruct
    | * [ 2: #x ] #l #r #t' whd in ⊢ (??%? → ??%?);
      #E destruct //
    ]
| #b' #IH *
  [ #t' normalize #E destruct
  | #x #l #r #t' whd in ⊢ (??%? → ??%?);
    lapply (IH r)
    cases (update A b' a r)
    [ #_ normalize #E destruct
    | #r' #H normalize #E destruct @H @refl
    ]
  ]
| #b' #IH *
  [ #t' normalize #E destruct
  | #x #l #r #t' whd in ⊢ (??%? → ??%?);
    lapply (IH l)
    cases (update A b' a l)
    [ #_ normalize #E destruct
    | #r' #H normalize #E destruct @H @refl
    ]
  ]
] qed.

lemma update_lookup_opt_other : ∀A,b,a,t,t'.
  update A b a t = Some ? t' →
  ∀b'. b ≠ b' →
  lookup_opt A b' t = lookup_opt A b' t'.
#A #b #a elim b
[ * [ #t' normalize #E destruct
    | * [2: #x] #l #r #t' normalize #E destruct
      * [ * #H elim (H (refl …)) ]
      #tl #NE normalize //
    ]
| #b' #IH *
  [ #t' normalize #E destruct
  | #x #l #r #t' normalize
    lapply (IH r)
    cases (update A b' a r)
    [ #_ normalize #E destruct
    | #t'' #H normalize #E destruct * // #b'' #NE @H /2/
    ]
  ] 
| #b' #IH *
  [ #t' normalize #E destruct
  | #x #l #r #t' normalize
    lapply (IH l)
    cases (update A b' a l)
    [ #_ normalize #E destruct
    | #t'' #H normalize #E destruct * // #b'' #NE @H /2/
    ]
  ]
] qed.

include "utilities/option.ma".

let rec map_opt A B (f : A → option B) (b : positive_map A) on b : positive_map B ≝
match b with
[ pm_leaf ⇒ pm_leaf ?
| pm_node a l r ⇒ pm_node ? (a »= f)
    (map_opt ?? f l)
    (map_opt ?? f r)
].

definition map ≝ λA,B,f.map_opt A B (λx. Some ? (f x)).

lemma lookup_opt_map : ∀A,B,f,b,p.
  lookup_opt … p (map_opt A B f b) = ! x ← lookup_opt … p b ; f x.
#A#B#f#b elim b [//]
#a #l #r #Hil #Hir * [//]
#p
whd in ⊢ (??(???%)(????%?));
whd in ⊢ (??%?); //
qed.

lemma map_opt_id_eq_ext : ∀A,m,f.(∀x.f x = Some ? x) → map_opt A A f m = m.
#A #m #f #Hf elim m [//]
* [2:#x] #l #r #Hil #Hir normalize [>Hf] //
qed.

lemma map_opt_id : ∀A,m.map_opt A A (λx. Some ? x) m = m.
#A #m @map_opt_id_eq_ext //
qed.

let rec merge A B C (choice : option A → option B → option C)
  (a : positive_map A) (b : positive_map B) on a : positive_map C ≝
match a with
[ pm_leaf ⇒ map_opt ?? (λx.choice (None ?) (Some ? x)) b
| pm_node o l r ⇒
  match b with
  [ pm_leaf ⇒ map_opt ?? (λx.choice (Some ? x) (None ?)) a
  | pm_node o' l' r' ⇒
    pm_node ? (choice o o') 
      (merge … choice l l')
      (merge … choice r r')
  ]
].

lemma lookup_opt_merge : ∀A,B,C,choice,a,b,p.
  choice (None ?) (None ?) = None ? →
  lookup_opt … p (merge A B C choice a b) =
    choice (lookup_opt … p a) (lookup_opt … p b).
 #A#B#C#choice#a elim a
[ normalize #b
| #o#l#r#Hil#Hir * [2: #o'#l'#r' * normalize /2 by /]
]
#p#choice_good >lookup_opt_map
elim (lookup_opt ???)
normalize //
qed.

let rec domain_size (A : Type[0]) (b : positive_map A) on b : ℕ ≝
match b with
[ pm_leaf ⇒ 0
| pm_node a l r ⇒
  (match a with
   [ Some _ ⇒ 1
   | None ⇒ 0
   ]) + domain_size A l + domain_size A r
].

(* just to load notation for 'norm (list.ma's notation overrides core's 'card)*)
include "basics/lists/list.ma".
interpretation "positive map size" 'norm p = (domain_size ? p).

lemma map_opt_size : ∀A,B,f,b.|map_opt A B f b| ≤ |b|.
#A#B#f#b elim b [//]
*[2:#x]#l#r#Hil#Hir normalize
[elim (f ?) normalize [@(transitive_le ? ? ? ? (le_n_Sn ?)) | #y @le_S_S ] ]
@le_plus assumption
qed.

lemma map_size : ∀A,B,f,b.|map A B f b| = |b|.
#A#B#f#b elim b [//]
*[2:#x]#l#r#Hil#Hir normalize
>Hil >Hir @refl
qed.

lemma lookup_opt_O_lt_size : ∀A,m,p. lookup_opt A p m ≠ None ? → 0 < |m|.
#A#m elim m
[#p normalize #F elim (absurd ? (refl ??) F)
|* [2: #x]  #l #r #Hil #Hir * normalize
  [1,2,3: //
  |4:  #F elim (absurd ? (refl ??) F)]
  #p #H [@(transitive_le … (Hir ? H)) | @(transitive_le … (Hil ? H))] //
qed.

lemma insert_size : ∀A,p,a,m. |insert A p a m| =
  (match lookup_opt … p m with [Some _ ⇒ 0 | None ⇒ 1]) + |m|.
#A#p elim p
[ #a * [2: * [2: #x] #l #r] normalize //
|*: #p #Hi #a * [2,4: * [2,4: #x] #l #r] normalize >Hi //
] qed.