examples_in_progress/avl/association_list.mlw

   1
   2 (* Association lists. *)
   3
   4 (* Association with respect to an equivalence relation. *)
   5 module Assoc
   6
   7   clone import key_type.KeyType as K
   8   clone import relations_params.EquivalenceParam as Eq with type t = key
   9
  10   use list.List
  11   use list.Mem
  12   use list.Append
  13   use option.Option
  14
  15   predicate appear (p:param 'a) (k:key 'a) (l:list (t 'a 'b)) =
  16     exists x. mem x l /\ correct_for p k /\ Eq.rel p k (key x)
  17
  18   lemma appear_append : forall p:param 'a,k:key 'a,l r:list (t 'a 'b).
  19     appear p k (l++r) <-> appear p k l \/ appear p k r
  20
  21   (* Correction. *)
  22   predicate correct (p:param 'a) (l:list (t 'a 'b)) =
  23     forall x. mem x l -> let kx = key x in correct_for p kx
  24
  25   (* Unique occurence (a desirable property of an association list). *)
  26   predicate unique (p:param 'a) (l:list (t 'a 'b)) = match l with
  27     | Nil -> true
  28     | Cons x q -> not appear p (key x) q /\ unique p q
  29     end
  30
  31   (* functional update with equivalence classes. *)
  32   function param_update (p:param 'a) (f:key 'a -> 'b)
  33     (k:key 'a) (b:'b) : key 'a -> 'b = \k2.
  34       if Eq.rel p k k2 then b else f k2
  35
  36   function const_none : 'a -> option 'b = \x.None
  37
  38   (* functional model of an association list. *)
  39   function model (p:param 'a) (l:list (t 'a 'b)) : key 'a -> option (t 'a 'b) =
  40     match l with
  41     | Nil -> const_none
  42     | Cons d q -> param_update p (model p q) (key d) (Some d)
  43     end
  44
  45   (* A key is bound iff it occurs in the association lists. *)
  46   let rec lemma model_occurence (p:param 'a) (k:key 'a)
  47     (l:list (t 'a 'b)) : unit
  48     requires { correct p l }
  49     requires { correct_for p k }
  50     ensures { appear p k l <-> match model p l k with None -> false
  51       | Some _ -> true end }
  52     ensures { not appear p k l <-> model p l k = None }
  53     variant { l }
  54   = match l with Cons _ q -> model_occurence p k q | _ -> () end
  55
  56   (* A key is bound to a value with an equivalent key. *)
  57   let rec lemma model_link (p:param 'a) (k:key 'a) (l:list (t 'a 'b)) : unit
  58     requires { correct p l }
  59     requires { correct_for p k }
  60     ensures { match model p l k with None -> true
  61       | Some d -> Eq.rel p k (key d) end }
  62     variant { l }
  63   = match l with Cons _ q -> model_link p k q | _ -> () end
  64
  65   (* Two equivalent keys are bound to the same value. *)
  66   let rec lemma model_equal (p:param 'a) (k1 k2:key 'a)
  67     (l:list (t 'a 'b)) : unit
  68     requires { correct p l }
  69     requires { correct_for p k1 /\ correct_for p k2 }
  70     requires { Eq.rel p k1 k2 }
  71     ensures { model p l k1 = model p l k2 }
  72     variant { l }
  73   = match l with
  74     | Cons x q -> assert { correct_for p x.key };
  75       model_equal p k1 k2 q
  76     | _ -> ()
  77     end
  78
  79   (* If the list satisfies the uniqueness property,
  80      then every value occuring in the list is the image of its key. *)
  81   let rec lemma model_unique (p:param 'a) (k:key 'a) (l:list (t 'a 'b)) : unit
  82     requires { correct p l }
  83     requires { unique p l }
  84     requires { correct_for p k }
  85     ensures { forall d. mem d l -> model p l (key d) = Some d }
  86     variant { l }
  87   = match l with Cons _ q -> model_unique p k q | _ -> () end
  88
  89   (* Singleton association list. *)
  90   let lemma model_singleton (p:param 'a) (k:key 'a) (d:t 'a 'b) : unit
  91     requires { correct_for p d.key }
  92     requires { correct_for p k }
  93     ensures { model p (Cons d Nil) k = if rel p k d.key
  94       then Some d
  95       else None }
  96   = ()
  97
  98   (* Unique union of association list by concatenation. *)
  99   let rec lemma model_concat (p:param 'a) (k:key 'a) (l r:list (t 'a 'b)) : unit
 100     requires { correct p (l++r) /\ correct p l /\ correct p r }
 101     requires { unique p (l++r) /\ unique p l /\ unique p r }
 102     requires { correct_for p k }
 103     ensures { match model p l k with None -> model p (l++r) k = model p r k
 104       | s -> model p (l++r) k = s end }
 105     ensures { match model p r k with None -> model p (l++r) k = model p l k
 106       | s -> model p (l++r) k = s end }
 107     ensures { model p (l++r) k = None <->
 108       model p l k = None /\ model p r k = None }
 109     ensures { model p l k = None \/ model p r k = None }
 110     variant { l }
 111   = match l with
 112     | Nil -> ()
 113     | Cons d q -> assert { rel p d.key k -> model p r k <> None ->
 114       match model p r k with None -> false | _ -> not appear p k r && false end
 115       && false };
 116       model_concat p k q r
 117     end
 118
 119 end
 120
 121
 122 (* Sorted (increasing) association list. *)
 123
 124 module AssocSorted
 125
 126   use list.List
 127   use list.Append
 128   use list.Mem
 129   use option.Option
 130
 131   clone import key_type.KeyType as K
 132   clone import preorder.FullParam as O with type t = key
 133   clone export Assoc with namespace K = K,
 134       type Eq.param = O.order,
 135       predicate Eq.correct_for = O.correct_for,
 136       predicate Eq.rel = O.eq,
 137       (* Duplicates, there is no need to keep them as lemma. *)
 138       goal Eq.trans,
 139       goal Eq.refl,
 140       goal Eq.symm
 141   clone sorted.Increasing as S with namespace K = K,
 142     type O.param = O.order,
 143     predicate O.correct_for = O.correct_for,
 144     predicate O.rel = O.lt,
 145     goal O.trans
 146
 147   (* Sorted lists are correct association lists with unicity property. *)
 148   let rec lemma increasing_unique_and_correct (o:order 'a)
 149     (l:list (t 'a 'b)) : unit
 150     requires { S.increasing o l }
 151     ensures { correct o l }
 152     ensures { unique o l }
 153     variant { l }
 154   = match l with Cons _ q -> increasing_unique_and_correct o q | _ -> () end
 155
 156   let lemma model_cut (o:order 'a) (k:key 'a) (l r:list (t 'a 'b)) : unit
 157     requires { correct_for o k }
 158     requires { S.increasing o r }
 159     requires { S.increasing o l }
 160     requires { S.majorate o k l }
 161     requires { S.minorate o k r }
 162     ensures { forall k2. correct_for o k2 /\ eq o k k2 ->
 163       model o (l++r) k2 = None }
 164     ensures { forall k2. correct_for o k2 /\ lt o k k2 ->
 165       model o (l++r) k2 = model o r k2 }
 166     ensures { forall k2. correct_for o k2 /\ le o k2 k ->
 167       model o r k2 = None }
 168     ensures { forall k2. correct_for o k2 /\ lt o k2 k ->
 169       model o (l++r) k2 = model o l k2 }
 170     ensures { forall k2. correct_for o k2 /\ le o k k2 ->
 171       model o l k2 = None }
 172   = assert { S.increasing o (l++r) };
 173     assert { forall k2. correct_for o k2 /\ lt o k k2 ->
 174     model o (l++r) k2 <> model o r k2 -> match model o r k2 with
 175       | None -> match model o l k2 with
 176         | None -> false
 177         | Some d -> lt o d.key k && false
 178         end && false
 179       | _ -> false
 180       end && false };
 181     assert { forall k2. correct_for o k2 /\ lt o k2 k ->
 182       model o (l++r) k2 <> model o l k2 -> match model o l k2 with
 183        | None -> match model o r k2 with
 184          | None -> false
 185          | Some d -> lt o k d.key && false
 186          end && false
 187        | _ -> false
 188        end && false }
 189
 190   let lemma model_split (o:order 'a) (d:t 'a 'b) (l r:list (t 'a 'b)) : unit
 191     requires { correct_for o d.key }
 192     requires { S.increasing o l }
 193     requires { S.increasing o r }
 194     requires { S.majorate o d.key l }
 195     requires { S.minorate o d.key r }
 196     ensures { forall k2. correct_for o k2 /\ eq o d.key k2 ->
 197       model o (l++Cons d r) k2 = Some d }
 198     ensures { forall k2. correct_for o k2 /\ lt o d.key k2 ->
 199       model o (l++Cons d r) k2 = model o r k2 }
 200     ensures { forall k2. correct_for o k2 /\ le o k2 d.key ->
 201       model o r k2 = None }
 202     ensures { forall k2. correct_for o k2 /\ lt o k2 d.key ->
 203       model o (l++Cons d r) k2 = model o l k2 }
 204     ensures { forall k2. correct_for o k2 /\ le o d.key k2 ->
 205       model o l k2 = None }
 206   = ()
 207
 208 end
 209