Zulip Chat Archive

Stream: new members

Topic: Tidying up some messy currying and option handling

Sam (Aug 05 2022 at 18:00):

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 (Aug 05 2022 at 18:01):

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

Yakov Pechersky (Aug 05 2022 at 18:02):

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

Sam (Aug 05 2022 at 18:03):

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

Sam (Aug 05 2022 at 18:05):

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 (Aug 05 2022 at 18:10):

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

Yakov Pechersky (Aug 05 2022 at 18:10):

You might like to write a helper lemma like find_eq_nth_zero_filter

Kyle Miller (Aug 05 2022 at 18:13):

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 (Aug 05 2022 at 18:16):

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 (Aug 05 2022 at 19:31):

@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₂))
  induction l₁,
  { simp [list.find, list.nil_prefix], },
  { simp [list.find],
    split_ifs with h,
    { simp, },
    { assumption, } }

Sam (Aug 05 2022 at 19:51):

Ooh that's pretty!

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

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

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 (Aug 05 2022 at 19:51):

Sam has marked this topic as unresolved.

Kyle Miller (Aug 05 2022 at 19:56):

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 (Aug 05 2022 at 19:57):

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

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

Kyle Miller (Aug 05 2022 at 19:58):

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

Sam (Aug 05 2022 at 20:13):

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

Sam (Aug 05 2022 at 20:19):

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 (Aug 05 2022 at 20:22):

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 (Aug 05 2022 at 21:18):

There's also pp.proofs

Sam (Aug 06 2022 at 02:02):

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 (Aug 06 2022 at 02:21):

E.g. this is pretty nice!

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

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 (Aug 06 2022 at 03:57):

@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 (Aug 06 2022 at 04:08):

@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).

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 :=
  cases q, cases q_h,

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


  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,

Matt Diamond (Aug 06 2022 at 04:10):

no worries!

Sam (Aug 06 2022 at 04:10):

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

Sam (Aug 06 2022 at 04:11):

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 (Aug 06 2022 at 04:12):

I.e. list.contains_pred

Last updated: Dec 20 2023 at 11:08 UTC