Theorem: quickSortImpl_sortedRange
Proof state before:
α : Type
inst✝ : Order α
n : Nat
arr : Vec α n
first : Nat
last : Fin n
⊢ sortedRange (quickSortImpl arr first last) first ↑last
Tactic:
induction arr, first, last using quickSortImpl.induct' with
| base arr first last h =>
  simp [*]
  intro i j fi ij jl
  have : first = last := Nat.le_antisymm (Nat.le_trans (Nat.le_trans fi ij) jl) (Nat.le_of_not_gt h)
  subst this
  have : i = last := Fin.eq_of_val_eq (Nat.le_antisymm (Nat.le_trans ij jl) fi)
  subst this
  have : i = j := Fin.eq_of_val_eq (Nat.le_antisymm ij jl)
  subst this
  apply Order.refl
| step arr first last lt parted eq ih₁ ih₂ =>
  have : first < n := Nat.lt_trans lt last.isLt
  simp [*]
  intro i j fi ij jl
  let mid := parted.1
  have mn : mid.val < n := Nat.lt_of_le_of_lt mid.property.2 last.isLt
  let sorted := quickSortImpl (quickSortImpl parted.snd first mid.val.prev) (mid.val + 1) last
  let ⟨l, m, r⟩ := partition.partition arr ⟨first, by assumption⟩ last (Nat.le_of_lt lt) parted eq
  have getL (k : Fin n) (fk : first ≤ k) (km : k < mid.val) : sorted[k] <o arr[first] := by
    rw [quickSortImpl.get_lt (lt := (Nat.lt_trans km (Nat.lt_succ_self ..)))]
    let p := quickSortImpl_permuted parted.2 first mid.val.prev
    let ⟨k', ⟨index, fk', km'⟩⟩ := permuted_map_index_in_range_inv p k fk (Nat.le_sub_one_of_lt km)
    let inv := index ▸ permuted_map_index p k'
    rw [←inv]
    apply l k' fk' (Nat.lt_of_le_of_lt km' (Nat.sub_lt_self (by decide) (Nat.zero_lt_of_lt km)))
  have getM (k : Fin n) (eq : mid.val = k.val): sorted[k] = arr[first] := by
    let mid' : Fin n := ⟨mid.val, mn⟩
    have : k = mid' := by
      apply Fin.eq_of_val_eq
      simp [eq]
    subst this
    rw [quickSortImpl.get_lt (k := mid') (lt := Nat.lt_succ_self ..)]
    cases Nat.eq_zero_or_pos mid.val with
    | inl zero =>
      have zero : mid.val = Fin.mk 0 mid.val.pos := by
        apply Fin.eq_of_val_eq
        simp [zero]
      simp [zero] at *
      exact m
    | inr pos =>
      rw [quickSortImpl.get_gt (k := mid') (gt := Nat.sub_lt_self (by decide) (Nat.zero_lt_of_lt pos))]
      exact m
  have getR (k : Fin n) (mk : mid.val < k) (kl : k ≤ last) : ¬sorted[k] <o arr[first] := by
    let p := quickSortImpl_permuted (quickSortImpl parted.snd first mid.val.prev) (mid.val + 1) last
    let ⟨k', ⟨index, mk', kl'⟩⟩ := permuted_map_index_in_range_inv p k mk kl
    let inv := index ▸ permuted_map_index p k'
    rw [←inv]
    have : mid.val.prev.val ≤ mid.val := by
      simp
      exact (Nat.sub_le ..)
    rw [quickSortImpl.get_gt (gt := Nat.lt_of_le_of_lt this mk')]
    apply r k' mk' kl'
  have getLM (k : Fin n) (fk : first ≤ k) (km : k ≤ mid.val) : sorted[k] ≤o arr[first] := by
    cases Nat.eq_or_lt_of_le km with
    | inl km =>
      rw [getM k km.symm]
      apply Order.refl
    | inr km => exact Order.le_of_lt (getL k fk km)
  have getMR (k : Fin n) (mk : mid.val ≤ k) (kl : k ≤ last) : ¬sorted[k] <o arr[first] := by
    match Nat.eq_or_lt_of_le mk with
    | .inl mk =>
      rw [getM k mk]
      apply Order.irrefl
    | .inr mk => exact getR k mk kl
  cases Nat.range_split i j mid ij with
  | lt im jm =>
    rw [quickSortImpl.get_lt (lt := Nat.lt_trans im (Nat.lt_succ_self ..))]
    rw [quickSortImpl.get_lt (lt := Nat.lt_trans jm (Nat.lt_succ_self ..))]
    exact ih₁ i j fi ij (Nat.le_sub_of_add_le jm)
  | ge mi mj => exact ih₂ i j mi ij jl
  | split im mj =>
    have h₁ : sorted[i] ≤o arr[first] := getLM i fi im
    have h₂ : arr[first] ≤o sorted[j] := Order.le_of_not_lt (getMR j mj jl)
    apply Order.trans h₁ h₂
Proof state after:
no goals