Proving List.reverseRecOn is correct

Stream: Is there code for X?

[Eric Wieser]

Is this statement provable? It feels like it needs some clever generalization trick that I'm out of practice with:

import Mathlib.Data.List.Basic

namespace List

-- the easy one
@[simp]
theorem reverseRecOn_nil {motive : List α → Sort*} (nil : motive [])
    (append_singleton : ∀ (l : List α) (a : α), motive l → motive (l ++ [a])) :
    reverseRecOn [] nil append_singleton = nil :=
  rfl

-- I can't make any progress here
@[simp]
theorem reverseRecOn_concat {motive : List α → Sort*} (x : α) (xs : List α) (nil : motive [])
    (append_singleton : ∀ (l : List α) (a : α), motive l → motive (l ++ [a])) :
    reverseRecOn (C := motive) (xs ++ [x]) nil append_singleton =
      append_singleton _ _ (reverseRecOn (C := motive) xs nil append_singleton) := by
  sorry

[Eric Wieser]

(docs#List.reverseRecOn)

[Eric Wieser]

I tried changing the definition to

def reverseRecOn {motive : List α → Sort*} (l : List α) (nil : motive [])
    (append_singleton : ∀ (l : List α) (a : α), motive l → motive (l ++ [a])) : motive l :=
  match h : reverse l with
  | [] => cast (congr_arg motive <| pf1 h) nil
  | head :: tail =>
    cast (congr_arg motive <| pf2 h) <|
      append_singleton _ head <| reverseRecOn (reverse tail) nil append_singleton
termination_by l.length
decreasing_by
  have : tail.length < l.length := by
    rw [← length_reverse l, h, length_cons]
    simp [Nat.lt_succ]
  simpa only [InvImage, length_reverse]
where
  pf1 (h : reverse l = []) : [] = l := by simpa using congr(reverse $h.symm)
  pf2 {head tail} (h : reverse l = head :: tail) : reverse tail ++ [head] = l := by
    simpa using congr(reverse $h.symm)

but it didn't seem to help; the match h : _ is super hard to do anything with

[Eric Wieser]

Ah, got it: #11257

[Eric Wieser]

A follow-up puzzle:

@[simp]
theorem bidirectionalRec_cons_append {motive : List α → Sort*}
    (nil : motive []) (singleton : ∀ a : α, motive [a])
    (cons_append : ∀ (a : α) (l : List α) (b : α), motive l → motive (a :: (l ++ [b])))
    (a : α) (l : List α) (b : α) :
    bidirectionalRec nil singleton cons_append (a :: (l ++ [b])) =
      cons_append a l b (bidirectionalRec nil singleton cons_append l) := by
  cases l
  · simp [bidirectionalRec]
  · simp_rw [List.cons_append, bidirectionalRec, ←List.cons_append]
    sorry

[Wrenna Robson]

Is there a reason we don't have List.reverseRec?

[Yaël Dillies]

Looks like an oversight

[Eric Wieser]

Arguably having On variants of recursion functions is a waste of time

[Floris van Doorn]

I agree, especially since nowadays we can choose the order of arguments ourselves using named arguments.