How to prove this seemingly trivial lemma?

Stream: general

[Yufan Lou]

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

[Mario Carneiro]

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

[Patrick Massot]

It's a bool

[Patrick Massot]

crazy computer science thing

[Mario Carneiro]

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

[Yufan Lou]

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

[Yufan Lou]

what is <:+

[Mario Carneiro]

I think its actual name is list.is_prefix

[Yufan Lou]

oh wow

[Mario Carneiro]

that's where you will find the theorems

[Mario Carneiro]

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

[Yufan Lou]

ah ok

[Yufan Lou]

I was only looking in init.list.basic

[Yufan Lou]

ah ok prefix_append already proved

[Mario Carneiro]

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]

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

[Mario Carneiro]

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

[Yufan Lou]

thx y'all, I've finished it

[Mario Carneiro]

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