Theory Counting_Tiles
theory Counting_Tiles
imports
"HOL-Library.Code_Target_Numeral"
"HOL-Library.Product_Lexorder"
"HOL-Library.RBT_Mapping"
"../state_monad/State_Main"
Example_Misc
begin
subsection ‹A Counting Problem›
text ‹
This formalization contains verified solutions for Project Euler problems
▪ ‹#›114 (🌐‹https://projecteuler.net/problem=114›) and
▪ ‹#›115 (🌐‹https://projecteuler.net/problem=115›).
This is the problem description for ‹#›115:
\begin{quote}
A row measuring n units in length has red blocks with a minimum length of m units placed on it,
such that any two red blocks (which are allowed to be different lengths) are separated
by at least one black square.
Let the fill-count function, F(m, n), represent the number of ways that a row can be filled.
For example, F(3, 29) = 673135 and F(3, 30) = 1089155.
That is, for m = 3, it can be seen that n = 30 is the smallest value for which the fill-count
function first exceeds one million.
In the same way, for m = 10, it can be verified that F(10, 56) = 880711 and F(10, 57) = 1148904,
so n = 57 is the least value for which the fill-count function first exceeds one million.
For m = 50, find the least value of n for which the fill-count function first exceeds one million.
\end{quote}
›
subsubsection ‹Misc›
lemma lists_of_len_fin1:
"finite (lists A ∩ {l. length l = n})" if "finite A"
using that
proof (induction n)
case 0 thus ?case
by auto
next
case (Suc n)
have "lists A ∩ { l. length l = Suc n } = (λ(a,l). a#l) ` (A × (lists A ∩ {l. length l = n}))"
by (auto simp: length_Suc_conv)
moreover from Suc have "finite …"
by auto
ultimately show ?case
by simp
qed
lemma disjE1:
"A ∨ B ⟹ (A ⟹ P) ⟹ (¬ A ⟹ B ⟹ P) ⟹ P"
by metis
subsubsection ‹Problem Specification›
text ‹Colors›
datatype color = R | B
text ‹Direct natural definition of a valid line›
context
fixes m :: nat
begin
inductive valid where
"valid []" |
"valid xs ⟹ valid (B # xs)" |
"valid xs ⟹ n ≥ m ⟹ valid (replicate n R @ xs)"
text ‹Definition of the fill-count function›
definition "F n = card {l. length l = n ∧ valid l}"
subsubsection ‹Combinatorial Identities›
text ‹This alternative variant helps us to prove the split lemma below.›
inductive valid' where
"valid' []" |
"n ≥ m ⟹ valid' (replicate n R)" |
"valid' xs ⟹ valid' (B # xs)" |
"valid' xs ⟹ n ≥ m ⟹ valid' (replicate n R @ B # xs)"
lemma valid_valid':
"valid l ⟹ valid' l"
by (induction rule: valid.induct)
(auto 4 4 intro: valid'.intros elim: valid'.cases
simp: replicate_add[symmetric] append_assoc[symmetric]
)
lemmas valid_red = valid.intros(3)[OF valid.intros(1), simplified]
lemma valid'_valid:
"valid' l ⟹ valid l"
by (induction rule: valid'.induct) (auto intro: valid.intros valid_red)
lemma valid_eq_valid':
"valid' l = valid l"
using valid_valid' valid'_valid by metis
text ‹Additional Facts on Replicate›
lemma replicate_iff:
"(∀i<length l. l ! i = R) ⟷ (∃ n. l = replicate n R)"
by auto (metis (full_types) in_set_conv_nth replicate_eqI)
lemma replicate_iff2:
"(∀i<n. l ! i = R) ⟷ (∃ l'. l = replicate n R @ l')" if "n < length l"
using that by (auto simp: list_eq_iff_nth_eq nth_append intro: exI[where x = "drop n l"])
lemma replicate_Cons_eq:
"replicate n x = y # ys ⟷ (∃ n'. n = Suc n' ∧ x = y ∧ replicate n' x = ys)"
by (cases n) auto
text ‹Main Case Analysis on ‹@term valid››
lemma valid_split:
"valid l ⟷
l = [] ∨
(l!0 = B ∧ valid (tl l)) ∨
length l ≥ m ∧ (∀ i < length l. l ! i = R) ∨
(∃ j < length l. j ≥ m ∧ (∀ i < j. l ! i = R) ∧ l ! j = B ∧ valid (drop (j + 1) l))"
unfolding valid_eq_valid'[symmetric]
apply standard
subgoal
by (erule valid'.cases) (auto simp: nth_append nth_Cons split: nat.splits)
subgoal
apply (auto intro: valid'.intros simp: replicate_iff elim!: disjE1)
apply (fastforce intro: valid'.intros simp: neq_Nil_conv)
apply (subst (asm) replicate_iff2; fastforce intro: valid'.intros simp: neq_Nil_conv nth_append)+
done
done
text ‹Base cases›
lemma valid_line_just_B:
"valid (replicate n B)"
by (induction n) (auto intro: valid.intros)
lemma F_base_0_aux:
"{l. l = [] ∧ valid l} = {[]}"
by (auto intro: valid.intros)
lemma F_base_0: "F 0 = 1"
by (auto simp: F_base_0_aux F_def)
lemma F_base_aux: "{l. length l=n ∧ valid l} = {replicate n B}" if "n > 0" "n < m"
using that
proof (induction n)
case 0
then show ?case
by simp
next
case (Suc n)
show ?case
proof (cases "n = 0")
case True
with Suc.prems show ?thesis
by (auto intro: valid.intros elim: valid.cases)
next
case False
with Suc.prems show ?thesis
apply safe
using Suc.IH
apply -
apply (erule valid.cases)
apply (auto intro: valid.intros elim: valid.cases)
done
qed
qed
lemma F_base_1:
"F n = 1" if "n > 0" "n < m"
using that unfolding F_def by (simp add: F_base_aux)
lemma valid_m_Rs [simp]:
"valid (replicate m R)"
using valid_red[of m, simplified] by simp
lemma F_base_aux_2: "{l. length l=m ∧ valid l} = {replicate m R, replicate m B}"
apply (auto simp: valid_line_just_B)
apply (erule Counting_Tiles.valid.cases)
apply auto
subgoal for xs
using F_base_aux[of "length xs"] by (cases "xs = []") auto
done
lemma F_base_2:
"F m = 2" if "0 < m"
using that unfolding F_def by (simp add: F_base_aux_2)
text ‹The recursion case›
lemma finite_valid_length:
"finite {l. length l = n ∧ valid l}" (is "finite ?S")
proof -
have "?S ⊆ lists {R, B} ∩ {l. length l = n}"
by (auto intro: color.exhaust)
moreover have "finite …"
by (auto intro: lists_of_len_fin1)
ultimately show ?thesis
by (rule finite_subset)
qed
lemma valid_line_aux:
"{l. length l = n ∧ valid l} ≠ {}" (is "?S ≠ {}")
using valid_line_just_B[of n] by force
lemma replicate_unequal_aux:
"replicate x R @ B # l ≠ replicate y R @ B # l'" (is "?l ≠ ?r") if ‹x < y› for l l'
proof -
have "?l ! x = B" "?r ! x = R"
using that by (auto simp: nth_append)
then show ?thesis
by auto
qed
lemma valid_prepend_B_iff:
"valid (B # xs) ⟷ valid xs" if "m > 0"
using that
by (auto 4 3 intro: valid.intros elim: valid.cases simp: Cons_replicate_eq Cons_eq_append_conv)
lemma F_rec: "F n = F (n-1) + 1 + (∑i=m..<n. F (n-i-1))" if ‹n>m› "m > 0"
proof -
have "{l. length l = n ∧ valid l}
= {l. length l = n ∧ valid (tl l) ∧ l!0=B}
∪ {l. length l = n ∧
(∃ i. i < n ∧ i ≥ m ∧ (∀ k < i. l!k = R) ∧ l!i = B ∧ valid (drop (i + 1) l))}
∪ {l. length l = n ∧ (∀i<n. l!i=R)}
" (is "?A = ?B ∪ ?D ∪ ?C")
using ‹n > m› by (subst valid_split) auto
let ?B1 = "((#) B) ` {l. length l = n - Suc 0 ∧ valid l}"
from ‹n > m› have "?B = ?B1"
apply safe
subgoal for l
by (cases l) (auto simp: valid_prepend_B_iff)
by auto
have 1: "card ?B1 = F (n-1)"
unfolding F_def by (auto intro: card_image)
have "?C = {replicate n R}"
by (auto simp: nth_equalityI)
have 2: "card {replicate n R} = 1"
by auto
let ?D1="(⋃ i ∈ {m..<n}. (λ l. replicate i R @ B # l)` {l. length l = n - i - 1 ∧ valid l})"
have "?D =
(⋃i ∈ {m..<n}. {l. length l = n ∧ (∀ k < i. l!k = R) ∧ l!i = B ∧ valid (drop (i + 1) l)})"
by auto
have "{l. length l = n ∧ (∀ k < i. l!k = R) ∧ l!i = B ∧ valid (drop (i + 1) l)}
= (λ l. replicate i R @ B # l)` {l. length l = n - i - 1 ∧ valid l}"
if "i < n" for i
apply safe
subgoal for l
apply (rule image_eqI[where x = "drop (i + 1) l"])
apply (rule nth_equalityI)
using that
apply (simp_all split: nat.split add: nth_Cons nth_append)
using add_diff_inverse_nat apply fastforce
done
using that by (simp add: nth_append; fail)+
then have D_eq: "?D = ?D1"
unfolding ‹?D = _› by auto
have inj: "inj_on (λl. replicate x R @ B # l) {l. length l = n - Suc x ∧ valid l}" for x
unfolding inj_on_def by auto
have *:
"(λl. replicate x R @ B # l) ` {l. length l = n - Suc x ∧ valid l} ∩
(λl. replicate y R @ B # l) ` {l. length l = n - Suc y ∧ valid l} = {}"
if "m ≤ x" "x < y" "y < n" for x y
using that replicate_unequal_aux[OF ‹x < y›] by auto
have 3: "card ?D1 = (∑i=m..<n. F (n-i-1))"
proof (subst card_Union_disjoint, goal_cases)
case 1
show ?case
unfolding pairwise_def disjnt_def
proof (clarsimp, goal_cases)
case prems: (1 x y)
from prems show ?case
apply -
apply (rule linorder_cases[of x y])
apply (rule *; assumption)
apply (simp; fail)
apply (subst Int_commute; rule *; assumption)
done
qed
next
case 3
show ?case
proof (subst sum.reindex, unfold inj_on_def, clarsimp, goal_cases)
case prems: (1 x y)
with *[of y x] *[of x y] valid_line_aux[of "n - Suc x"] show ?case
by - (rule linorder_cases[of x y], auto)
next
case 2
then show ?case
by (simp add: F_def card_image[OF inj])
qed
qed (auto intro: finite_subset[OF _ finite_valid_length])
show ?thesis
apply (subst F_def)
unfolding ‹?A = _› ‹?B = _› ‹?C = _› D_eq
apply (subst card_Un_disjoint)
apply (blast intro: finite_subset[OF _ finite_valid_length])+
subgoal
using Cons_replicate_eq[of B _ n R] replicate_unequal_aux by fastforce
apply (subst card_Un_disjoint)
apply (blast intro: finite_subset[OF _ finite_valid_length])+
unfolding 1 2 3 using ‹m > 0› by (auto simp: Cons_replicate_eq Cons_eq_append_conv)
qed
subsubsection ‹Computing the Fill-Count Function›
fun lcount :: "nat ⇒ nat" where
"lcount n = (
if n < m then 1
else if n = m then 2
else lcount (n - 1) + 1 + (∑i ← [m..<n]. lcount (n - i - 1))
)"
lemmas [simp del] = lcount.simps
lemma lcount_correct:
"lcount n = F n" if "m > 0"
proof (induction n rule: less_induct)
case (less n)
from ‹m > 0› show ?case
apply (cases "n = 0")
subgoal
by (simp add: lcount.simps F_base_0)
by (subst lcount.simps)
(simp add: less.IH F_base_1 F_base_2 F_rec interv_sum_list_conv_sum_set_nat)
qed
subsubsection ‹Memoization›
memoize_fun lcount⇩m: lcount with_memory dp_consistency_mapping monadifies (state) lcount.simps
memoize_correct
by memoize_prover
lemmas [code] = lcount⇩m.memoized_correct
end
subsubsection ‹Problem solutions›
text ‹Example and solution for problem ‹#›114›
value "lcount 3 7"
value "lcount 3 50"
text ‹Examples for problem ‹#›115›
value "lcount 3 29"
value "lcount 3 30"
value "lcount 10 56"
value "lcount 10 57"
text ‹Binary search for the solution of problem ‹#›115›
value "lcount 50 100"
value "lcount 50 150"
value "lcount 50 163"
value "lcount 50 166"
value "lcount 50 167"
value "lcount 50 168"
value "lcount 50 169"
value "lcount 50 175"
value "lcount 50 200"
value "lcount 50 300"
value "lcount 50 500"
value "lcount 50 1000"
text ‹We prove that 168 is the solution for problem ‹#›115›
theorem
"(LEAST n. F 50 n > 1000000) = 168"
proof -
have "lcount 50 168 > 1000000"
by eval
moreover have "∀ n ∈ {0..<168}. lcount 50 n < 1000000"
by eval
ultimately show ?thesis
by - (rule Least_equality; rule ccontr; force simp: not_le lcount_correct)
qed
end