internlm/Lean-Github huggingface dataset:
Theorem: permuted_map_index_in_range_inv
Proof state before:
n first last : Nat
α✝ : Type
arr1 arr2 arr✝ arr'✝ : Vec α✝ n
i j : Fin n
fi : first ≤ ↑i
ij : i ≤ j
jl : ↑j ≤ last
p : permuted n first last (arr✝.swap i j) arr'✝
ih : ∀ (k : Fin n), first ≤ ↑k → ↑k ≤ last → ∃ k', p.to_map k' = k ∧ first ≤ ↑k' ∧ ↑k' ≤ last
k : Fin n
fk : first ≤ ↑k
kl : ↑k ≤ last
k' : Fin n
index : p.to_map k' = k
fk' : first ≤ ↑k'
kl' : ↑k' ≤ last
k'' : Fin n := if k' = i then j else if k' = j then i else k'
this : (if k'' = i then j else if k'' = j then i else k'') = k'
ki : ¬k' = i
kj : ¬k' = j
⊢ first ≤ ↑k' ∧ ↑k' ≤ last
Tactic:
exact ⟨fk', kl'⟩
Proof state after:
no goals
Theorem: permuted.get_lt
Proof state before:
n first last : Nat
α✝ : Type
arr1 arr2 : Vec α✝ n
p : permuted n first last arr1 arr2
k : Fin n
lt : ↑k < first
⊢ arr2[k] = arr1[k]
Tactic:
induction p with
| refl => rfl
| step i j fi ij jl p ih =>
  rw [ih]
  rw [Vec.get_swap_neq _ i j k]
  . apply Fin.ne_of_val_ne
    exact Nat.ne_of_lt (Nat.lt_of_lt_of_le lt fi)
  . apply Fin.ne_of_val_ne
    exact Nat.ne_of_lt (Nat.lt_of_lt_of_le lt (Nat.le_trans fi ij))
Proof state after:
no goals
Theorem: permuted.get_lt
Proof state before:
case refl
n first last : Nat
α✝ : Type
arr1 arr2 : Vec α✝ n
k : Fin n
lt : ↑k < first
arr✝ : Vec α✝ n
⊢ arr✝[k] = arr✝[k]
Tactic:
rfl
Proof state after:
no goals
Theorem: permuted.get_lt
Proof state before:
case step
n first last : Nat
α✝ : Type
arr1 arr2 : Vec α✝ n
k : Fin n
lt : ↑k < first
arr✝ arr'✝ : Vec α✝ n
i j : Fin n
fi : first ≤ ↑i
ij : i ≤ j
jl : ↑j ≤ last
p : permuted n first last (arr✝.swap i j) arr'✝
ih : arr'✝[k] = (arr✝.swap i j)[k]
⊢ arr'✝[k] = arr✝[k]
Tactic:
rw [ih]
Proof state after:
case step
n first last : Nat
α✝ : Type
arr1 arr2 : Vec α✝ n
k : Fin n
lt : ↑k < first
arr✝ arr'✝ : Vec α✝ n
i j : Fin n
fi : first ≤ ↑i
ij : i ≤ j
jl : ↑j ≤ last
p : permuted n first last (arr✝.swap i j) arr'✝
ih : arr'✝[k] = (arr✝.swap i j)[k]
⊢ (arr✝.swap i j)[k] = arr✝[k]
Theorem: permuted.get_lt
Proof state before:
case step
n first last : Nat
α✝ : Type
arr1 arr2 : Vec α✝ n
k : Fin n
lt : ↑k < first
arr✝ arr'✝ : Vec α✝ n
i j : Fin n
fi : first ≤ ↑i
ij : i ≤ j
jl : ↑j ≤ last
p : permuted n first last (arr✝.swap i j) arr'✝
ih : arr'✝[k] = (arr✝.swap i j)[k]
⊢ (arr✝.swap i j)[k] = arr✝[k]
Tactic:
rw [Vec.get_swap_neq _ i j k]
Proof state after:
case step.ki
n first last : Nat
α✝ : Type
arr1 arr2 : Vec α✝ n
k : Fin n
lt : ↑k < first
arr✝ arr'✝ : Vec α✝ n
i j : Fin n
fi : first ≤ ↑i
ij : i ≤ j
jl : ↑j ≤ last
p : permuted n first last (arr✝.swap i j) arr'✝
ih : arr'✝[k] = (arr✝.swap i j)[k]
⊢ k ≠ i

