# Theory Predicate_Compile_Quickcheck_Examples

```theory Predicate_Compile_Quickcheck_Examples
imports "HOL-Library.Predicate_Compile_Quickcheck"
begin

(*
section {* Sets *}

lemma "x ∈ {(1::nat)} ==> False"
quickcheck[generator=predicate_compile_wo_ff, iterations=10]
oops

lemma "x ∈ {Suc 0, Suc (Suc 0)} ==> x ≠ Suc 0"
quickcheck[generator=predicate_compile_wo_ff]
oops

lemma "x ∈ {Suc 0, Suc (Suc 0)} ==> x = Suc 0"
quickcheck[generator=predicate_compile_wo_ff]
oops

lemma "x ∈ {Suc 0, Suc (Suc 0)} ==> x <= Suc 0"
quickcheck[generator=predicate_compile_wo_ff]
oops

section {* Numerals *}

lemma
"x ∈ {1, 2, (3::nat)} ==> x = 1 ∨ x = 2"
quickcheck[generator=predicate_compile_wo_ff]
oops

lemma "x ∈ {1, 2, (3::nat)} ==> x < 3"
quickcheck[generator=predicate_compile_wo_ff]
oops

lemma
"x ∈ {1, 2} ∪ {3, 4} ==> x = (1::nat) ∨ x = (2::nat)"
quickcheck[generator=predicate_compile_wo_ff]
oops
*)

section ‹Equivalences›

inductive is_ten :: "nat => bool"
where
"is_ten 10"

inductive is_eleven :: "nat => bool"
where
"is_eleven 11"

lemma
"is_ten x = is_eleven x"
quickcheck[tester = smart_exhaustive, iterations = 1, size = 1, expect = counterexample]
oops

section ‹Context Free Grammar›

datatype alphabet = a | b

inductive_set S⇩1 and A⇩1 and B⇩1 where
"[] ∈ S⇩1"
| "w ∈ A⇩1 ⟹ b # w ∈ S⇩1"
| "w ∈ B⇩1 ⟹ a # w ∈ S⇩1"
| "w ∈ S⇩1 ⟹ a # w ∈ A⇩1"
| "w ∈ S⇩1 ⟹ b # w ∈ S⇩1"
| "⟦v ∈ B⇩1; v ∈ B⇩1⟧ ⟹ a # v @ w ∈ B⇩1"

lemma
"S⇩1p w ⟹ w = []"
quickcheck[tester = smart_exhaustive, iterations=1]
oops

theorem S⇩1_sound:
"S⇩1p w ⟹ length [x ← w. x = a] = length [x ← w. x = b]"
quickcheck[tester=smart_exhaustive, size=15]
oops

inductive_set S⇩2 and A⇩2 and B⇩2 where
"[] ∈ S⇩2"
| "w ∈ A⇩2 ⟹ b # w ∈ S⇩2"
| "w ∈ B⇩2 ⟹ a # w ∈ S⇩2"
| "w ∈ S⇩2 ⟹ a # w ∈ A⇩2"
| "w ∈ S⇩2 ⟹ b # w ∈ B⇩2"
| "⟦v ∈ B⇩2; v ∈ B⇩2⟧ ⟹ a # v @ w ∈ B⇩2"
(*
code_pred [random_dseq inductify] S⇩2 .
thm S⇩2.random_dseq_equation
thm A⇩2.random_dseq_equation
thm B⇩2.random_dseq_equation

values [random_dseq 1, 2, 8] 10 "{x. S⇩2 x}"

lemma "w ∈ S⇩2 ==> w ≠ [] ==> w ≠ [b, a] ==> w ∈ {}"
quickcheck[generator=predicate_compile, size=8]
oops

lemma "[x <- w. x = a] = []"
quickcheck[generator=predicate_compile]
oops

declare list.size(3,4)[code_pred_def]

(*
lemma "length ([x ← w. x = a]) = (0::nat)"
quickcheck[generator=predicate_compile]
oops
*)

lemma
"w ∈ S⇩2 ==> length [x ← w. x = a] <= Suc (Suc 0)"
quickcheck[generator=predicate_compile, size = 10, iterations = 1]
oops
*)
theorem S⇩2_sound:
"S⇩2p w ⟶ length [x ← w. x = a] = length [x ← w. x = b]"
quickcheck[tester=smart_exhaustive, size=5, iterations=10]
oops

inductive_set S⇩3 and A⇩3 and B⇩3 where
"[] ∈ S⇩3"
| "w ∈ A⇩3 ⟹ b # w ∈ S⇩3"
| "w ∈ B⇩3 ⟹ a # w ∈ S⇩3"
| "w ∈ S⇩3 ⟹ a # w ∈ A⇩3"
| "w ∈ S⇩3 ⟹ b # w ∈ B⇩3"
| "⟦v ∈ B⇩3; w ∈ B⇩3⟧ ⟹ a # v @ w ∈ B⇩3"

code_pred [inductify, skip_proof] S⇩3p .
thm S⇩3p.equation
(*
values 10 "{x. S⇩3 x}"
*)

lemma S⇩3_sound:
"S⇩3p w ⟶ length [x ← w. x = a] = length [x ← w. x = b]"
quickcheck[tester=smart_exhaustive, size=10, iterations=10]
oops

lemma "¬ (length w > 2) ∨ ¬ (length [x ← w. x = a] = length [x ← w. x = b])"
quickcheck[size=10, tester = smart_exhaustive]
oops

theorem S⇩3_complete:
"length [x ← w. x = a] = length [x ← w. b = x] ⟶ S⇩3p w"
(*quickcheck[generator=SML]*)
quickcheck[tester=smart_exhaustive, size=10, iterations=100]
oops

inductive_set S⇩4 and A⇩4 and B⇩4 where
"[] ∈ S⇩4"
| "w ∈ A⇩4 ⟹ b # w ∈ S⇩4"
| "w ∈ B⇩4 ⟹ a # w ∈ S⇩4"
| "w ∈ S⇩4 ⟹ a # w ∈ A⇩4"
| "⟦v ∈ A⇩4; w ∈ A⇩4⟧ ⟹ b # v @ w ∈ A⇩4"
| "w ∈ S⇩4 ⟹ b # w ∈ B⇩4"
| "⟦v ∈ B⇩4; w ∈ B⇩4⟧ ⟹ a # v @ w ∈ B⇩4"

theorem S⇩4_sound:
"S⇩4p w ⟶ length [x ← w. x = a] = length [x ← w. x = b]"
quickcheck[tester = smart_exhaustive, size=5, iterations=1]
oops

theorem S⇩4_complete:
"length [x ← w. x = a] = length [x ← w. x = b] ⟶ S⇩4p w"
quickcheck[tester = smart_exhaustive, size=5, iterations=1]
oops

hide_const a b

subsection ‹Lexicographic order›
(* TODO *)
(*
lemma
"(u, v) : lexord r ==> (x @ u, y @ v) : lexord r"
oops
*)
subsection ‹IMP›

type_synonym var = nat
type_synonym state = "int list"

datatype com =
Skip |
Ass var "int" |
Seq com com |
IF "state list" com com |
While "state list" com

inductive exec :: "com => state => state => bool" where
"exec Skip s s" |
"exec (Ass x e) s (s[x := e])" |
"exec c1 s1 s2 ==> exec c2 s2 s3 ==> exec (Seq c1 c2) s1 s3" |
"s ∈ set b ==> exec c1 s t ==> exec (IF b c1 c2) s t" |
"s ∉ set b ==> exec c2 s t ==> exec (IF b c1 c2) s t" |
"s ∉ set b ==> exec (While b c) s s" |
"s1 ∈ set b ==> exec c s1 s2 ==> exec (While b c) s2 s3 ==> exec (While b c) s1 s3"

code_pred [random_dseq] exec .

values [random_dseq 1, 2, 3] 10 "{(c, s, s'). exec c s s'}"

lemma
"exec c s s' ==> exec (Seq c c) s s'"
quickcheck[tester = smart_exhaustive, size=2, iterations=20, expect = counterexample]
oops

subsection ‹Lambda›

datatype type =
Atom nat
| Fun type type    (infixr "⇒" 200)

datatype dB =
Var nat
| App dB dB (infixl "°" 200)
| Abs type dB

primrec
nth_el :: "'a list ⇒ nat ⇒ 'a option" ("_⟨_⟩" [90, 0] 91)
where
"[]⟨i⟩ = None"
| "(x # xs)⟨i⟩ = (case i of 0 ⇒ Some x | Suc j ⇒ xs ⟨j⟩)"

inductive nth_el' :: "'a list ⇒ nat ⇒ 'a ⇒ bool"
where
"nth_el' (x # xs) 0 x"
| "nth_el' xs i y ⟹ nth_el' (x # xs) (Suc i) y"

inductive typing :: "type list ⇒ dB ⇒ type ⇒ bool"  ("_ ⊢ _ : _" [50, 50, 50] 50)
where
Var [intro!]: "nth_el' env x T ⟹ env ⊢ Var x : T"
| Abs [intro!]: "T # env ⊢ t : U ⟹ env ⊢ Abs T t : (T ⇒ U)"
| App [intro!]: "env ⊢ s : U ⇒ T ⟹ env ⊢ t : T ⟹ env ⊢ (s ° t) : U"

primrec
lift :: "[dB, nat] => dB"
where
"lift (Var i) k = (if i < k then Var i else Var (i + 1))"
| "lift (s ° t) k = lift s k ° lift t k"
| "lift (Abs T s) k = Abs T (lift s (k + 1))"

primrec
subst :: "[dB, dB, nat] => dB"  ("_[_'/_]" [300, 0, 0] 300)
where
subst_Var: "(Var i)[s/k] =
(if k < i then Var (i - 1) else if i = k then s else Var i)"
| subst_App: "(t ° u)[s/k] = t[s/k] ° u[s/k]"
| subst_Abs: "(Abs T t)[s/k] = Abs T (t[lift s 0 / k+1])"

inductive beta :: "[dB, dB] => bool"  (infixl "→⇩β" 50)
where
beta [simp, intro!]: "Abs T s ° t →⇩β s[t/0]"
| appL [simp, intro!]: "s →⇩β t ==> s ° u →⇩β t ° u"
| appR [simp, intro!]: "s →⇩β t ==> u ° s →⇩β u ° t"
| abs [simp, intro!]: "s →⇩β t ==> Abs T s →⇩β Abs T t"

lemma
"Γ ⊢ t : U ⟹ t →⇩β t' ⟹ Γ ⊢ t' : U"
quickcheck[tester = smart_exhaustive, size = 7, iterations = 10]
oops

definition matrix :: "('a :: semiring_0) list list ⇒ nat ⇒ nat ⇒ bool" where
"matrix M rs cs ⟷ (∀ row ∈ set M. length row = cs) ∧ length M = rs"
(*
code_pred [random_dseq inductify] matrix .
thm matrix.random_dseq_equation

thm matrix_aux.random_dseq_equation

values [random_dseq 3, 2] 10 "{(M, rs, cs). matrix (M:: int list list) rs cs}"
*)
lemma [code_pred_intro]:
"matrix [] 0 m"
"matrix xss n m ==> length xs = m ==> matrix (xs # xss) (Suc n) m"
proof -
show "matrix [] 0 m" unfolding matrix_def by auto
next
show "matrix xss n m ==> length xs = m ==> matrix (xs # xss) (Suc n) m"
unfolding matrix_def by auto
qed

code_pred [random_dseq] matrix
apply (cases x)
unfolding matrix_def apply fastforce
apply fastforce done

values [random_dseq 2, 2, 15] 6 "{(M::int list list, n, m). matrix M n m}"

definition "scalar_product v w = (∑ (x, y)←zip v w. x * y)"

definition mv :: "('a :: semiring_0) list list ⇒ 'a list ⇒ 'a list"
where [simp]: "mv M v = map (scalar_product v) M"
text ‹
This defines the matrix vector multiplication. To work properly \<^term>‹matrix M m n ∧ length v = n› must hold.
›

subsection "Compressed matrix"

definition "sparsify xs = [i ← zip [0..<length xs] xs. snd i ≠ 0]"
(*
lemma sparsify_length: "(i, x) ∈ set (sparsify xs) ⟹ i < length xs"
by (auto simp: sparsify_def set_zip)

lemma sum_list_sparsify[simp]:
fixes v :: "('a :: semiring_0) list"
assumes "length w = length v"
shows "(∑x←sparsify w. (λ(i, x). v ! i) x * snd x) = scalar_product v w"
(is "(∑x←_. ?f x) = _")
unfolding sparsify_def scalar_product_def
using assms sum_list_map_filter[where f="?f" and P="λ i. snd i ≠ (0::'a)"]
*)
definition [simp]: "unzip w = (map fst w, map snd w)"

primrec insert :: "('a ⇒ 'b :: linorder) => 'a ⇒ 'a list => 'a list" where
"insert f x [] = [x]" |
"insert f x (y # ys) = (if f y < f x then y # insert f x ys else x # y # ys)"

primrec sort :: "('a ⇒ 'b :: linorder) ⇒ 'a list => 'a list" where
"sort f [] = []" |
"sort f (x # xs) = insert f x (sort f xs)"

definition
"length_permutate M = (unzip o sort (length o snd)) (zip [0 ..< length M] M)"
(*
definition
"transpose M = [map (λ xs. xs ! i) (takeWhile (λ xs. i < length xs) M). i ← [0 ..< length (M ! 0)]]"
*)
definition
"inflate upds = foldr (λ (i, x) upds. upds[i := x]) upds (replicate (length upds) 0)"

definition
"jad = apsnd transpose o length_permutate o map sparsify"

definition
"jad_mv v = inflate o case_prod zip o apsnd (map sum_list o transpose o map (map (λ (i, x). v ! i * x)))"

lemma "matrix (M::int list list) rs cs ⟹ False"
quickcheck[tester = smart_exhaustive, size = 6]
oops

lemma
"⟦ matrix M rs cs ; length v = cs ⟧ ⟹ jad_mv v (jad M) = mv M v"
quickcheck[tester = smart_exhaustive]
oops

end
```