Stream: general

Topic: alternative definition of list.is_prefix

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?

@Mario Carneiro

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

Mario Carneiro (Apr 19 2018 at 03:27):

where n is the length of the smaller list

Kenny Lau (Apr 19 2018 at 03:27):

right, but has this been done in mathlib?

Mario Carneiro (Apr 19 2018 at 03:27):

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

Kenny Lau (Apr 19 2018 at 03:28):

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

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],