how to fill this `sorry`?

Stream: general

[Asei Inoue]

import Batteries

open Std

@[grind <=]
theorem Array.sorted_take_swap {α : Type} [LE α] [IsPreorder α] {arr : Array α}
  (s t : Nat) (hs : s < arr.size) (ht : t < arr.size)
  (h : Array.Pairwise (· ≤ ·) (arr.take s))
  (le1 : arr[s] ≤ arr[t])
  (le2 : ∀ (i : Nat) (_ : i < t), arr[i] ≤ arr[s])
    : Array.Pairwise (· ≤ ·) ((arr.swap s t).take s) := by
  simp [Array.pairwise_iff_getElem] at h ⊢
  grind

@[grind <=]
theorem Array.pairwise_take_swap {α : Type} {R : α → α → Prop} [Refl R] [Trans R R R] {arr : Array α}
  (s t : Nat) (hs : s < arr.size) (ht : t < arr.size)
  (h : Array.Pairwise R (arr.take s))
  (le1 : R arr[s] arr[t])
  (le2 : ∀ (i : Nat) (_ : i < t), R arr[i] arr[s])
    : Array.Pairwise R ((arr.swap s t).take s) := by
  simp [Array.pairwise_iff_getElem] at h ⊢
  sorry

[Asei Inoue]

Background

I'm refactoring the grind lemmas.
Some of them assume stronger conditions than necessary, so I'd like to refactor the theorems so that they work with the minimal required assumptions.
Since Array.sorted_take_swap is already proved, I believe Array.pairwise_take_swap should be provable as well.

[Aaron Liu]

Can you make a #mwe?

[Asei Inoue]

removed

[Asei Inoue]

@Aaron Liu sorry, I have fixed the code

[Aaron Liu]

import Batteries

open Std

@[grind <=]
theorem Array.sorted_take_swap {α : Type} [LE α] [IsPreorder α] {arr : Array α}
  (s t : Nat) (hs : s < arr.size) (ht : t < arr.size)
  (h : Array.Pairwise (· ≤ ·) (arr.take s))
  (le1 : arr[s] ≤ arr[t])
  (le2 : ∀ (i : Nat) (_ : i < t), arr[i] ≤ arr[s])
    : Array.Pairwise (· ≤ ·) ((arr.swap s t).take s) := by
  simp [Array.pairwise_iff_getElem] at h ⊢
  grind

@[grind <=]
theorem Array.pairwise_take_swap {α : Type} {R : α → α → Prop} [Refl R] [Trans R R R] {arr : Array α}
  (s t : Nat) (hs : s < arr.size) (ht : t < arr.size)
  (h : Array.Pairwise R (arr.take s))
  (le1 : R arr[s] arr[t])
  (le2 : ∀ (i : Nat) (_ : i < t), R arr[i] arr[s])
    : Array.Pairwise R ((arr.swap s t).take s) :=
  @Array.sorted_take_swap α ⟨R⟩ (@IsPreorder.mk α ⟨R⟩ Refl.refl (@Trans.trans α α α R R R _))
    arr s t hs ht h le1 le2

[Asei Inoue]

Thank you but IsPreorder.mk is needed?

[Aaron Liu]

is this better?

import Batteries

open Std

@[grind <=]
theorem Array.sorted_take_swap {α : Type} [LE α] [IsPreorder α] {arr : Array α}
  (s t : Nat) (hs : s < arr.size) (ht : t < arr.size)
  (h : Array.Pairwise (· ≤ ·) (arr.take s))
  (le1 : arr[s] ≤ arr[t])
  (le2 : ∀ (i : Nat) (_ : i < t), arr[i] ≤ arr[s])
    : Array.Pairwise (· ≤ ·) ((arr.swap s t).take s) := by
  simp [Array.pairwise_iff_getElem] at h ⊢
  grind

@[grind <=]
theorem Array.pairwise_take_swap {α : Type} {R : α → α → Prop} [Refl R] [Trans R R R] {arr : Array α}
  (s t : Nat) (hs : s < arr.size) (ht : t < arr.size)
  (h : Array.Pairwise R (arr.take s))
  (le1 : R arr[s] arr[t])
  (le2 : ∀ (i : Nat) (_ : i < t), R arr[i] arr[s])
    : Array.Pairwise R ((arr.swap s t).take s) :=
  let : LE α := {
    le := R
  }
  have : IsPreorder α := {
    le_refl := Refl.refl
    le_trans _ _ _ := trans
  }
  Array.sorted_take_swap s t hs ht h le1 le2

[Asei Inoue]

oh sorry
I wanted to say "a proof without Array.sorted_take_swap is better"

[Aaron Liu]

import Batteries

open Std

@[grind <=]
theorem Array.pairwise_take_swap {α : Type} {R : α → α → Prop} [Refl R] [Trans R R R] {arr : Array α}
  (s t : Nat) (hs : s < arr.size) (ht : t < arr.size)
  (h : Array.Pairwise R (arr.take s))
  (le1 : R arr[s] arr[t])
  (le2 : ∀ (i : Nat) (_ : i < t), R arr[i] arr[s])
    : Array.Pairwise R ((arr.swap s t).take s) := by
  obtain ⟨_, _, rfl⟩ : ∃ o : LE α, IsPreorder α ∧ R = o.le :=
    ⟨⟨R⟩, @IsPreorder.mk α ⟨R⟩ (Refl.refl) (@Trans.trans α α α R R R _), rfl⟩
  simp [Array.pairwise_iff_getElem] at h ⊢
  grind

[Asei Inoue]

oh... grind can only treat IsPreorder? grind does not treat Refl, Trans?

[Aaron Liu]

I guess not :shrug:

[Asei Inoue]

@Aaron Liu Thank you anyway