Email Gateway (Aug 19 2022 at 09:00): Email Gateway (Aug 19 2022 at 09:00):From: "Aaron W. Hsu" <arcfide@sacrideo.us>
Dear Isabelle Users:
I have been trying unsuccessfully for the past couple of days to get
Isabelle to do my bidding when it comes to the following lemma and
definition. I wonder if someone might be able to give me some hints on how
to approach this. It seems like it ought to be a simple thing to prove,
but I think my Isabelle skills are still too weak.
definition sv2vl :: "nat ⇒ 'a list ⇒ 'a list" where
"sv2vl n ls ≡
if ls = []
then (replicate n fill)
else take n (concat (replicate (1 + n div length ls) ls))"
lemma sv2vl_mod [simp]:
"i < n ∧ ls ≠ [] ⟹ sv2vl n ls ! i = ls ! (i mod length ls)"
by ???
I have been able to prove the following:
lemma sv2vl_len [simp]:
"length (sv2vl n ls) = n"
but that required significantly more work than I would have thought it
ought to. If someone could provide some assistance on these, I would
appreciate it.
Email Gateway (Aug 19 2022 at 09:01):From: Andreas Lochbihler <andreas.lochbihler@kit.edu>
Dear Aaron,
it would have helped a lot to describe what you want to achieve with sv2vl. I
guess that sv2vl denotes the prefix of length n of the list that always repeats
the list ls, i.e., sv2vl 5 [1, 2] = [1, 2, 1, 2, 1].
If this is the case, you can simplify your definition a bit, which makes proofs
easier:
"sv2vl n ls ==
if ls = []
then (replicate n fill)
else take n (concat (replicate n ls))"
Both definitions are equivalent because "take n" cuts off any extra stuff that
"replicate n" produces. Note that HOL has no notion of computation, so
efficiency is not an issue here -- if you want to generate efficient code for
it, you can still prove your definition as a code equation later on.
Your sv2vl_mod lemma requires the following lemma that is not yet present in
Isabelle's List library:
lemma nth_concat_replicate:
"i < n * length xs
==> concat (replicate n xs) ! i = xs ! (i mod length xs)"
by(induct n arbitrary: i)(auto simp add: nth_append mod_geq)
Then, your lemma can be proven automatically:
lemma sv2vl_mod [simp]:
"i < n & ls ~= [] ==> sv2vl n ls ! i = ls ! (i mod length ls)"
by(auto simp add: sv2vl_def neq_Nil_conv nth_concat_replicate)
Hope this helps,
Andreas
Last updated: Apr 16 2024 at 08:18 UTC