src/HOL/Quickcheck_Examples/Quickcheck_Examples.thy
author haftmann
Mon Jun 05 15:59:41 2017 +0200 (2017-06-05)
changeset 66010 2f7d39285a1a
parent 63901 4ce989e962e0
child 66453 cc19f7ca2ed6
permissions -rw-r--r--
executable domain membership checks
     1 (*  Title:      HOL/Quickcheck_Examples/Quickcheck_Examples.thy
     2     Author:     Stefan Berghofer, Lukas Bulwahn
     3     Copyright   2004 - 2010 TU Muenchen
     4 *)
     5 
     6 section \<open>Examples for the 'quickcheck' command\<close>
     7 
     8 theory Quickcheck_Examples
     9 imports Complex_Main "~~/src/HOL/Library/Dlist" "~~/src/HOL/Library/DAList_Multiset"
    10 begin
    11 
    12 text \<open>
    13 The 'quickcheck' command allows to find counterexamples by evaluating
    14 formulae.
    15 Currently, there are two different exploration schemes:
    16 - random testing: this is incomplete, but explores the search space faster.
    17 - exhaustive testing: this is complete, but increasing the depth leads to
    18   exponentially many assignments.
    19 
    20 quickcheck can handle quantifiers on finite universes.
    21 
    22 \<close>
    23 
    24 declare [[quickcheck_timeout = 3600]]
    25 
    26 subsection \<open>Lists\<close>
    27 
    28 theorem "map g (map f xs) = map (g o f) xs"
    29   quickcheck[random, expect = no_counterexample]
    30   quickcheck[exhaustive, size = 3, expect = no_counterexample]
    31   oops
    32 
    33 theorem "map g (map f xs) = map (f o g) xs"
    34   quickcheck[random, expect = counterexample]
    35   quickcheck[exhaustive, expect = counterexample]
    36   oops
    37 
    38 theorem "rev (xs @ ys) = rev ys @ rev xs"
    39   quickcheck[random, expect = no_counterexample]
    40   quickcheck[exhaustive, expect = no_counterexample]
    41   quickcheck[exhaustive, size = 1000, timeout = 0.1]
    42   oops
    43 
    44 theorem "rev (xs @ ys) = rev xs @ rev ys"
    45   quickcheck[random, expect = counterexample]
    46   quickcheck[exhaustive, expect = counterexample]
    47   oops
    48 
    49 theorem "rev (rev xs) = xs"
    50   quickcheck[random, expect = no_counterexample]
    51   quickcheck[exhaustive, expect = no_counterexample]
    52   oops
    53 
    54 theorem "rev xs = xs"
    55   quickcheck[tester = random, finite_types = true, report = false, expect = counterexample]
    56   quickcheck[tester = random, finite_types = false, report = false, expect = counterexample]
    57   quickcheck[tester = random, finite_types = true, report = true, expect = counterexample]
    58   quickcheck[tester = random, finite_types = false, report = true, expect = counterexample]
    59   quickcheck[tester = exhaustive, finite_types = true, expect = counterexample]
    60   quickcheck[tester = exhaustive, finite_types = false, expect = counterexample]
    61 oops
    62 
    63 
    64 text \<open>An example involving functions inside other data structures\<close>
    65 
    66 primrec app :: "('a \<Rightarrow> 'a) list \<Rightarrow> 'a \<Rightarrow> 'a" where
    67   "app [] x = x"
    68   | "app (f # fs) x = app fs (f x)"
    69 
    70 lemma "app (fs @ gs) x = app gs (app fs x)"
    71   quickcheck[random, expect = no_counterexample]
    72   quickcheck[exhaustive, size = 2, expect = no_counterexample]
    73   by (induct fs arbitrary: x) simp_all
    74 
    75 lemma "app (fs @ gs) x = app fs (app gs x)"
    76   quickcheck[random, expect = counterexample]
    77   quickcheck[exhaustive, expect = counterexample]
    78   oops
    79 
    80 primrec occurs :: "'a \<Rightarrow> 'a list \<Rightarrow> nat" where
    81   "occurs a [] = 0"
    82   | "occurs a (x#xs) = (if (x=a) then Suc(occurs a xs) else occurs a xs)"
    83 
    84 primrec del1 :: "'a \<Rightarrow> 'a list \<Rightarrow> 'a list" where
    85   "del1 a [] = []"
    86   | "del1 a (x#xs) = (if (x=a) then xs else (x#del1 a xs))"
    87 
    88 text \<open>A lemma, you'd think to be true from our experience with delAll\<close>
    89 lemma "Suc (occurs a (del1 a xs)) = occurs a xs"
    90   \<comment> \<open>Wrong. Precondition needed.\<close>
    91   quickcheck[random, expect = counterexample]
    92   quickcheck[exhaustive, expect = counterexample]
    93   oops
    94 
    95 lemma "xs ~= [] \<longrightarrow> Suc (occurs a (del1 a xs)) = occurs a xs"
    96   quickcheck[random, expect = counterexample]
    97   quickcheck[exhaustive, expect = counterexample]
    98     \<comment> \<open>Also wrong.\<close>
    99   oops
   100 
   101 lemma "0 < occurs a xs \<longrightarrow> Suc (occurs a (del1 a xs)) = occurs a xs"
   102   quickcheck[random, expect = no_counterexample]
   103   quickcheck[exhaustive, expect = no_counterexample]
   104   by (induct xs) auto
   105 
   106 primrec replace :: "'a \<Rightarrow> 'a \<Rightarrow> 'a list \<Rightarrow> 'a list" where
   107   "replace a b [] = []"
   108   | "replace a b (x#xs) = (if (x=a) then (b#(replace a b xs)) 
   109                             else (x#(replace a b xs)))"
   110 
   111 lemma "occurs a xs = occurs b (replace a b xs)"
   112   quickcheck[random, expect = counterexample]
   113   quickcheck[exhaustive, expect = counterexample]
   114   \<comment> \<open>Wrong. Precondition needed.\<close>
   115   oops
   116 
   117 lemma "occurs b xs = 0 \<or> a=b \<longrightarrow> occurs a xs = occurs b (replace a b xs)"
   118   quickcheck[random, expect = no_counterexample]
   119   quickcheck[exhaustive, expect = no_counterexample]
   120   by (induct xs) simp_all
   121 
   122 
   123 subsection \<open>Trees\<close>
   124 
   125 datatype 'a tree = Twig |  Leaf 'a | Branch "'a tree" "'a tree"
   126 
   127 primrec leaves :: "'a tree \<Rightarrow> 'a list" where
   128   "leaves Twig = []"
   129   | "leaves (Leaf a) = [a]"
   130   | "leaves (Branch l r) = (leaves l) @ (leaves r)"
   131 
   132 primrec plant :: "'a list \<Rightarrow> 'a tree" where
   133   "plant [] = Twig "
   134   | "plant (x#xs) = Branch (Leaf x) (plant xs)"
   135 
   136 primrec mirror :: "'a tree \<Rightarrow> 'a tree" where
   137   "mirror (Twig) = Twig "
   138   | "mirror (Leaf a) = Leaf a "
   139   | "mirror (Branch l r) = Branch (mirror r) (mirror l)"
   140 
   141 theorem "plant (rev (leaves xt)) = mirror xt"
   142   quickcheck[random, expect = counterexample]
   143   quickcheck[exhaustive, expect = counterexample]
   144     \<comment>\<open>Wrong!\<close> 
   145   oops
   146 
   147 theorem "plant((leaves xt) @ (leaves yt)) = Branch xt yt"
   148   quickcheck[random, expect = counterexample]
   149   quickcheck[exhaustive, expect = counterexample]
   150     \<comment>\<open>Wrong!\<close> 
   151   oops
   152 
   153 datatype 'a ntree = Tip "'a" | Node "'a" "'a ntree" "'a ntree"
   154 
   155 primrec inOrder :: "'a ntree \<Rightarrow> 'a list" where
   156   "inOrder (Tip a)= [a]"
   157   | "inOrder (Node f x y) = (inOrder x)@[f]@(inOrder y)"
   158 
   159 primrec root :: "'a ntree \<Rightarrow> 'a" where
   160   "root (Tip a) = a"
   161   | "root (Node f x y) = f"
   162 
   163 theorem "hd (inOrder xt) = root xt"
   164   quickcheck[random, expect = counterexample]
   165   quickcheck[exhaustive, expect = counterexample]
   166   \<comment>\<open>Wrong!\<close> 
   167   oops
   168 
   169 
   170 subsection \<open>Exhaustive Testing beats Random Testing\<close>
   171 
   172 text \<open>Here are some examples from mutants from the List theory
   173 where exhaustive testing beats random testing\<close>
   174 
   175 lemma
   176   "[] ~= xs ==> hd xs = last (x # xs)"
   177 quickcheck[random]
   178 quickcheck[exhaustive, expect = counterexample]
   179 oops
   180 
   181 lemma
   182   assumes "!!i. [| i < n; i < length xs |] ==> P (xs ! i)" "n < length xs ==> ~ P (xs ! n)"
   183   shows "drop n xs = takeWhile P xs"
   184 quickcheck[random, iterations = 10000, quiet]
   185 quickcheck[exhaustive, expect = counterexample]
   186 oops
   187 
   188 lemma
   189   "i < length (List.transpose (List.transpose xs)) ==> xs ! i = map (%xs. xs ! i) [ys<-xs. i < length ys]"
   190 quickcheck[random, iterations = 10000]
   191 quickcheck[exhaustive, expect = counterexample]
   192 oops
   193 
   194 lemma
   195   "i < n - m ==> f (lcm m i) = map f [m..<n] ! i"
   196 quickcheck[random, iterations = 10000, finite_types = false]
   197 quickcheck[exhaustive, finite_types = false, expect = counterexample]
   198 oops
   199 
   200 lemma
   201   "i < n - m ==> f (lcm m i) = map f [m..<n] ! i"
   202 quickcheck[random, iterations = 10000, finite_types = false]
   203 quickcheck[exhaustive, finite_types = false, expect = counterexample]
   204 oops
   205 
   206 lemma
   207   "ns ! k < length ns ==> k <= sum_list ns"
   208 quickcheck[random, iterations = 10000, finite_types = false, quiet]
   209 quickcheck[exhaustive, finite_types = false, expect = counterexample]
   210 oops
   211 
   212 lemma
   213   "[| ys = x # xs1; zs = xs1 @ xs |] ==> ys @ zs = x # xs"
   214 quickcheck[random, iterations = 10000]
   215 quickcheck[exhaustive, expect = counterexample]
   216 oops
   217 
   218 lemma
   219 "i < length xs ==> take (Suc i) xs = [] @ xs ! i # take i xs"
   220 quickcheck[random, iterations = 10000]
   221 quickcheck[exhaustive, expect = counterexample]
   222 oops
   223 
   224 lemma
   225   "i < length xs ==> take (Suc i) xs = (xs ! i # xs) @ take i []"
   226 quickcheck[random, iterations = 10000]
   227 quickcheck[exhaustive, expect = counterexample]
   228 oops
   229 
   230 lemma
   231   "[| sorted (rev (map length xs)); i < length xs |] ==> xs ! i = map (%ys. ys ! i) [ys<-remdups xs. i < length ys]"
   232 quickcheck[random]
   233 quickcheck[exhaustive, expect = counterexample]
   234 oops
   235 
   236 lemma
   237   "[| sorted (rev (map length xs)); i < length xs |] ==> xs ! i = map (%ys. ys ! i) [ys<-List.transpose xs. length ys \<in> {..<i}]"
   238 quickcheck[random]
   239 quickcheck[exhaustive, expect = counterexample]
   240 oops
   241 
   242 lemma
   243   "(ys = zs) = (xs @ ys = splice xs zs)"
   244 quickcheck[random]
   245 quickcheck[exhaustive, expect = counterexample]
   246 oops
   247 
   248 subsection \<open>Random Testing beats Exhaustive Testing\<close>
   249 
   250 lemma mult_inj_if_coprime_nat:
   251   "inj_on f A \<Longrightarrow> inj_on g B
   252    \<Longrightarrow> inj_on (%(a,b). f a * g b::nat) (A \<times> B)"
   253 quickcheck[exhaustive]
   254 quickcheck[random]
   255 oops
   256 
   257 subsection \<open>Examples with quantifiers\<close>
   258 
   259 text \<open>
   260   These examples show that we can handle quantifiers.
   261 \<close>
   262 
   263 lemma "(\<exists>x. P x) \<longrightarrow> (\<forall>x. P x)"
   264   quickcheck[random, expect = counterexample]
   265   quickcheck[exhaustive, expect = counterexample]
   266 oops
   267 
   268 lemma "(\<forall>x. \<exists>y. P x y) \<longrightarrow> (\<exists>y. \<forall>x. P x y)"
   269   quickcheck[random, expect = counterexample]
   270   quickcheck[expect = counterexample]
   271 oops
   272 
   273 lemma "(\<exists>x. P x) \<longrightarrow> (\<exists>!x. P x)"
   274   quickcheck[random, expect = counterexample]
   275   quickcheck[expect = counterexample]
   276 oops
   277 
   278 
   279 subsection \<open>Examples with sets\<close>
   280 
   281 lemma
   282   "{} = A Un - A"
   283 quickcheck[exhaustive, expect = counterexample]
   284 oops
   285 
   286 lemma
   287   "[| bij_betw f A B; bij_betw f C D |] ==> bij_betw f (A Un C) (B Un D)"
   288 quickcheck[exhaustive, expect = counterexample]
   289 oops
   290 
   291 
   292 subsection \<open>Examples with relations\<close>
   293 
   294 lemma
   295   "acyclic (R :: ('a * 'a) set) ==> acyclic S ==> acyclic (R Un S)"
   296 quickcheck[exhaustive, expect = counterexample]
   297 oops
   298 
   299 lemma
   300   "acyclic (R :: (nat * nat) set) ==> acyclic S ==> acyclic (R Un S)"
   301 quickcheck[exhaustive, expect = counterexample]
   302 oops
   303 
   304 (* FIXME: some dramatic performance decrease after changing the code equation of the ntrancl *)
   305 lemma
   306   "(x, z) : rtrancl (R Un S) ==> \<exists> y. (x, y) : rtrancl R & (y, z) : rtrancl S"
   307 (*quickcheck[exhaustive, expect = counterexample]*)
   308 oops
   309 
   310 lemma
   311   "wf (R :: ('a * 'a) set) ==> wf S ==> wf (R Un S)"
   312 quickcheck[exhaustive, expect = counterexample]
   313 oops
   314 
   315 lemma
   316   "wf (R :: (nat * nat) set) ==> wf S ==> wf (R Un S)"
   317 quickcheck[exhaustive, expect = counterexample]
   318 oops
   319 
   320 lemma
   321   "wf (R :: (int * int) set) ==> wf S ==> wf (R Un S)"
   322 quickcheck[exhaustive, expect = counterexample]
   323 oops
   324 
   325 
   326 subsection \<open>Examples with the descriptive operator\<close>
   327 
   328 lemma
   329   "(THE x. x = a) = b"
   330 quickcheck[random, expect = counterexample]
   331 quickcheck[exhaustive, expect = counterexample]
   332 oops
   333 
   334 subsection \<open>Examples with Multisets\<close>
   335 
   336 lemma
   337   "X + Y = Y + (Z :: 'a multiset)"
   338 quickcheck[random, expect = counterexample]
   339 quickcheck[exhaustive, expect = counterexample]
   340 oops
   341 
   342 lemma
   343   "X - Y = Y - (Z :: 'a multiset)"
   344 quickcheck[random, expect = counterexample]
   345 quickcheck[exhaustive, expect = counterexample]
   346 oops
   347 
   348 lemma
   349   "N + M - N = (N::'a multiset)"
   350 quickcheck[random, expect = counterexample]
   351 quickcheck[exhaustive, expect = counterexample]
   352 oops
   353 
   354 subsection \<open>Examples with numerical types\<close>
   355 
   356 text \<open>
   357 Quickcheck supports the common types nat, int, rat and real.
   358 \<close>
   359 
   360 lemma
   361   "(x :: nat) > 0 ==> y > 0 ==> z > 0 ==> x * x + y * y \<noteq> z * z"
   362 quickcheck[exhaustive, size = 10, expect = counterexample]
   363 quickcheck[random, size = 10]
   364 oops
   365 
   366 lemma
   367   "(x :: int) > 0 ==> y > 0 ==> z > 0 ==> x * x + y * y \<noteq> z * z"
   368 quickcheck[exhaustive, size = 10, expect = counterexample]
   369 quickcheck[random, size = 10]
   370 oops
   371 
   372 lemma
   373   "(x :: rat) > 0 ==> y > 0 ==> z > 0 ==> x * x + y * y \<noteq> z * z"
   374 quickcheck[exhaustive, size = 10, expect = counterexample]
   375 quickcheck[random, size = 10]
   376 oops
   377 
   378 lemma "(x :: rat) >= 0"
   379 quickcheck[random, expect = counterexample]
   380 quickcheck[exhaustive, expect = counterexample]
   381 oops
   382 
   383 lemma
   384   "(x :: real) > 0 ==> y > 0 ==> z > 0 ==> x * x + y * y \<noteq> z * z"
   385 quickcheck[exhaustive, size = 10, expect = counterexample]
   386 quickcheck[random, size = 10]
   387 oops
   388 
   389 lemma "(x :: real) >= 0"
   390 quickcheck[random, expect = counterexample]
   391 quickcheck[exhaustive, expect = counterexample]
   392 oops
   393 
   394 subsubsection \<open>floor and ceiling functions\<close>
   395 
   396 lemma "\<lfloor>x\<rfloor> + \<lfloor>y\<rfloor> = \<lfloor>x + y :: rat\<rfloor>"
   397 quickcheck[expect = counterexample]
   398 oops
   399 
   400 lemma "\<lfloor>x\<rfloor> + \<lfloor>y\<rfloor> = \<lfloor>x + y :: real\<rfloor>"
   401 quickcheck[expect = counterexample]
   402 oops
   403 
   404 lemma "\<lceil>x\<rceil> + \<lceil>y\<rceil> = \<lceil>x + y :: rat\<rceil>"
   405 quickcheck[expect = counterexample]
   406 oops
   407 
   408 lemma "\<lceil>x\<rceil> + \<lceil>y\<rceil> = \<lceil>x + y :: real\<rceil>"
   409 quickcheck[expect = counterexample]
   410 oops
   411 
   412 subsection \<open>Examples with abstract types\<close>
   413 
   414 lemma
   415   "Dlist.length (Dlist.remove x xs) = Dlist.length xs - 1"
   416 quickcheck[exhaustive]
   417 quickcheck[random]
   418 oops
   419 
   420 lemma
   421   "Dlist.length (Dlist.insert x xs) = Dlist.length xs + 1"
   422 quickcheck[exhaustive]
   423 quickcheck[random]
   424 oops
   425 
   426 subsection \<open>Examples with Records\<close>
   427 
   428 record point =
   429   xpos :: nat
   430   ypos :: nat
   431 
   432 lemma
   433   "xpos r = xpos r' ==> r = r'"
   434 quickcheck[exhaustive, expect = counterexample]
   435 quickcheck[random, expect = counterexample]
   436 oops
   437 
   438 datatype colour = Red | Green | Blue
   439 
   440 record cpoint = point +
   441   colour :: colour
   442 
   443 lemma
   444   "xpos r = xpos r' ==> ypos r = ypos r' ==> (r :: cpoint) = r'"
   445 quickcheck[exhaustive, expect = counterexample]
   446 quickcheck[random, expect = counterexample]
   447 oops
   448 
   449 subsection \<open>Examples with locales\<close>
   450 
   451 locale Truth
   452 
   453 context Truth
   454 begin
   455 
   456 lemma "False"
   457 quickcheck[exhaustive, expect = counterexample]
   458 oops
   459 
   460 end
   461 
   462 interpretation Truth .
   463 
   464 context Truth
   465 begin
   466 
   467 lemma "False"
   468 quickcheck[exhaustive, expect = counterexample]
   469 oops
   470 
   471 end
   472 
   473 locale antisym =
   474   fixes R
   475   assumes "R x y --> R y x --> x = y"
   476 
   477 interpretation equal : antisym "op =" by standard simp
   478 interpretation order_nat : antisym "op <= :: nat => _ => _" by standard simp
   479 
   480 lemma (in antisym)
   481   "R x y --> R y z --> R x z"
   482 quickcheck[exhaustive, finite_type_size = 2, expect = no_counterexample]
   483 quickcheck[exhaustive, expect = counterexample]
   484 oops
   485 
   486 declare [[quickcheck_locale = "interpret"]]
   487 
   488 lemma (in antisym)
   489   "R x y --> R y z --> R x z"
   490 quickcheck[exhaustive, expect = no_counterexample]
   491 oops
   492 
   493 declare [[quickcheck_locale = "expand"]]
   494 
   495 lemma (in antisym)
   496   "R x y --> R y z --> R x z"
   497 quickcheck[exhaustive, finite_type_size = 2, expect = no_counterexample]
   498 quickcheck[exhaustive, expect = counterexample]
   499 oops
   500 
   501 
   502 subsection \<open>Examples with HOL quantifiers\<close>
   503 
   504 lemma
   505   "\<forall> xs ys. xs = [] --> xs = ys"
   506 quickcheck[exhaustive, expect = counterexample]
   507 oops
   508 
   509 lemma
   510   "ys = [] --> (\<forall>xs. xs = [] --> xs = y # ys)"
   511 quickcheck[exhaustive, expect = counterexample]
   512 oops
   513 
   514 lemma
   515   "\<forall>xs. (\<exists> ys. ys = []) --> xs = ys"
   516 quickcheck[exhaustive, expect = counterexample]
   517 oops
   518 
   519 subsection \<open>Examples with underspecified/partial functions\<close>
   520 
   521 lemma
   522   "xs = [] ==> hd xs \<noteq> x"
   523 quickcheck[exhaustive, expect = no_counterexample]
   524 quickcheck[random, report = false, expect = no_counterexample]
   525 quickcheck[random, report = true, expect = no_counterexample]
   526 oops
   527 
   528 lemma
   529   "xs = [] ==> hd xs = x"
   530 quickcheck[exhaustive, expect = no_counterexample]
   531 quickcheck[random, report = false, expect = no_counterexample]
   532 quickcheck[random, report = true, expect = no_counterexample]
   533 oops
   534 
   535 lemma "xs = [] ==> hd xs = x ==> x = y"
   536 quickcheck[exhaustive, expect = no_counterexample]
   537 quickcheck[random, report = false, expect = no_counterexample]
   538 quickcheck[random, report = true, expect = no_counterexample]
   539 oops
   540 
   541 text \<open>with the simple testing scheme\<close>
   542 
   543 setup Exhaustive_Generators.setup_exhaustive_datatype_interpretation
   544 declare [[quickcheck_full_support = false]]
   545 
   546 lemma
   547   "xs = [] ==> hd xs \<noteq> x"
   548 quickcheck[exhaustive, expect = no_counterexample]
   549 oops
   550 
   551 lemma
   552   "xs = [] ==> hd xs = x"
   553 quickcheck[exhaustive, expect = no_counterexample]
   554 oops
   555 
   556 lemma "xs = [] ==> hd xs = x ==> x = y"
   557 quickcheck[exhaustive, expect = no_counterexample]
   558 oops
   559 
   560 declare [[quickcheck_full_support = true]]
   561 
   562 
   563 subsection \<open>Equality Optimisation\<close>
   564 
   565 lemma
   566   "f x = y ==> y = (0 :: nat)"
   567 quickcheck
   568 oops
   569 
   570 lemma
   571   "y = f x ==> y = (0 :: nat)"
   572 quickcheck
   573 oops
   574 
   575 lemma
   576   "f y = zz # zzs ==> zz = (0 :: nat) \<and> zzs = []"
   577 quickcheck
   578 oops
   579 
   580 lemma
   581   "f y = x # x' # xs ==> x = (0 :: nat) \<and> x' = 0 \<and> xs = []"
   582 quickcheck
   583 oops
   584 
   585 lemma
   586   "x = f x \<Longrightarrow> x = (0 :: nat)"
   587 quickcheck
   588 oops
   589 
   590 lemma
   591   "f y = x # x # xs ==> x = (0 :: nat) \<and> xs = []"
   592 quickcheck
   593 oops
   594 
   595 lemma
   596   "m1 k = Some v \<Longrightarrow> (m1 ++ m2) k = Some v"
   597 quickcheck
   598 oops
   599 
   600 
   601 end