theory week08A_demo imports Complex_Main "~~/src/HOL/Library/RBT_Impl" begin text \ Sledgehammer setup \ sledgehammer_params [provers = e spass z3 cvc4, timeout = 10] text \ Quickcheck setup \ declare [[quickcheck_narrowing_active = false, quickcheck_size = 5]] section\ Standard Proof Automation \ subsection\ Simplification & Co \ lemma "length(xs @ xs) = 2 * length xs" using [[simp_trace]] by simp text\ Beyond simp: \ lemma "\ \xs\A. length xs \ 3; \xs\B. length xs \ 2 \ \ \xs \ A \ B. length xs \ {2,3}" apply simp try0 by fastforce subsection\ Logic & sets \ lemma "((P \ Q) \ P) \ P" by blast lemma "(\i \ I \ J. M i) \ (\i\I. M i) \ (\i\J. M i)" by blast subsection\ Arithmetic \ lemma "\k::nat > 119. \i j. k = 9*i + 16*j" by arith lemma "(x::int)^3 - x^2 - 5*x - 3 = 0 \ (x = 3 \ x = -1)" by algebra text\ But there is always a limit: \ lemma "(R \ S)^* \ R^*" try0 oops section \ Sledgehammer \ lemma "xs = Nil \ xs = Cons (hd xs) (tl xs)" try0 sledgehammer oops lemma "y = x * k \ gcd (x::int) y = abs x" sledgehammer sorry lemma "xs = ys @ xs @ ys \ ys = []" sledgehammer sorry lemma "\!x. f (g x) = x \ \!y. g (f y) = y" sledgehammer sorry lemma "(X = Y \ Z) = (X \ Y \ X \ Z \ (\V. V \ Y \ V \ Z \ V \ X))" sledgehammer [isar_proof] (* sledgehammer [isar_proof, compress=3] *) sorry section \ Quickcheck \ lemma "rev (xs @ ys) = rev xs @ rev ys" quickcheck oops lemma "map (f o g) xs = map g (map f xs)" quickcheck oops subsection \ Quantifiers \ text \ Typical beginner errors: Existential and Universal Quantifiers can be swapped... ... but not this way. \ lemma "(\x. \y. P x y) \ (\y. \x. P x y)" quickcheck oops lemma "(\x :: nat. \y :: nat. P x y) \ (\y. \x. P x y)" quickcheck nitpick (*quickcheck -- fails, because the natural numbers are infinite *) (*nitpick only finds a potential one *) oops subsection \ Inequalities on reals \ (* we switch off support for printing functions, but obtain a faster execution for the next examples *) declare [[quickcheck_full_support = false]] text \ An example about inequalities on real numbers: \ lemma "\ (a::real) > 0; b > 0; c > 0; a * a \ b * (c + 1); b \ 4 * c \ \ (a - 1) * (a - 1) < b * c" quickcheck oops text \ So, it does not hold, for arbitrary positive rational numbers. In the context, the lemma was used, the user actually knew that a >= 1. \ lemma "\ (a::real) \ 1; b > 0; c > 0; a * a \ b * (c + 1); b \ 4 * c \ \ (a - 1) * (a - 1) < b * c" quickcheck oops text \ But let us now explore what the exact constraints and bounds are: First, we drop the constraints b > 0 and c > 0. \ lemma "\ (a::real) \ 1; a * a \ b * (c + 1); b \ 4 * c \ \ (a - 1) * (a - 1) < b * c" quickcheck oops text \ Secondly, we determine an exact bound for a. 1/2 was a counterexample beforehand -- is there another larger one? \ lemma "\ (a::real) > 1/2; a * a \ b * (c + 1); b \ 4 * c \ \ (a - 1) * (a - 1) < b * c" quickcheck oops text \ But is there a counterexample with a > 3/4 ?? \ lemma "\ (a::real) > 3/4; a * a \ b * (c + 1); b \ 4 * c \ \ (a - 1) * (a - 1) < b * c" quickcheck oops text \ Is 3/4 a tight bound for a? Let's try. \ lemma "\ (a::real) \ 3/4; a * a \ b * (c + 1); b \ 4 * c \ \ (a - 1) * (a - 1) < b * c" quickcheck quickcheck[size = 10] oops text\ More numeric curiosities: \ definition prime :: "nat \ bool" where "prime p \ (1 < p \ (\m m = 1))" lemma "prime(n^2 + n + 41)" quickcheck oops lemma "\n<40. prime(n^2 + n + 41)" by eval declare [[quickcheck_full_support = true]] subsection \ Narrowing-based Quickcheck \ text \ The example with quantifiers from before: With symbolic execution we can actually find a counterexample even on infinite domains. \ lemma "(\x::nat. \y::nat. P x y) \ (\y'. \x'. P x' y')" quickcheck nitpick quickcheck[narrowing, size = 7] oops text \ a slightly flawed delete operation on Red-Black-Trees \ (* replaced balance_left by balance_right in del_from_left x (Branch B lt z v rt) y s b *) fun del_from_left :: "('a::linorder) \ ('a,'b) rbt \ 'a \ 'b \ ('a,'b) rbt \ ('a,'b) rbt" and del_from_right :: "('a::linorder) \ ('a,'b) rbt \ 'a \ 'b \ ('a,'b) rbt \ ('a,'b) rbt" and del :: "('a::linorder) \ ('a,'b) rbt \ ('a,'b) rbt" where "del x rbt.Empty = rbt.Empty" | "del x (Branch c a y s b) = (if x < y then del_from_left x a y s b else (if x > y then del_from_right x a y s b else combine a b))" | "del_from_left x (Branch RBT_Impl.B lt z v rt) y s b = balance_right (del x (Branch RBT_Impl.B lt z v rt)) y s b" | "del_from_left x a y s b = Branch RBT_Impl.R (del x a) y s b" | "del_from_right x a y s (Branch RBT_Impl.B lt z v rt) = balance_right a y s (del x (Branch RBT_Impl.B lt z v rt))" | "del_from_right x a y s b = Branch RBT_Impl.R a y s (del x b)" definition delete where delete_def: "delete k t = paint RBT_Impl.B (del k t)" theorem delete_is_rbt: "is_rbt (t :: (int,int)rbt) \ is_rbt (delete k t)" quickcheck[narrowing] (* compare with exhaustive and random *) quickcheck quickcheck[random,size=20] oops section \ Nitpick \ lemma "(R \ S)^* = R^* \ S^*" nitpick oops lemma "acyclic R \ acyclic S \ acyclic(R \ S)" nitpick oops lemma "append xs ys = xs \ ys = Nil" nitpick oops end