---------------------------------------------------------------------------------- -- Induction and Simplification -- ---------------------------------------------------------------------------------- 37 theorems solved by induction and simplification, supplied with only with function defintions. term | time ------------------------------------------------+------- xs ~= [] ==> butlast xs @ [last xs] = xs | 0.01 butlast (xs @ [x]) = xs | 0.016 count n l + count n m = count n (l @ m) | 0.008 count n l leq count n (l @ m) | 0.007 suc 0 + count n l = count n (n # l) | 0.006 n = x ==> suc 0 + count n l = count n (x # l) | 0.009 n minus (n + m) = 0 | 0.016 (n + m) minus n = m | 0.02 (k + m) minus (k + n) = m minus n | 0.007 m minus m = 0 | 0.003 drop 0 xs = xs | 0.003 drop (suc n) (x # xs) = drop n xs | 0.006 filter P (xs @ ys) = filter P xs @ filter P ys | 0.013 len ins x l = suc len l | 0.007 ys = [] ==> last (xs @ ys) = last xs | 0.025 xs = [] ==> last (x # xs) = x | 0.008 xs ~= [] ==> last (x # xs) = last xs | 0.009 last (xs @ [x]) = x | 0.019 n leq 0 = (n = 0) | 0.004 i less (suc (i + m)) | 0.005 n leq (n + m) | 0.014 x mem l --> x mem l @ t | 0.011 x mem t --> x mem l @ t | 0.01 x mem l @ [x] | 0.007 x mem ins_1 x l | 0.007 x ~= y ==> x mem ins y l = x mem l | 0.02 x mem ins x l | 0.008 dropWhile (%x. False) xs = xs | 0.003 takeWhile (%x. True) xs = xs | 0.003 ~ x mem delete x l | 0.007 count n (x @ [n]) = suc count n x | 0.007 count n [h] + count n t = count n (h # t) | 0.017 take 0 xs = [] | 0.003 take (suc n) (x # xs) = x # take n xs | 0.007 takeWhile P xs @ dropWhile P xs = xs | 0.007 zip (x # xs) (y # ys) = (x, y) # zip xs ys | 0.01 zip [] ys = [] | 0.003 (37 rows) 50 theorems where induction and simplification fails. Timeout limit is 30 seconds. term | time -------------------------------------------------------------------------------------------+------- take n xs @ drop n xs = xs | 30 butlast (xs @ ys) = (if ys = [] then butlast xs else xs @ butlast ys) | 0.56 butlast xs = take ((len xs) minus (suc 0)) xs | 0.066 count n l = count n (rev l) | 0.078 count x l = count x (sort l) | 0.608 (m + n) minus n = m | 30 (i minus j) minus k = i minus (k minus j) | 30 (i minus j) minus k = i minus (j + k) | 30 drop n (xs @ ys) = drop n xs @ drop (n minus (len xs)) ys | 30 drop n (drop m xs) = drop (n + m) xs | 30 drop n (map f xs) = map f (drop n xs) | 30 drop n (take m xs) = take (m minus n) (drop n xs) | 30 drop n (zip xs ys) = zip (drop n xs) (drop n ys) | 30 ys ~= [] ==> last (xs @ ys) = last ys | 0.127 last (xs @ ys) = (if ys = [] then last xs else last ys) | 0.427 n less (len xs) ==> last (drop n xs) = last xs | 30 i less (suc (m + i)) | 30 (len filter P xs) leq (len xs) | 30 len butlast xs = (len xs) minus (suc 0) | 0.03 (len delete x l) leq (len l) | 30 len drop n xs = (len xs) minus n | 30 len sort l = len l | 30 n leq (m + n) | 30 m leq n ==> m leq (suc n) | 0.038 CaseAnalysis2.max (CaseAnalysis2.max a b) c = CaseAnalysis2.max a (CaseAnalysis2.max b c) | 30 CaseAnalysis2.max a b = CaseAnalysis2.max b a | 30 (CaseAnalysis2.max a b = a) = b leq a | 30 (CaseAnalysis2.max a b = b) = a leq b | 30 x less y ==> x mem ins y l = x mem l | 30 CaseAnalysis2.min (CaseAnalysis2.min a b) c = CaseAnalysis2.min a (CaseAnalysis2.min b c) | 30 CaseAnalysis2.min a b = CaseAnalysis2.min b a | 30 (CaseAnalysis2.min a b = a) = a leq b | 30 (CaseAnalysis2.min a b = b) = b leq a | 30 rev (drop i xs) = take ((len xs) minus i) (rev xs) | 30 rev (filter P xs) = filter P (rev xs) | 0.077 rev (take i xs) = drop ((len xs) minus i) (rev xs) | 30 n ~= h ==> count n (x @ [h]) = count n x | 0.023 count n t + count n [h] = count n (h # t) | 5.501 sorted l ==> sorted (insort x l) | 30 sorted (sort l) | 30 ((suc m) minus n) minus (suc k) = (m minus n) minus k | 30 take n (xs @ ys) = take n xs @ take (n minus (len xs)) ys | 30 take n (drop m xs) = drop m (take (n + m) xs) | 30 take n (map f xs) = map f (take n xs) | 30 take n (zip xs ys) = zip (take n xs) (take n ys) | 30 zip (xs @ ys) zs = zip xs (take (len xs) zs) @ zip ys (drop (len xs) zs) | 30 zip xs (ys @ zs) = zip (take (length ys) xs) ys @ zip (drop (length ys) xs) zs | 30 zip (x # xs) ys = (case ys of [] => [] | y # ys => (x, y) # zip xs ys) | 30 len xs = len ys ==> zip (rev xs) (rev ys) = rev (zip xs ys) | 30 height (mirror a) = height a | 30 (50 rows)