proving about `Rco`

Stream: Is there code for X?

[Asei Inoue]

how to show this?

theorem lem (n : Nat) : (0...n).toList = List.range n := by
  sorry

[Asei Inoue]

Background: I want to construct a proof by using mvcgen and my function is based on Rco

[Ruben Van de Velde]

Obviously (obviously) like this:

theorem lem (n : Nat) : (0...n).toList = List.range n := by
  induction n with
  | zero => simp only [Std.Rco.toList_eq_if, Nat.lt_irrefl, ↓reduceIte, List.range_zero]
  | succ n ih =>
    simp only [Std.Rco.toList_eq_if, Nat.zero_lt_succ, ↓reduceIte, List.range_succ_eq_map,
      List.cons.injEq, true_and]
    rw [← ih]
    rw [← Std.PRange.Nat.toList_Rco_succ_succ]
    simp only [Nat.zero_add]
    rw [Std.toList_Roo_eq_toList_Rco_of_isSome_succ? Std.PRange.isSome_succ?]
    simp [Std.PRange.Nat.succ_eq]

[Ruben Van de Velde]

I conclude there is significant missing API

[Paul Reichert]

How does the function (or for...in construct) look on which you applied mvcgen?

[Asei Inoue]

(deleted)

[Asei Inoue]

here is my code

import Lean
import Batteries

open Std Do

variable {α : Type} [LE α] [LT α]
variable [DecidableLE α] [DecidableLT α]
variable [IsLinearOrder α] [LawfulOrderLT α]

def Array.isSorted (l : Array α) : Bool := Id.run do
  let n := l.size
  for h : i in (0...n-1) do
    if l[i] > l[i + 1] then
      return false
  return true

set_option mvcgen.warning false

theorem Array.isSorted_spec (l : Array α) :
    l.isSorted ↔ l.Pairwise (· ≤ ·) := by
  generalize h : l.isSorted = r
  apply Id.of_wp_run_eq h
  mvcgen invariants
  · Invariant.withEarlyReturn
      (onContinue := fun cursor _ => ⌜l.take (cursor.pos + 1) |>.Pairwise (· ≤ ·)⌝)
      (onReturn := fun ret _ => ⌜ret = false ∧ ¬ l.Pairwise (· ≤ ·)⌝)

  case vc1 =>
    sorry

  all_goals sorry

[Paul Reichert]

Thanks! I am working on adding the lemmas for the new ranges and slices to the API until the end of this year. Proving things about range-based loops will get more comfortable, but for now, Ruben Van de Velde's lemma is probably the best way for you to deal with this.

[Ruben Van de Velde]

Shorter:

@[simp]
theorem aux0 (n k : Nat) : Std.PRange.succMany? n k = k + n := by
  simp [Std.PRange.succMany?]

theorem aux6 (m n i : Nat) : (m...n).toList[i]? = if i < n - m then some (m + i) else none := by
  simp [Std.Rco.getElem?_toList_eq]
  grind

theorem lem (n : Nat) : (0...n).toList = List.range n := by
  ext i x
  rw [aux6]
  grind [List.getElem?_range]

[Ruben Van de Velde]

More code if you're interested

attribute [simp] Std.PRange.Nat.succ_eq Std.Rco.length_toList Std.Roo.length_toList

@[simp]
theorem aux0 (n k : Nat) : Std.PRange.succMany? n k = k + n := by
  simp [Std.PRange.succMany?]

@[simp]
theorem aux1 (n : Nat) : (n...0).toList = [] := by
  simp [Std.Rco.toList_eq_if]

@[simp]
theorem aux2 (n : Nat) : (n<...0).toList = [] := by
  rw [Std.toList_Roo_eq_toList_Rco_of_isSome_succ? Std.PRange.isSome_succ?]
  simp

@[simp]
theorem aux5 (n i : Nat) : (0...n).toList[i]? = if i < n then some i else none := by
  simp [Std.Rco.getElem?_toList_eq, *]
  grind

@[simp]
theorem aux8 (n i : Nat) : (0<...n).toList[i]? = if i < n - 1 then some (i + 1) else none := by
  simp [Std.Roo.getElem?_toList_eq, *]
  grind

@[simp]
theorem aux6 (m n i : Nat) : (m...n).toList[i]? = if i < n - m then some (m + i) else none := by
  simp [Std.Rco.getElem?_toList_eq, *]
  grind

@[simp]
theorem aux7 (n : Nat) : (0...n + 1).toList = (0...n).toList ++ [n] := by
  ext i x
  simp [List.getElem?_append]
  grind

@[simp]
theorem aux9 (m n : Nat) : (m<...n).toList = ((m + 1)...n).toList := by
  rw [Std.toList_Roo_eq_toList_Rco_of_isSome_succ? rfl]
  simp

@[simp]
theorem aux10 (n : Nat) (hn : 0 < n) : (0<...n + 1).toList = (0<...n).toList ++ [n] := by
  rw [Std.toList_Roo_eq_toList_Rco_of_isSome_succ? Std.PRange.isSome_succ?]
  simp only [Std.PRange.Nat.succ_eq]
  simp only [← Std.PRange.Nat.succ_eq]
  rw [Std.Rco.toList_succ_succ_eq_map]
  ext i x
  simp [List.getElem?_append, List.getElem?_singleton]
  grind

