Zulip Chat Archive

Stream: general

Topic: How to prove this seemingly trivial lemma?


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

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

view this post on Zulip Patrick Massot (Feb 21 2020 at 18:22):

It's a bool

view this post on Zulip Patrick Massot (Feb 21 2020 at 18:23):

crazy computer science thing

view this post on Zulip Mario Carneiro (Feb 21 2020 at 18:23):

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

view this post on Zulip Yufan Lou (Feb 21 2020 at 18:23):

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

view this post on Zulip Yufan Lou (Feb 21 2020 at 18:24):

what is <:+

view this post on Zulip Mario Carneiro (Feb 21 2020 at 18:24):

I think its actual name is list.is_prefix

view this post on Zulip Yufan Lou (Feb 21 2020 at 18:24):

oh wow

view this post on Zulip Mario Carneiro (Feb 21 2020 at 18:24):

that's where you will find the theorems

view this post on Zulip Mario Carneiro (Feb 21 2020 at 18:26):

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

view this post on Zulip Yufan Lou (Feb 21 2020 at 18:26):

ah ok

view this post on Zulip Yufan Lou (Feb 21 2020 at 18:26):

I was only looking in init.list.basic

view this post on Zulip Yufan Lou (Feb 21 2020 at 18:27):

ah ok prefix_append already proved

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

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

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

view this post on Zulip Yufan Lou (Feb 21 2020 at 18:34):

thx y'all, I've finished it

view this post on Zulip 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: May 10 2021 at 19:16 UTC