internlm/Lean-Github huggingface dataset:
Theorem: Permutation.transpos_conj
Proof state before:
case refl
n : Nat
i j : Fin n
x : Permutation n
hk : ↑j < n
⊢ x[↑(if ↑j = ↑j then i else if ↑i = ↑j then j else { val := ↑j, isLt := hk })] =
    if ↑x[↑j] = ↑x[↑j] then x[↑i] else if ↑x[↑i] = ↑x[↑j] then x[↑j] else { val := ↑x[↑j], isLt := (_ : ↑x[↑j] < n) }
Tactic:
simp only [if_pos]
Proof state after:
no goals
Theorem: Permutation.transpos_conj
Proof state before:
n : Nat
i j : Fin n
x : Permutation n
k : Nat
hk : k < n
hjk : ¬↑j = k
⊢ x[↑(if ↑j = k then i else if ↑i = k then j else { val := k, isLt := hk })] =
    if ↑x[↑j] = ↑x[k] then x[↑i] else if ↑x[↑i] = ↑x[k] then x[↑j] else { val := ↑x[k], isLt := (_ : ↑x[k] < n) }
Tactic:
have : x[j.1].1 ≠ x[k].1 :=
  fun h => hjk <| x.get_inj _ _ (Fin.eq_of_val_eq h)
Proof state after:
n : Nat
i j : Fin n
x : Permutation n
k : Nat
hk : k < n
hjk : ¬↑j = k
this : ↑x[↑j] ≠ ↑x[k]
⊢ x[↑(if ↑j = k then i else if ↑i = k then j else { val := k, isLt := hk })] =
    if ↑x[↑j] = ↑x[k] then x[↑i] else if ↑x[↑i] = ↑x[k] then x[↑j] else { val := ↑x[k], isLt := (_ : ↑x[k] < n) }
Theorem: Permutation.transpos_conj
Proof state before:
n : Nat
i j : Fin n
x : Permutation n
k : Nat
hk : k < n
hjk : ¬↑j = k
this : ↑x[↑j] ≠ ↑x[k]
⊢ x[↑(if ↑j = k then i else if ↑i = k then j else { val := k, isLt := hk })] =
    if ↑x[↑j] = ↑x[k] then x[↑i] else if ↑x[↑i] = ↑x[k] then x[↑j] else { val := ↑x[k], isLt := (_ : ↑x[k] < n) }
Tactic:
simp only [hjk, this, if_neg]
Proof state after:
n : Nat
i j : Fin n
x : Permutation n
k : Nat
hk : k < n
hjk : ¬↑j = k
this : ↑x[↑j] ≠ ↑x[k]
⊢ x[↑(if ↑i = k then j else { val := k, isLt := hk })] =
    if ↑x[↑i] = ↑x[k] then x[↑j] else { val := ↑x[k], isLt := (_ : ↑x[k] < n) }
Theorem: Permutation.transpos_conj
Proof state before:
n : Nat
i j : Fin n
x : Permutation n
k : Nat
hk : k < n
hjk : ¬↑j = k
this : ↑x[↑j] ≠ ↑x[k]
⊢ x[↑(if ↑i = k then j else { val := k, isLt := hk })] =
    if ↑x[↑i] = ↑x[k] then x[↑j] else { val := ↑x[k], isLt := (_ : ↑x[k] < n) }
Tactic:
if hik : i.1 = k then
  cases hik; simp only [if_pos]
else
  have : x[i.1].1 ≠ x[k].1 :=
    fun h => hik <| x.get_inj _ _ (Fin.eq_of_val_eq h)
  simp only [hik, this, if_neg]
Proof state after:
no goals
Theorem: Permutation.transpos_conj
Proof state before:
n : Nat
i j : Fin n
x : Permutation n
k : Nat
hk : k < n
hjk : ¬↑j = k
this : ↑x[↑j] ≠ ↑x[k]
hik : ↑i = k
⊢ x[↑(if ↑i = k then j else { val := k, isLt := hk })] =
    if ↑x[↑i] = ↑x[k] then x[↑j] else { val := ↑x[k], isLt := (_ : ↑x[k] < n) }
Tactic:
cases hik
Proof state after:
case refl
n : Nat
i j : Fin n
x : Permutation n
hk : ↑i < n
hjk : ¬↑j = ↑i
this : ↑x[↑j] ≠ ↑x[↑i]
⊢ x[↑(if ↑i = ↑i then j else { val := ↑i, isLt := hk })] =
    if ↑x[↑i] = ↑x[↑i] then x[↑j] else { val := ↑x[↑i], isLt := (_ : ↑x[↑i] < n) }