theorem aux11 (m n : Nat) : ((m + 1)...(n + 1)).toList = (m...n).toList.map (· + 1) := by
  simp [← Std.PRange.Nat.succ_eq]
  rw [Std.Rco.toList_succ_succ_eq_map]

theorem aux14 (m n : Nat) : ((m + 1)<...(n + 1)).toList = (m<...n).toList.map (· + 1) := by
  simp [← Std.PRange.Nat.succ_eq]
  rw [Std.Rco.toList_succ_succ_eq_map]

@[simp]
theorem aux4 (m n : Nat) (h : m ≤ n) : (m...n + 1).toList = (m...n).toList ++ [n] := by
  induction m generalizing n with
  | zero => simp
  | succ m ih =>
    have hmn := Nat.sub_add_cancel (m := 1) (n := n) (by grind)
    simp [aux11]
    have := ih (n - 1) (by grind)
    rw [hmn] at this
    rw [this]
    simp [hmn]
    rw [← aux11, hmn]

@[simp]
theorem aux12 (n : Nat) : (n...n).toList = [] := by
  rw [@Std.Rco.toList_eq_nil_iff]
  simp

@[simp]
theorem aux13 (n : Nat) : (n<...n).toList = [] := by
  rw [@Std.Roo.toList_eq_nil_iff]
  simp [Std.PRange.succ?]

@[simp]
theorem aux3 (m n : Nat) (h : m < n) : (m<...n + 1).toList = (m<...n).toList ++ [n] := by
  rw [aux9, aux4, aux9]
  grind

theorem lem (n : Nat) : (0...n).toList = List.range n := by
  ext i x
  rw [aux6]
  grind [List.getElem?_range]

[Asei Inoue]

I want to construct a proof by using mvcgen and my function is based on Rco

I have done! Thank you!!

import Std.Tactic.Do
import Batteries.Data.Array

open Std

variable {α : Type} [LT α] [DecidableLT α]

def Array.isSorted (arr : Array α) : Bool := Id.run do
  let n := arr.size
  for h : i in (0...n-1) do
    if arr[i] > arr[i + 1] then
      return false
  return true

open Std.Do
set_option mvcgen.warning false

namespace Std

  @[simp]
  theorem PRange.succMany?_spec (n k : Nat) : PRange.succMany? n k = k + n := by
    simp [PRange.succMany?]

  theorem Rco.toList_getElem? (m n i : Nat)
      : (m...n).toList[i]? = if i < n - m then some (m + i) else none := by
    simp [Rco.getElem?_toList_eq]
    grind

  @[simp]
  theorem Rco.toList_eq {n : Nat} : (0...n).toList = List.range n := by
    ext i x
    rw [Rco.toList_getElem?]
    grind [List.getElem?_range]

  @[simp]
  theorem Range.toList_eq {n : Nat} : [0:n].toList = List.range n := by
    ext i x
    grind

  @[grind =]
  theorem Rco_eq_Range_of_toList {n : Nat} : (0...n).toList = [0:n].toList := by
    simp

end Std

@[grind <=]
theorem Array.not_pairwise_of_succ_pair {α : Type} (arr : Array α) {R : α → α → Prop} (i : Nat)
  (hi : i + 1 < arr.size) (h : ¬ R arr[i] arr[i + 1])
    : ¬Pairwise R arr := by
  simp [Array.pairwise_iff_getElem]
  grind

@[grind <=]
theorem Array.sorted_take_cons_cons {α : Type} [LE α] [IsPreorder α] (arr : Array α)
  (i : Nat) (hi : i + 1 < arr.size) (harr : arr[i] ≤ arr[i + 1])
  (h : Pairwise (· ≤ ·) (arr.take (i + 1)))
    : Pairwise (· ≤ ·) (arr.take (i + 1 + 1)) := by
  simp [Array.pairwise_iff_getElem] at *
  grind

@[grind <=]
theorem Array.pairwise_subsingleton {α : Type} {R : α → α → Prop} {arr : Array α}
  (h : arr.size ≤ 1) : Pairwise R arr := by
  simp [Array.pairwise_iff_getElem] at *
  grind

@[grind =]
theorem Array.Grind.extract_all {α : Type} (arr : Array α) (n : Nat) (h : n = arr.size)
    : arr.extract 0 n = arr := by
  grind

variable [LE α] [IsLinearOrder α] [LawfulOrderLT α]

theorem Array.isSorted_spec (arr : Array α) :
    arr.isSorted = true ↔ arr.Pairwise (· ≤ ·) := by
  generalize h : arr.isSorted = r
  apply Id.of_wp_run_eq h

  mvcgen invariants
  · Invariant.withEarlyReturn
    (onContinue := fun cursor _ => ⌜arr.take (cursor.pos + 1) |>.Pairwise (· ≤ ·)⌝)
    (onReturn := fun ret _ => ⌜ret = false ∧ ¬ arr.Pairwise (· ≤ ·)⌝)
  with (simp at *; grind)

[Paul Reichert]

lean#11321 #11321 is going to add a lot of lemmas about Std.Rco specialized to Nat. It also adds a lemma List.range_eq_toList_rco that does what you were asking for, but the API support for Rco is better than for List.range with this PR, so you hopefully won't need to rewrite to List.range anymore.

[Asei Inoue]

you mean lean4#11321?

[Paul Reichert]

Yes, that's the one I meant. Thanks.