prove list monotonic for known list

Stream: new members

[Quinn]

I can't seem to leverage known information about xs to accomplish this proof. What syntax would I use to just exhaustively go through each element?

def xs := [0, 1, 2, 10]

theorem nonDecreasing : forall i j (H0 : j < xs.length) (H1 : i < j),  xs[i] <= xs[j] := by
  intros i j H0 H1;
  -- stuck

I tried some induction approaches

[Will Crichton]

simp seems to be able to do this automatically if you use List.Pairwise.

import Mathlib.Data.List.Basic

def xs := [0, 1, 2, 10]

set_option trace.Meta.Tactic.simp.rewrite true

theorem nonDecreasing : List.Pairwise (· ≤ ·) xs := by simp [xs]

You can check out the trace to see what steps it uses.

[Quinn]

thanks! I'm trying to do this in a lightwegiht project that doens't have mathlib installed, though

[Bolton Bailey]

You don't actually need mathlib I think, just Batteries

import Batteries.Data.List.Basic

def xs := [0, 1, 2, 10]

set_option trace.Meta.Tactic.simp.rewrite true

theorem nonDecreasing : List.Pairwise (· ≤ ·) xs := by simp [xs]

All it's doing is evaluation of the definition of the Pairwise function, which seems like the more idiomatic way to state this theorem anyway.

[Quinn]

Cool. Is batteries an external dep? I couldn't find it when I googled, but I don't remember seeing anything like that when I grepped around lean4 source a few weeks ago

[Bolton Bailey]

Do you need the full O(n^2) comparisons here or just that adjacent elements are ordered? List.Chain might be good too if you have a long list.

[Bolton Bailey]

Quinn said:

Cool. Is batteries an external dep? I couldn't find it when I googled, but I don't remember seeing anything like that when I grepped around lean4 source a few weeks ago

As of a few days ago, Batteries is the new name of Std

[Quinn]

List.chain should be fine!