examples/verifythis_2018_le_rouge_et_le_noir_1.mlw

   1 (**
   2
   3 {1 VerifyThis @ ETAPS 2018 competition
   4    Challenge 2: Le rouge et le noir}
   5
   6 Author: Raphaël Rieu-Helft (LRI, Université Paris Sud)
   7 *)
   8
   9 module ColoredTiles
  10
  11 use int.Int
  12 use set.Fset
  13 use seq.Seq
  14
  15 type color = Red | Black
  16
  17 type coloring = seq color
  18
  19 predicate tworedneighbors (c: coloring) (i:int)
  20   = ((c[i-2] = Red /\ c[i-1] = Red /\ 2 <= i)
  21      \/ (c[i-1] = Red /\ c[i+1] = Red /\ 1 <= i <= length c - 2)
  22      \/ (c[i+1] = Red /\ c[i+2] = Red /\ i <= length c - 3))
  23
  24 predicate valid (c:coloring) =
  25   forall i. 0 <= i < length c -> c[i] = Red -> tworedneighbors c i
  26
  27 function black (_n:int) : color = Black
  28 function red (_n:int) : color = Red
  29
  30 function colorings0 : fset coloring = add (create 0 black) Fset.empty
  31 function colorings1 : fset coloring = add (create 1 black) Fset.empty
  32 function colorings2 : fset coloring = add (create 2 black) Fset.empty
  33 function colorings3: fset coloring =
  34          add (create 3 red) (add (create 3 black) Fset.empty)
  35
  36 lemma valid_contr:
  37   forall c i. valid c -> 0 <= i < length c -> not (tworedneighbors c i) -> c[i] = Black
  38
  39 lemma colo_0 : forall c: coloring. length c = 0 ->
  40       (valid c <-> mem c colorings0 by Seq.(==) c (create 0 black))
  41
  42 lemma colo_1 : forall c: coloring. length c = 1 ->
  43       (valid c <-> mem c colorings1
  44                    by c[0] = Black
  45                    so Seq.(==) c (create 1 black))
  46
  47 lemma colo_2 : forall c: coloring. length c = 2 ->
  48       (valid c <-> mem c colorings2
  49                    by c[0] = Black = c[1]
  50                    so Seq.(==) c (create 2 black)
  51                    so c = create 2 black)
  52
  53 lemma colo_3 : forall c: coloring. length c = 3 ->
  54       (valid c <-> mem c colorings3
  55                    by if c[0] = Black
  56                       then (c[0]=c[1]=c[2]=Black
  57                             so c == create 3 black
  58                             so c = create 3 black)
  59                       else (c[0]=c[1]=c[2]=Red
  60                             so c == create 3 red
  61                             so c = create 3 red))
  62
  63 let lemma valid_split_fb (c:coloring) (k: int)
  64   requires { 3 <= k < length c }
  65   requires { forall i. 0 <= i < k -> c[i] = Red }
  66   requires { valid c[k+1 ..] }
  67   ensures  { valid c }
  68 = let c' = c[k+1 ..] in
  69   assert { forall i. k+1 <= i < length c -> c[i] = Red ->
  70              (tworedneighbors c i
  71               by c'[i - (k+1)] = Red
  72               so [@case_split] tworedneighbors c' (i - (k+1))) }
  73
  74 let lemma valid_restrict (c: coloring) (k: int)
  75   requires { valid c }
  76   requires { 0 <= k < length c }
  77   requires { c[k] = Black }
  78   ensures  { valid c[k+1 ..] }
  79 = ()
  80
  81 (*1st black tile starting at i *)
  82 let rec function first_black_tile (c:coloring) : int
  83   ensures { 0 <= result <= length c }
  84   ensures { forall j. 0 <= j < result <= length c
  85             -> c[j] = Red }
  86   ensures { result < length c -> c[result] = Black }
  87   ensures { valid c -> result = 0 \/ 3 <= result }
  88   variant { length c }
  89 = if Seq.length c = 0 then 0
  90   else match c[0] with
  91        | Black -> 0
  92        | Red ->
  93            assert { valid c -> c[1]=Red /\ c[2] = Red };
  94            let r = first_black_tile c[1 ..] in
  95            assert { forall j. 1 <= j < 1+r
  96                     -> c[j] = Red
  97                        by c[1 ..][j-1] = Red };
  98            1+r end
  99
 100 let rec function addleft (nr:int) (c:coloring) : coloring
 101   variant { nr }
 102   ensures { nr >= 0 -> Seq.length result = Seq.length c + nr + 1 }
 103 = if nr <= 0 then cons Black c
 104   else cons Red (addleft (nr-1) c)
 105
 106 (* add nr red tiles and a black tile to the left of each coloring *)
 107 function mapaddleft (s:fset coloring) (nr:int) : fset coloring
 108 =  map (addleft nr) s
 109
 110 lemma addleft_fb:
 111   forall c nr. 0 <= nr -> first_black_tile (addleft nr c) = nr
 112
 113 lemma mapaddleft_fb:
 114   forall s c nr. 0 <= nr -> mem c (mapaddleft s nr) -> first_black_tile c = nr
 115
 116 predicate reciprocal (f: 'a -> 'b) (g: 'b -> 'a)
 117   = forall y. g (f y) = y
 118
 119 let lemma bij_image (u: fset 'a) (f: 'a -> 'b) (g: 'b -> 'a)
 120   requires { reciprocal f g }
 121   ensures  { subset u (map g (map f u)) }
 122 = assert { forall x. mem x u -> mem (f x) (map f u)
 123                      -> mem (g (f x)) (map g (map f u))
 124                      -> mem x (map g (map f u)) }
 125
 126 let lemma bij_cardinal (u: fset 'a) (f: 'a -> 'b) (g: 'b -> 'a)
 127   requires { reciprocal f g }
 128   ensures  { cardinal (map f u) = cardinal u }
 129 = assert { cardinal (map f u) <= cardinal u };
 130   assert { cardinal (map g (map f u)) <= cardinal (map f u) };
 131   assert { cardinal u <= cardinal (map g (map f u)) }
 132
 133 function rmleft (nr:int) (c:coloring) : coloring = c[nr+1 ..]
 134
 135 use seq.FreeMonoid
 136
 137 lemma ext: forall c1 c2: coloring. Seq.(==) c1 c2 -> c1 = c2
 138 lemma app_eq: forall c1 c2 c3 c4: coloring. c1 = c2 -> c3 = c4 -> c1 ++ c3 = c2 ++ c4
 139
 140 let rec lemma addleft_result (c:coloring) (nr:int)
 141   requires { 0 <= nr }
 142   ensures  { addleft nr c = (Seq.create nr red) ++ (cons Black c) }
 143   variant  { nr }
 144 = if nr = 0 then assert { addleft nr c = (Seq.create nr red) ++ (cons Black c) }
 145   else begin
 146     let cnr = create nr red in
 147     let cnrm = create (nr - 1) red in
 148     addleft_result c (nr-1);
 149     assert { addleft (nr-1) c = cnrm ++ cons Black c };
 150     assert { cons Red cnrm = cnr
 151                by Seq.(==) (cons Red cnrm) cnr };
 152     assert { addleft nr c = cnr ++ cons Black c
 153              by addleft nr c
 154                 = cons Red (addleft (nr-1) c)
 155                 = cons Red (cnrm ++ cons Black c)
 156                 = (cons Red cnrm) ++ cons Black c
 157                 = cnr ++ cons Black c }
 158   end
 159
 160 let lemma addleft_bijective (nr:int)
 161   requires { 0 <= nr }
 162   ensures  { reciprocal (addleft nr) (rmleft nr) }
 163 = assert { forall c i. 0 <= i < length c -> (rmleft nr (addleft nr c))[i] = c[i] };
 164   assert { forall c. Seq.(==) (rmleft nr (addleft nr c)) c }
 165
 166 let lemma mapaddleft_card (s: fset coloring) (nr: int)
 167   requires { 0 <= nr }
 168   ensures  { cardinal (mapaddleft s nr) = cardinal s }
 169 = addleft_bijective nr;
 170   bij_cardinal s (addleft nr) (rmleft nr)
 171
 172 let lemma addleft_valid (c:coloring) (nr:int)
 173   requires { nr = 0 \/ 3 <= nr }
 174   requires { valid c }
 175   ensures  { valid (addleft nr c) }
 176 = addleft_result c nr;
 177   if nr = 0 then assert { valid (addleft 0 c) }
 178   else valid_split_fb (addleft nr c) nr
 179
 180 let lemma mapaddleft_valid (s: fset coloring) (nr: int)
 181   requires { forall c. mem c s -> valid c }
 182   requires { nr = 0 \/ 3 <= nr }
 183   ensures  { forall c. mem c (mapaddleft s nr) -> valid c }
 184 = assert { forall c. mem c (mapaddleft s nr) ->
 185                      valid c
 186                      by mem c (map (addleft nr) s)
 187                      so (exists y. mem y s /\ c = addleft nr y) }
 188
 189 let lemma mapaddleft_length (s: fset coloring) (nr: int) (l1 l2: int)
 190   requires { forall c. mem c s -> Seq.length c = l1 }
 191   requires { 0 <= nr }
 192   requires { l2 = l1 + nr + 1 }
 193   ensures  { forall c. mem c (mapaddleft s nr) -> Seq.length c = l2 }
 194 = ()
 195
 196 let rec ghost disjoint_union (s1 s2: fset coloring) : fset coloring
 197   requires { forall x. mem x s1 -> not mem x s2 }
 198   ensures  { result = union s1 s2 }
 199   ensures  { cardinal result = cardinal s1 + cardinal s2 }
 200   variant  { cardinal s1 }
 201 = if is_empty s1
 202   then begin
 203     assert { union s1 s2 = s2
 204              by (forall x. mem x (union s1 s2)
 205                 -> mem x s1 \/ mem x s2 -> mem x s2)
 206              so subset (union s1 s2) s2 };
 207     s2
 208   end
 209   else
 210     let x = pick s1 in
 211     let s1' = remove x s1 in
 212     let s2' = add x s2 in
 213     let u = disjoint_union s1' s2' in
 214     assert { u = union s1 s2
 215              by u = union s1' s2'
 216              so (forall y. (mem y s2' <-> (mem y s2 \/ y = x)))
 217              so (forall y. ((mem y s1' \/ y = x) <-> mem y s1))
 218              so (forall y. mem y u <-> mem y s1' \/ mem y s2'
 219                        <-> mem y s1' \/ mem y s2 \/ y = x
 220                        <-> mem y s1 \/ mem y s2
 221                        <-> mem y (union s1 s2))
 222              so (forall y. mem y u <-> mem y (union s1 s2))
 223              so Fset.(==) u (union s1 s2)};
 224     u
 225
 226 use array.Array
 227
 228 let enum () : (count: array int, ghost sets: array (fset coloring))
 229   ensures { Array.length count = 51 = Array.length sets
 230             /\ (forall i. 0 <= i <= 50 ->
 231                (forall c: coloring. Seq.length c = i ->
 232                           (valid c <-> mem c (sets[i]))))
 233             /\ (forall i. 0 <= i < 50 ->
 234                           count[i] = cardinal (sets[i])) }
 235 = let count = Array.make 51 0 in
 236   let ghost sets : array (fset coloring) = Array.make 51 Fset.empty in
 237   count[0] <- 1;
 238   sets[0] <- colorings0;
 239   assert { forall c. ((Seq.length c = 0 /\ valid c) <-> mem c (sets[0])) };
 240   count[1] <- 1;
 241   sets[1] <- colorings1;
 242   assert { forall i c. (i=0 \/ i=1)
 243            -> ((Seq.length c = i /\ valid c) <-> mem c (sets[i])) };
 244   count[2] <- 1;
 245   sets[2] <- colorings2;
 246   assert { forall i c. (i=0 \/ i=1 \/ i=2)
 247            -> ((Seq.length c = i /\ valid c) <-> mem c (sets[i])) };
 248   count[3] <- 2;
 249   sets[3] <- colorings3;
 250   assert { sets[3] = colorings3 };
 251   assert { forall i c. (i=0 \/ i=1 \/ i=2 \/ i = 3)
 252            -> ((Seq.length c = i /\ valid c) <-> mem c (sets[i])) };
 253   assert { cardinal colorings3 = 2 };
 254   for n = 4 to 50 do
 255     invariant { forall c i. 0 <= i < n -> Seq.length c = i ->
 256                          valid c -> mem c (sets[i]) }
 257     invariant { forall c i. 0 <= i < n -> mem c (sets[i]) ->
 258                          (Seq.length c = i /\ valid c) }
 259     invariant { forall i. 0 <= i < n ->
 260                          count[i] = cardinal (sets[i]) }
 261     label StartLoop in
 262     (* colorings with first_black_tile = 0 *)
 263     count[n] <- count[n-1];
 264     mapaddleft_valid (sets[n-1]) 0;
 265     sets[n] <- mapaddleft (sets[n-1]) 0;
 266     assert { forall i. 0 <= i < n -> sets[i] = sets[i] at StartLoop };
 267     assert { forall i. 0 <= i < n -> count[i] = count[i] at StartLoop };
 268     assert { forall c. Seq.length c = n -> valid c -> first_black_tile c < 3 ->
 269                        mem c sets[n]
 270                        by first_black_tile c = 0
 271                        so valid c[1 ..]
 272                        so mem c[1 ..] (sets[n-1])
 273                        so addleft 0 c[1 ..] = c
 274                        so mem c (mapaddleft sets[n-1] 0) };
 275     for k = 3 to n-1 do
 276       invariant { forall c i. 0 <= i < n -> Seq.length c = i ->
 277                            valid c -> mem c (sets[i]) }
 278       invariant { forall c i. 0 <= i < n -> mem c (sets[i]) ->
 279                              (Seq.length c = i /\ valid c) }
 280       invariant { forall i. 0 <= i < n ->
 281                             count[i] = cardinal (sets[i]) }
 282       invariant { forall c. (mem c (sets[n]) <->
 283                             (Seq.length c = n /\ valid c
 284                             /\ first_black_tile c < k)) }
 285       invariant { count[n] = cardinal (sets[n]) }
 286       label InnerLoop in
 287       (* colorings with first_black_tile = k *)
 288       count[n] <- count [n] + count [n-k-1];
 289       mapaddleft_length (sets[n-k-1]) k (n-k-1) n;
 290       mapaddleft_valid  (sets[n-k-1]) k;
 291       mapaddleft_card   (sets[n-k-1]) k;
 292       let ghost ns = mapaddleft sets[n-k-1] k in
 293       assert { forall c. mem c ns -> first_black_tile c = k };
 294       assert { forall c. Seq.length c = n -> valid c -> first_black_tile c = k
 295                          -> mem c ns
 296                          by valid c[k+1 ..]
 297                          so mem c[k+1 ..] (sets[n-k-1])
 298                          so let c' = addleft k c[k+1 ..] in
 299                             ((forall i. 0 <= i < n -> Seq.get c i = Seq.get c' i)
 300                              by c[k+1 ..] = c'[k+1 ..])
 301                          so Seq.(==) c' c
 302                          so c' = c
 303                          so mem c (mapaddleft sets[n-k-1] k) };
 304       sets[n] <- disjoint_union (sets[n]) ns;
 305       assert { forall i. 0 <= i < n -> sets[i] = sets[i] at InnerLoop };
 306       assert { forall i. 0 <= i < n -> count[i] = count[i] at InnerLoop };
 307     done;
 308     (* coloring with first_black_tile = n *)
 309     label LastAdd in
 310     let ghost r = Seq.create n red in
 311     let ghost sr = Fset.singleton r in
 312     assert { forall c. mem c sets[n] -> first_black_tile c < n };
 313     assert { first_black_tile r = n };
 314     assert { valid r /\ Seq.length r = n };
 315     count[n] <- count[n]+1;
 316     sets[n] <- disjoint_union (sets[n]) sr;
 317     assert { forall c. mem c sets[n] -> valid c /\ Seq.length c = n
 318                        by [@case_split] mem c (sets[n] at LastAdd) \/ mem c sr };
 319     assert { forall c. Seq.length c = n -> first_black_tile c = n ->
 320                        mem c sets[n]
 321                        by (forall k. 0 <= k < n -> Seq.get c k = Red)
 322                        so c == r so c = r };
 323     assert { forall i. 0 <= i < n -> sets[i] = sets[i] at LastAdd };
 324     assert { forall i. 0 <= i < n -> count[i] = count[i] at LastAdd };
 325   done;
 326   count, sets
 327
 328 end