Tidying up some messy currying and option handling

Stream: new members

[Sam]

I have the following messy function definition. I think I'm missing some syntax tricks to make this pretty. How can I improve this?

This finds the first/longest tail of l1 that is also a prefix of l2.

def overlap {α : Type u} (l₁ l₂ : list α) [decidable_pred (λ (a : list α), a.is_prefix l₂)] : list α :=
  (l₁.tails.find (λ (a : list α), a.is_prefix l₂)).get_or_else []

The lambda thing feels wrong. I'm using it to curry is_prefix with reversed argument order. Is there a neater way of doing that? I especially dislike having it repeated in the decidable_pred! Can that be fixed? Is there a way to avoid the currying altogether?

I'm not sure whether I'm handling the option value in the best way. list.find returns an option, but in this case I can actually guarantee/prove that it will always be some, because the last tail of any list is [], which is a prefix of all lists. I use get_or_else [] to get this behaviour, but is it better to use some other proved unwrapping or find variant?

[Yakov Pechersky]

You can likely just have the stronger assumption [decidable_eq α], unless you have a pretty complex type your lists operate over

[Yakov Pechersky]

I think using get_or_else [] makes total sense -- you're providing a junk value for a state you know is inaccessible.

[Sam]

Oh! Yes decidable_eq works nicely. I'm actually only planning on using this for nats, so that's perfect. Thanks!

[Sam]

My concern with get_or_else [] is that maybe it will complicate proving properties of this function? But I haven't actually started working on that yet, so maybe it's fine.

[Yakov Pechersky]

You'll use docs#list.find_cons_of_pos and docs#option.get_or_else_some

[Yakov Pechersky]

You might like to write a helper lemma like find_eq_nth_zero_filter

[Kyle Miller]

If you want to save the lambda, you can take advantage of the operator for is_prefix:

def overlap {α : Type u} (l₁ l₂ : list α) [decidable_eq α] : option (list α) :=
(l₁.tails.find (<+: l₂)).get_or_else []

[Sam]

Oh that operator thing is nice! Thanks Kyle!

I'd thought there might be some general way to do something like (list.find _ l₂)to do a form of partial application, but I'll take this trick in this case.

[Kyle Miller]

@Sam It occurred to me that you can also do this to organize the definition, which I don't think sacrifices readability. I forgot about doing it this way because the option argument is implicit (and if it were explicit, you could even do (l₁.tails.find (<+: l₂)).get begin ... end)

def overlap {α : Type u} (l₁ l₂ : list α) [decidable_eq α] : list α :=
@option.get _ (l₁.tails.find (<+: l₂))
begin
  induction l₁,
  { simp [list.find, list.nil_prefix], },
  { simp [list.find],
    split_ifs with h,
    { simp, },
    { assumption, } }
end

[Sam]

Ooh that's pretty!

I actually haven't got very far with the option.get version yet, because when doing something simple like this

@[simp]
lemma overlap_get_nil_list {α : Type u} [decidable_eq α] (l₂ : list α) : (overlap_get [] l₂) = [] :=
begin
  rw overlap_get,
end

The tactic state just looks like this

1 goal
α: Type u
_inst_1: decidable_eq α
l₂: list α
⊢ option.get _ = list.nil

Which is kind of confusing! I assume all of the details of the goal are hidden in the _ somehow? I'm not sure how to proceed from here.

[Notification Bot]

Sam has marked this topic as unresolved.

[Kyle Miller]

This is an unfortunate feature of option.get, and I think it really should have the option argument be explicit. One thing you can do to help here is use the set_option pp.implicit true command to make implicit arguments pretty print as explicit.

[Kyle Miller]

But a fun thing is that this lemma is true by definition:

@[simp]
lemma overlap_get_nil_list {α : Type u} [decidable_eq α] (l₂ : list α) : (overlap_get [] l₂) = [] :=
rfl

[Kyle Miller]

(Think about how all the definitions work and what happens when the first argument is [].)

[Sam]

Oh! That's very cool that that's refl. pp.implicit seems like a nice trick for this.

[Sam]

