## Stream: Beginner Questions

### Topic: relating list indices to appended lists

#### Jakub Kądziołka (Feb 12 2021 at 21:23):

I have defined a property of lists:

``````definition property :: "color list ⇒ bool" where
"property clrs ⟷ (∀a < length clrs. ∀b < length clrs.
a < b ∧ clrs ! a = clrs ! b ⟶ (∃m ∈ {a..b}. clrs ! m ≠ clrs ! a))"
``````

I would now like to show that `property (xs @ ys) ==> property (ys @ zs) ==> property (xs @ zs) ==> property (xs @ ys @ zs)`. AFAICS, the proof would involve some unpleasant index arithmetic to distinguish the cases of which list `a` and `b` point into. Is there an easier way to express this? Maybe some way of manipulating sequences where "m is between a and b" is more of a first-class construct?

#### Manuel Eberl (Feb 13 2021 at 00:17):

Your property is just a very complicated way to say that the list must not have adjacent equal elements:

``````lemma successively_conv_nth: "successively R xs ⟷ (∀i<length xs - 1. R (xs ! i) (xs ! Suc i))"
by (induction xs rule: induct_list012; force simp: nth_Cons split: nat.splits)

definition property :: "'a list ⇒ bool" where
"property clrs ⟷ (∀a < length clrs. ∀b < length clrs.
a < b ∧ clrs ! a = clrs ! b ⟶ (∃m ∈ {a..b}. clrs ! m ≠ clrs ! a))"

lemma propertyD: "property xs ⟹ i < j ⟹ j < length xs ⟹ xs ! i = xs ! j ⟹ ∃m ∈ {i..j}. xs ! m ≠ xs ! i"
unfolding property_def by auto

lemma property_altdef: "property xs ⟷ distinct_adj xs"
proof (intro iffI)
assume p: "property xs"
proof (intro allI impI)
fix i assume i: "i < length xs - 1"
show "xs ! i ≠ xs ! Suc i"
proof
assume *: "xs ! i = xs ! Suc i"
with p i have "∃m∈{i..Suc i}. xs ! m ≠ xs ! i"
by (intro propertyD) auto
thus False using * by (auto simp: le_Suc_eq)
qed
qed
next
show "property xs" unfolding property_def
proof safe
fix i j assume ij: "i < j" "j < length xs" "xs ! i = xs ! j"
from ‹distinct_adj xs› have "xs ! i ≠ xs ! Suc i"
using ij by (auto simp: successively_conv_nth distinct_adj_def)
thus "∃m∈{i..j}. xs ! m ≠ xs ! i"
using ij by (intro bexI[of _ "Suc i"]) auto
qed
qed
``````

Your property then easily follows with the library theorems:

``````lemma "property (xs @ ys) ⟹ property (ys @ zs) ⟹ property (xs @ zs) ⟹ property (xs @ ys @ zs)"
by (auto simp: property_altdef distinct_adj_append_iff hd_append split: if_splits)
``````

Note that this uses `successively` and `distinct_adj`, which is not yet in Isabelle2020 (but in Isabelle2021).

``````
``````

#### Manuel Eberl (Feb 13 2021 at 00:19):

And, yes, you are right in thinking that with the indices it would end up being quite messy (quite a few more case distinctions). Even more so with your original definition of `property` using an existential quantifier, since the automation is not good at instantiating existentials.

Last updated: Aug 10 2022 at 19:17 UTC