Jakub Kądziołka (Feb 12 2021 at 21:23): 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"
show "distinct_adj xs"
unfolding distinct_adj_def successively_conv_nth
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
assume "distinct_adj xs"
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).
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: Dec 21 2024 at 16:20 UTC