Theorem: Permutation.transpos_conj
Proof state before:
case refl
n : Nat
i j : Fin n
x : Permutation n
hk : ↑i < n
hjk : ¬↑j = ↑i
this : ↑x[↑j] ≠ ↑x[↑i]
⊢ x[↑(if ↑i = ↑i then j else { val := ↑i, isLt := hk })] =
    if ↑x[↑i] = ↑x[↑i] then x[↑j] else { val := ↑x[↑i], isLt := (_ : ↑x[↑i] < n) }
Tactic:
simp only [if_pos]
Proof state after:
no goals
Theorem: Permutation.transpos_conj
Proof state before:
n : Nat
i j : Fin n
x : Permutation n
k : Nat
hk : k < n
hjk : ¬↑j = k
this : ↑x[↑j] ≠ ↑x[k]
hik : ¬↑i = k
⊢ x[↑(if ↑i = k then j else { val := k, isLt := hk })] =
    if ↑x[↑i] = ↑x[k] then x[↑j] else { val := ↑x[k], isLt := (_ : ↑x[k] < n) }
Tactic:
have : x[i.1].1 ≠ x[k].1 :=
  fun h => hik <| x.get_inj _ _ (Fin.eq_of_val_eq h)
Proof state after:
n : Nat
i j : Fin n
x : Permutation n
k : Nat
hk : k < n
hjk : ¬↑j = k
this✝ : ↑x[↑j] ≠ ↑x[k]
hik : ¬↑i = k
this : ↑x[↑i] ≠ ↑x[k]
⊢ x[↑(if ↑i = k then j else { val := k, isLt := hk })] =
    if ↑x[↑i] = ↑x[k] then x[↑j] else { val := ↑x[k], isLt := (_ : ↑x[k] < n) }
Theorem: Permutation.transpos_conj
Proof state before:
n : Nat
i j : Fin n
x : Permutation n
k : Nat
hk : k < n
hjk : ¬↑j = k
this✝ : ↑x[↑j] ≠ ↑x[k]
hik : ¬↑i = k
this : ↑x[↑i] ≠ ↑x[k]
⊢ x[↑(if ↑i = k then j else { val := k, isLt := hk })] =
    if ↑x[↑i] = ↑x[k] then x[↑j] else { val := ↑x[k], isLt := (_ : ↑x[k] < n) }
