decidable instance for `List.IsInfix`

Stream: general

[Asei Inoue]

I think decidable instance for List.IsInfix is missing.
I have proved this.
If you’re okay with it, I’d be happy to submit a PR.

import Lean

#check List.IsInfix

example : List.IsInfix [2, 3] [1, 2, 3, 4] := by
  fail_if_success decide
  exists [1], [4]

@[simp, grind]
def List.isInfix [DecidableEq α] (xs ys : List α) : Bool :=
  match xs, ys with
  | [], _ => true
  | _ :: _, [] => false
  | xs, ys@(_ :: ys') =>
    if isPrefixOf xs ys then
      true
    else
      isInfix xs ys'

#guard [2, 3].isInfix [1, 2, 3, 4]
#guard [1, 2].isInfix [1, 2, 3, 4]
#guard [3, 4].isInfix [1, 2, 3, 4]
#guard ! [2, 4].isInfix [1, 2, 3, 4]

theorem List.IsInfix_iff_isInfix [DecidableEq α] (xs ys : List α) :
    xs.isInfix ys ↔ List.IsInfix xs ys := by
  fun_induction List.isInfix with
  | case1 => grind
  | case2 => grind
  | case3 => grind
  | case4 =>
    simp_all only [imp_false, List.isPrefixOf_iff_prefix]
    grind [List.infix_cons_iff]

instance [DecidableEq α] (xs ys : List α) : Decidable (List.IsInfix xs ys) :=
  decidable_of_iff _ (List.IsInfix_iff_isInfix xs ys)

example : List.IsInfix [2, 3] [1, 2, 3, 4] := by
  decide

[Yury G. Kudryashov]

AFAIR, there is a better implementation in Batteries.

[Yury G. Kudryashov]

See https://github.com/leanprover-community/batteries/blob/main/Batteries/Data/Array/Match.lean, https://github.com/leanprover-community/batteries/blob/main/Batteries/Data/List/Matcher.lean, and https://github.com/leanprover-community/batteries/blob/main/Batteries/Data/String/Matcher.lean

[Yury G. Kudryashov]

It looks like their version has no proof of correctness.

[Eric Wieser]

docs#List.decidableInfix already exists