case step.kj
n first last : Nat
α✝ : Type
arr1 arr2 : Vec α✝ n
k : Fin n
lt : ↑k < first
arr✝ arr'✝ : Vec α✝ n
i j : Fin n
fi : first ≤ ↑i
ij : i ≤ j
jl : ↑j ≤ last
p : permuted n first last (arr✝.swap i j) arr'✝
ih : arr'✝[k] = (arr✝.swap i j)[k]
⊢ k ≠ j
Theorem: permuted.get_lt
Proof state before:
case step.ki
n first last : Nat
α✝ : Type
arr1 arr2 : Vec α✝ n
k : Fin n
lt : ↑k < first
arr✝ arr'✝ : Vec α✝ n
i j : Fin n
fi : first ≤ ↑i
ij : i ≤ j
jl : ↑j ≤ last
p : permuted n first last (arr✝.swap i j) arr'✝
ih : arr'✝[k] = (arr✝.swap i j)[k]
⊢ k ≠ i

case step.kj
n first last : Nat
α✝ : Type
arr1 arr2 : Vec α✝ n
k : Fin n
lt : ↑k < first
arr✝ arr'✝ : Vec α✝ n
i j : Fin n
fi : first ≤ ↑i
ij : i ≤ j
jl : ↑j ≤ last
p : permuted n first last (arr✝.swap i j) arr'✝
ih : arr'✝[k] = (arr✝.swap i j)[k]
⊢ k ≠ j
Tactic:
. apply Fin.ne_of_val_ne
  exact Nat.ne_of_lt (Nat.lt_of_lt_of_le lt fi)
Proof state after:
case step.kj
n first last : Nat
α✝ : Type
arr1 arr2 : Vec α✝ n
k : Fin n
lt : ↑k < first
arr✝ arr'✝ : Vec α✝ n
i j : Fin n
fi : first ≤ ↑i
ij : i ≤ j
jl : ↑j ≤ last
p : permuted n first last (arr✝.swap i j) arr'✝
ih : arr'✝[k] = (arr✝.swap i j)[k]
⊢ k ≠ j
Theorem: permuted.get_lt
Proof state before:
case step.kj
n first last : Nat
α✝ : Type
arr1 arr2 : Vec α✝ n
k : Fin n
lt : ↑k < first
arr✝ arr'✝ : Vec α✝ n
i j : Fin n
fi : first ≤ ↑i
ij : i ≤ j
jl : ↑j ≤ last
p : permuted n first last (arr✝.swap i j) arr'✝
ih : arr'✝[k] = (arr✝.swap i j)[k]
⊢ k ≠ j
Tactic:
. apply Fin.ne_of_val_ne
  exact Nat.ne_of_lt (Nat.lt_of_lt_of_le lt (Nat.le_trans fi ij))
