Theorem: partitionImpl_permuted (QuickSortInLean/QuickSortPermutation.lean)

State before:
α : Type
inst✝ : Ord α
n : Nat
arr : Vec α n
first i j : Fin n
fi : first ≤ i
ij : i ≤ j
⊢ Nonempty (permuted n (↑first) (↑j) arr (partitionImpl arr first i j fi ij).snd)
Tactic:
induction arr, first, i, j, fi, ij using partitionImpl.induct with
| case1 arr first i j fi ij lt jl h prev ih =>
  unfold partitionImpl
  simp [*]
| @case2 arr first i j fi ij lt jl h swapped mid hm arr' eq ih =>
  unfold partitionImpl
  simp [*] at *
  have ⟨p₂⟩ := ih
  have p₁ : permuted n first j arr swapped := .step i j fi ij (Nat.le_refl _) .refl
  exact ⟨p₁.trans $ p₂.cast_last (Nat.sub_le ..)⟩
| case3 arr first i j fi ij jn =>
  simp [partitionImpl, *]
  exact ⟨.refl⟩
State after:
no goals

State before:
case case1
α : Type
inst✝ : Ord α
n : Nat
first✝ i✝ j✝ : Fin n
arr : Vec α n
first i j : Fin n
fi : first ≤ i
ij : i ≤ j
lt : first < i
jl : ↑first ≤ ↑i - 1
h : arr[i] < arr[first]
prev : ↑i - 1 ≤ ↑j
ih : Nonempty (permuted n (↑first) (↑j) arr (partitionImpl arr first i.prev j jl prev).snd)
⊢ Nonempty (permuted n (↑first) (↑j) arr (partitionImpl arr first i j fi ij).snd)
Tactic:
unfold partitionImpl
State after:
case case1
α : Type
inst✝ : Ord α
n : Nat
first✝ i✝ j✝ : Fin n
arr : Vec α n
first i j : Fin n
fi : first ≤ i
ij : i ≤ j
lt : first < i
jl : ↑first ≤ ↑i - 1
h : arr[i] < arr[first]
prev : ↑i - 1 ≤ ↑j
ih : Nonempty (permuted n (↑first) (↑j) arr (partitionImpl arr first i.prev j jl prev).snd)
⊢ Nonempty
    (permuted n (↑first) (↑j) arr
      (if h : first < i then
          let_fun this := ⋯;
          if arr[i] < arr[first] then
            let_fun this_1 := ⋯;
            partitionImpl arr first i.prev j this this_1
          else
            let arr := (dbgTraceIfShared "swap1" arr).swap i j;
            match partitionImpl arr first i.prev j.prev this ⋯ with
            | (⟨mid, hm⟩, arr) => (⟨mid, ⋯⟩, arr)
        else (⟨j, ⋯⟩, arr)).snd)

State before:
case case1
α : Type
inst✝ : Ord α
n : Nat
first✝ i✝ j✝ : Fin n
arr : Vec α n
first i j : Fin n
fi : first ≤ i
ij : i ≤ j
lt : first < i
jl : ↑first ≤ ↑i - 1
h : arr[i] < arr[first]
prev : ↑i - 1 ≤ ↑j
ih : Nonempty (permuted n (↑first) (↑j) arr (partitionImpl arr first i.prev j jl prev).snd)
⊢ Nonempty
    (permuted n (↑first) (↑j) arr
      (if h : first < i then
          let_fun this := ⋯;
          if arr[i] < arr[first] then
            let_fun this_1 := ⋯;
            partitionImpl arr first i.prev j this this_1
          else
            let arr := (dbgTraceIfShared "swap1" arr).swap i j;
            match partitionImpl arr first i.prev j.prev this ⋯ with
            | (⟨mid, hm⟩, arr) => (⟨mid, ⋯⟩, arr)
        else (⟨j, ⋯⟩, arr)).snd)
Tactic:
simp [*]
State after:
no goals

