Stream: Beginner Questions

Topic: relating list indices to appended lists


view this post on Zulip 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?

view this post on Zulip 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).


view this post on Zulip 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: Sep 25 2021 at 08:21 UTC