Proof state after:
no goals
Theorem: permuted.get_lt
Proof state before:
case step.ki
n first last : Nat
α✝ : Type
arr1 arr2 : Vec α✝ n
k : Fin n
lt : ↑k < first
arr✝ arr'✝ : Vec α✝ n
i j : Fin n
fi : first ≤ ↑i
ij : i ≤ j
jl : ↑j ≤ last
p : permuted n first last (arr✝.swap i j) arr'✝
ih : arr'✝[k] = (arr✝.swap i j)[k]
⊢ k ≠ i
Tactic:
apply Fin.ne_of_val_ne
Proof state after:
case step.ki.h
n first last : Nat
α✝ : Type
arr1 arr2 : Vec α✝ n
k : Fin n
lt : ↑k < first
arr✝ arr'✝ : Vec α✝ n
i j : Fin n
fi : first ≤ ↑i
ij : i ≤ j
jl : ↑j ≤ last
p : permuted n first last (arr✝.swap i j) arr'✝
ih : arr'✝[k] = (arr✝.swap i j)[k]
⊢ ¬↑k = ↑i
Theorem: permuted.get_lt
Proof state before:
case step.ki.h
n first last : Nat
α✝ : Type
arr1 arr2 : Vec α✝ n
k : Fin n
lt : ↑k < first
arr✝ arr'✝ : Vec α✝ n
i j : Fin n
fi : first ≤ ↑i
ij : i ≤ j
jl : ↑j ≤ last
p : permuted n first last (arr✝.swap i j) arr'✝
ih : arr'✝[k] = (arr✝.swap i j)[k]
⊢ ¬↑k = ↑i
Tactic:
exact Nat.ne_of_lt (Nat.lt_of_lt_of_le lt fi)
Proof state after:
no goals
Theorem: permuted.get_lt
Proof state before:
case step.kj
n first last : Nat
α✝ : Type
arr1 arr2 : Vec α✝ n
k : Fin n
lt : ↑k < first
arr✝ arr'✝ : Vec α✝ n
i j : Fin n
fi : first ≤ ↑i
ij : i ≤ j
jl : ↑j ≤ last
p : permuted n first last (arr✝.swap i j) arr'✝
ih : arr'✝[k] = (arr✝.swap i j)[k]
⊢ k ≠ j
Tactic:
apply Fin.ne_of_val_ne
Proof state after:
case step.kj.h
n first last : Nat
α✝ : Type
arr1 arr2 : Vec α✝ n
k : Fin n
lt : ↑k < first
arr✝ arr'✝ : Vec α✝ n
i j : Fin n
fi : first ≤ ↑i
ij : i ≤ j
jl : ↑j ≤ last
p : permuted n first last (arr✝.swap i j) arr'✝
ih : arr'✝[k] = (arr✝.swap i j)[k]
⊢ ¬↑k = ↑j
Theorem: permuted.get_lt
Proof state before:
case step.kj.h
n first last : Nat
α✝ : Type
arr1 arr2 : Vec α✝ n
k : Fin n
lt : ↑k < first
arr✝ arr'✝ : Vec α✝ n
i j : Fin n
fi : first ≤ ↑i
ij : i ≤ j
jl : ↑j ≤ last
p : permuted n first last (arr✝.swap i j) arr'✝
ih : arr'✝[k] = (arr✝.swap i j)[k]
⊢ ¬↑k = ↑j
Tactic:
exact Nat.ne_of_lt (Nat.lt_of_lt_of_le lt (Nat.le_trans fi ij))
Proof state after:
no goals
Theorem: permuted.get_gt
Proof state before:
n first last : Nat
α✝ : Type
arr1 arr2 : Vec α✝ n
p : permuted n first last arr1 arr2
k : Fin n
gt : last < ↑k
⊢ arr2[k] = arr1[k]
Tactic:
induction p with
| refl => rfl
| step i j fi ij jl p ih =>
  rw [ih]
  rw [Vec.get_swap_neq _ i j k]
  . apply Fin.ne_of_val_ne
    exact Nat.ne_of_gt (Nat.lt_of_le_of_lt (Nat.le_trans ij jl) gt)
  . apply Fin.ne_of_val_ne
    exact Nat.ne_of_gt (Nat.lt_of_le_of_lt jl gt)
Proof state after:
no goals
Theorem: permuted.get_gt
Proof state before:
case refl
n first last : Nat
α✝ : Type
arr1 arr2 : Vec α✝ n
k : Fin n
gt : last < ↑k
arr✝ : Vec α✝ n
⊢ arr✝[k] = arr✝[k]
Tactic:
rfl
Proof state after:
no goals
Theorem: permuted.get_gt
Proof state before:
case step
n first last : Nat
α✝ : Type
arr1 arr2 : Vec α✝ n
k : Fin n
gt : last < ↑k
arr✝ arr'✝ : Vec α✝ n
i j : Fin n
fi : first ≤ ↑i
ij : i ≤ j
jl : ↑j ≤ last
p : permuted n first last (arr✝.swap i j) arr'✝
ih : arr'✝[k] = (arr✝.swap i j)[k]
⊢ arr'✝[k] = arr✝[k]
Tactic:
rw [ih]
Proof state after:
case step
n first last : Nat
α✝ : Type
arr1 arr2 : Vec α✝ n
k : Fin n
gt : last < ↑k
arr✝ arr'✝ : Vec α✝ n
i j : Fin n
fi : first ≤ ↑i
ij : i ≤ j
jl : ↑j ≤ last
p : permuted n first last (arr✝.swap i j) arr'✝
ih : arr'✝[k] = (arr✝.swap i j)[k]
⊢ (arr✝.swap i j)[k] = arr✝[k]
Theorem: permuted.get_gt
Proof state before:
case step
n first last : Nat
α✝ : Type
arr1 arr2 : Vec α✝ n
k : Fin n
gt : last < ↑k
arr✝ arr'✝ : Vec α✝ n
i j : Fin n
fi : first ≤ ↑i
ij : i ≤ j
jl : ↑j ≤ last
p : permuted n first last (arr✝.swap i j) arr'✝
ih : arr'✝[k] = (arr✝.swap i j)[k]
⊢ (arr✝.swap i j)[k] = arr✝[k]
Tactic:
rw [Vec.get_swap_neq _ i j k]
Proof state after:
case step.ki
n first last : Nat
α✝ : Type
arr1 arr2 : Vec α✝ n
k : Fin n
gt : last < ↑k
arr✝ arr'✝ : Vec α✝ n
i j : Fin n
fi : first ≤ ↑i
ij : i ≤ j
jl : ↑j ≤ last
p : permuted n first last (arr✝.swap i j) arr'✝
ih : arr'✝[k] = (arr✝.swap i j)[k]
⊢ k ≠ i

