## Stream: general

### Topic: How to prove this seemingly trivial lemma?

#### Yufan Lou (Feb 21 2020 at 18:20):

lemma append_is_prefix [decidable_eq α] (l₁ : list α) (l₂ : list α) :
is_prefix_of l₁ (l₁ ++ l₂) = tt := sorry


#### Mario Carneiro (Feb 21 2020 at 18:22):

is_prefix_of is a Prop, right? So there is a bool coercion there that you should first get rid of

It's a bool

#### Patrick Massot (Feb 21 2020 at 18:23):

crazy computer science thing

#### Mario Carneiro (Feb 21 2020 at 18:23):

In that case there should be a theorem relating it to <:+ which is a prop

#### Yufan Lou (Feb 21 2020 at 18:23):

XD
yeah I had no idea how to work with bool in lean

#### Yufan Lou (Feb 21 2020 at 18:24):

what is <:+

#### Mario Carneiro (Feb 21 2020 at 18:24):

I think its actual name is list.is_prefix

oh wow

#### Mario Carneiro (Feb 21 2020 at 18:24):

that's where you will find the theorems

#### Mario Carneiro (Feb 21 2020 at 18:26):

Oops, prefix is <+:, suffix is <:+

ah ok

#### Yufan Lou (Feb 21 2020 at 18:26):

I was only looking in init.list.basic

#### Yufan Lou (Feb 21 2020 at 18:27):

ah ok prefix_append already proved

#### Mario Carneiro (Feb 21 2020 at 18:28):

Oh, looks like you found a hole in the library. The equivalence of list.is_prefix and list.is_prefix_of is not proved

#### Mario Carneiro (Feb 21 2020 at 18:29):

You should just use list.is_prefix anyway, it has a decidable instance so it's better than a bool function

#### Mario Carneiro (Feb 21 2020 at 18:29):

but list.is_prefix_of is in core... maybe now we can finally do something about these bits and bobs

#### Yufan Lou (Feb 21 2020 at 18:34):

thx y'all, I've finished it

#### Mario Carneiro (Feb 21 2020 at 18:48):

import data.list.basic data.bool

namespace list

theorem is_prefix_of_iff {α} [decidable_eq α] : ∀ {l₁ l₂ : list α},
is_prefix_of l₁ l₂ ↔ l₁ <+: l₂
| [] l₂ := ⟨λ _, nil_prefix _, λ _, by cases l₂; exact rfl⟩
| (_::_) [] := ⟨by rintro ⟨⟩, λ h, by cases eq_nil_of_prefix_nil h⟩
| (a::l₁) (b::l₂) := begin
rw [is_prefix_of, band_coe_iff, bool.coe_to_bool, is_prefix_of_iff],
split,
{ rintro ⟨rfl, h⟩, exact (prefix_cons_inj _).2 h },
{ rintro ⟨l, e⟩, injection e with h₁ h₂, exact ⟨h₁, _, h₂⟩ }
end

end list


Last updated: Dec 20 2023 at 11:08 UTC