enumerate all prefixes of List

Stream: general

[Asei Inoue]

module

import Lean

namespace List

/-- Enumerate all prefixes of a list `xs`. -/
@[simp, grind]
def prefixes (xs : List α) : List (List α) :=
  match xs with
  | [] => [[]]
  | x :: xs => [] :: xs.prefixes.map (x :: ·)

#guard prefixes [1, 2, 3] = [[], [1], [1, 2], [1, 2, 3]]

variable [DecidableEq α]

/-- Every list returned by `prefixes` is indeed a prefix of the original list. -/
@[grind ->]
theorem isPrefix_of_prefixes (xs : List α) :
    ∀ ys ∈ xs.prefixes, isPrefixOf ys xs := by
  induction xs with grind

/-- Every prefix is enumerated by the `prefixes` function. -/
@[grind ->]
theorem prefixes_of_isPrefix (xs ys : List α) :
    isPrefixOf ys xs → ys ∈ xs.prefixes := by
  fun_induction isPrefixOf with grind [prefixes.eq_def]

theorem prefixes_iff_isPrefixOf (xs ys : List α) :
    ys ∈ xs.prefixes ↔ isPrefixOf ys xs :=
  ⟨isPrefix_of_prefixes xs ys, prefixes_of_isPrefix xs ys⟩

end List

[Asei Inoue]

Recently, I wrote a function that enumerates all prefixes of a list and proved its correctness.
I think this function could be useful in other contexts as well, but after checking with Loogle, it seems that it is not yet available in the libraries.
If others think this would be useful, I would be happy to open a PR.

[Eric Wieser]

This seems like a reasonable definition to have

[Eric Wieser]

(though I think the lemmas could do with some bikeshedding)

[Asei Inoue]

This is suitable for Batteries?

[Jakub Nowak]

That's List.inits I think?

[Jakub Nowak]

And List.mem_inits is more or less prefixes_iff_isPrefixOf, but with List.IsPrefix. Adding List.isPrefixOf version to Batteries could be useful though.

[Eric Wieser]

I don't see why we'd want the isPrefixOf version, that's only simp-normal when working with bool, which ↔ doesn't.

[Jakub Nowak]

Why do we even have List.isPrefixOf? Also, its doc-string mentions List.IsPrefixOf which doesn't exist?

[Eric Wieser]

The Bool one is used to implement decidability of the Prop one

[Violeta Hernández]

Eric Wieser said:

The Bool one is used to implement decidability of the Prop one

This feels like an instance of missing automation for decidability.

[Chris Henson]

As in you would like to automate docs#decidable_of_iff or docs#decidable_of_decidable_of_iff instances somehow?

[Eric Wieser]

The point is to have an optimized implementation

[Violeta Hernández]

My proposal is that you should be able to write a function returning bool, tag it with something, and get the same function returning Prop + a decidable instance.

[Jakub Nowak]

The Prop one is the one you should usually be working with in proofs. So that one is defined in a way to be easy to work with in proofs. The boolean one (i.e. decidable instance) is made with performance in mind. Though, I think that we shouldn't have List.isPrefixOf? be public. Having public decidable instance should be enough?

[Edward van de Meent]

Violeta Hernández said:

My proposal is that you should be able to write a function returning bool, tag it with something, and get the same function returning Prop + a decidable instance.

This practically already exists with the coercion from Bool to Prop (which is defined as b => b = true) and the DecidableEq instance for Bool

[Violeta Hernández]

Does that mean we should just be using bool-valued functions for all computational purposes? And skip the Prop valued ones entirely.

[Asei Inoue]

When you define something as an inductive predicate rather than a recursive function, there are times when I find it inconvenient because functional induction cannot be used.

[Asei Inoue]

Nat.le is defined as an inductive predicate, whereas List.Prefix is written as an existential proposition rather than an inductive predicate. I would like to know if there are any guidelines for deciding when one should use an inductive predicate.