case step.kj
n first last : Nat
α✝ : Type
arr1 arr2 : Vec α✝ n
k : Fin n
gt : last < ↑k
arr✝ arr'✝ : Vec α✝ n
i j : Fin n
fi : first ≤ ↑i
ij : i ≤ j
jl : ↑j ≤ last
p : permuted n first last (arr✝.swap i j) arr'✝
ih : arr'✝[k] = (arr✝.swap i j)[k]
⊢ k ≠ j
Theorem: permuted.get_gt
Proof state before:
case step.ki
n first last : Nat
α✝ : Type
arr1 arr2 : Vec α✝ n
k : Fin n
gt : last < ↑k
arr✝ arr'✝ : Vec α✝ n
i j : Fin n
fi : first ≤ ↑i
ij : i ≤ j
jl : ↑j ≤ last
p : permuted n first last (arr✝.swap i j) arr'✝
ih : arr'✝[k] = (arr✝.swap i j)[k]
⊢ k ≠ i

case step.kj
n first last : Nat
α✝ : Type
arr1 arr2 : Vec α✝ n
k : Fin n
gt : last < ↑k
arr✝ arr'✝ : Vec α✝ n
i j : Fin n
fi : first ≤ ↑i
ij : i ≤ j
jl : ↑j ≤ last
p : permuted n first last (arr✝.swap i j) arr'✝
ih : arr'✝[k] = (arr✝.swap i j)[k]
⊢ k ≠ j
Tactic:
. apply Fin.ne_of_val_ne
  exact Nat.ne_of_gt (Nat.lt_of_le_of_lt (Nat.le_trans ij jl) gt)
Proof state after:
case step.kj
n first last : Nat
α✝ : Type
arr1 arr2 : Vec α✝ n
k : Fin n
gt : last < ↑k
arr✝ arr'✝ : Vec α✝ n
i j : Fin n
fi : first ≤ ↑i
ij : i ≤ j
jl : ↑j ≤ last
p : permuted n first last (arr✝.swap i j) arr'✝
ih : arr'✝[k] = (arr✝.swap i j)[k]
⊢ k ≠ j
Theorem: permuted.get_gt
Proof state before:
case step.kj
n first last : Nat
α✝ : Type
arr1 arr2 : Vec α✝ n
k : Fin n
gt : last < ↑k
arr✝ arr'✝ : Vec α✝ n
i j : Fin n
fi : first ≤ ↑i
ij : i ≤ j
jl : ↑j ≤ last
p : permuted n first last (arr✝.swap i j) arr'✝
ih : arr'✝[k] = (arr✝.swap i j)[k]
⊢ k ≠ j
Tactic:
. apply Fin.ne_of_val_ne
  exact Nat.ne_of_gt (Nat.lt_of_le_of_lt jl gt)