I'm finding that I can get through proving at least some basic lemmas on the option.get version now, although the state still looks very messy and I'm mostly just relying on tactics to brute force it. I had naively hoped that option.get would lead to a cleaner solving experience. My thinking was that, because we proved some in the definition itself, that would effectively vanish from the proof. I thought it would let me pretend that there was never even an option involved. I appear to have been very wrong about that!

[Kyle Miller]

Yeah, all you really get is that if you can reduce the value in option.get to some ... then the some goes away. This function also introduces somewhat complex dependent types that make rw more difficult to use, too.

Maybe it's easier to prove things about l₁.tails.find (<+: l₂) first and then write proofs about overlap_get as corollaries... Or even the get_or_else version (which doesn't have dependent type issues).

[Eric Rodriguez]

There's also pp.proofs

[Sam]

What I ended up doing was defining this. It needs a better name and some tidying up, but I haven't found a problem with this approach yet. Perhaps something based on this idea would be useful in the library?

-- TODO: Decent name
def list.find_guaranteed
{α : Type u}
(l : list α)
(p : α → Prop) [decidable_pred p]
(q : ∃ (a : α), (p a ∧ a ∈ l)) : α :=
@option.get _ (list.find p l) (@list.find_mem_some α l p (λ (a : α), _inst_1 a) q)

I've got nearly all of the applicable find lemmas from data.list.basic reimplemented for this (but they're a mess, because I'm a newb). find_guranteed_cons_of_neg and find_guranteed_cons_of_pos both have a sorry in them for now, but I don't think everything's going to come crashing down when I try to fix that... Famous last words.

I use it like this

-- TODO: Decent name
lemma tails_has_match
{α : Type u}
(l₁ l₂ : list α) :
∃ (a : list α), (((<+: l₂) a) ∧ (a ∈ l₁.tails)) := sorry --omitted for brevity

def overlap {α : Type u} [decidable_eq α] (l₁ l₂ : list α) : list α :=
  l₁.tails.find_guaranteed (<+: l₂) (@tails_has_match α l₁ l₂)

This seems to be working well so far. I've been able to define and prove a number of simple lemmas on overlap without ever having to touch option, because I never need to look inside find_guaranteed. It certainly seems much easier to use than either of the other approaches.

[Sam]

E.g. this is pretty nice!

@[simp]
lemma overlap_suffix
{α : Type u} [decidable_eq α]
(l₁ l₂ : list α) :
list.is_suffix (overlap l₁ l₂) l₁ :=
begin
  have : (overlap l₁ l₂) ∈ l₁.tails := list.find_guranteed_mem,
  finish,
end

I'm sure there's a way to tidy up that have, but I'm happy with how tiny this proof is using the find_guaranteed approach!

[Matt Diamond]

@Sam I can't find list.find_mem_some in the mathlib docs... is that supposed to be list.find_some, or is it something you defined?

[Sam]

@Matt Diamond Oops sorry! I forgot to include that. That's mine, it looks like this (with another messy newb proof that I need to tidy up).

@[simp]
lemma list.find_mem_some
{α : Type u}
(l : list α)
(p : α → Prop) [decidable_pred p]
(q : ∃ (a : α), (p a ∧ a ∈ l)) :
(list.find p l).is_some :=
begin
  cases q, cases q_h,

  have h : l ≠ [] := @list.ne_nil_of_mem α q_w l q_h_right,

  unfold_coes,

  induction l,
  { contradiction },

  simp only [list.find],

  split_ifs with h₂,
  { simp only [option.is_some_some, coe_sort_tt] },

  simp at l_ih,
  have h₁ : q_w ∈ l_tl := by finish,
  have h₂ : l_tl ≠ [] := list.ne_nil_of_mem h₁,
  simp [h₁, h₂] at l_ih,
  assumption,
end

[Matt Diamond]

no worries!

[Sam]

Actually the name seems like nonsense now that I look at it again.

[Sam]

I think I need to break out some named def for "list is guaranteed to have an item matching predicate" or something like that.

[Sam]

I.e. list.contains_pred