Tactic:
simp only [hik, this, if_neg]
Proof state after:
no goals
Theorem: Permutation.get_transposAdj_self
Proof state before:
n i : Nat
h : i + 1 < n
h' : i < n
⊢ (transposAdj i h)[i] = { val := i + 1, isLt := h }
Tactic:
simp only [transposAdj, get_transpos, i.succ_ne_self, if_neg, if_pos]
Proof state after:
no goals
Theorem: Permutation.get_transAdj_succ
Proof state before:
n i : Nat
h : i + 1 < n
⊢ (transposAdj i h)[i + 1] = { val := i, isLt := (_ : i < n) }
Tactic:
simp only [transposAdj, get_transpos, if_pos]
Proof state after:
no goals
Theorem: Permutation.get_transposAdj_of_lt
Proof state before:
n i : Nat
h : i + 1 < n
j : Nat
hj : j < i
hj' : j < n
⊢ (transposAdj i h)[j] = { val := j, isLt := hj' }
Tactic:
simp only [transposAdj, get_transpos]
Proof state after:
n i : Nat
h : i + 1 < n
j : Nat
hj : j < i
hj' : j < n
⊢ (if i + 1 = j then { val := i, isLt := (_ : i < n) }
    else
      if i = j then { val := i + 1, isLt := h }
      else
        { val := j,
          isLt :=
            (_ : (fun x i => i < n) (transpos { val := i, isLt := (_ : i < n) } { val := i + 1, isLt := h }) j) }) =
    { val := j, isLt := hj' }
Theorem: Permutation.get_transposAdj_of_lt
Proof state before:
n i : Nat
h : i + 1 < n
j : Nat
hj : j < i
hj' : j < n
⊢ (if i + 1 = j then { val := i, isLt := (_ : i < n) }
    else
      if i = j then { val := i + 1, isLt := h }
      else
        { val := j,
          isLt :=
            (_ : (fun x i => i < n) (transpos { val := i, isLt := (_ : i < n) } { val := i + 1, isLt := h }) j) }) =
    { val := j, isLt := hj' }
Tactic:
simp only [Nat.ne_of_gt <| .step hj, Nat.ne_of_gt hj, if_neg]
Proof state after:
no goals
Theorem: Permutation.get_transposAdj_of_gt
Proof state before:
n i : Nat
h : i + 1 < n
j : Nat
hj : j > i + 1
hj' : j < n
⊢ (transposAdj i h)[j] = { val := j, isLt := hj' }
Tactic:
simp only [transposAdj, get_transpos]
Proof state after:
n i : Nat
h : i + 1 < n
j : Nat
hj : j > i + 1
hj' : j < n
⊢ (if i + 1 = j then { val := i, isLt := (_ : i < n) }
    else
      if i = j then { val := i + 1, isLt := h }
      else
        { val := j,
          isLt :=
            (_ : (fun x i => i < n) (transpos { val := i, isLt := (_ : i < n) } { val := i + 1, isLt := h }) j) }) =
    { val := j, isLt := hj' }
Theorem: Permutation.get_transposAdj_of_gt
Proof state before:
n i : Nat
h : i + 1 < n
j : Nat
hj : j > i + 1
hj' : j < n
⊢ (if i + 1 = j then { val := i, isLt := (_ : i < n) }
    else
      if i = j then { val := i + 1, isLt := h }
      else
        { val := j,
          isLt :=
            (_ : (fun x i => i < n) (transpos { val := i, isLt := (_ : i < n) } { val := i + 1, isLt := h }) j) }) =
    { val := j, isLt := hj' }
Tactic:
simp only [Nat.ne_of_lt hj, Nat.ne_of_lt <| Nat.lt_of_succ_lt hj, if_neg]
Proof state after:
no goals
Theorem: Permutation.get_cyclic_not_mem
Proof state before:
n : Nat
l : List (Fin n)
i : Fin n
h : ¬i ∈ l
⊢ (cyclic l)[↑i] = i
Tactic:
cases l with
| nil => exact get_one i.1
| cons j l =>
  dsimp [cyclic]
  simp only [List.mem_cons, not_or] at h
  suffices ∀ (y : Permutation n), (l.foldr _ y)[i.1] = y[i.1] by
    rewrite [this 1]; exact get_one i.1
  induction l with
  | nil => intros; rfl
  | cons k l IH =>
    intro y
    simp only [List.mem_cons, not_or] at h 
    specialize IH ⟨h.1,h.2.2⟩ y
    dsimp only [List.foldr]
    rewrite [get_swap, if_neg (Fin.val_ne_of_ne <| Ne.symm h.2.1), if_neg (Fin.val_ne_of_ne <| Ne.symm h.1)]
    exact IH
Proof state after:
no goals
Theorem: Permutation.get_cyclic_not_mem
Proof state before:
case nil
n : Nat
i : Fin n
h : ¬i ∈ []
⊢ (cyclic [])[↑i] = i
Tactic:
exact get_one i.1
Proof state after:
no goals
Theorem: Permutation.get_cyclic_not_mem
Proof state before:
case cons
n : Nat
i j : Fin n
l : List (Fin n)
h : ¬i ∈ j :: l
⊢ (cyclic (j :: l))[↑i] = i
Tactic:
dsimp [cyclic]
Proof state after:
case cons
n : Nat
i j : Fin n
l : List (Fin n)
h : ¬i ∈ j :: l
⊢ (List.foldr (fun j_1 x => swap x j j_1) 1 l)[↑i] = i
Theorem: Permutation.get_cyclic_not_mem
Proof state before:
case cons
n : Nat
i j : Fin n
l : List (Fin n)
h : ¬i ∈ j :: l
⊢ (List.foldr (fun j_1 x => swap x j j_1) 1 l)[↑i] = i
Tactic:
simp only [List.mem_cons, not_or] at h
Proof state after:
case cons
n : Nat
i j : Fin n
l : List (Fin n)
h : ¬i = j ∧ ¬i ∈ l
⊢ (List.foldr (fun j_1 x => swap x j j_1) 1 l)[↑i] = i
Theorem: Permutation.get_cyclic_not_mem
Proof state before:
case cons
n : Nat
i j : Fin n
l : List (Fin n)
h : ¬i = j ∧ ¬i ∈ l
⊢ (List.foldr (fun j_1 x => swap x j j_1) 1 l)[↑i] = i
Tactic:
suffices ∀ (y : Permutation n), (l.foldr _ y)[i.1] = y[i.1] by
  rewrite [this 1]; exact get_one i.1
Proof state after:
case cons
n : Nat
i j : Fin n
l : List (Fin n)
h : ¬i = j ∧ ¬i ∈ l
⊢ ∀ (y : Permutation n), (List.foldr (fun j_1 x => swap x j j_1) y l)[↑i] = y[↑i]
Theorem: Permutation.get_cyclic_not_mem
Proof state before:
case cons
n : Nat
i j : Fin n
l : List (Fin n)
h : ¬i = j ∧ ¬i ∈ l
⊢ ∀ (y : Permutation n), (List.foldr (fun j_1 x => swap x j j_1) y l)[↑i] = y[↑i]
Tactic:
induction l with
| nil => intros; rfl
| cons k l IH =>
  intro y
  simp only [List.mem_cons, not_or] at h 
  specialize IH ⟨h.1,h.2.2⟩ y
  dsimp only [List.foldr]
  rewrite [get_swap, if_neg (Fin.val_ne_of_ne <| Ne.symm h.2.1), if_neg (Fin.val_ne_of_ne <| Ne.symm h.1)]
  exact IH
Proof state after:
no goals
Theorem: Permutation.get_cyclic_not_mem
Proof state before:
n : Nat
i j : Fin n
l : List (Fin n)
h : ¬i = j ∧ ¬i ∈ l
this : ∀ (y : Permutation n), (List.foldr (?m.45215 y) y l)[↑i] = y[↑i]
⊢ (List.foldr (fun j_1 x => swap x j j_1) 1 l)[↑i] = i
Tactic:
rewrite [this 1]
Proof state after:
n : Nat
i j : Fin n
l : List (Fin n)
h : ¬i = j ∧ ¬i ∈ l
this : ∀ (y : Permutation n), (List.foldr (fun j_1 x => swap x j j_1) y l)[↑i] = y[↑i]
⊢ 1[↑i] = i
Theorem: Permutation.get_cyclic_not_mem
Proof state before:
n : Nat
i j : Fin n
l : List (Fin n)
h : ¬i = j ∧ ¬i ∈ l
this : ∀ (y : Permutation n), (List.foldr (fun j_1 x => swap x j j_1) y l)[↑i] = y[↑i]
⊢ 1[↑i] = i
Tactic:
exact get_one i.1
Proof state after:
no goals
Theorem: Permutation.get_cyclic_not_mem
Proof state before:
case cons.nil
n : Nat
i j : Fin n
h : ¬i = j ∧ ¬i ∈ []
⊢ ∀ (y : Permutation n), (List.foldr (fun j_1 x => swap x j j_1) y [])[↑i] = y[↑i]
Tactic:
intros
Proof state after:
case cons.nil
n : Nat
i j : Fin n
h : ¬i = j ∧ ¬i ∈ []
y✝ : Permutation n
⊢ (List.foldr (fun j_1 x => swap x j j_1) y✝ [])[↑i] = y✝[↑i]
Theorem: Permutation.get_cyclic_not_mem
Proof state before:
case cons.nil
n : Nat
i j : Fin n
h : ¬i = j ∧ ¬i ∈ []
y✝ : Permutation n
⊢ (List.foldr (fun j_1 x => swap x j j_1) y✝ [])[↑i] = y✝[↑i]
Tactic:
rfl
Proof state after:
no goals
Theorem: Permutation.get_cyclic_not_mem
Proof state before:
case cons.cons
n : Nat
i j k : Fin n
l : List (Fin n)
IH : ¬i = j ∧ ¬i ∈ l → ∀ (y : Permutation n), (List.foldr (fun j_1 x => swap x j j_1) y l)[↑i] = y[↑i]
h : ¬i = j ∧ ¬i ∈ k :: l
⊢ ∀ (y : Permutation n), (List.foldr (fun j_1 x => swap x j j_1) y (k :: l))[↑i] = y[↑i]
Tactic:
intro y
Proof state after:
case cons.cons
n : Nat
i j k : Fin n
l : List (Fin n)
IH : ¬i = j ∧ ¬i ∈ l → ∀ (y : Permutation n), (List.foldr (fun j_1 x => swap x j j_1) y l)[↑i] = y[↑i]
h : ¬i = j ∧ ¬i ∈ k :: l
y : Permutation n
⊢ (List.foldr (fun j_1 x => swap x j j_1) y (k :: l))[↑i] = y[↑i]
Theorem: Permutation.get_cyclic_not_mem
Proof state before:
case cons.cons
n : Nat
i j k : Fin n
l : List (Fin n)
IH : ¬i = j ∧ ¬i ∈ l → ∀ (y : Permutation n), (List.foldr (fun j_1 x => swap x j j_1) y l)[↑i] = y[↑i]
h : ¬i = j ∧ ¬i ∈ k :: l
y : Permutation n
⊢ (List.foldr (fun j_1 x => swap x j j_1) y (k :: l))[↑i] = y[↑i]
Tactic:
simp only [List.mem_cons, not_or] at h
Proof state after:
case cons.cons
n : Nat
i j k : Fin n
l : List (Fin n)
IH : ¬i = j ∧ ¬i ∈ l → ∀ (y : Permutation n), (List.foldr (fun j_1 x => swap x j j_1) y l)[↑i] = y[↑i]
y : Permutation n
h : ¬i = j ∧ ¬i = k ∧ ¬i ∈ l
⊢ (List.foldr (fun j_1 x => swap x j j_1) y (k :: l))[↑i] = y[↑i]
Theorem: Permutation.get_cyclic_not_mem
Proof state before:
case cons.cons
n : Nat
i j k : Fin n
l : List (Fin n)
IH : ¬i = j ∧ ¬i ∈ l → ∀ (y : Permutation n), (List.foldr (fun j_1 x => swap x j j_1) y l)[↑i] = y[↑i]
y : Permutation n
h : ¬i = j ∧ ¬i = k ∧ ¬i ∈ l
⊢ (List.foldr (fun j_1 x => swap x j j_1) y (k :: l))[↑i] = y[↑i]
Tactic:
specialize IH ⟨h.1,h.2.2⟩ y
Proof state after:
case cons.cons
n : Nat
i j k : Fin n
l : List (Fin n)
y : Permutation n
h : ¬i = j ∧ ¬i = k ∧ ¬i ∈ l
IH : (List.foldr (fun j_1 x => swap x j j_1) y l)[↑i] = y[↑i]
⊢ (List.foldr (fun j_1 x => swap x j j_1) y (k :: l))[↑i] = y[↑i]
Theorem: Permutation.get_cyclic_not_mem
Proof state before:
case cons.cons
n : Nat
i j k : Fin n
l : List (Fin n)
y : Permutation n
h : ¬i = j ∧ ¬i = k ∧ ¬i ∈ l
IH : (List.foldr (fun j_1 x => swap x j j_1) y l)[↑i] = y[↑i]
⊢ (List.foldr (fun j_1 x => swap x j j_1) y (k :: l))[↑i] = y[↑i]
Tactic:
dsimp only [List.foldr]
Proof state after:
case cons.cons
n : Nat
i j k : Fin n
l : List (Fin n)
y : Permutation n
h : ¬i = j ∧ ¬i = k ∧ ¬i ∈ l
IH : (List.foldr (fun j_1 x => swap x j j_1) y l)[↑i] = y[↑i]
⊢ (swap (List.foldr (fun j_1 x => swap x j j_1) y l) j k)[↑i] = y[↑i]
Theorem: Permutation.get_cyclic_not_mem
Proof state before:
case cons.cons
n : Nat
i j k : Fin n
l : List (Fin n)
y : Permutation n
h : ¬i = j ∧ ¬i = k ∧ ¬i ∈ l
IH : (List.foldr (fun j_1 x => swap x j j_1) y l)[↑i] = y[↑i]
⊢ (swap (List.foldr (fun j_1 x => swap x j j_1) y l) j k)[↑i] = y[↑i]
Tactic:
rewrite [get_swap, if_neg (Fin.val_ne_of_ne <| Ne.symm h.2.1), if_neg (Fin.val_ne_of_ne <| Ne.symm h.1)]
Proof state after:
case cons.cons
n : Nat
i j k : Fin n
l : List (Fin n)
y : Permutation n
h : ¬i = j ∧ ¬i = k ∧ ¬i ∈ l
IH : (List.foldr (fun j_1 x => swap x j j_1) y l)[↑i] = y[↑i]
⊢ (List.foldr (fun j_1 x => swap x j j_1) y l)[↑i] = y[↑i]
Theorem: Permutation.get_cyclic_not_mem
Proof state before:
case cons.cons
n : Nat
i j k : Fin n
l : List (Fin n)
y : Permutation n
h : ¬i = j ∧ ¬i = k ∧ ¬i ∈ l
IH : (List.foldr (fun j_1 x => swap x j j_1) y l)[↑i] = y[↑i]
⊢ (List.foldr (fun j_1 x => swap x j j_1) y l)[↑i] = y[↑i]
Tactic:
exact IH
Proof state after:
no goals
Theorem: Array.size_append
Proof state before:
α : Type u
as bs : Array α
⊢ size (as ++ bs) = size as + size bs
Tactic:
dsimp [size]
Proof state after:
α : Type u
as bs : Array α
⊢ List.length (as ++ bs).data = List.length as.data + List.length bs.data
Theorem: Array.size_append
Proof state before:
α : Type u
as bs : Array α
⊢ List.length (as ++ bs).data = List.length as.data + List.length bs.data
Tactic:
rw [append_data, List.length_append]
Proof state after:
no goals
Theorem: Array.size_shrink_loop
Proof state before:
α : Type u
as : Array α
k : Nat
h : k ≤ size as
⊢ size (shrink.loop k as) = size as - k
Tactic:
induction k generalizing as with
| zero => rfl
| succ k IH =>
  dsimp [shrink.loop]
  have : as.size = as.pop.size + 1 := by
    rw [as.size_pop, Nat.sub_add_cancel (trans (r:=LE.le (α:=Nat)) (s:=LT.lt (α:=Nat)) k.zero_le h)]
  rewrite [this] at h ⊢
  rewrite [IH as.pop (Nat.le_of_succ_le_succ h)]
  simp only [Nat.succ_sub_succ_eq_sub]
Proof state after:
no goals
Theorem: Array.size_shrink_loop
Proof state before:
case zero
α : Type u
as : Array α
h : Nat.zero ≤ size as
⊢ size (shrink.loop Nat.zero as) = size as - Nat.zero
Tactic:
rfl
Proof state after:
no goals
Theorem: Array.size_shrink_loop
Proof state before:
case succ
α : Type u
k : Nat
IH : ∀ (as : Array α), k ≤ size as → size (shrink.loop k as) = size as - k
as : Array α
h : Nat.succ k ≤ size as
⊢ size (shrink.loop (Nat.succ k) as) = size as - Nat.succ k
Tactic:
dsimp [shrink.loop]
Proof state after:
case succ
α : Type u
k : Nat
IH : ∀ (as : Array α), k ≤ size as → size (shrink.loop k as) = size as - k
as : Array α
h : Nat.succ k ≤ size as
⊢ size (shrink.loop k (pop as)) = size as - Nat.succ k
Theorem: Array.size_shrink_loop
Proof state before:
case succ
α : Type u
k : Nat
IH : ∀ (as : Array α), k ≤ size as → size (shrink.loop k as) = size as - k
as : Array α
h : Nat.succ k ≤ size as
⊢ size (shrink.loop k (pop as)) = size as - Nat.succ k
Tactic:
have : as.size = as.pop.size + 1 := by
  rw [as.size_pop, Nat.sub_add_cancel (trans (r:=LE.le (α:=Nat)) (s:=LT.lt (α:=Nat)) k.zero_le h)]
Proof state after:
case succ
α : Type u
k : Nat
IH : ∀ (as : Array α), k ≤ size as → size (shrink.loop k as) = size as - k
as : Array α
h : Nat.succ k ≤ size as
this : size as = size (pop as) + 1
⊢ size (shrink.loop k (pop as)) = size as - Nat.succ k
Theorem: Array.size_shrink_loop
Proof state before:
case succ
α : Type u
k : Nat
IH : ∀ (as : Array α), k ≤ size as → size (shrink.loop k as) = size as - k
as : Array α
h : Nat.succ k ≤ size as
this : size as = size (pop as) + 1
⊢ size (shrink.loop k (pop as)) = size as - Nat.succ k
Tactic:
rewrite [this] at h ⊢
Proof state after:
case succ
α : Type u
k : Nat
IH : ∀ (as : Array α), k ≤ size as → size (shrink.loop k as) = size as - k
as : Array α
h : Nat.succ k ≤ size (pop as) + 1
this : size as = size (pop as) + 1
⊢ size (shrink.loop k (pop as)) = size (pop as) + 1 - Nat.succ k
Theorem: Array.size_shrink_loop
Proof state before:
case succ
α : Type u
k : Nat
IH : ∀ (as : Array α), k ≤ size as → size (shrink.loop k as) = size as - k
as : Array α
h : Nat.succ k ≤ size (pop as) + 1
this : size as = size (pop as) + 1
⊢ size (shrink.loop k (pop as)) = size (pop as) + 1 - Nat.succ k
Tactic:
rewrite [IH as.pop (Nat.le_of_succ_le_succ h)]
Proof state after:
case succ
α : Type u
k : Nat
IH : ∀ (as : Array α), k ≤ size as → size (shrink.loop k as) = size as - k
as : Array α
h : Nat.succ k ≤ size (pop as) + 1
this : size as = size (pop as) + 1
⊢ size (pop as) - k = size (pop as) + 1 - Nat.succ k
Theorem: Array.size_shrink_loop
Proof state before:
case succ
α : Type u
k : Nat
IH : ∀ (as : Array α), k ≤ size as → size (shrink.loop k as) = size as - k
as : Array α
h : Nat.succ k ≤ size (pop as) + 1
this : size as = size (pop as) + 1
⊢ size (pop as) - k = size (pop as) + 1 - Nat.succ k
Tactic:
simp only [Nat.succ_sub_succ_eq_sub]
Proof state after:
no goals
Theorem: Array.size_shrink_loop
Proof state before:
α : Type u
k : Nat
IH : ∀ (as : Array α), k ≤ size as → size (shrink.loop k as) = size as - k
as : Array α
h : Nat.succ k ≤ size as
⊢ size as = size (pop as) + 1
Tactic:
rw [as.size_pop, Nat.sub_add_cancel (trans (r:=LE.le (α:=Nat)) (s:=LT.lt (α:=Nat)) k.zero_le h)]
Proof state after:
no goals
Theorem: Array.size_shrink
Proof state before:
α : Type u
as : Array α
n : Nat
h : n ≤ size as
⊢ size (shrink as n) = n
Tactic:
refine Eq.trans (size_shrink_loop as ?_) ?_
Proof state after:
case refine_1
α : Type u
as : Array α
n : Nat
h : n ≤ size as
⊢ size as - n ≤ size as

case refine_2
α : Type u
as : Array α
n : Nat
h : n ≤ size as
⊢ size as - (size as - n) = n
Theorem: Array.size_shrink
Proof state before:
case refine_1
α : Type u
as : Array α
n : Nat
h : n ≤ size as
⊢ size as - n ≤ size as

case refine_2
α : Type u
as : Array α
n : Nat
h : n ≤ size as
⊢ size as - (size as - n) = n
Tactic:
. exact as.size.sub_le_self n
Proof state after:
case refine_2
α : Type u
as : Array α
n : Nat
h : n ≤ size as
⊢ size as - (size as - n) = n
Theorem: Array.size_shrink
Proof state before:
case refine_2
α : Type u
as : Array α
n : Nat
h : n ≤ size as
⊢ size as - (size as - n) = n
Tactic:
. exact Nat.sub_sub_self h
Proof state after:
no goals
Theorem: Array.size_shrink
Proof state before:
case refine_1
α : Type u
as : Array α
n : Nat
h : n ≤ size as
⊢ size as - n ≤ size as
Tactic:
exact as.size.sub_le_self n
Proof state after:
no goals
Theorem: Array.size_shrink
Proof state before:
case refine_2
α : Type u
as : Array α
n : Nat
h : n ≤ size as
⊢ size as - (size as - n) = n
Tactic:
exact Nat.sub_sub_self h
Proof state after:
no goals
Theorem: Array.any_eq_any_data
Proof state before:
α : Type u
as : Array α
p : α → Bool
⊢ any as p 0 (size as) = List.any as.data p
Tactic:
dsimp [any, anyM]
Proof state after:
α : Type u
as : Array α
p : α → Bool
⊢ Id.run
      (if h : size as ≤ size as then anyM.loop p as (size as) h 0
      else anyM.loop p as (size as) (_ : size as ≤ size as) 0) =
    List.any as.data p
Theorem: Array.any_eq_any_data
Proof state before:
α : Type u
as : Array α
p : α → Bool
⊢ Id.run
      (if h : size as ≤ size as then anyM.loop p as (size as) h 0
      else anyM.loop p as (size as) (_ : size as ≤ size as) 0) =
    List.any as.data p
Tactic:
simp
Proof state after:
α : Type u
as : Array α
p : α → Bool
⊢ Id.run (anyM.loop p as (size as) (_ : size as ≤ size as) 0) = List.any as.data p
Theorem: Array.any_eq_any_data
Proof state before:
α : Type u
as : Array α
p : α → Bool
⊢ Id.run (anyM.loop p as (size as) (_ : size as ≤ size as) 0) = List.any as.data p
Tactic:
conv => rhs; change (as.data.drop 0).any p
Proof state after:
α : Type u
as : Array α
p : α → Bool
⊢ Id.run (anyM.loop p as (size as) (_ : size as ≤ size as) 0) = List.any (List.drop 0 as.data) p
Theorem: Array.any_eq_any_data
Proof state before:
α : Type u
as : Array α
p : α → Bool
⊢ Id.run (anyM.loop p as (size as) (_ : size as ≤ size as) 0) = List.any (List.drop 0 as.data) p
Tactic:
refine Nat.decreasing_induction (m:=0) (n:=as.size) ?_ ?_ as.size.zero_le
Proof state after:
case refine_1
α : Type u
as : Array α
p : α → Bool
⊢ ∀ (n : Nat),
    Id.run (anyM.loop p as (size as) (_ : size as ≤ size as) (n + 1)) = List.any (List.drop (n + 1) as.data) p →
      Id.run (anyM.loop p as (size as) (_ : size as ≤ size as) n) = List.any (List.drop n as.data) p

case refine_2
α : Type u
as : Array α
p : α → Bool
⊢ Id.run (anyM.loop p as (size as) (_ : size as ≤ size as) (size as)) = List.any (List.drop (size as) as.data) p
Theorem: Array.any_eq_any_data
Proof state before:
case refine_1
α : Type u
as : Array α
p : α → Bool
⊢ ∀ (n : Nat),
    Id.run (anyM.loop p as (size as) (_ : size as ≤ size as) (n + 1)) = List.any (List.drop (n + 1) as.data) p →
      Id.run (anyM.loop p as (size as) (_ : size as ≤ size as) n) = List.any (List.drop n as.data) p

case refine_2
α : Type u
as : Array α
p : α → Bool
⊢ Id.run (anyM.loop p as (size as) (_ : size as ≤ size as) (size as)) = List.any (List.drop (size as) as.data) p
Tactic:
. intro j IH
  unfold anyM.loop; dsimp
  if hlt : j < as.size then
    rewrite [dif_pos hlt, ← List.get_drop_eq_drop _ _ hlt, List.any_cons, List.getElem_eq_get, ← Array.getElem_eq_data_get]
    if hpj : p (as[j]'hlt) = true then
      rewrite [if_pos hpj, hpj, Bool.true_or]
      rfl
    else
      rw [if_neg hpj, IH, Bool.eq_false_iff.mpr hpj, Bool.false_or]
  else
    rewrite [dif_neg hlt, List.drop_eq_nil_of_le (Nat.le_of_not_lt hlt)]
    rfl
Proof state after:
case refine_2
α : Type u
as : Array α
p : α → Bool
⊢ Id.run (anyM.loop p as (size as) (_ : size as ≤ size as) (size as)) = List.any (List.drop (size as) as.data) p
Theorem: Array.any_eq_any_data
Proof state before:
case refine_2
α : Type u
as : Array α
p : α → Bool
⊢ Id.run (anyM.loop p as (size as) (_ : size as ≤ size as) (size as)) = List.any (List.drop (size as) as.data) p
Tactic:
. unfold anyM.loop; dsimp
  rewrite [dif_neg (Nat.lt_irrefl _), List.drop_eq_nil_of_le .refl]
  rfl
Proof state after:
no goals
Theorem: Array.any_eq_any_data
Proof state before:
case refine_1
α : Type u
as : Array α
p : α → Bool
⊢ ∀ (n : Nat),
    Id.run (anyM.loop p as (size as) (_ : size as ≤ size as) (n + 1)) = List.any (List.drop (n + 1) as.data) p →
      Id.run (anyM.loop p as (size as) (_ : size as ≤ size as) n) = List.any (List.drop n as.data) p
Tactic:
intro j IH
Proof state after:
case refine_1
α : Type u
as : Array α
p : α → Bool
j : Nat
IH : Id.run (anyM.loop p as (size as) (_ : size as ≤ size as) (j + 1)) = List.any (List.drop (j + 1) as.data) p
⊢ Id.run (anyM.loop p as (size as) (_ : size as ≤ size as) j) = List.any (List.drop j as.data) p