Proof state after:
no goals
Theorem: permuted.get_gt
Proof state before:
case step.ki
n first last : Nat
α✝ : Type
arr1 arr2 : Vec α✝ n
k : Fin n
gt : last < ↑k
arr✝ arr'✝ : Vec α✝ n
i j : Fin n
fi : first ≤ ↑i
ij : i ≤ j
jl : ↑j ≤ last
p : permuted n first last (arr✝.swap i j) arr'✝
ih : arr'✝[k] = (arr✝.swap i j)[k]
⊢ k ≠ i
Tactic:
apply Fin.ne_of_val_ne
Proof state after:
case step.ki.h
n first last : Nat
α✝ : Type
arr1 arr2 : Vec α✝ n
k : Fin n
gt : last < ↑k
arr✝ arr'✝ : Vec α✝ n
i j : Fin n
fi : first ≤ ↑i
ij : i ≤ j
jl : ↑j ≤ last
p : permuted n first last (arr✝.swap i j) arr'✝
ih : arr'✝[k] = (arr✝.swap i j)[k]
⊢ ¬↑k = ↑i
Theorem: permuted.get_gt
Proof state before:
case step.ki.h
n first last : Nat
α✝ : Type
arr1 arr2 : Vec α✝ n
k : Fin n
gt : last < ↑k
arr✝ arr'✝ : Vec α✝ n
i j : Fin n
fi : first ≤ ↑i
ij : i ≤ j
jl : ↑j ≤ last
p : permuted n first last (arr✝.swap i j) arr'✝
ih : arr'✝[k] = (arr✝.swap i j)[k]
⊢ ¬↑k = ↑i
Tactic:
exact Nat.ne_of_gt (Nat.lt_of_le_of_lt (Nat.le_trans ij jl) gt)
Proof state after:
no goals
Theorem: permuted.get_gt
Proof state before:
case step.kj
n first last : Nat
α✝ : Type
arr1 arr2 : Vec α✝ n
k : Fin n
gt : last < ↑k
arr✝ arr'✝ : Vec α✝ n
i j : Fin n
fi : first ≤ ↑i
ij : i ≤ j
jl : ↑j ≤ last
p : permuted n first last (arr✝.swap i j) arr'✝
ih : arr'✝[k] = (arr✝.swap i j)[k]
⊢ k ≠ j
Tactic:
apply Fin.ne_of_val_ne
Proof state after:
case step.kj.h
n first last : Nat
α✝ : Type
arr1 arr2 : Vec α✝ n
k : Fin n
gt : last < ↑k
arr✝ arr'✝ : Vec α✝ n
i j : Fin n
fi : first ≤ ↑i
ij : i ≤ j
jl : ↑j ≤ last
p : permuted n first last (arr✝.swap i j) arr'✝
ih : arr'✝[k] = (arr✝.swap i j)[k]
⊢ ¬↑k = ↑j
Theorem: permuted.get_gt
Proof state before:
case step.kj.h
n first last : Nat
α✝ : Type
arr1 arr2 : Vec α✝ n
k : Fin n
gt : last < ↑k
arr✝ arr'✝ : Vec α✝ n
i j : Fin n
fi : first ≤ ↑i
ij : i ≤ j
jl : ↑j ≤ last
p : permuted n first last (arr✝.swap i j) arr'✝
ih : arr'✝[k] = (arr✝.swap i j)[k]
⊢ ¬↑k = ↑j
Tactic:
exact Nat.ne_of_gt (Nat.lt_of_le_of_lt jl gt)
Proof state after:
no goals
Theorem: sorted_of_adjacentSorted
Proof state before:
α : Type
inst✝ : Order α
n : Nat
arr : Vec α n
assms : ∀ (i : Nat) (isLt : i + 1 < n), arr[i] ≤ arr[i + 1]
j k : Nat
kn : k < n
jk : j ≤ k
⊢ arr[j] ≤ arr[k]
Tactic:
induction jk with
| refl => exact Order.refl
| step h ih =>
  apply Order.trans
  . exact ih (Nat.lt_of_le_of_lt (Nat.le_succ ..) kn)
  . apply assms
Proof state after:
no goals
Theorem: sorted_of_adjacentSorted
Proof state before:
case refl
α : Type
inst✝ : Order α
n : Nat
arr : Vec α n
assms : ∀ (i : Nat) (isLt : i + 1 < n), arr[i] ≤ arr[i + 1]
j k : Nat
kn : j < n
⊢ arr[j] ≤ arr[j]
Tactic:
exact Order.refl
Proof state after:
no goals
Theorem: sorted_of_adjacentSorted
Proof state before:
case step
α : Type
inst✝ : Order α
n : Nat
arr : Vec α n
assms : ∀ (i : Nat) (isLt : i + 1 < n), arr[i] ≤ arr[i + 1]
j k m✝ : Nat
h : j.le m✝
ih : ∀ (kn : m✝ < n), arr[j] ≤ arr[m✝]
kn : m✝.succ < n
⊢ arr[j] ≤ arr[m✝.succ]
Tactic:
apply Order.trans
Proof state after:
case step.a
α : Type
inst✝ : Order α
n : Nat
arr : Vec α n
assms : ∀ (i : Nat) (isLt : i + 1 < n), arr[i] ≤ arr[i + 1]
j k m✝ : Nat
h : j.le m✝
ih : ∀ (kn : m✝ < n), arr[j] ≤ arr[m✝]
kn : m✝.succ < n
⊢ arr[j] ≤ ?step.y

case step.a
α : Type
inst✝ : Order α
n : Nat
arr : Vec α n
assms : ∀ (i : Nat) (isLt : i + 1 < n), arr[i] ≤ arr[i + 1]
j k m✝ : Nat
h : j.le m✝
ih : ∀ (kn : m✝ < n), arr[j] ≤ arr[m✝]
kn : m✝.succ < n
⊢ ?step.y ≤ arr[m✝.succ]

