examples/logic/isa_planner.why

   1
   2 (** Benchmarks goals for proof by induction
   3     From http://dream.inf.ed.ac.uk/projects/isaplanner/
   4 *)
   5
   6 theory Nat
   7
   8   type nat = Zero | Suc nat
   9
  10   function (+) (x y: nat) : nat = match x with
  11   | Zero -> y
  12   | Suc xs -> Suc (xs + y)
  13   end
  14
  15   function ( * ) (x y: nat) : nat = match y with
  16   | Zero -> Zero
  17   | Suc ys -> x + x * ys
  18   end
  19
  20   function (-) (x y: nat) : nat = match x with
  21   | Zero -> Zero
  22   | Suc xs -> match y with
  23               | Zero -> Suc xs
  24               | Suc ys -> xs - ys
  25               end
  26   end
  27
  28   predicate ( < ) (x y: nat) = match y with
  29   | Zero -> false
  30   | Suc ys -> match x with
  31               | Zero -> true
  32               | Suc xs -> xs < ys end
  33   end
  34
  35   predicate ( <= ) (x y: nat) = match x with
  36   | Zero -> true
  37   | Suc xs -> match y with
  38               | Zero -> false
  39               | Suc ys -> xs <= ys
  40              end
  41   end
  42
  43   function max (x y: nat) : nat = match x with
  44   | Zero -> y
  45   | Suc xs -> match y with
  46               | Zero -> Suc xs
  47               | Suc ys -> Suc (max xs ys) end end
  48
  49   function min (x y: nat) : nat = match x with
  50   | Zero -> Zero
  51   | Suc xs -> match y with
  52               | Zero -> y
  53               | Suc ys -> Suc (min xs ys) end end
  54
  55 end
  56
  57 theory List
  58   use Nat
  59
  60   type list 'a = Nil | Cons 'a  (list 'a)
  61
  62   function len (l : list 'a) : nat = match l with
  63   | Nil -> Zero
  64   | Cons _ s -> Suc (len s)
  65   end
  66
  67   predicate mem (x: 'a) (l: list 'a) = match l with
  68   | Nil      -> false
  69   | Cons y ys -> if x = y then true else mem x ys
  70   end
  71
  72   function (++) (l r : list 'a) : list 'a  = match l with
  73   | Nil -> r
  74   | Cons x ls -> Cons x (ls ++ r)
  75   end
  76
  77   function rev (l: list 'a) : list 'a = match l with
  78   | Nil       -> Nil
  79   | Cons x xs -> rev xs ++ Cons x Nil
  80   end
  81
  82   function insert (x : 'a) (l : list 'a) : list 'a = match l with
  83   | Nil -> Cons x Nil
  84   | Cons h t -> if x = h then Cons x t else Cons h (insert x t)
  85   end
  86
  87   function delete (x: 'a) (l : list 'a) : list 'a = match l with
  88   | Nil -> Nil
  89   | Cons h t -> if x = h then delete x t else Cons h (delete x t)
  90   end
  91
  92   function take (n: nat) (l : list 'a) : list 'a = match l with
  93   | Nil -> Nil
  94   | Cons h t -> match n with
  95                  | Zero -> Nil
  96                  | Suc m ->  Cons h (take m t)
  97                 end
  98   end
  99
 100   function drop (n: nat) (l : list 'a) : list 'a = match l with
 101   | Nil -> Nil
 102   | Cons h t -> match n with
 103                  | Zero -> Cons h t
 104                  | Suc m ->  drop m t
 105                 end
 106   end
 107
 108   function last (l : list 'a) : 'a
 109   axiom last_single :
 110         forall x: 'a. last (Cons x Nil) = x
 111   axiom last_cons :
 112         forall x: 'a, l : list 'a. l <> Nil -> last (Cons x l)  = last l
 113
 114   function butlast (l : list 'a) : list 'a = match l with
 115   | Nil -> Nil
 116   | Cons _ Nil -> Nil
 117   | Cons x xs -> Cons x (butlast xs)
 118   end
 119
 120   function zip (l r : list 'a) : list ('a, 'a) = match r with
 121   | Nil -> Nil
 122   | Cons y rs -> match l with
 123                  | Nil -> Nil
 124                  | Cons x ls -> Cons (x,y) (zip ls rs)
 125                  end
 126   end
 127
 128   function count (x: 'a) (l: list 'a) : nat = match l with
 129   | Nil -> Zero
 130   | Cons y ys -> if x = y then Suc (count x ys) else count x ys
 131   end
 132
 133   function map (f: 'a -> 'b) (l: list 'a) : list 'b = match l with
 134   | Nil      -> Nil
 135   | Cons x xs -> Cons (f x) (map f xs)
 136   end
 137
 138   function filter (p: 'a -> bool) (l : list 'a) : list 'a = match l with
 139   | Nil -> Nil
 140   | Cons x xs -> if p x then Cons x (filter p xs) else filter p xs
 141   end
 142
 143   function takeWhile (p: 'a -> bool) (l : list 'a) : list 'a = match l with
 144   | Nil -> Nil
 145   | Cons x xs -> if p x then Cons x (takeWhile p xs) else Nil
 146   end
 147
 148   function dropWhile (p: 'a -> bool) (l : list 'a) : list 'a = match l with
 149   | Nil -> Nil
 150   | Cons x xs -> if p x then (dropWhile p xs) else (Cons x xs)
 151   end
 152
 153   predicate pfalse (_x: 'a) = false
 154
 155   function dropWhile_False (l : list 'a) : list 'a = match l with
 156   | Nil -> Nil
 157   | Cons x xs -> if pfalse x then (dropWhile_False xs) else (Cons x xs)
 158   end
 159
 160   predicate ptrue (_x: 'a) = true
 161
 162  function takeWhile_True (l : list 'a) : list 'a = match l with
 163   | Nil -> Nil
 164   | Cons x xs -> if ptrue x then Cons x (takeWhile_True xs) else Nil
 165   end
 166
 167  (******************** INSERTION SORT WITH NAT LIST ***************)
 168
 169   predicate sorted (l : list nat) = match l with
 170   | Nil -> true
 171   | Cons x xs -> match xs with
 172                 | Nil -> true
 173                 | Cons y _ -> x <= y && sorted xs
 174                 end
 175   end
 176
 177   function insert_nat (n : nat) (l : list nat) : list nat = match l with
 178   | Nil -> Cons n Nil
 179   | Cons h t -> if n < h then Cons n (Cons h t) else Cons h (insert_nat n t)
 180   end
 181
 182   function insertion_sort_aux (x : nat) (l : list nat) : list nat =
 183   match l with
 184   | Nil -> Cons x Nil
 185   | Cons y ys ->
 186     if x <= y then Cons x (Cons y ys) else Cons y (insertion_sort_aux x ys)
 187   end
 188
 189   function insertion_sort (l : list nat) : list nat = match l with
 190   | Nil -> Nil
 191   | Cons x xs -> insertion_sort_aux x (insertion_sort xs)
 192   end
 193
 194 end
 195
 196 theory Tree
 197
 198   use Nat
 199
 200   type tree 'a =
 201   | Leaf
 202   | Node (tree 'a) 'a (tree 'a)
 203
 204   function mirror (t: tree 'a) : tree 'a = match t with
 205   | Leaf -> Leaf
 206   | Node l x r -> Node (mirror r) x (mirror l)
 207   end
 208
 209   function nodes (t: tree 'a) : nat = match t with
 210   | Leaf -> Zero
 211   | Node l _ r-> (Suc Zero) + nodes l + nodes r
 212   end
 213
 214   function height (t: tree 'a) : nat = match t with
 215   | Leaf -> Zero
 216   | Node l _ r -> Suc (max (height l) (height r))
 217   end
 218
 219 end
 220
 221 (******************************************************************************)
 222 (************************** ISAPLANNER THEOREMS *******************************)
 223 (******************************************************************************)
 224
 225 (*Pas d'induction(13): 4, 5, 11, 13, 16, 17, 35, 39, 40, 42, 44, 45, 46 *)
 226 (*Induction sur une variable(22): 2, 3, 6, 7, 8, 10, 12, 14, 15, 18, 19,
 227   21, 26, 27, 28, 29, 30, 32, 36, 37, 38, 43 *)
 228 (*Induction sur plusieurs variables à cause de raisonnement par cas (9):
 229   1, 9, 22, 23, 24, 25, 31, 33, 34, *)
 230 (*Problème résolu avec un lemme supplémentaire (2): 20(15), 47(23)  *)
 231 (******************************************************************************)
 232 theory IsaPlanner_all
 233
 234   use Nat
 235   use List
 236   use Tree
 237
 238   goal P1: forall l: list 'a, n : nat.
 239   take n l ++ drop n l = l
 240
 241   goal P2: forall l m: list 'a, x: 'a.
 242   count x l + count x m =  count  x (l ++ m)
 243
 244   goal P3: forall l m: list 'a, x: 'a.
 245   count x l <= count x (l ++ m)
 246
 247   goal P4: forall l: list 'a, x: 'a.
 248   Suc Zero + count x l = count x (Cons x l)
 249
 250   goal P5: forall l: list 'a, x y : 'a.
 251   x = y -> Suc Zero + count x l = count x (Cons y l)
 252
 253   goal P6: forall n m: nat.
 254   n - (n + m) = Zero
 255
 256   goal P7: forall n m: nat.
 257   (n + m) - n = m
 258
 259   goal P8: forall  k [@induction] n m: nat.
 260   (k + m) - (k + n) = (m - n)
 261
 262   goal P9: forall i j k: nat.
 263   (i - j) - k = i - (j + k)
 264
 265   goal P10: forall m: nat.
 266   m - m = Zero
 267
 268   goal P11: forall l: list 'a.
 269   drop Zero l = l
 270
 271   goal P12: forall f: 'a -> 'b, l, n.
 272   drop n (map f l) = map f (drop n l)
 273
 274   goal P13: forall n: nat, x: 'a, ls: list 'a.
 275   drop (Suc n) (Cons x ls) = drop n ls
 276
 277   goal P14: forall p, xs ys: list 'a.
 278   filter p (xs ++ ys) = filter p xs ++ filter p ys
 279
 280   goal P15: forall l: list nat, n: nat.
 281   len (insertion_sort_aux n l) = Suc (len l)
 282
 283   goal P16: forall l: list 'a, x: 'a.
 284   l = Nil -> last (Cons x l) = x
 285
 286   goal P17: forall n: nat.
 287   (n <= Zero) <-> (n = Zero)
 288
 289   goal P18: forall i m: nat.
 290   i < (Suc (i + m))
 291
 292   goal P19: forall l: list 'a, n: nat.
 293   len (drop n l) = (len l) - n
 294
 295   (* requires the lemma
 296       forall l: list nat, n: nat. len (insertion_sort_aux n l) = Suc (len l) *)
 297   goal P20: forall l: list nat.
 298   len (insertion_sort l) = len l
 299
 300   goal P21: forall n m: nat.
 301   n <= (n + m)
 302
 303   goal P22: forall a [@induction] b [@induction] c [@induction]: nat .
 304   max (max a b) c = max a (max b c)
 305
 306   goal P23: forall a b: nat.
 307   max a b = max b a
 308
 309   goal P24: forall a b: nat.
 310   (max a b = a) <-> b <= a
 311
 312   goal P25: forall a b: nat.
 313   (max a b = b) <-> a <= b
 314
 315   goal P26: forall l t: list 'a, x: 'a.
 316   mem x l -> mem x (l ++ t)
 317
 318   goal P27: forall l t: list 'a, x: 'a.
 319   mem x t -> mem x (l ++ t)
 320
 321   goal P28: forall l: list 'a, x: 'a.
 322   mem x (l ++ Cons x Nil)
 323
 324   goal P29: forall l : list nat, x : nat.
 325   mem x (insert_nat x l)
 326
 327   goal P30: forall l: list 'a, x: 'a.
 328   mem x (insert x l)
 329
 330   goal P31: forall a [@induction] b [@induction] c [@induction]: nat.
 331   min (min a b) c = min a (min b c)
 332
 333   goal P32: forall a b: nat.
 334   min a b = min b a
 335
 336   goal P33: forall a b: nat.
 337   (min a b = a) <-> a <= b
 338
 339   goal P34: forall a b: nat.
 340   (min a b = b) <-> b <= a
 341
 342   goal P35: forall xs : list 'a.
 343   dropWhile_False xs = xs
 344
 345   goal P36: forall xs: list 'a.
 346   takeWhile_True xs = xs
 347
 348   goal P37: forall l: list 'a, x: 'a.
 349   not mem x (delete x l)
 350
 351   goal P38: forall l: list 'a, n: 'a.
 352   count n (l ++ Cons n Nil) = Suc (count n l)
 353
 354   goal P39: forall t: list 'a, n h: 'a.
 355   count n (Cons h Nil) + count n t = count n (Cons h t)
 356
 357   goal P40: forall xs: list 'a.
 358   take Zero xs = Nil
 359
 360   goal P41: forall f, xs : list 'a, n: nat.
 361   take n (map f xs : list 'b) = map f (take n xs)
 362
 363   goal P42: forall xs: list 'a, n: nat, x: 'a.
 364   take (Suc n) (Cons x xs) = Cons x (take n xs)
 365
 366   goal P43: forall p, xs : list 'a.
 367   takeWhile p xs ++ dropWhile p xs = xs
 368
 369   goal P44: forall xs ys: list 'a, x: 'a.
 370   zip (Cons x xs) ys =
 371                   match ys with
 372                     | Nil -> Nil
 373                     | Cons y ys -> Cons (x,y) (zip xs ys)
 374                   end
 375
 376   goal P45: forall xs ys: list 'a, x y: 'a .
 377   zip (Cons x xs) (Cons y ys) = Cons (x, y) (zip xs ys)
 378
 379   goal P46: forall ys: list 'a.
 380   zip Nil ys = Nil
 381
 382   (* requires P23: forall a b: nat. max a b = max b a *)
 383   goal P47: forall a : tree 'a.
 384   height (mirror a) = height a
 385
 386 end
 387
 388 theory IsaPlanner_beyond
 389
 390   use Nat
 391   use List
 392   use Tree
 393
 394   goal P48: forall xs : list 'a.
 395   xs <> Nil  -> butlast xs ++ (Cons (last xs) Nil) = xs
 396
 397   goal P49: forall xs ys: list 'a .
 398   butlast (xs ++ ys) = (if ys = Nil then butlast xs else xs ++ butlast ys)
 399
 400   goal P50: forall xs : list 'a.
 401   butlast xs = take ((len xs) - (Suc Zero)) xs
 402
 403   goal P51: forall xs : list 'a, x: 'a.
 404   butlast (xs ++ Cons x Nil) = xs
 405
 406   goal P52: forall l : list 'a, n: 'a.
 407   count n l = count n (rev l)
 408
 409   goal P53: forall l : list nat, x : nat.
 410   count x l = count x (insertion_sort l)
 411
 412   goal P54: forall m n: nat.
 413   (m + n) - n = m
 414
 415   goal P55: forall i [@induction] k [@induction] j [@induction] : nat.
 416   (i - j) - k = i - (k - j)
 417
 418   goal P56: forall xs ys: list 'a, n: nat.
 419   drop n (xs ++ ys) = drop n xs ++ drop (n - (len xs)) ys
 420
 421   goal P57: forall n [@induction] m [@induction]: nat,
 422   xs [@induction]: list nat.
 423   drop n (drop m xs) = drop (n + m) xs
 424
 425   goal P58: forall xs [@induction]: list 'a,
 426   m [@induction] n [@induction]: nat.
 427   drop n (take m xs) = take (m - n) (drop n xs)
 428
 429 end