internlm/Lean-Github huggingface dataset:
Theorem: partitionImpl_permuted
Proof 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
Proof 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)
Theorem: partitionImpl_permuted
Proof 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 *
Proof 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')
Theorem: partitionImpl_permuted
Proof 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
Proof 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')
Theorem: partitionImpl_permuted
Proof 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
Proof 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')
Theorem: partitionImpl_permuted
Proof 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 ..)⟩
Proof state after:
no goals
Theorem: partitionImpl_permuted
Proof 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, *]
Proof 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)
Theorem: partitionImpl_permuted
Proof 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⟩
Proof state after:
no goals
Theorem: quickSort'_map_index_invertible
Proof state before:
α : Type
inst✝ : Ord α
n : Nat
arr : Vec α n
⊢ ∃ f, invertible f ∧ ∀ (i : Fin n), arr[i] = (quickSort' arr)[f i]
Tactic:
let p := quickSort'_permuted arr
Proof state after:
α : Type
inst✝ : Ord α
n : Nat
arr : Vec α n
p : permuted n 0 (n - 1) arr (quickSort' arr) := quickSort'_permuted arr
⊢ ∃ f, invertible f ∧ ∀ (i : Fin n), arr[i] = (quickSort' arr)[f i]
Theorem: quickSort'_map_index_invertible
Proof state before:
α : Type
inst✝ : Ord α
n : Nat
arr : Vec α n
p : permuted n 0 (n - 1) arr (quickSort' arr) := quickSort'_permuted arr
⊢ ∃ f, invertible f ∧ ∀ (i : Fin n), arr[i] = (quickSort' arr)[f i]
Tactic:
exists p.to_map
Proof state after:
α : Type
inst✝ : Ord α
n : Nat
arr : Vec α n
p : permuted n 0 (n - 1) arr (quickSort' arr) := quickSort'_permuted arr
⊢ invertible p.to_map ∧ ∀ (i : Fin n), arr[i] = (quickSort' arr)[p.to_map i]
Theorem: quickSort'_map_index_invertible
Proof state before:
α : Type
inst✝ : Ord α
n : Nat
arr : Vec α n
p : permuted n 0 (n - 1) arr (quickSort' arr) := quickSort'_permuted arr
⊢ invertible p.to_map ∧ ∀ (i : Fin n), arr[i] = (quickSort' arr)[p.to_map i]
Tactic:
apply And.intro
Proof state after:
case left
α : Type
inst✝ : Ord α
n : Nat
arr : Vec α n
p : permuted n 0 (n - 1) arr (quickSort' arr) := quickSort'_permuted arr
⊢ invertible p.to_map

case right
α : Type
inst✝ : Ord α
n : Nat
arr : Vec α n
p : permuted n 0 (n - 1) arr (quickSort' arr) := quickSort'_permuted arr
⊢ ∀ (i : Fin n), arr[i] = (quickSort' arr)[p.to_map i]
Theorem: quickSort'_map_index_invertible
Proof state before:
case left
α : Type
inst✝ : Ord α
n : Nat
arr : Vec α n
p : permuted n 0 (n - 1) arr (quickSort' arr) := quickSort'_permuted arr
⊢ invertible p.to_map

case right
α : Type
inst✝ : Ord α
n : Nat
arr : Vec α n
p : permuted n 0 (n - 1) arr (quickSort' arr) := quickSort'_permuted arr
⊢ ∀ (i : Fin n), arr[i] = (quickSort' arr)[p.to_map i]
Tactic:
. exact permuted_map_invertible p
Proof state after:
case right
α : Type
inst✝ : Ord α
n : Nat
arr : Vec α n
p : permuted n 0 (n - 1) arr (quickSort' arr) := quickSort'_permuted arr
⊢ ∀ (i : Fin n), arr[i] = (quickSort' arr)[p.to_map i]
Theorem: quickSort'_map_index_invertible
Proof state before:
case right
α : Type
inst✝ : Ord α
n : Nat
arr : Vec α n
p : permuted n 0 (n - 1) arr (quickSort' arr) := quickSort'_permuted arr
⊢ ∀ (i : Fin n), arr[i] = (quickSort' arr)[p.to_map i]
Tactic:
. exact permuted_map_index p
Proof state after:
no goals
Theorem: quickSort'_map_index_invertible
Proof state before:
case left
α : Type
inst✝ : Ord α
n : Nat
arr : Vec α n
p : permuted n 0 (n - 1) arr (quickSort' arr) := quickSort'_permuted arr
⊢ invertible p.to_map
Tactic:
exact permuted_map_invertible p
Proof state after:
no goals
Theorem: quickSort'_map_index_invertible
Proof state before:
case right
α : Type
inst✝ : Ord α
n : Nat
arr : Vec α n
p : permuted n 0 (n - 1) arr (quickSort' arr) := quickSort'_permuted arr
⊢ ∀ (i : Fin n), arr[i] = (quickSort' arr)[p.to_map i]
Tactic:
exact permuted_map_index p
Proof state after:
no goals
Theorem: Order.total
Proof state before:
α : Type
inst✝ : Order α
x y : α
⊢ x ≤ y ∨ y ≤ x
Tactic:
show (compare x y).isLE ∨ (compare y x).isLE
Proof state after:
α : Type
inst✝ : Order α
x y : α
⊢ (compare x y).isLE = true ∨ (compare y x).isLE = true
Theorem: Order.total
Proof state before:
α : Type
inst✝ : Order α
x y : α
⊢ (compare x y).isLE = true ∨ (compare y x).isLE = true
Tactic:
match cmp : compare x y with
| .lt | .eq => simp [Ordering.isLE, cmp]
| .gt =>
  apply Or.inr
  rw [←symm, cmp]
  decide
Proof state after:
no goals
Theorem: Order.total
Proof state before:
α : Type
inst✝ : Order α
x y : α
cmp : compare x y = Ordering.eq
⊢ Ordering.eq.isLE = true ∨ (compare y x).isLE = true
Tactic:
simp [Ordering.isLE, cmp]
Proof state after:
no goals
Theorem: Order.total
Proof state before:
α : Type
inst✝ : Order α
x y : α
cmp : compare x y = Ordering.gt
⊢ Ordering.gt.isLE = true ∨ (compare y x).isLE = true
Tactic:
apply Or.inr
Proof state after:
case h
α : Type
inst✝ : Order α
x y : α
cmp : compare x y = Ordering.gt
⊢ (compare y x).isLE = true
Theorem: Order.total
Proof state before:
case h
α : Type
inst✝ : Order α
x y : α
cmp : compare x y = Ordering.gt
⊢ (compare y x).isLE = true
Tactic:
rw [←symm, cmp]
Proof state after:
case h
α : Type
inst✝ : Order α
x y : α
cmp : compare x y = Ordering.gt
⊢ Ordering.gt.swap.isLE = true
Theorem: Order.total
Proof state before:
case h
α : Type
inst✝ : Order α
x y : α
cmp : compare x y = Ordering.gt
⊢ Ordering.gt.swap.isLE = true
Tactic:
decide
Proof state after:
no goals
Theorem: Order.cmp_eq_of_eq
Proof state before:
α : Type
inst✝ : Order α
x : α
⊢ compare x x = Ordering.eq
Tactic:
match cmp : compare x x with
| .eq => rfl
| .lt =>
  have h₁ : (compare x x).swap = .gt := by rw [cmp]; decide
  have h₂ : (compare x x).swap = .lt := by rw [symm]; assumption
  rw [h₂] at h₁
  contradiction
| .gt =>
  have h₁ : (compare x x).swap = .lt := by rw [cmp]; decide
  have h₂ : (compare x x).swap = .gt := by rw [symm]; assumption
  rw [h₂] at h₁
  contradiction
Proof state after:
no goals
Theorem: Order.cmp_eq_of_eq
Proof state before:
α : Type
inst✝ : Order α
x : α
cmp : compare x x = Ordering.eq
⊢ Ordering.eq = Ordering.eq
Tactic:
rfl
Proof state after:
no goals
Theorem: Order.cmp_eq_of_eq
Proof state before:
α : Type
inst✝ : Order α
x : α
cmp : compare x x = Ordering.lt
⊢ Ordering.lt = Ordering.eq
Tactic:
have h₁ : (compare x x).swap = .gt := by rw [cmp]; decide
Proof state after:
α : Type
inst✝ : Order α
x : α
cmp : compare x x = Ordering.lt
h₁ : (compare x x).swap = Ordering.gt
⊢ Ordering.lt = Ordering.eq
Theorem: Order.cmp_eq_of_eq
Proof state before:
α : Type
inst✝ : Order α
x : α
cmp : compare x x = Ordering.lt
h₁ : (compare x x).swap = Ordering.gt
⊢ Ordering.lt = Ordering.eq
Tactic:
have h₂ : (compare x x).swap = .lt := by rw [symm]; assumption
Proof state after:
α : Type
inst✝ : Order α
x : α
cmp : compare x x = Ordering.lt
h₁ : (compare x x).swap = Ordering.gt
h₂ : (compare x x).swap = Ordering.lt
⊢ Ordering.lt = Ordering.eq
Theorem: Order.cmp_eq_of_eq
Proof state before:
α : Type
inst✝ : Order α
x : α
cmp : compare x x = Ordering.lt
h₁ : (compare x x).swap = Ordering.gt
h₂ : (compare x x).swap = Ordering.lt
⊢ Ordering.lt = Ordering.eq
Tactic:
rw [h₂] at h₁
Proof state after:
α : Type
inst✝ : Order α
x : α
cmp : compare x x = Ordering.lt
h₁ : Ordering.lt = Ordering.gt
h₂ : (compare x x).swap = Ordering.lt
⊢ Ordering.lt = Ordering.eq
Theorem: Order.cmp_eq_of_eq
Proof state before:
α : Type
inst✝ : Order α
x : α
cmp : compare x x = Ordering.lt
h₁ : Ordering.lt = Ordering.gt
h₂ : (compare x x).swap = Ordering.lt
⊢ Ordering.lt = Ordering.eq
Tactic:
contradiction
Proof state after:
no goals
Theorem: Order.cmp_eq_of_eq
Proof state before:
α : Type
inst✝ : Order α
x : α
cmp : compare x x = Ordering.lt
⊢ (compare x x).swap = Ordering.gt
Tactic:
rw [cmp]
Proof state after:
α : Type
inst✝ : Order α
x : α
cmp : compare x x = Ordering.lt
⊢ Ordering.lt.swap = Ordering.gt
Theorem: Order.cmp_eq_of_eq
Proof state before:
α : Type
inst✝ : Order α
x : α
cmp : compare x x = Ordering.lt
⊢ Ordering.lt.swap = Ordering.gt
Tactic:
decide
Proof state after:
no goals
Theorem: Order.cmp_eq_of_eq
Proof state before:
α : Type
inst✝ : Order α
x : α
cmp : compare x x = Ordering.lt
h₁ : (compare x x).swap = Ordering.gt
⊢ (compare x x).swap = Ordering.lt
Tactic:
rw [symm]
Proof state after:
α : Type
inst✝ : Order α
x : α
cmp : compare x x = Ordering.lt
h₁ : (compare x x).swap = Ordering.gt
⊢ compare x x = Ordering.lt
Theorem: Order.cmp_eq_of_eq
Proof state before:
α : Type
inst✝ : Order α
x : α
cmp : compare x x = Ordering.lt
h₁ : (compare x x).swap = Ordering.gt
⊢ compare x x = Ordering.lt
Tactic:
assumption
Proof state after:
no goals
Theorem: Order.cmp_eq_of_eq
Proof state before:
α : Type
inst✝ : Order α
x : α
cmp : compare x x = Ordering.gt
⊢ Ordering.gt = Ordering.eq
Tactic:
have h₁ : (compare x x).swap = .lt := by rw [cmp]; decide
Proof state after:
α : Type
inst✝ : Order α
x : α
cmp : compare x x = Ordering.gt
h₁ : (compare x x).swap = Ordering.lt
⊢ Ordering.gt = Ordering.eq
Theorem: Order.cmp_eq_of_eq
Proof state before:
α : Type
inst✝ : Order α
x : α
cmp : compare x x = Ordering.gt
h₁ : (compare x x).swap = Ordering.lt
⊢ Ordering.gt = Ordering.eq
Tactic:
have h₂ : (compare x x).swap = .gt := by rw [symm]; assumption
Proof state after:
α : Type
inst✝ : Order α
x : α
cmp : compare x x = Ordering.gt
h₁ : (compare x x).swap = Ordering.lt
h₂ : (compare x x).swap = Ordering.gt
⊢ Ordering.gt = Ordering.eq
Theorem: Order.cmp_eq_of_eq
Proof state before:
α : Type
inst✝ : Order α
x : α
cmp : compare x x = Ordering.gt
h₁ : (compare x x).swap = Ordering.lt
h₂ : (compare x x).swap = Ordering.gt
⊢ Ordering.gt = Ordering.eq
Tactic:
rw [h₂] at h₁
Proof state after:
α : Type
inst✝ : Order α
x : α
cmp : compare x x = Ordering.gt
h₁ : Ordering.gt = Ordering.lt
h₂ : (compare x x).swap = Ordering.gt
⊢ Ordering.gt = Ordering.eq
Theorem: Order.cmp_eq_of_eq
Proof state before:
α : Type
inst✝ : Order α
x : α
cmp : compare x x = Ordering.gt
h₁ : Ordering.gt = Ordering.lt
h₂ : (compare x x).swap = Ordering.gt
⊢ Ordering.gt = Ordering.eq
Tactic:
contradiction
Proof state after:
no goals
Theorem: Order.cmp_eq_of_eq
Proof state before:
α : Type
inst✝ : Order α
x : α
cmp : compare x x = Ordering.gt
⊢ (compare x x).swap = Ordering.lt
Tactic:
rw [cmp]
Proof state after:
α : Type
inst✝ : Order α
x : α
cmp : compare x x = Ordering.gt
⊢ Ordering.gt.swap = Ordering.lt
Theorem: Order.cmp_eq_of_eq
Proof state before:
α : Type
inst✝ : Order α
x : α
cmp : compare x x = Ordering.gt
⊢ Ordering.gt.swap = Ordering.lt
Tactic:
decide
Proof state after:
no goals
Theorem: Order.cmp_eq_of_eq
Proof state before:
α : Type
inst✝ : Order α
x : α
cmp : compare x x = Ordering.gt
h₁ : (compare x x).swap = Ordering.lt
⊢ (compare x x).swap = Ordering.gt
Tactic:
rw [symm]
Proof state after:
α : Type
inst✝ : Order α
x : α
cmp : compare x x = Ordering.gt
h₁ : (compare x x).swap = Ordering.lt
⊢ compare x x = Ordering.gt
Theorem: Order.cmp_eq_of_eq
Proof state before:
α : Type
inst✝ : Order α
x : α
cmp : compare x x = Ordering.gt
h₁ : (compare x x).swap = Ordering.lt
⊢ compare x x = Ordering.gt
Tactic:
assumption
Proof state after:
no goals
Theorem: Order.refl
Proof state before:
α : Type
inst✝ : Order α
x : α
⊢ x ≤ x
Tactic:
show (compare x x).isLE
Proof state after:
α : Type
inst✝ : Order α
x : α
⊢ (compare x x).isLE = true
Theorem: Order.refl
Proof state before:
α : Type
inst✝ : Order α
x : α
⊢ (compare x x).isLE = true
Tactic:
simp [cmp_eq_of_eq]
Proof state after:
α : Type
inst✝ : Order α
x : α
⊢ Ordering.eq.isLE = true
Theorem: Order.refl
Proof state before:
α : Type
inst✝ : Order α
x : α
⊢ Ordering.eq.isLE = true
Tactic:
decide
Proof state after:
no goals
Theorem: Order.irrefl
Proof state before:
α : Type
inst✝ : Order α
x : α
⊢ ¬x < x
Tactic:
simp [ltOfOrd, cmp_eq_of_eq]
Proof state after:
no goals
Theorem: Order.le_of_not_lt
Proof state before:
α : Type
inst✝ : Order α
x y : α
h : ¬y < x
⊢ x ≤ y
Tactic:
show (compare x y).isLE
Proof state after:
α : Type
inst✝ : Order α
x y : α
h : ¬y < x
⊢ (compare x y).isLE = true
Theorem: Order.le_of_not_lt
Proof state before:
α : Type
inst✝ : Order α
x y : α
h : ¬y < x
⊢ (compare x y).isLE = true
Tactic:
match cmp : compare x y with
| .lt | .eq => decide
| .gt =>
  simp [ltOfOrd] at h
  have : compare y x = .lt := by rw [←symm, cmp]; decide
  rw [this] at h
  contradiction
Proof state after:
no goals
Theorem: Order.le_of_not_lt
Proof state before:
α : Type
inst✝ : Order α
x y : α
h : ¬y < x
cmp : compare x y = Ordering.eq
⊢ Ordering.eq.isLE = true
Tactic:
decide
Proof state after:
no goals
Theorem: Order.le_of_not_lt
Proof state before:
α : Type
inst✝ : Order α
x y : α
h : ¬y < x
cmp : compare x y = Ordering.gt
⊢ Ordering.gt.isLE = true
Tactic:
simp [ltOfOrd] at h
Proof state after:
α : Type
inst✝ : Order α
x y : α
h : ¬compare y x = Ordering.lt
cmp : compare x y = Ordering.gt
⊢ Ordering.gt.isLE = true
Theorem: Order.le_of_not_lt
Proof state before:
α : Type
inst✝ : Order α
x y : α
h : ¬compare y x = Ordering.lt
cmp : compare x y = Ordering.gt
⊢ Ordering.gt.isLE = true
Tactic:
have : compare y x = .lt := by rw [←symm, cmp]; decide
Proof state after:
α : Type
inst✝ : Order α
x y : α
h : ¬compare y x = Ordering.lt
cmp : compare x y = Ordering.gt
this : compare y x = Ordering.lt
⊢ Ordering.gt.isLE = true
Theorem: Order.le_of_not_lt
Proof state before:
α : Type
inst✝ : Order α
x y : α
h : ¬compare y x = Ordering.lt
cmp : compare x y = Ordering.gt
this : compare y x = Ordering.lt
⊢ Ordering.gt.isLE = true
Tactic:
rw [this] at h
Proof state after:
α : Type
inst✝ : Order α
x y : α
h : ¬Ordering.lt = Ordering.lt
cmp : compare x y = Ordering.gt
this : compare y x = Ordering.lt
⊢ Ordering.gt.isLE = true
Theorem: Order.le_of_not_lt
Proof state before:
α : Type
inst✝ : Order α
x y : α
h : ¬Ordering.lt = Ordering.lt
cmp : compare x y = Ordering.gt
this : compare y x = Ordering.lt
⊢ Ordering.gt.isLE = true
Tactic:
contradiction
Proof state after:
no goals
Theorem: Order.le_of_not_lt
Proof state before:
α : Type
inst✝ : Order α
x y : α
h : ¬compare y x = Ordering.lt
cmp : compare x y = Ordering.gt
⊢ compare y x = Ordering.lt
Tactic:
rw [←symm, cmp]
Proof state after:
α : Type
inst✝ : Order α
x y : α
h : ¬compare y x = Ordering.lt
cmp : compare x y = Ordering.gt
⊢ Ordering.gt.swap = Ordering.lt
Theorem: Order.le_of_not_lt
Proof state before:
α : Type
inst✝ : Order α
x y : α
h : ¬compare y x = Ordering.lt
cmp : compare x y = Ordering.gt
⊢ Ordering.gt.swap = Ordering.lt
Tactic:
decide
Proof state after:
no goals
Theorem: Order.not_lt_of_le
Proof state before:
α : Type
inst✝ : Order α
x y : α
h : x ≤ y
⊢ ¬y < x
Tactic:
match cmp : compare x y with
| .lt | .eq =>
  simp [ltOfOrd]
  rw [←symm, cmp]
  decide
| .gt =>
  simp [leOfOrd, cmp] at h
  contradiction
Proof state after:
no goals
Theorem: Order.not_lt_of_le
Proof state before:
α : Type
inst✝ : Order α
x y : α
h : x ≤ y
cmp : compare x y = Ordering.eq
⊢ ¬y < x
Tactic:
simp [ltOfOrd]
Proof state after:
α : Type
inst✝ : Order α
x y : α
h : x ≤ y
cmp : compare x y = Ordering.eq
⊢ ¬compare y x = Ordering.lt
Theorem: Order.not_lt_of_le
Proof state before:
α : Type
inst✝ : Order α
x y : α
h : x ≤ y
cmp : compare x y = Ordering.eq
⊢ ¬compare y x = Ordering.lt
Tactic:
rw [←symm, cmp]
Proof state after:
α : Type
inst✝ : Order α
x y : α
h : x ≤ y
cmp : compare x y = Ordering.eq
⊢ ¬Ordering.eq.swap = Ordering.lt
Theorem: Order.not_lt_of_le
Proof state before:
α : Type
inst✝ : Order α
x y : α
h : x ≤ y
cmp : compare x y = Ordering.eq
⊢ ¬Ordering.eq.swap = Ordering.lt
Tactic:
decide
Proof state after:
no goals
Theorem: Order.not_lt_of_le
Proof state before:
α : Type
inst✝ : Order α
x y : α
h : x ≤ y
cmp : compare x y = Ordering.gt
⊢ ¬y < x
Tactic:
simp [leOfOrd, cmp] at h
Proof state after:
α : Type
inst✝ : Order α
x y : α
cmp : compare x y = Ordering.gt
h : Ordering.gt.isLE = true
⊢ ¬y < x
Theorem: Order.not_lt_of_le
Proof state before:
α : Type
inst✝ : Order α
x y : α
cmp : compare x y = Ordering.gt
h : Ordering.gt.isLE = true
⊢ ¬y < x
Tactic:
contradiction
Proof state after:
no goals
Theorem: Order.le_of_lt
Proof state before:
α : Type
inst✝ : Order α
x y : α
h : x < y
⊢ x ≤ y
Tactic:
show (compare x y).isLE
Proof state after:
α : Type
inst✝ : Order α
x y : α
h : x < y
⊢ (compare x y).isLE = true
Theorem: Order.le_of_lt
Proof state before:
α : Type
inst✝ : Order α
x y : α
h : x < y
⊢ (compare x y).isLE = true
Tactic:
simp [ltOfOrd] at h
Proof state after:
α : Type
inst✝ : Order α
x y : α
h : compare x y = Ordering.lt
⊢ (compare x y).isLE = true
Theorem: Order.le_of_lt
Proof state before:
α : Type
inst✝ : Order α
x y : α
h : compare x y = Ordering.lt
⊢ (compare x y).isLE = true
Tactic:
match cmp : compare x y with
| .lt => decide
| .eq | .gt =>
  rw [cmp] at h
  contradiction
Proof state after:
no goals
Theorem: Order.le_of_lt
Proof state before:
α : Type
inst✝ : Order α
x y : α
h cmp : compare x y = Ordering.lt
⊢ Ordering.lt.isLE = true
Tactic:
decide
Proof state after:
no goals
Theorem: Order.le_of_lt
Proof state before:
α : Type
inst✝ : Order α
x y : α
h : compare x y = Ordering.lt
cmp : compare x y = Ordering.gt
⊢ Ordering.gt.isLE = true
Tactic:
rw [cmp] at h
Proof state after:
α : Type
inst✝ : Order α
x y : α
h : Ordering.gt = Ordering.lt
cmp : compare x y = Ordering.gt
⊢ Ordering.gt.isLE = true
Theorem: Order.le_of_lt
Proof state before:
α : Type
inst✝ : Order α
x y : α
h : Ordering.gt = Ordering.lt
cmp : compare x y = Ordering.gt
⊢ Ordering.gt.isLE = true
Tactic:
contradiction
Proof state after:
no goals
Theorem: partitionImpl.loop_invariant
Proof state before:
case base
α : Type
inst✝ : Ord α
n : Nat
first✝ i✝ j✝ last : Fin n
arr : Vec α n
first i j : Fin n
fi : first ≤ i
ij✝ : i ≤ j
h : ¬first < i
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:
revert result
Proof state after:
case base
α : Type
inst✝ : Ord α
n : Nat
first✝ i✝ j✝ last : Fin n
arr : Vec α n
first i j : Fin n
fi : first ≤ i
ij✝ : i ≤ j
h : ¬first < i
inv : LoopInvariant arr first i j last
⊢ ∀ (result : { mid // first ≤ mid ∧ mid ≤ j } × Vec α n),
    partitionImpl arr first i j fi ij✝ = result → LoopInvariant result.snd first first ⟨↑result.fst.val, ⋯⟩ last