Working with a list in a lemma

Stream: new members

[An Qi Zhang]

Hello! I wanted to show that the elements of a sorted list are ordered, but I'm stuck and I'm not sure what are the tactics and/or theorems required to reason about the lists in the goal are. I was wondering if anyone knows how does one work with lists in a lemma?

Here's a MWE to illustrate:

import Mathlib

/- List is sorted, and totally ordered. -/
def List.isOrdered {α} (l : List α) (r : α → α → Prop) : Prop :=
  ∀ i : Fin (l.length), ∀ j : Fin (l.length), i < j ↔ r l[i] l[j]

instance : DecidableRel Nat.lt := by
  unfold Nat.lt
  simp[Nat.succ_eq_add_one, Nat.le_eq]
  infer_instance

lemma list_is_ordered (l : List Nat) :
  let l_sorted := l.insertionSort Nat.lt
  l_sorted.isOrdered Nat.lt := by
  intro l_sorted
  unfold List.isOrdered
  intro i j
  apply Iff.intro
  . case mp =>
    intro hi_lt_j
    /- What is the best way to handle `sorted_list` here? -/
    simp[l_sorted]
    simp[List.insertionSort]
    sorry
  . case mpr =>
    sorry

[Kyle Miller]

Is this for the exercise of it, or are you looking for docs#List.sorted_insertionSort ?

[Kyle Miller]

lemma list_is_ordered (l : List Nat) :
    List.Sorted (· ≤ · ) (l.insertionSort (· ≤ ·)) := by
  apply List.sorted_insertionSort