Theory SMT_Examples_CVC
section ‹Examples for the cvc5-SMT binding›
theory SMT_Examples_CVC
imports Complex_Main
options [condition = "$CVC5_INSTALLED"]
begin
external_file ‹SMT_Examples_CVC.certs›
declare [[smt_certificates = "SMT_Examples_CVC.certs"]]
declare [[smt_read_only_certificates = true]]
declare [[smt_trace=false,smt_verbose=false,smt_debug_verit=false,smt_statistics]]
declare [[smt_nat_as_int]]
declare[[smt_expert_debug_alethe_level=0]]
declare[[smt_expert_debug_alethe_files="all"]]
lemma
assumes "x ≥ (3::int)" and "y = x + 4"
shows "y - x > 0"
using assms supply [[smt_trace,smt_debug_verit]] by (smt (cvc5_proof))
section ‹Propositional and first-order logic›
lemma "True" supply [[smt_trace]] by (smt (cvc5_proof))
declare[[smt_expert_debug_alethe_level=0]]
lemma "p ∨ ¬p" by (smt (cvc5_proof))
lemma "(p ∧ True) = p" by (smt (cvc5_proof))
lemma "(p ∨ q) ∧ ¬p ⟹ q" by (smt (cvc5_proof))
lemma "(a ∧ b) ∨ (c ∧ d) ⟹ (a ∧ b) ∨ (c ∧ d)" by (smt (cvc5_proof))
lemma "(p1 ∧ p2) ∨ p3 ⟶ (p1 ⟶ (p3 ∧ p2) ∨ (p1 ∧ p3)) ∨ p1" by (smt (cvc5_proof))
lemma "P = P = P = P = P = P = P = P = P = P" by (smt (cvc5_proof))
lemma
assumes "a ∨ b ∨ c ∨ d"
and "e ∨ f ∨ (a ∧ d)"
and "¬ (a ∨ (c ∧ ~c)) ∨ b"
and "¬ (b ∧ (x ∨ ¬ x)) ∨ c"
and "¬ (d ∨ False) ∨ c"
and "¬ (c ∨ (¬ p ∧ (p ∨ (q ∧ ¬ q))))"
shows False
using assms supply [[smt_trace]] by (smt (cvc5_proof))
axiomatization symm_f :: "'a ⇒ 'a ⇒ 'a" where
symm_f: "symm_f x y = symm_f y x"
lemma "a = a ∧ symm_f a b = symm_f b a"
supply [[smt_trace]]
by (smt (cvc5) symm_f)
lemma
assumes "~x0"
and "~x30"
and "~x29"
and "~x59"
and "x1 ∨ x31 ∨ x0"
and "x2 ∨ x32 ∨ x1"
and "x3 ∨ x33 ∨ x2"
and "x4 ∨ x34 ∨ x3"
and "x35 ∨ x4"
and "x5 ∨ x36 ∨ x30"
and "x6 ∨ x37 ∨ x5 ∨ x31"
and "x7 ∨ x38 ∨ x6 ∨ x32"
and "x8 ∨ x39 ∨ x7 ∨ x33"
and "x9 ∨ x40 ∨ x8 ∨ x34"
and "x41 ∨ x9 ∨ x35"
and "x10 ∨ x42 ∨ x36"
and "x11 ∨ x43 ∨ x10 ∨ x37"
and "x12 ∨ x44 ∨ x11 ∨ x38"
and "x13 ∨ x45 ∨ x12 ∨ x39"
and "x14 ∨ x46 ∨ x13 ∨ x40"
and "x47 ∨ x14 ∨ x41"
and "x15 ∨ x48 ∨ x42"
and "x16 ∨ x49 ∨ x15 ∨ x43"
and "x17 ∨ x50 ∨ x16 ∨ x44"
and "x18 ∨ x51 ∨ x17 ∨ x45"
and "x19 ∨ x52 ∨ x18 ∨ x46"
and "x53 ∨ x19 ∨ x47"
and "x20 ∨ x54 ∨ x48"
and "x21 ∨ x55 ∨ x20 ∨ x49"
and "x22 ∨ x56 ∨ x21 ∨ x50"
and "x23 ∨ x57 ∨ x22 ∨ x51"
and "x24 ∨ x58 ∨ x23 ∨ x52"
and "x59 ∨ x24 ∨ x53"
and "x25 ∨ x54"
and "x26 ∨ x25 ∨ x55"
and "x27 ∨ x26 ∨ x56"
and "x28 ∨ x27 ∨ x57"
and "x29 ∨ x28 ∨ x58"
and "~x1 ∨ ~x31"
and "~x1 ∨ ~x0"
and "~x31 ∨ ~x0"
and "~x2 ∨ ~x32"
and "~x2 ∨ ~x1"
and "~x32 ∨ ~x1"
and "~x3 ∨ ~x33"
and "~x3 ∨ ~x2"
and "~x33 ∨ ~x2"
and "~x4 ∨ ~x34"
and "~x4 ∨ ~x3"
and "~x34 ∨ ~x3"
and "~x35 ∨ ~x4"
and "~x5 ∨ ~x36"
and "~x5 ∨ ~x30"
and "~x36 ∨ ~x30"
and "~x6 ∨ ~x37"
and "~x6 ∨ ~x5"
and "~x6 ∨ ~x31"
and "~x37 ∨ ~x5"
and "~x37 ∨ ~x31"
and "~x5 ∨ ~x31"
and "~x7 ∨ ~x38"
and "~x7 ∨ ~x6"
and "~x7 ∨ ~x32"
and "~x38 ∨ ~x6"
and "~x38 ∨ ~x32"
and "~x6 ∨ ~x32"
and "~x8 ∨ ~x39"
and "~x8 ∨ ~x7"
and "~x8 ∨ ~x33"
and "~x39 ∨ ~x7"
and "~x39 ∨ ~x33"
and "~x7 ∨ ~x33"
and "~x9 ∨ ~x40"
and "~x9 ∨ ~x8"
and "~x9 ∨ ~x34"
and "~x40 ∨ ~x8"
and "~x40 ∨ ~x34"
and "~x8 ∨ ~x34"
and "~x41 ∨ ~x9"
and "~x41 ∨ ~x35"
and "~x9 ∨ ~x35"
and "~x10 ∨ ~x42"
and "~x10 ∨ ~x36"
and "~x42 ∨ ~x36"
and "~x11 ∨ ~x43"
and "~x11 ∨ ~x10"
and "~x11 ∨ ~x37"
and "~x43 ∨ ~x10"
and "~x43 ∨ ~x37"
and "~x10 ∨ ~x37"
and "~x12 ∨ ~x44"
and "~x12 ∨ ~x11"
and "~x12 ∨ ~x38"
and "~x44 ∨ ~x11"
and "~x44 ∨ ~x38"
and "~x11 ∨ ~x38"
and "~x13 ∨ ~x45"
and "~x13 ∨ ~x12"
and "~x13 ∨ ~x39"
and "~x45 ∨ ~x12"
and "~x45 ∨ ~x39"
and "~x12 ∨ ~x39"
and "~x14 ∨ ~x46"
and "~x14 ∨ ~x13"
and "~x14 ∨ ~x40"
and "~x46 ∨ ~x13"
and "~x46 ∨ ~x40"
and "~x13 ∨ ~x40"
and "~x47 ∨ ~x14"
and "~x47 ∨ ~x41"
and "~x14 ∨ ~x41"
and "~x15 ∨ ~x48"
and "~x15 ∨ ~x42"
and "~x48 ∨ ~x42"
and "~x16 ∨ ~x49"
and "~x16 ∨ ~x15"
and "~x16 ∨ ~x43"
and "~x49 ∨ ~x15"
and "~x49 ∨ ~x43"
and "~x15 ∨ ~x43"
and "~x17 ∨ ~x50"
and "~x17 ∨ ~x16"
and "~x17 ∨ ~x44"
and "~x50 ∨ ~x16"
and "~x50 ∨ ~x44"
and "~x16 ∨ ~x44"
and "~x18 ∨ ~x51"
and "~x18 ∨ ~x17"
and "~x18 ∨ ~x45"
and "~x51 ∨ ~x17"
and "~x51 ∨ ~x45"
and "~x17 ∨ ~x45"
and "~x19 ∨ ~x52"
and "~x19 ∨ ~x18"
and "~x19 ∨ ~x46"
and "~x52 ∨ ~x18"
and "~x52 ∨ ~x46"
and "~x18 ∨ ~x46"
and "~x53 ∨ ~x19"
and "~x53 ∨ ~x47"
and "~x19 ∨ ~x47"
and "~x20 ∨ ~x54"
and "~x20 ∨ ~x48"
and "~x54 ∨ ~x48"
and "~x21 ∨ ~x55"
and "~x21 ∨ ~x20"
and "~x21 ∨ ~x49"
and "~x55 ∨ ~x20"
and "~x55 ∨ ~x49"
and "~x20 ∨ ~x49"
and "~x22 ∨ ~x56"
and "~x22 ∨ ~x21"
and "~x22 ∨ ~x50"
and "~x56 ∨ ~x21"
and "~x56 ∨ ~x50"
and "~x21 ∨ ~x50"
and "~x23 ∨ ~x57"
and "~x23 ∨ ~x22"
and "~x23 ∨ ~x51"
and "~x57 ∨ ~x22"
and "~x57 ∨ ~x51"
and "~x22 ∨ ~x51"
and "~x24 ∨ ~x58"
and "~x24 ∨ ~x23"
and "~x24 ∨ ~x52"
and "~x58 ∨ ~x23"
and "~x58 ∨ ~x52"
and "~x23 ∨ ~x52"
and "~x59 ∨ ~x24"
and "~x59 ∨ ~x53"
and "~x24 ∨ ~x53"
and "~x25 ∨ ~x54"
and "~x26 ∨ ~x25"
and "~x26 ∨ ~x55"
and "~x25 ∨ ~x55"
and "~x27 ∨ ~x26"
and "~x27 ∨ ~x56"
and "~x26 ∨ ~x56"
and "~x28 ∨ ~x27"
and "~x28 ∨ ~x57"
and "~x27 ∨ ~x57"
and "~x29 ∨ ~x28"
and "~x29 ∨ ~x58"
and "~x28 ∨ ~x58"
shows False
supply [[smt_trace=false]] using assms by (smt (cvc5_proof))
lemma "∀x::int. P x ⟶ (∀y::int. P x ∨ P y)"
supply[[smt_trace]]
by (smt (cvc5_proof))
lemma "∃x::int. x + 1 = x * 2"
by (smt (cvc5_proof))
lemma
assumes "(∀x y. P x y = x)"
shows "(∃y. P x y) = P x c"
supply[[smt_trace=false]]
using assms by (smt (cvc5_proof))
lemma
assumes "(∀x y. P x y = x)"
and "(∀x. ∃y. P x y) = (∀x. P x c)"
shows "(∃y. P x y) = P x c"
supply[[smt_trace=false]]
using assms by (smt (cvc5_proof))
lemma
assumes "if P x then ¬(∃y. P y) else (∀y. ¬P y)"
shows "P x ⟶ P y"
using assms by (smt (cvc5_proof))
lemma "(case a of
True ⇒ False |
False ⇒ True)
= (¬a)"
supply[[smt_trace]] by (smt (cvc5_proof))
lemma "min (3::int) 5 = 3"
supply[[smt_trace]] by (smt (cvc5_proof))
lemma "min (3::nat) 5 = 3"
supply[[smt_trace,smt_nat_as_int]] by (smt (cvc5_proof))
lemma "min (3::nat) 5 = 3"
supply[[smt_nat_as_int,smt_trace]] by (smt (cvc5_proof))
lemma "(3::nat) + x = (x + 3)"
supply[[smt_nat_as_int,show_types,smt_trace]]
by (smt (cvc5))
section ‹Arithmetic›
subsection ‹Linear arithmetic over integers and reals›
declare[[smt_debug_arith_verit=false]]
lemma "(3::nat) = 3" by (smt (cvc5_proof))
lemma "(3::int) = 3" by (smt (cvc5_proof))
lemma "(3::real) = 3" by (smt (cvc5_proof))
lemma "(3 :: int) + 1 = 4" by (smt (cvc5_proof))
lemma "x + (y + z) = y + (z + (x::int))" by (smt (cvc5_proof))
lemma "max (3::int) 8 > 5" by (smt (cvc5_proof))
lemma "¦x :: real¦ + ¦y¦ ≥ ¦x + y¦" supply[[smt_trace=false,smt_verbose=false]] by (smt (cvc5_proof))
lemma "P ((2::int) < 3) = P True" by (smt (cvc5_proof))
lemma "x + 3 ≥ 4 ∨ x < (1::int)" by (smt (cvc5_proof))
lemma
assumes "x ≥ (3::int)" and "y = x + 4"
shows "y - x > 0"
using assms by (smt (cvc5_proof))
lemma "let x = (2 :: int) in x + x ≠ 5" by (smt (cvc5_proof))
lemma
fixes x :: int
assumes "3 * x + 7 * a < 4" and "3 < 2 * x"
shows "a < 0"
supply[[smt_trace]]
using assms by (smt (cvc5_proof))
lemma "(0 ≤ y + -1 * x ∨ ¬ 0 ≤ x ∨ 0 ≤ (x::int)) = (¬ False)" by (smt (cvc5_proof))
lemma "
(n < m ∧ m < n') ∨ (n < m ∧ m = n') ∨ (n < n' ∧ n' < m) ∨
(n = n' ∧ n' < m) ∨ (n = m ∧ m < n') ∨
(n' < m ∧ m < n) ∨ (n' < m ∧ m = n) ∨
(n' < n ∧ n < m) ∨ (n' = n ∧ n < m) ∨ (n' = m ∧ m < n) ∨
(m < n ∧ n < n') ∨ (m < n ∧ n' = n) ∨ (m < n' ∧ n' < n) ∨
(m = n ∧ n < n') ∨ (m = n' ∧ n' < n) ∨
(n' = m ∧ m = (n::int))"
supply[[smt_trace=false]]
by (smt (cvc5_proof))
text‹
The following example was taken from HOL/ex/PresburgerEx.thy, where it says:
This following theorem proves that all solutions to the
recurrence relation $x_{i+2} = |x_{i+1}| - x_i$ are periodic with
period 9. The example was brought to our attention by John
Harrison. It does does not require Presburger arithmetic but merely
quantifier-free linear arithmetic and holds for the rationals as well.
Warning: it takes (in 2006) over 4.2 minutes!
There, it is proved by "arith". (smt (cvc5)) is not able to prove this within a fraction
of one second. With proof reconstruction, it takes about 13 seconds on a Core2
processor.
›
lemma "let P = 2 * x + 1 > x + (x::real) in P ∨ False ∨ P" by (smt (cvc5_proof))
subsection ‹Linear arithmetic with quantifiers›
lemma "~ (∃x::int. False)" by (smt (cvc5_proof))
lemma "~ (∃x::real. False)" by (smt (cvc5_proof))
lemma "∀x y::int. (x = 0 ∧ y = 1) ⟶ x ≠ y" supply [[smt_trace]] by (smt (cvc5_proof))
lemma "∀x y::int. x < y ⟶ (2 * x + 1) < (2 * y)" by (smt (cvc5_proof))
lemma "∀x y::int. x + y > 2 ∨ x + y = 2 ∨ x + y < 2" supply[[smt_trace]] by (smt (cvc5_proof))
lemma "∀x::int. if x > 0 then x + 1 > 0 else 1 > x" by (smt (cvc5_proof))
lemma "(if (∀x::int. x < 0 ∨ x > 0) then -1 else 3) > (0::int)" by (smt (cvc5_proof))
lemma "∃x::int. ∀x y. 0 < x ∧ 0 < y ⟶ (0::int) < x + y" supply [[verit_compress_proofs=false,smt_trace]]by (smt (cvc5_proof))
experiment
begin
lemma [cvc5_holes_simp]: ‹¬(∀v2::real. v2 ≤ 0)›
by (auto intro: exI[of _ ‹1 :: real›])
lemma "∃u::int. ∀(x::int) y::real. 0 < x ∧ 0 < y ⟶ -1 < x"
supply [[smt_trace]] by (smt (cvc5_proof))
end
lemma "∀(a::int) b::int. 0 < b ∨ b < 1" by (smt (cvc5_proof))
subsection ‹Linear arithmetic for natural numbers›
lemma "2 * (5+ (1::int)) = 12" supply[[smt_trace]] by (smt (cvc5_proof))
lemma "2 * (x::nat) ≠ 1" supply[[smt_trace]] by (smt (cvc5_proof))
lemma "a < 3 ⟹ (7::nat) > 2 * a" by (smt (cvc5_proof))
lemma "let x = (1::nat) + y in x - y > 0 * x" by (smt (cvc5_proof))
lemma
"let x = (1::nat) + y in
let P = (if x > 0 then True else False) in
False ∨ P = (x - 1 = y) ∨ (¬P ⟶ False)"
supply[[smt_trace=false,smt_verbose=false]]
by (smt (cvc5_proof))
lemma "int (nat ¦x::int¦) = ¦x¦" supply[[smt_trace=false,smt_verbose=false]] by (smt (cvc5) int_nat_eq)
definition prime_nat :: "nat ⇒ bool" where
"prime_nat p = (1 < p ∧ (∀m. m dvd p --> m = 1 ∨ m = p))"
lemma "prime_nat (4*m + 1) ⟹ m ≥ (1::nat)" using prime_nat_def by (smt (cvc5))
lemma "2 * (x::nat) ≠ 1"
by (smt (cvc5_proof))
lemma ‹2*(x :: int) ≠ 1›
supply [[smt_trace]]
by (smt (cvc5_proof))
section ‹Pairs›
lemma "fst (x, y) = a ⟹ x = a"
using fst_conv by (smt (cvc5_proof))
lemma "p1 = (x, y) ∧ p2 = (y, x) ⟹ fst p1 = snd p2"
using fst_conv snd_conv by (smt (cvc5_proof))
section ‹Higher-order problems and recursion›
lemma "i ≠ i1 ∧ i ≠ i2 ⟹ (f (i1 := v1, i2 := v2)) i = f i"
using fun_upd_same fun_upd_apply by (smt (cvc5_proof))
lemma "(f g (x::'a::type) = (g x ∧ True)) ∨ (f g x = True) ∨ (g x = True)"
by (smt (cvc5_proof))
lemma "id x = x ∧ id True = True"
by (smt (cvc5) id_def)
lemma "i ≠ i1 ∧ i ≠ i2 ⟹ ((f (i1 := v1)) (i2 := v2)) i = f i"
using fun_upd_same fun_upd_apply by (smt (cvc5_proof))
lemma
"f (∃x. g x) ⟹ True"
"f (∀x. g x) ⟹ True"
by (smt (cvc5_proof))+
lemma True using let_rsp by (smt (cvc5_proof))
lemma "le = (≤) ⟹ le (3::int) 42" by (smt (cvc5_proof))
lemma "map (λi::int. i + 1) [0, 1] = [1, 2]" by (smt (cvc5) list.map)
lemma "(∀x. P x) ∨ ¬ All P" by (smt (cvc5_proof))
fun dec_10 :: "int ⇒ int" where
"dec_10 n = (if n < 10 then n else dec_10 (n - 10))"
lemma "dec_10 (4 * dec_10 4) = 6"
supply[[smt_trace=false,smt_verbose=false]] by (smt (cvc5) dec_10.simps)
experiment
begin
lemma (in complete_lattice) [cvc5_holes_pre]:
‹(∀(v0) (v1) v2. v0 ≤ v1 ∧ v1 ≤ v2 ⟶ v0 ≤ v2) = (∀v0 v1 v2. ¬ v0 ≤ v1 ∨ ¬ v1 ≤ v2 ∨ v0 ≤ v2) ›
by auto
lemma (in complete_lattice)
assumes "Sup {a | i::bool. True} ≤ Sup {b | i::bool. True}"
and "Sup {b | i::bool. True} ≤ Sup {a | i::bool. True}"
shows "Sup {a | i::bool. True} ≤ Sup {a | i::bool. True}"
using assms by (smt (cvc5) order_trans)
end
experiment
begin
lemma
"eq_set (List.coset xs) (set ys) = rhs"
if "⋀ys. subset' (List.coset xs) (set ys) = (let n = card (UNIV::'a set) in 0 < n ∧ card (set (xs @ ys)) = n)"
and "⋀uu A. (uu::'a) ∈ - A ⟹ uu ∉ A"
and "⋀uu. card (set (uu::'a list)) = length (remdups uu)"
and "⋀uu. finite (set (uu::'a list))"
and "⋀uu. (uu::'a) ∈ UNIV"
and "(UNIV::'a set) ≠ {}"
and "⋀c A B P. ⟦(c::'a) ∈ A ∪ B; c ∈ A ⟹ P; c ∈ B ⟹ P⟧ ⟹ P"
and "⋀a b. (a::nat) + b = b + a"
and "⋀a b. ((a::nat) = a + b) = (b = 0)"
and "card' (set xs) = length (remdups xs)"
and "card' = (card :: 'a set ⇒ nat)"
and "⋀A B. ⟦finite (A::'a set); finite B⟧ ⟹ card A + card B = card (A ∪ B) + card (A ∩ B)"
and "⋀A. (card (A::'a set) = 0) = (A = {} ∨ infinite A)"
and "⋀A. ⟦finite (UNIV::'a set); card (A::'a set) = card (UNIV::'a set)⟧ ⟹ A = UNIV"
and "⋀xs. - List.coset (xs::'a list) = set xs"
and "⋀xs. - set (xs::'a list) = List.coset xs"
and "⋀A B. (A ∩ B = {}) = (∀x. (x::'a) ∈ A ⟶ x ∉ B)"
and "eq_set = (=)"
and "⋀A. finite (A::'a set) ⟹ finite (- A) = finite (UNIV::'a set)"
and "rhs ≡ let n = card (UNIV::'a set) in if n = 0 then False else let xs' = remdups xs; ys' = remdups ys in length xs' + length ys' = n ∧ (∀x∈set xs'. x ∉ set ys') ∧ (∀y∈set ys'. y ∉ set xs')"
and "⋀xs ys. set ((xs::'a list) @ ys) = set xs ∪ set ys"
and "⋀A B. ((A::'a set) = B) = (A ⊆ B ∧ B ⊆ A)"
and "⋀xs. set (remdups (xs::'a list)) = set xs"
and "subset' = (⊆)"
and "⋀A B. (⋀x. (x::'a) ∈ A ⟹ x ∈ B) ⟹ A ⊆ B"
and "⋀A B. ⟦(A::'a set) ⊆ B; B ⊆ A⟧ ⟹ A = B"
and "⋀A ys. (A ⊆ List.coset ys) = (∀y∈set ys. (y::'a) ∉ A)"
using that supply[[smt_trace=false,smt_verbose=false,smt_statistics]] by (smt (cvc5_proof))
end
notepad
begin
have "line_integral F {i, j} g = line_integral F {i} g + line_integral F {j} g"
if ‹(k, g) ∈ one_chain_typeI›
‹⋀A b B. ({} = (A::(real × real) set) ∩ insert (b::real × real) (B::(real × real) set)) = (b ∉ A ∧ {} = A ∩ B)›
‹finite ({} :: (real × real) set)›
‹⋀a A. finite (A::(real × real) set) ⟹ finite (insert (a::real × real) A)›
‹(i::real × real) = (1::real, 0::real)›
‹ ⋀a A. (a::real × real) ∈ (A::(real × real) set) ⟹ insert a A = A› ‹j = (0, 1)›
‹⋀x. (x::(real × real) set) ∩ {} = {}›
‹⋀y x A. insert (x::real × real) (insert (y::real × real) (A::(real × real) set)) = insert y (insert x A)›
‹⋀a A. insert (a::real × real) (A::(real × real) set) = {a} ∪ A›
‹⋀F u basis2 basis1 γ. finite (u :: (real × real) set) ⟹
line_integral_exists F basis1 γ ⟹
line_integral_exists F basis2 γ ⟹
basis1 ∪ basis2 = u ⟹
basis1 ∩ basis2 = {} ⟹
line_integral F u γ = line_integral F basis1 γ + line_integral F basis2 γ›
‹one_chain_line_integral F {i} one_chain_typeI =
one_chain_line_integral F {i} one_chain_typeII ∧
(∀(k, γ)∈one_chain_typeI. line_integral_exists F {i} γ) ∧
(∀(k, γ)∈one_chain_typeII. line_integral_exists F {i} γ)›
‹ one_chain_line_integral (F::real × real ⇒ real × real) {j::real × real}
(one_chain_typeII::(int × (real ⇒ real × real)) set) =
one_chain_line_integral F {j} (one_chain_typeI::(int × (real ⇒ real × real)) set) ∧
(∀(k::int, γ::real ⇒ real × real)∈one_chain_typeII. line_integral_exists F {j} γ) ∧
(∀(k::int, γ::real ⇒ real × real)∈one_chain_typeI. line_integral_exists F {j} γ)›
for F i j g one_chain_typeI one_chain_typeII and
line_integral :: ‹(real × real ⇒ real × real) ⇒ (real × real) set ⇒ (real ⇒ real × real) ⇒ real› and
line_integral_exists :: ‹(real × real ⇒ real × real) ⇒ (real × real) set ⇒ (real ⇒ real × real) ⇒ bool› and
one_chain_line_integral :: ‹(real × real ⇒ real × real) ⇒ (real × real) set ⇒ (int × (real ⇒ real × real)) set ⇒ real› and
k
using prod.case_eq_if singleton_inject snd_conv
that [[smt_trace=false,smt_verbose=false]] by (smt (cvc5_proof))
end
lemma
fixes x y z :: real
assumes ‹x + 2 * y > 0› and
‹x - 2 * y > 0› and
‹x < 0›
shows False
using assms by (smt (cvc5_proof))
context
begin
lemma
fixes d :: real
assumes ‹0 < d›
‹diamond_y ≡ λt. d / 2 - ¦t¦›
‹⋀a b c :: real. (a / c < b / c) =
((0 < c ⟶ a < b) ∧ (c < 0 ⟶ b < a) ∧ c ≠ 0)›
‹⋀a b c :: real. (a / c < b / c) =
((0 < c ⟶ a < b) ∧ (c < 0 ⟶ b < a) ∧ c ≠ 0)›
‹⋀a b :: real. - a / b = - (a / b)›
‹⋀a b :: real. - a * b = - (a * b)›
‹⋀(x1 :: real) x2 y1 y2 :: real. ((x1, x2) = (y1, y2)) = (x1 = y1 ∧ x2 = y2)›
shows ‹(λy. (d / 2, (2 * y - 1) * diamond_y (d / 2))) ≠
(λx. ((x - 1 / 2) * d, - diamond_y ((x - 1 / 2) * d))) ⟹
(λy. (- (d / 2), (2 * y - 1) * diamond_y (- (d / 2)))) =
(λx. ((x - 1 / 2) * d, diamond_y ((x - 1 / 2) * d))) ⟹
False›
using assms supply [[smt_trace=false,smt_verbose=false]] by (smt (cvc5_proof))
lemma
fixes d :: real
assumes ‹0 < d›
‹diamond_y ≡ λt. d / 2 - ¦t¦›
‹⋀a b c :: real. (a / c < b / c) =
((0 < c ⟶ a < b) ∧ (c < 0 ⟶ b < a) ∧ c ≠ 0)›
‹⋀a b c :: real. (a / c < b / c) =
((0 < c ⟶ a < b) ∧ (c < 0 ⟶ b < a) ∧ c ≠ 0)›
‹⋀a b :: real. - a / b = - (a / b)›
‹⋀a b :: real. - a * b = - (a * b)›
‹⋀(x1 :: real) x2 y1 y2 :: real. ((x1, x2) = (y1, y2)) = (x1 = y1 ∧ x2 = y2)›
shows ‹(λy. (d / 2, (2 * y - 1) * diamond_y (d / 2))) ≠
(λx. ((x - 1 / 2) * d, - diamond_y ((x - 1 / 2) * d))) ⟹
(λy. (- (d / 2), (2 * y - 1) * diamond_y (- (d / 2)))) =
(λx. ((x - 1 / 2) * d, diamond_y ((x - 1 / 2) * d))) ⟹
False›
using assms supply [[smt_trace=false,smt_verbose=false]]
by (smt (cvc5_proof))
end
lemma
assumes ‹∀z y x. P z y›
‹P z y ⟹ False›
shows False
using assms
by (smt (cvc5_proof))
lemma
"max (x::int) y ≥ y"
supply [[smt_trace=false,smt_verbose=false]]
by (smt (cvc5_proof))+
context
begin
abbreviation finite' :: "'a set ⇒ bool"
where "finite' A ≡ finite A ∧ A ≠ {}"
lemma
fixes f :: "'b ⇒ 'c :: linorder"
assumes
‹∀(S::'b::type set) f::'b::type ⇒ 'c::linorder. finite' S ⟶ arg_min_on f S ∈ S›
‹∀(S::'a::type set) f::'a::type ⇒ 'c::linorder. finite' S ⟶ arg_min_on f S ∈ S›
‹∀(S::'b::type set) (y::'b::type) f::'b::type ⇒ 'c::linorder.
finite S ∧ S ≠ {} ∧ y ∈ S ⟶ f (arg_min_on f S) ≤ f y›
‹∀(S::'a::type set) (y::'a::type) f::'a::type ⇒ 'c::linorder.
finite S ∧ S ≠ {} ∧ y ∈ S ⟶ f (arg_min_on f S) ≤ f y›
‹∀(f::'b::type ⇒ 'c::linorder) (g::'a::type ⇒ 'b::type) x::'a::type. (f ∘ g) x = f (g x)›
‹∀(F::'b::type set) h::'b::type ⇒ 'a::type. finite F ⟶ finite (h ` F)›
‹∀(F::'b::type set) h::'b::type ⇒ 'b::type. finite F ⟶ finite (h ` F)›
‹∀(F::'a::type set) h::'a::type ⇒ 'b::type. finite F ⟶ finite (h ` F)›
‹∀(F::'a::type set) h::'a::type ⇒ 'a::type. finite F ⟶ finite (h ` F)›
‹∀(b::'a::type) (f::'b::type ⇒ 'a::type) A::'b::type set.
b ∈ f ` A ∧ (∀x::'b::type. b = f x ∧ x ∈ A ⟶ False) ⟶ False›
‹∀(b::'b::type) (f::'b::type ⇒ 'b::type) A::'b::type set.
b ∈ f ` A ∧ (∀x::'b::type. b = f x ∧ x ∈ A ⟶ False) ⟶ False›
‹∀(b::'b::type) (f::'a::type ⇒ 'b::type) A::'a::type set.
b ∈ f ` A ∧ (∀x::'a::type. b = f x ∧ x ∈ A ⟶ False) ⟶ False›
‹∀(b::'a::type) (f::'a::type ⇒ 'a::type) A::'a::type set.
b ∈ f ` A ∧ (∀x::'a::type. b = f x ∧ x ∈ A ⟶ False) ⟶ False›
‹∀(b::'a::type) (f::'b::type ⇒ 'a::type) (x::'b::type) A::'b::type set. b = f x ∧ x ∈ A ⟶ b ∈ f ` A ›
‹∀(b::'b::type) (f::'b::type ⇒ 'b::type) (x::'b::type) A::'b::type set. b = f x ∧ x ∈ A ⟶ b ∈ f ` A ›
‹∀(b::'b::type) (f::'a::type ⇒ 'b::type) (x::'a::type) A::'a::type set. b = f x ∧ x ∈ A ⟶ b ∈ f ` A ›
‹∀(b::'a::type) (f::'a::type ⇒ 'a::type) (x::'a::type) A::'a::type set. b = f x ∧ x ∈ A ⟶ b ∈ f ` A ›
‹∀(f::'b::type ⇒ 'a::type) A::'b::type set. (f ` A = {}) = (A = {}) ›
‹∀(f::'b::type ⇒ 'b::type) A::'b::type set. (f ` A = {}) = (A = {}) ›
‹∀(f::'a::type ⇒ 'b::type) A::'a::type set. (f ` A = {}) = (A = {}) ›
‹∀(f::'a::type ⇒ 'a::type) A::'a::type set. (f ` A = {}) = (A = {}) ›
‹∀(f::'b::type ⇒ 'c::linorder) (A::'b::type set) (x::'b::type) y::'b::type.
inj_on f A ∧ f x = f y ∧ x ∈ A ∧ y ∈ A ⟶ x = y›
‹∀(x::'c::linorder) y::'c::linorder. (x < y) = (x ≤ y ∧ x ≠ y)›
‹inj_on (f::'b::type ⇒ 'c::linorder) ((g::'a::type ⇒ 'b::type) ` (B::'a::type set))›
‹finite (B::'a::type set)›
‹(B::'a::type set) ≠ {}›
‹arg_min_on ((f::'b::type ⇒ 'c::linorder) ∘ (g::'a::type ⇒ 'b::type)) (B::'a::type set) ∈ B›
‹∄x::'a::type.
x ∈ (B::'a::type set) ∧
((f::'b::type ⇒ 'c::linorder) ∘ (g::'a::type ⇒ 'b::type)) x < (f ∘ g) (arg_min_on (f ∘ g) B)›
‹∀(f::'b::type ⇒ 'c::linorder) (P::'b::type ⇒ bool) a::'b::type.
inj_on f (Collect P) ∧ P a ∧ (∀y::'b::type. P y ⟶ f a ≤ f y) ⟶ arg_min f P = a›
‹∀(S::'b::type set) f::'b::type ⇒ 'c::linorder. finite' S ⟶ arg_min_on f S ∈ S›
‹∀(S::'a::type set) f::'a::type ⇒ 'c::linorder. finite' S ⟶ arg_min_on f S ∈ S›
‹∀(S::'b::type set) (y::'b::type) f::'b::type ⇒ 'c::linorder.
finite S ∧ S ≠ {} ∧ y ∈ S ⟶ f (arg_min_on f S) ≤ f y›
‹∀(S::'a::type set) (y::'a::type) f::'a::type ⇒ 'c::linorder.
finite S ∧ S ≠ {} ∧ y ∈ S ⟶ f (arg_min_on f S) ≤ f y›
‹∀(f::'b::type ⇒ 'c::linorder) (g::'a::type ⇒ 'b::type) x::'a::type. (f ∘ g) x = f (g x)›
‹∀(F::'b::type set) h::'b::type ⇒ 'a::type. finite F ⟶ finite (h ` F)›
‹∀(F::'b::type set) h::'b::type ⇒ 'b::type. finite F ⟶ finite (h ` F)›
‹∀(F::'a::type set) h::'a::type ⇒ 'b::type. finite F ⟶ finite (h ` F)›
‹∀(F::'a::type set) h::'a::type ⇒ 'a::type. finite F ⟶ finite (h ` F)›
‹∀(b::'a::type) (f::'b::type ⇒ 'a::type) A::'b::type set.
b ∈ f ` A ∧ (∀x::'b::type. b = f x ∧ x ∈ A ⟶ False) ⟶ False›
‹∀(b::'b::type) (f::'b::type ⇒ 'b::type) A::'b::type set.
b ∈ f ` A ∧ (∀x::'b::type. b = f x ∧ x ∈ A ⟶ False) ⟶ False›
‹∀(b::'b::type) (f::'a::type ⇒ 'b::type) A::'a::type set.
b ∈ f ` A ∧ (∀x::'a::type. b = f x ∧ x ∈ A ⟶ False) ⟶ False›
‹∀(b::'a::type) (f::'a::type ⇒ 'a::type) A::'a::type set.
b ∈ f ` A ∧ (∀x::'a::type. b = f x ∧ x ∈ A ⟶ False) ⟶ False›
‹∀(b::'a::type) (f::'b::type ⇒ 'a::type) (x::'b::type) A::'b::type set. b = f x ∧ x ∈ A ⟶ b ∈ f ` A ›
‹∀(b::'b::type) (f::'b::type ⇒ 'b::type) (x::'b::type) A::'b::type set. b = f x ∧ x ∈ A ⟶ b ∈ f ` A ›
‹∀(b::'b::type) (f::'a::type ⇒ 'b::type) (x::'a::type) A::'a::type set. b = f x ∧ x ∈ A ⟶ b ∈ f ` A ›
‹∀(b::'a::type) (f::'a::type ⇒ 'a::type) (x::'a::type) A::'a::type set. b = f x ∧ x ∈ A ⟶ b ∈ f ` A ›
‹∀(f::'b::type ⇒ 'a::type) A::'b::type set. (f ` A = {}) = (A = {}) ›
‹∀(f::'b::type ⇒ 'b::type) A::'b::type set. (f ` A = {}) = (A = {}) ›
‹∀(f::'a::type ⇒ 'b::type) A::'a::type set. (f ` A = {}) = (A = {}) ›
‹∀(f::'a::type ⇒ 'a::type) A::'a::type set. (f ` A = {}) = (A = {})›
‹∀(f::'b::type ⇒ 'c::linorder) (A::'b::type set) (x::'b::type) y::'b::type.
inj_on f A ∧ f x = f y ∧ x ∈ A ∧ y ∈ A ⟶ x = y›
‹∀(x::'c::linorder) y::'c::linorder. (x < y) = (x ≤ y ∧ x ≠ y)›
‹arg_min_on (f::'b::type ⇒ 'c::linorder) ((g::'a::type ⇒ 'b::type) ` (B::'a::type set)) ≠
g (arg_min_on (f ∘ g) B) ›
shows False
using assms supply [[smt_trace=false,smt_verbose=false]]
by (smt (cvc5_proof))
end
context
fixes piecewise_C1 :: "('real :: {one,zero,ord} ⇒ 'a :: {one,zero,ord}) ⇒ 'real set ⇒ bool" and
joinpaths :: "('real ⇒ 'a) ⇒ ('real ⇒ 'a) ⇒ 'real ⇒ 'a"
begin
notation piecewise_C1 (infixr "piecewise'_C1'_differentiable'_on" 50)
notation joinpaths (infixr "+++" 75)
lemma
‹(⋀v1. ∀v0. (rec_join v0 = v1 ∧
(v0 = [] ∧ (λuu. 0) = v1 ⟶ False) ∧
(∀v2. v0 = [v2] ∧ v1 = coeff_cube_to_path v2 ⟶ False) ∧
(∀v2 v3 v4.
v0 = v2 # v3 # v4 ∧ v1 = coeff_cube_to_path v2 +++ rec_join (v3 # v4) ⟶ False) ⟶
False) =
(rec_join v0 = rec_join v0 ∧
(v0 = [] ∧ (λuu. 0) = rec_join v0 ⟶ False) ∧
(∀v2. v0 = [v2] ∧ rec_join v0 = coeff_cube_to_path v2 ⟶ False) ∧
(∀v2 v3 v4.
v0 = v2 # v3 # v4 ∧ rec_join v0 = coeff_cube_to_path v2 +++ rec_join (v3 # v4) ⟶
False) ⟶
False)) ⟹
(∀v0 v1.
rec_join v0 = v1 ∧
(v0 = [] ∧ (λuu. 0) = v1 ⟶ False) ∧
(∀v2. v0 = [v2] ∧ v1 = coeff_cube_to_path v2 ⟶ False) ∧
(∀v2 v3 v4. v0 = v2 # v3 # v4 ∧ v1 = coeff_cube_to_path v2 +++ rec_join (v3 # v4) ⟶ False) ⟶
False) =
(∀v0. rec_join v0 = rec_join v0 ∧
(v0 = [] ∧ (λuu. 0) = rec_join v0 ⟶ False) ∧
(∀v2. v0 = [v2] ∧ rec_join v0 = coeff_cube_to_path v2 ⟶ False) ∧
(∀v2 v3 v4.
v0 = v2 # v3 # v4 ∧ rec_join v0 = coeff_cube_to_path v2 +++ rec_join (v3 # v4) ⟶
False) ⟶
False)›
supply [[smt_trace=false,smt_verbose=false]]
by (smt (cvc5_proof))
end
section ‹Bugs›
context
fixes centered_divide :: ‹int ⇒ int ⇒ int› (infixl ‹cdiv› 70) and
centered_modulo :: ‹int ⇒ int ⇒ int› (infixl ‹cmod› 70)
begin
declare[[cvc5_options="--dag-thres=0 --proof-format-mode=alethe --proof-granularity=dsl-rewrite --proof-alethe-experimental --proof-prune-input --full-saturate-quant --proof-alethe-define-skolems --proof-elim-subtypes --no-stats --sat-random-seed=1 --lang=smt2"]]
lemma zero_cdiv_eq [simp]:
assumes
"∀(b::int) (a::int) c::int. b * (a div b) + a mod b + c = a + c"
"∀k::int. k cdiv (0::int) = (0::int)"
"∀(k::int) l::int. k cdiv l * l + k cmod l = k"
"∀(k::int) l::int.
k cmod l = (k + (if l < (0::int) then - l else l) div (2::int)) mod (if l < (0::int) then - l else l) - (if l < (0::int) then - l else l) div (2::int)"
"∀(A::int) n::int. A = A div n * n + A mod n"
"∀a::int. even a = (a mod (2::int) = (0::int))"
"∀k::int. ((0::int) ≤ k div (2::int)) = ((0::int) ≤ k)"
"∀(k::int) l::int. (0::int) ≤ k ∧ k < l ⟶ k mod l = k"
"∀(c::int) b::int. (c = b * c) = (c = (0::int) ∨ b = (1::int))"
"∀(a::int) b::int. a ≠ (0::int) ⟶ a * b div a = b"
"∀a::int. odd a = (a mod (2::int) = (1::int))"
shows
‹0 cdiv k = 0›
supply [[smt_trace=false,smt_verbose=false,smt_statistics]]
by (smt (cvc5) assms)
end
context
fixes
round_up :: "int ⇒ real ⇒ real"and
round_down :: "int ⇒ real ⇒ real" and
powr :: ‹real ⇒ real ⇒ real› (infix "powr2" 80)
assumes powr_gt_zero: ‹⋀a b :: real. 0 < x powr2 a ⟷ x ≠ 0›
and powr_minus_divide: "⋀a x :: real. x powr2 (- a) = 1/(x powr2 a)"
and round_up_diff_round_down: ‹⋀prec (x::real). round_up prec x - round_down prec x
≤ 2 powr2 (- real_of_int prec)›
and round_down_uminus_eq: ‹⋀prec x. round_down p (- x) = - round_up p x›
and round_up: ‹⋀prec x. x ≤ round_up prec x›
and round_up_diff_round_down: ‹⋀prec x. round_up prec x - round_down prec x ≤ 2 powr2 (- real_of_int prec)›
begin
lemma
assumes "x < 1 / 2" ‹p > 0›
‹1 / 2 * 2 powr2 real_of_int p ≤ 2 powr2 real_of_int p - 1›
‹x * 2 powr2 real_of_int p < 1 / 2 * 2 powr2 real_of_int p›
shows "round_up p x < 1"
supply [[smt_trace=false,smt_statistics=true,smt_verbose=false,
ML_print_depth=1000,show_types]]
using comm_semiring_class.distrib divide_divide_eq_right
mult.assoc mult.commute mult_cancel_left1 mult_cancel_right mult_cancel_right2
mult_less_cancel_left_pos mult_minus_left nonzero_eq_divide_eq nonzero_mult_div_cancel_left
nonzero_mult_div_cancel_right powr_gt_zero powr_minus_divide round_down_uminus_eq
round_up round_up_diff_round_down times_divide_eq_right assms
by (smt (cvc5))
lemma
assumes "x < 1 / 2" ‹p > 0›
‹1 / 2 * 2 powr2 real_of_int p ≤ 2 powr2 real_of_int p - 1›
‹x * 2 powr2 real_of_int p < 1 / 2 * 2 powr2 real_of_int p›
shows "round_up p x < 1"
supply [[smt_trace=false,smt_statistics=true,smt_verbose=false,
ML_print_depth=1000,show_types,alethe_use_propositional_skeleton=false]]
using comm_semiring_class.distrib divide_divide_eq_right
mult.assoc mult.commute mult_cancel_left1 mult_cancel_right mult_cancel_right2
mult_less_cancel_left_pos mult_minus_left nonzero_eq_divide_eq nonzero_mult_div_cancel_left
nonzero_mult_div_cancel_right powr_gt_zero powr_minus_divide round_down_uminus_eq
round_up round_up_diff_round_down times_divide_eq_right assms
by (smt (cvc5))
end
section ‹Monomorphization examples›
definition Pred :: "'a ⇒ bool" where
"Pred x = True"
lemma poly_Pred: "Pred x ∧ (Pred [x] ∨ ¬ Pred [x])"
by (simp add: Pred_def)
lemma "Pred (1::int)"
by (smt (cvc5) poly_Pred)
axiomatization g :: "'a ⇒ nat"
axiomatization where
g1: "g (Some x) = g [x]" and
g2: "g None = g []" and
g3: "g xs = length xs"
lemma "g (Some (3::int)) = g (Some True)" by (smt (cvc5) g1 g2 g3 list.size)
section ‹cvc5 only examples›
declare[[smt_expert_debug_alethe_files="smt_global_normalize"]]
declare[[smt_expert_debug_alethe_level=3]]
lemma "(3::nat) ^ 3 = 27"
using power_0 power_Suc
oops