case step.y
α : Type
inst✝ : Order α
n : Nat
arr : Vec α n
assms : ∀ (i : Nat) (isLt : i + 1 < n), arr[i] ≤ arr[i + 1]
j k m✝ : Nat
h : j.le m✝
ih : ∀ (kn : m✝ < n), arr[j] ≤ arr[m✝]
kn : m✝.succ < n
⊢ α
Theorem: sorted_of_adjacentSorted
Proof state before:
case step.a
α : Type
inst✝ : Order α
n : Nat
arr : Vec α n
assms : ∀ (i : Nat) (isLt : i + 1 < n), arr[i] ≤ arr[i + 1]
j k m✝ : Nat
h : j.le m✝
ih : ∀ (kn : m✝ < n), arr[j] ≤ arr[m✝]
kn : m✝.succ < n
⊢ arr[j] ≤ ?step.y

case step.a
α : Type
inst✝ : Order α
n : Nat
arr : Vec α n
assms : ∀ (i : Nat) (isLt : i + 1 < n), arr[i] ≤ arr[i + 1]
j k m✝ : Nat
h : j.le m✝
ih : ∀ (kn : m✝ < n), arr[j] ≤ arr[m✝]
kn : m✝.succ < n
⊢ ?step.y ≤ arr[m✝.succ]

case step.y
α : Type
inst✝ : Order α
n : Nat
arr : Vec α n
assms : ∀ (i : Nat) (isLt : i + 1 < n), arr[i] ≤ arr[i + 1]
j k m✝ : Nat
h : j.le m✝
ih : ∀ (kn : m✝ < n), arr[j] ≤ arr[m✝]
kn : m✝.succ < n
⊢ α
Tactic:
. exact ih (Nat.lt_of_le_of_lt (Nat.le_succ ..) kn)
Proof state after:
case step.a
α : Type
inst✝ : Order α
n : Nat
arr : Vec α n
assms : ∀ (i : Nat) (isLt : i + 1 < n), arr[i] ≤ arr[i + 1]
j k m✝ : Nat
h : j.le m✝
ih : ∀ (kn : m✝ < n), arr[j] ≤ arr[m✝]
kn : m✝.succ < n
⊢ arr[m✝] ≤ arr[m✝.succ]
Theorem: sorted_of_adjacentSorted
Proof state before:
case step.a
α : Type
inst✝ : Order α
n : Nat
arr : Vec α n
assms : ∀ (i : Nat) (isLt : i + 1 < n), arr[i] ≤ arr[i + 1]
j k m✝ : Nat
h : j.le m✝
ih : ∀ (kn : m✝ < n), arr[j] ≤ arr[m✝]
kn : m✝.succ < n
⊢ arr[m✝] ≤ arr[m✝.succ]
Tactic:
. apply assms
Proof state after:
no goals
Theorem: sorted_of_adjacentSorted
Proof state before:
case step.a
α : Type
inst✝ : Order α
n : Nat
arr : Vec α n
assms : ∀ (i : Nat) (isLt : i + 1 < n), arr[i] ≤ arr[i + 1]
j k m✝ : Nat
h : j.le m✝
ih : ∀ (kn : m✝ < n), arr[j] ≤ arr[m✝]
kn : m✝.succ < n
⊢ arr[j] ≤ ?step.y
Tactic:
exact ih (Nat.lt_of_le_of_lt (Nat.le_succ ..) kn)
Proof state after:
no goals
Theorem: sorted_of_adjacentSorted
Proof state before:
case step.a
α : Type
inst✝ : Order α
n : Nat
arr : Vec α n
assms : ∀ (i : Nat) (isLt : i + 1 < n), arr[i] ≤ arr[i + 1]
j k m✝ : Nat
h : j.le m✝
ih : ∀ (kn : m✝ < n), arr[j] ≤ arr[m✝]
kn : m✝.succ < n
⊢ arr[m✝] ≤ arr[m✝.succ]
Tactic:
apply assms
Proof state after:
no goals
Theorem: Vec.get_set_eq
Proof state before:
α : Type
n : Nat
a : Vec α n
i : Fin n
v : α
⊢ (a.set i v)[i] = v
Tactic:
show (a.set i v).get i = v
Proof state after:
α : Type
n : Nat
a : Vec α n
i : Fin n
v : α
⊢ (a.set i v).get i = v
Theorem: Vec.get_set_eq
Proof state before:
α : Type
n : Nat
a : Vec α n
i : Fin n
v : α
⊢ (a.set i v).get i = v
Tactic:
simp [Vec.get, Vec.set]
Proof state after:
no goals
Theorem: Vec.get_set_ne
Proof state before:
α : Type
n : Nat
a : Vec α n
i j : Fin n
v : α
h : i ≠ j
⊢ (a.set i v)[j] = a[j]
Tactic:
show (a.set i v).get j = a.get j
Proof state after:
α : Type
n : Nat
a : Vec α n
i j : Fin n
v : α
h : i ≠ j
⊢ (a.set i v).get j = a.get j
Theorem: Vec.get_set_ne
Proof state before:
α : Type
n : Nat
a : Vec α n
i j : Fin n
v : α
h : i ≠ j
⊢ (a.set i v).get j = a.get j
Tactic:
simp [Vec.get, Vec.set]
Proof state after:
α : Type
n : Nat
a : Vec α n
i j : Fin n
v : α
h : i ≠ j
⊢ (a.val.set ⟨↑i, ⋯⟩ v)[↑j] = a.val[↑j]
Theorem: Vec.get_set_ne
Proof state before:
α : Type
n : Nat
a : Vec α n
i j : Fin n
v : α
h : i ≠ j
⊢ (a.val.set ⟨↑i, ⋯⟩ v)[↑j] = a.val[↑j]
Tactic:
exact Array.get_set_ne (j := j.val) a.val ⟨i, by simp [a.property, i.isLt]⟩ v
  (by simp [a.property, j.isLt]) (Fin.val_ne_of_ne h)