State before:
case case2
α : Type
inst✝ : Ord α
n : Nat
first✝ i✝ j✝ : Fin n
arr : Vec α n
first i j : Fin n
fi : first ≤ i
ij : i ≤ j
lt : first < i
jl : ↑first ≤ ↑i - 1
h : ¬arr[i] < arr[first]
swapped : Vec α n := (dbgTraceIfShared "swap1" arr).swap i j
mid : Fin n
hm : first ≤ mid ∧ mid ≤ j.prev
arr' : Vec α n
eq : partitionImpl swapped first i.prev j.prev jl ⋯ = (⟨mid, hm⟩, arr')
ih : Nonempty (permuted n (↑first) (↑j.prev) swapped (partitionImpl swapped first i.prev j.prev jl ⋯).snd)
⊢ Nonempty (permuted n (↑first) (↑j) arr (partitionImpl arr first i j fi ij).snd)
Tactic:
unfold partitionImpl
State after:
case case2
α : Type
inst✝ : Ord α
n : Nat
first✝ i✝ j✝ : Fin n
arr : Vec α n
first i j : Fin n
fi : first ≤ i
ij : i ≤ j
lt : first < i
jl : ↑first ≤ ↑i - 1
h : ¬arr[i] < arr[first]
swapped : Vec α n := (dbgTraceIfShared "swap1" arr).swap i j
mid : Fin n
hm : first ≤ mid ∧ mid ≤ j.prev
arr' : Vec α n
eq : partitionImpl swapped first i.prev j.prev jl ⋯ = (⟨mid, hm⟩, arr')
ih : Nonempty (permuted n (↑first) (↑j.prev) swapped (partitionImpl swapped first i.prev j.prev jl ⋯).snd)
⊢ Nonempty
    (permuted n (↑first) (↑j) arr
      (if h : first < i then
          let_fun this := ⋯;
          if arr[i] < arr[first] then
            let_fun this_1 := ⋯;
            partitionImpl arr first i.prev j this this_1
          else
            let arr := (dbgTraceIfShared "swap1" arr).swap i j;
            match partitionImpl arr first i.prev j.prev this ⋯ with
            | (⟨mid, hm⟩, arr) => (⟨mid, ⋯⟩, arr)
        else (⟨j, ⋯⟩, arr)).snd)

State before:
case case2
α : Type
inst✝ : Ord α
n : Nat
first✝ i✝ j✝ : Fin n
arr : Vec α n
first i j : Fin n
fi : first ≤ i
ij : i ≤ j
lt : first < i
jl : ↑first ≤ ↑i - 1
h : ¬arr[i] < arr[first]
swapped : Vec α n := (dbgTraceIfShared "swap1" arr).swap i j
mid : Fin n
hm : first ≤ mid ∧ mid ≤ j.prev
arr' : Vec α n
eq : partitionImpl swapped first i.prev j.prev jl ⋯ = (⟨mid, hm⟩, arr')
ih : Nonempty (permuted n (↑first) (↑j.prev) swapped (partitionImpl swapped first i.prev j.prev jl ⋯).snd)
⊢ Nonempty
    (permuted n (↑first) (↑j) arr
      (if h : first < i then
          let_fun this := ⋯;
          if arr[i] < arr[first] then
            let_fun this_1 := ⋯;
            partitionImpl arr first i.prev j this this_1
          else
            let arr := (dbgTraceIfShared "swap1" arr).swap i j;
            match partitionImpl arr first i.prev j.prev this ⋯ with
            | (⟨mid, hm⟩, arr) => (⟨mid, ⋯⟩, arr)
        else (⟨j, ⋯⟩, arr)).snd)
Tactic:
simp [*] at *
State after:
case case2
α : Type
inst✝ : Ord α
n : Nat
first✝ i✝ j✝ : Fin n
arr : Vec α n
first i j : Fin n
fi : first ≤ i
ij : i ≤ j
lt : first < i
jl : ↑first ≤ ↑i - 1
h : ¬arr[i] < arr[first]
swapped : Vec α n := (dbgTraceIfShared "swap1" arr).swap i j
mid : Fin n
hm : first ≤ mid ∧ mid ≤ j.prev
arr' : Vec α n
eq : partitionImpl swapped first i.prev j.prev jl ⋯ = (⟨mid, hm⟩, arr')
ih : Nonempty (permuted n (↑first) (↑j - 1) swapped arr')
⊢ Nonempty (permuted n (↑first) (↑j) arr arr')

State before:
case case2
α : Type
inst✝ : Ord α
n : Nat
first✝ i✝ j✝ : Fin n
arr : Vec α n
first i j : Fin n
fi : first ≤ i
ij : i ≤ j
lt : first < i
jl : ↑first ≤ ↑i - 1
h : ¬arr[i] < arr[first]
swapped : Vec α n := (dbgTraceIfShared "swap1" arr).swap i j
mid : Fin n
hm : first ≤ mid ∧ mid ≤ j.prev
arr' : Vec α n
eq : partitionImpl swapped first i.prev j.prev jl ⋯ = (⟨mid, hm⟩, arr')
ih : Nonempty (permuted n (↑first) (↑j - 1) swapped arr')
⊢ Nonempty (permuted n (↑first) (↑j) arr arr')
Tactic:
have ⟨p₂⟩ := ih
State after:
case case2
α : Type
inst✝ : Ord α
n : Nat
first✝ i✝ j✝ : Fin n
arr : Vec α n
first i j : Fin n
fi : first ≤ i
ij : i ≤ j
lt : first < i
jl : ↑first ≤ ↑i - 1
h : ¬arr[i] < arr[first]
swapped : Vec α n := (dbgTraceIfShared "swap1" arr).swap i j
mid : Fin n
hm : first ≤ mid ∧ mid ≤ j.prev
arr' : Vec α n
eq : partitionImpl swapped first i.prev j.prev jl ⋯ = (⟨mid, hm⟩, arr')
ih : Nonempty (permuted n (↑first) (↑j - 1) swapped arr')
p₂ : permuted n (↑first) (↑j - 1) swapped arr'
⊢ Nonempty (permuted n (↑first) (↑j) arr arr')

State before:
case case2
α : Type
inst✝ : Ord α
n : Nat
first✝ i✝ j✝ : Fin n
arr : Vec α n
first i j : Fin n
fi : first ≤ i
ij : i ≤ j
lt : first < i
jl : ↑first ≤ ↑i - 1
h : ¬arr[i] < arr[first]
swapped : Vec α n := (dbgTraceIfShared "swap1" arr).swap i j
mid : Fin n
hm : first ≤ mid ∧ mid ≤ j.prev
arr' : Vec α n
eq : partitionImpl swapped first i.prev j.prev jl ⋯ = (⟨mid, hm⟩, arr')
ih : Nonempty (permuted n (↑first) (↑j - 1) swapped arr')
p₂ : permuted n (↑first) (↑j - 1) swapped arr'
⊢ Nonempty (permuted n (↑first) (↑j) arr arr')
Tactic:
have p₁ : permuted n first j arr swapped := .step i j fi ij (Nat.le_refl _) .refl
State after:
case case2
α : Type
inst✝ : Ord α
n : Nat
first✝ i✝ j✝ : Fin n
arr : Vec α n
first i j : Fin n
fi : first ≤ i
ij : i ≤ j
lt : first < i
jl : ↑first ≤ ↑i - 1
h : ¬arr[i] < arr[first]
swapped : Vec α n := (dbgTraceIfShared "swap1" arr).swap i j
mid : Fin n
hm : first ≤ mid ∧ mid ≤ j.prev
arr' : Vec α n
eq : partitionImpl swapped first i.prev j.prev jl ⋯ = (⟨mid, hm⟩, arr')
ih : Nonempty (permuted n (↑first) (↑j - 1) swapped arr')
p₂ : permuted n (↑first) (↑j - 1) swapped arr'
p₁ : permuted n (↑first) (↑j) arr swapped
⊢ Nonempty (permuted n (↑first) (↑j) arr arr')

State before:
case case2
α : Type
inst✝ : Ord α
n : Nat
first✝ i✝ j✝ : Fin n
arr : Vec α n
first i j : Fin n
fi : first ≤ i
ij : i ≤ j
lt : first < i
jl : ↑first ≤ ↑i - 1
h : ¬arr[i] < arr[first]
swapped : Vec α n := (dbgTraceIfShared "swap1" arr).swap i j
mid : Fin n
hm : first ≤ mid ∧ mid ≤ j.prev
arr' : Vec α n
eq : partitionImpl swapped first i.prev j.prev jl ⋯ = (⟨mid, hm⟩, arr')
ih : Nonempty (permuted n (↑first) (↑j - 1) swapped arr')
p₂ : permuted n (↑first) (↑j - 1) swapped arr'
p₁ : permuted n (↑first) (↑j) arr swapped
⊢ Nonempty (permuted n (↑first) (↑j) arr arr')
Tactic:
exact ⟨p₁.trans $ p₂.cast_last (Nat.sub_le ..)⟩
State after:
no goals

State before:
case case3
α : Type
inst✝ : Ord α
n : Nat
first✝ i✝ j✝ : Fin n
arr : Vec α n
first i j : Fin n
fi : first ≤ i
ij : i ≤ j
jn : ¬first < i
⊢ Nonempty (permuted n (↑first) (↑j) arr (partitionImpl arr first i j fi ij).snd)
Tactic:
simp [partitionImpl, *]
State after:
case case3
α : Type
inst✝ : Ord α
n : Nat
first✝ i✝ j✝ : Fin n
arr : Vec α n
first i j : Fin n
fi : first ≤ i
ij : i ≤ j
jn : ¬first < i
⊢ Nonempty (permuted n (↑first) (↑j) arr arr)

State before:
case case3
α : Type
inst✝ : Ord α
n : Nat
first✝ i✝ j✝ : Fin n
arr : Vec α n
first i j : Fin n
fi : first ≤ i
ij : i ≤ j
jn : ¬first < i
⊢ Nonempty (permuted n (↑first) (↑j) arr arr)
Tactic:
exact ⟨.refl⟩
State after:
no goals