Theory Quickcheck_Narrowing_Examples
section ‹Examples for narrowing-based testing›
theory Quickcheck_Narrowing_Examples
imports Main
begin
declare [[quickcheck_timeout = 3600]]
subsection ‹Minimalistic examples›
lemma
"x = y"
quickcheck[tester = narrowing, finite_types = false, default_type = int, expect = counterexample]
oops
lemma
"x = y"
quickcheck[tester = narrowing, finite_types = false, default_type = nat, expect = counterexample]
oops
subsection ‹Simple examples with existentials›
lemma
"∃ y :: nat. ∀ x. x = y"
quickcheck[tester = narrowing, finite_types = false, expect = counterexample]
oops
lemma
"x > 1 --> (∃y :: nat. x < y & y <= 1)"
quickcheck[tester = narrowing, finite_types = false, expect = counterexample]
oops
lemma
"x > 2 ⟶ (∃y :: nat. x < y ∧ y ≤ 2)"
quickcheck[tester = narrowing, finite_types = false, size = 10]
oops
lemma
"∀x. ∃y :: nat. x > 3 ⟶ (y < x ∧ y > 3)"
quickcheck[tester = narrowing, finite_types = false, size = 7]
oops
text ‹A false conjecture derived from an partial copy-n-paste of @{thm not_distinct_decomp}›
lemma
"¬ distinct ws ⟹ ∃xs ys zs y. ws = xs @ [y] @ ys @ [y]"
quickcheck[tester = narrowing, finite_types = false, default_type = nat, expect = counterexample]
oops
text ‹A false conjecture derived from theorems @{thm split_list_first} and @{thm split_list_last}›
lemma
"x ∈ set xs ⟹ ∃ys zs. xs = ys @ x # zs ∧ x ∉ set zs ∧ x ∉ set ys"
quickcheck[tester = narrowing, finite_types = false, default_type = nat, expect = counterexample]
oops
text ‹A false conjecture derived from @{thm map_eq_Cons_conv} with a typo›
lemma
"(map f xs = y # ys) = (∃z zs. xs = z' # zs & f z = y ∧ map f zs = ys)"
quickcheck[tester = narrowing, finite_types = false, default_type = nat, expect = counterexample]
oops
lemma "a # xs = ys @ [a] ⟹ ∃zs. xs = zs @ [a] ∧ ys = a#zs"
quickcheck[narrowing, expect = counterexample]
quickcheck[exhaustive, random, expect = no_counterexample]
oops
subsection ‹Simple list examples›
lemma "rev xs = xs"
quickcheck[tester = narrowing, finite_types = false, default_type = nat, expect = counterexample]
oops
lemma "rev xs = xs"
quickcheck[tester = narrowing, finite_types = false, default_type = int, expect = counterexample]
oops
lemma "rev xs = xs"
quickcheck[tester = narrowing, finite_types = true, expect = counterexample]
oops
subsection ‹Simple examples with functions›
lemma "map f xs = map g xs"
quickcheck[tester = narrowing, finite_types = false, expect = counterexample]
oops
lemma "map f xs = map f ys ==> xs = ys"
quickcheck[tester = narrowing, finite_types = false, expect = counterexample]
oops
lemma
"list_all2 P (rev xs) (rev ys) = list_all2 P xs (rev ys)"
quickcheck[tester = narrowing, finite_types = false, expect = counterexample]
oops
lemma "map f xs = F f xs"
quickcheck[tester = narrowing, finite_types = false, expect = counterexample]
oops
lemma "map f xs = F f xs"
quickcheck[tester = narrowing, finite_types = false, expect = counterexample]
oops
subsection ‹Simple examples with inductive predicates›
inductive even where
"even 0" |
"even n ==> even (Suc (Suc n))"
code_pred even .
lemma "even (n - 2) ==> even n"
quickcheck[narrowing, expect = counterexample]
oops
subsection ‹AVL Trees›