Proof state after:
no goals
Theorem: Vec.get_set_ne
Proof state before:
α : Type
n : Nat
a : Vec α n
i j : Fin n
v : α
h : i ≠ j
⊢ ↑i < a.val.size
Tactic:
simp [a.property, i.isLt]
Proof state after:
no goals
Theorem: Vec.get_set_ne
Proof state before:
α : Type
n : Nat
a : Vec α n
i j : Fin n
v : α
h : i ≠ j
⊢ ↑j < a.val.size
Tactic:
simp [a.property, j.isLt]
Proof state after:
no goals
Theorem: Vec.get_set
Proof state before:
α : Type
n : Nat
a : Vec α n
i j : Fin n
v : α
⊢ (a.set i v)[j] = if i = j then v else a[j]
Tactic:
if h : i = j then
  simp [h]
  exact Vec.get_set_eq a j v
else
  simp [h]
  exact Vec.get_set_ne a i j v h
Proof state after:
no goals
Theorem: Vec.get_set
Proof state before:
α : Type
n : Nat
a : Vec α n
i j : Fin n
v : α
h : i = j
⊢ (a.set i v)[j] = if i = j then v else a[j]
Tactic:
simp [h]
Proof state after:
α : Type
n : Nat
a : Vec α n
i j : Fin n
v : α
h : i = j
⊢ (a.set j v)[j] = v
Theorem: Vec.get_set
Proof state before:
α : Type
n : Nat
a : Vec α n
i j : Fin n
v : α
h : i = j
⊢ (a.set j v)[j] = v
Tactic:
exact Vec.get_set_eq a j v
Proof state after:
no goals
Theorem: Vec.get_set
Proof state before:
α : Type
n : Nat
a : Vec α n
i j : Fin n
v : α
h : ¬i = j
⊢ (a.set i v)[j] = if i = j then v else a[j]
Tactic:
simp [h]
Proof state after:
α : Type
n : Nat
a : Vec α n
i j : Fin n
v : α
h : ¬i = j
⊢ (a.set i v)[j] = a[j]
Theorem: Vec.get_set
Proof state before:
α : Type
n : Nat
a : Vec α n
i j : Fin n
v : α
h : ¬i = j
⊢ (a.set i v)[j] = a[j]
Tactic:
exact Vec.get_set_ne a i j v h
Proof state after:
no goals
Theorem: Vec.swap_def
Proof state before:
α : Type
n : Nat
a : Vec α n
i j : Fin n
⊢ a.swap i j = (a.set i (a.get j)).set j (a.get i)
Tactic:
simp [Vec.swap]
Proof state after:
α : Type
n : Nat
a : Vec α n
i j : Fin n
⊢ ⟨a.val.swap (Fin.cast ⋯ i) (Fin.cast ⋯ j), ⋯⟩ = (a.set i (a.get j)).set j (a.get i)
Theorem: Vec.swap_def
Proof state before:
α : Type
n : Nat
a : Vec α n
i j : Fin n
⊢ ⟨a.val.swap (Fin.cast ⋯ i) (Fin.cast ⋯ j), ⋯⟩ = (a.set i (a.get j)).set j (a.get i)
Tactic:
apply Subtype.eq
Proof state after:
case a
α : Type
n : Nat
a : Vec α n
i j : Fin n
⊢ ⟨a.val.swap (Fin.cast ⋯ i) (Fin.cast ⋯ j), ⋯⟩.val = ((a.set i (a.get j)).set j (a.get i)).val
Theorem: Vec.swap_def
Proof state before:
case a
α : Type
n : Nat
a : Vec α n
i j : Fin n
⊢ ⟨a.val.swap (Fin.cast ⋯ i) (Fin.cast ⋯ j), ⋯⟩.val = ((a.set i (a.get j)).set j (a.get i)).val
Tactic:
simp [Vec.get, Vec.set, Array.swap_def]
Proof state after:
case a
α : Type
n : Nat
a : Vec α n
i j : Fin n
⊢ (a.val.set (Fin.cast ⋯ i) a.val[↑j]).set ⟨↑j, ⋯⟩ a.val[↑i] = (a.val.set ⟨↑i, ⋯⟩ a.val[↑j]).set ⟨↑j, ⋯⟩ a.val[↑i]
Theorem: Vec.swap_def
Proof state before:
case a
α : Type
n : Nat
a : Vec α n
i j : Fin n
⊢ (a.val.set (Fin.cast ⋯ i) a.val[↑j]).set ⟨↑j, ⋯⟩ a.val[↑i] = (a.val.set ⟨↑i, ⋯⟩ a.val[↑j]).set ⟨↑j, ⋯⟩ a.val[↑i]
Tactic:
rfl
Proof state after:
no goals
Theorem: Vec.get_swap_left
Proof state before:
α : Type
n : Nat
a : Vec α n
i j : Fin n
⊢ (a.swap i j)[i] = a[j]
Tactic:
simp [Vec.swap_def, Vec.get_set, Vec.get_set_eq]
Proof state after:
α : Type
n : Nat
a : Vec α n
i j : Fin n
⊢ (if j = i then a.get i else a.get j) = a[j]
Theorem: Vec.get_swap_left
Proof state before:
α : Type
n : Nat
a : Vec α n
i j : Fin n
⊢ (if j = i then a.get i else a.get j) = a[j]
Tactic:
cases decEq j i <;> simp [*] <;> rfl
Proof state after:
no goals
Theorem: Vec.get_swap_right
Proof state before:
α : Type
n : Nat
a : Vec α n
i j : Fin n
⊢ (a.swap i j)[j] = a[i]
Tactic:
simp [Vec.swap_def, Vec.get_set_eq]
Proof state after:
α : Type
n : Nat
a : Vec α n
i j : Fin n
⊢ a.get i = a[i]
Theorem: Vec.get_swap_right
Proof state before:
α : Type
n : Nat
a : Vec α n
i j : Fin n
⊢ a.get i = a[i]
Tactic:
rfl
Proof state after:
no goals
Theorem: Vec.get_swap_neq
Proof state before:
α : Type
n : Nat
a : Vec α n
i j k : Fin n
ki : k ≠ i
kj : k ≠ j
⊢ (a.swap i j)[k] = a[k]
Tactic:
simp [Vec.swap_def]
Proof state after:
α : Type
n : Nat
a : Vec α n
i j k : Fin n
ki : k ≠ i
kj : k ≠ j
⊢ ((a.set i (a.get j)).set j (a.get i))[k] = a[k]
Theorem: Vec.get_swap_neq
Proof state before:
α : Type
n : Nat
a : Vec α n
i j k : Fin n
ki : k ≠ i
kj : k ≠ j
⊢ ((a.set i (a.get j)).set j (a.get i))[k] = a[k]
Tactic:
rw [Vec.get_set_ne (h := kj.symm), Vec.get_set_ne (h := ki.symm)]
Proof state after:
no goals
Theorem: Vec.getElem_eq_getElem
Proof state before:
α : Type
n : Nat
a : Vec α n
i : Fin n
⊢ a[i] = a.val[↑i]
Tactic:
rfl
Proof state after:
no goals
Theorem: partitionImpl_permuted
Proof 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⟩
Proof state after:
no goals
Theorem: partitionImpl_permuted
Proof 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
Proof 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)
Theorem: partitionImpl_permuted
Proof 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 [*]
Proof state after:
no goals