Zulip Chat Archive

Stream: general

Topic: alternative definition of list.is_prefix


view this post on Zulip Kenny Lau (Apr 19 2018 at 03:26):

Could we have a subtype instead of an existential here, as the data is lost in the latter?

view this post on Zulip Kenny Lau (Apr 19 2018 at 03:26):

@Mario Carneiro

view this post on Zulip Mario Carneiro (Apr 19 2018 at 03:27):

the data isn't lost, you can recover it by dropping the first n elements of the larger list

view this post on Zulip Mario Carneiro (Apr 19 2018 at 03:27):

where n is the length of the smaller list

view this post on Zulip Kenny Lau (Apr 19 2018 at 03:27):

right, but has this been done in mathlib?

view this post on Zulip Mario Carneiro (Apr 19 2018 at 03:27):

The existential is used because I want it to be a prop

view this post on Zulip Kenny Lau (Apr 19 2018 at 03:28):

I mean, the choice function for this existential isn't in mathlib

view this post on Zulip Mario Carneiro (Apr 19 2018 at 03:43):

theorem prefix_iff_eq_append (l₁ l₂ : list α) : l₁ <+: l₂ ↔ l₁ ++ drop (length l₁) l₂ = l₂ :=
⟨λ h, let ⟨r, e⟩ := h in begin
  rwa append_inj_right ((take_append_drop (length l₁) l₂).trans e.symm) _,
  simp [min_eq_left, length_le_of_sublist (sublist_of_prefix h)],
end, λ e, ⟨_, e⟩⟩

theorem suffix_iff_eq_append (l₁ l₂ : list α) : l₁ <:+ l₂ ↔ take (length l₂ - length l₁) l₂ ++ l₁ = l₂ :=
⟨λ ⟨r, e⟩, begin
  rwa append_inj_left ((take_append_drop (length l₂ - length l₁) l₂).trans e.symm) _,
  simp [min_eq_left, nat.sub_le, e.symm],
  apply nat.add_sub_cancel_left
end, λ e, ⟨_, e⟩⟩

Last updated: May 14 2021 at 06:16 UTC