Theorem: partitionImpl.loop_invariant
Proof state before:
α : Type
inst✝ : Ord α
n : Nat
arr : Vec α n
first i j last : Fin n
fi : first ≤ i
ij : i ≤ j
inv : LoopInvariant arr first i j last
result : { mid // first ≤ mid ∧ mid ≤ j } × Vec α n
eq : partitionImpl arr first i j fi ij = result
⊢ LoopInvariant result.snd first first ⟨↑result.fst.val, ⋯⟩ last
Tactic:
induction arr, first, i, j, fi, ij using partitionImpl.induct' with
| base arr first i j fi _ h =>
  revert result
  simp [*]
  have : i = first := Fin.eq_of_val_eq (Nat.le_antisymm (Nat.le_of_not_lt h) fi)
  exact this ▸ inv
| step_lt arr first i j _ _ fi _ lt _ ih =>
  have inv : LoopInvariant arr first i.prev j last := by
    apply LoopInvariant.intro
    . intro k ik kj
      have ik : i.val ≤ k.val := by
        rw [←Nat.sub_add_cancel (Nat.zero_lt_of_lt fi)]
        exact ik
      cases Nat.eq_or_lt_of_le ik with
      | inl ik =>
        simp [Fin.eq_of_val_eq ik] at lt
        exact lt
      | inr ik => exact inv.1 k ik kj
    . exact inv.2
    . intro ij
      have ij : i.val ≤ j.val := by
        rw [←Nat.sub_add_cancel (Nat.zero_lt_of_lt fi)]
        exact ij
      cases Nat.eq_or_lt_of_le ij with
      | inl ij =>
        simp [Fin.eq_of_val_eq ij.symm]
        assumption
      | inr ij => exact inv.3 ij
  simp [*] at eq
  apply ih inv result eq
| step_ge arr first i j _ ij fi _ _ _ ih =>
  let swapped := arr.swap i j
  have sf : swapped[first] = arr[first] := by
    apply Vec.get_swap_neq
    . apply Fin.ne_of_val_ne
      exact Nat.ne_of_lt fi
    . apply Fin.ne_of_val_ne
      exact Nat.ne_of_lt (Nat.lt_of_lt_of_le fi ij)
  let result := partitionImpl swapped first i.prev j.prev (by assumption) (by assumption)
  subst eq
  simp [*]
  have inv : LoopInvariant swapped first i.prev j.prev last := by
    apply LoopInvariant.intro
    . intro k ik kj
      have ik : i.val ≤ k.val := by
        rw [←Nat.sub_add_cancel (Nat.zero_lt_of_lt fi)]
        exact ik
      cases Nat.eq_or_lt_of_le ik with
      | inl ik =>
        have : swapped[k] = arr[j] := by
          simp [Fin.eq_of_val_eq ik.symm]
          apply Vec.get_swap_left
        rw [this, sf]
        exact inv.3 (Nat.lt_of_lt_of_le (Fin.eq_of_val_eq ik.symm ▸ kj) (Nat.sub_le ..))
      | inr ik =>
        have kj : k < j := (Nat.lt_of_lt_of_le kj (Nat.sub_le ..))
        have : swapped[k] = arr[k] := by
          apply Vec.get_swap_neq
          . apply Fin.ne_of_val_ne
            exact Nat.ne_of_gt ik
          . apply Fin.ne_of_val_ne
            exact Nat.ne_of_lt kj
        rw [this, sf]
        exact inv.1 k ik kj
    . intro k jk kl
      have jk : j.val ≤ k.val := by
        rw [←Nat.sub_add_cancel (Nat.zero_lt_of_lt (Nat.zero_lt_of_lt (Nat.lt_of_lt_of_le fi ij)))]
        exact jk
      cases Nat.eq_or_lt_of_le jk with
      | inl jk =>
        have : swapped[k] = arr[i] := by
          simp [Fin.eq_of_val_eq jk.symm]
          apply Vec.get_swap_right
        rw [this, sf]
        assumption
      | inr jk =>
        have : swapped[k] = arr[k] := by
          apply Vec.get_swap_neq
          . apply Fin.ne_of_val_ne
            exact Nat.ne_of_gt (Nat.lt_of_le_of_lt ij jk)
          . apply Fin.ne_of_val_ne
            exact Nat.ne_of_gt jk
        rw [this, sf]
        exact inv.2 k jk kl
    . intro ij
      have : j.val - 1 < j.val := by
        show j.val - 1 + 1 ≤ j.val
        rw [Nat.sub_add_cancel (Nat.zero_lt_of_lt (Nat.lt_of_lt_of_le fi (by assumption)))]
        apply Nat.le_refl
      have ij : i.val ≤ j.val - 1 := by
        rw [←Nat.sub_add_cancel (Nat.zero_lt_of_lt fi)]
        exact ij
      cases Nat.eq_or_lt_of_le ij with
      | inl ij =>
        have : swapped[j.prev] = arr[j] := by
          simp [ij.symm, Fin.prev]
          apply Vec.get_swap_left
        rw [this, sf]
        have : i < j := Nat.lt_of_le_of_lt (by assumption : i.val ≤ j.val - 1) (by assumption)
        exact inv.3 this
      | inr ij =>
        have : swapped[j.prev] = arr[j.prev] := by
          apply Vec.get_swap_neq
          . apply Fin.ne_of_val_ne
            exact Nat.ne_of_gt ij
          . apply Fin.ne_of_val_ne
            exact Nat.ne_of_lt (by assumption)
        rw [this, sf]
        apply inv.1 j.prev ij (by assumption)
  exact ih inv result (by rfl)
Proof state after:
no goals