internlm/Lean-Github huggingface dataset:
Theorem: SizedArray.get_mapIdx
Proof state before:
case cons.succ
α : Type u
β : Type v
γ : Type w
n n✝ : Nat
a : α
x : SizedArray α n✝
IH : ∀ (f : Fin n✝ → α → β) (i : Nat) {hi : i < n✝}, (mapIdx f x)[i] = f { val := i, isLt := hi } x[i]
f : Fin (n✝ + 1) → α → β
i : Nat
hi : Nat.succ i < n✝ + 1
⊢ (cons (f { val := 0, isLt := (_ : 0 < Nat.succ n✝) } a) (mapIdx (f ∘ Fin.succ) x))[Nat.succ i] =
    f { val := Nat.succ i, isLt := hi } (cons a x)[Nat.succ i]
Tactic:
simp only [Nat.zero_eq, Nat.succ_eq_add_one]
Proof state after:
case cons.succ
α : Type u
β : Type v
γ : Type w
n n✝ : Nat
a : α
x : SizedArray α n✝
IH : ∀ (f : Fin n✝ → α → β) (i : Nat) {hi : i < n✝}, (mapIdx f x)[i] = f { val := i, isLt := hi } x[i]
f : Fin (n✝ + 1) → α → β
i : Nat
hi : Nat.succ i < n✝ + 1
⊢ (cons (f { val := 0, isLt := (_ : 0 < Nat.succ n✝) } a) (mapIdx (f ∘ Fin.succ) x))[i + 1] =
    f { val := i + 1, isLt := hi } (cons a x)[i + 1]
Theorem: SizedArray.get_mapIdx
Proof state before:
case cons.succ
α : Type u
β : Type v
γ : Type w
n n✝ : Nat
a : α
x : SizedArray α n✝
IH : ∀ (f : Fin n✝ → α → β) (i : Nat) {hi : i < n✝}, (mapIdx f x)[i] = f { val := i, isLt := hi } x[i]
f : Fin (n✝ + 1) → α → β
i : Nat
hi : Nat.succ i < n✝ + 1
⊢ (cons (f { val := 0, isLt := (_ : 0 < Nat.succ n✝) } a) (mapIdx (f ∘ Fin.succ) x))[i + 1] =
    f { val := i + 1, isLt := hi } (cons a x)[i + 1]
Tactic:
rw [get_cons_succ (hi₂:=Nat.lt_of_succ_lt_succ hi)]
Proof state after:
case cons.succ
α : Type u
β : Type v
γ : Type w
n n✝ : Nat
a : α
x : SizedArray α n✝
IH : ∀ (f : Fin n✝ → α → β) (i : Nat) {hi : i < n✝}, (mapIdx f x)[i] = f { val := i, isLt := hi } x[i]
f : Fin (n✝ + 1) → α → β
i : Nat
hi : Nat.succ i < n✝ + 1
⊢ (mapIdx (f ∘ Fin.succ) x)[i] = f { val := i + 1, isLt := hi } (cons a x)[i + 1]
Theorem: SizedArray.get_mapIdx
Proof state before:
case cons.succ
α : Type u
β : Type v
γ : Type w
n n✝ : Nat
a : α
x : SizedArray α n✝
IH : ∀ (f : Fin n✝ → α → β) (i : Nat) {hi : i < n✝}, (mapIdx f x)[i] = f { val := i, isLt := hi } x[i]
f : Fin (n✝ + 1) → α → β
i : Nat
hi : Nat.succ i < n✝ + 1
⊢ (mapIdx (f ∘ Fin.succ) x)[i] = f { val := i + 1, isLt := hi } (cons a x)[i + 1]
Tactic:
rw [get_cons_succ (hi₂:=Nat.lt_of_succ_lt_succ hi)]
Proof state after:
case cons.succ
α : Type u
β : Type v
γ : Type w
n n✝ : Nat
a : α
x : SizedArray α n✝
IH : ∀ (f : Fin n✝ → α → β) (i : Nat) {hi : i < n✝}, (mapIdx f x)[i] = f { val := i, isLt := hi } x[i]
f : Fin (n✝ + 1) → α → β
i : Nat
hi : Nat.succ i < n✝ + 1
⊢ (mapIdx (f ∘ Fin.succ) x)[i] = f { val := i + 1, isLt := hi } x[i]
Theorem: SizedArray.get_mapIdx
Proof state before:
case cons.succ
α : Type u
β : Type v
γ : Type w
n n✝ : Nat
a : α
x : SizedArray α n✝
IH : ∀ (f : Fin n✝ → α → β) (i : Nat) {hi : i < n✝}, (mapIdx f x)[i] = f { val := i, isLt := hi } x[i]
f : Fin (n✝ + 1) → α → β
i : Nat
hi : Nat.succ i < n✝ + 1
⊢ (mapIdx (f ∘ Fin.succ) x)[i] = f { val := i + 1, isLt := hi } x[i]
Tactic:
exact IH ..
Proof state after:
no goals
Theorem: SizedArray.findIdx_loop_le
Proof state before:
α : Type u
n : Nat
x : SizedArray α n
p : α → Bool
stop : Nat
h : stop ≤ n
i : Nat
⊢ findIdx.loop x p stop h i ≤ stop
Tactic:
unfold findIdx.loop
Proof state after:
α : Type u
n : Nat
x : SizedArray α n
p : α → Bool
stop : Nat
h : stop ≤ n
i : Nat
⊢ (if hi : i < stop then
      let_fun this := (_ : i < n);
      bif p x[i] then i else findIdx.loop x p stop h (i + 1)
    else stop) ≤
    stop
Theorem: SizedArray.findIdx_loop_le
Proof state before:
α : Type u
n : Nat
x : SizedArray α n
p : α → Bool
stop : Nat
h : stop ≤ n
i : Nat
⊢ (if hi : i < stop then
      let_fun this := (_ : i < n);
      bif p x[i] then i else findIdx.loop x p stop h (i + 1)
    else stop) ≤
    stop
Tactic:
if hi : i < stop then
  rewrite [dif_pos hi]; dsimp
  match p (x[i]'(trans (r:=LT.lt) (s:=LE.le) hi h)) with
  | true => exact Nat.le_of_lt hi
  | false => exact findIdx_loop_le x p stop h (i+1)
else
  rewrite [dif_neg hi]
  exact .refl
Proof state after:
no goals
Theorem: SizedArray.findIdx_loop_le
Proof state before:
α : Type u
n : Nat
x : SizedArray α n
p : α → Bool
stop : Nat
h : stop ≤ n
i : Nat
hi : i < stop
⊢ (if hi : i < stop then
      let_fun this := (_ : i < n);
      bif p x[i] then i else findIdx.loop x p stop h (i + 1)
    else stop) ≤
    stop
Tactic:
rewrite [dif_pos hi]
Proof state after:
α : Type u
n : Nat
x : SizedArray α n
p : α → Bool
stop : Nat
h : stop ≤ n
i : Nat
hi : i < stop
⊢ (let_fun this := (_ : i < n);
    bif p x[i] then i else findIdx.loop x p stop h (i + 1)) ≤
    stop
Theorem: SizedArray.findIdx_loop_le
Proof state before:
α : Type u
n : Nat
x : SizedArray α n
p : α → Bool
stop : Nat
h : stop ≤ n
i : Nat
hi : i < stop
⊢ (let_fun this := (_ : i < n);
    bif p x[i] then i else findIdx.loop x p stop h (i + 1)) ≤
    stop
Tactic:
dsimp
Proof state after:
α : Type u
n : Nat
x : SizedArray α n
p : α → Bool
stop : Nat
h : stop ≤ n
i : Nat
hi : i < stop
⊢ (bif p x[i] then i else findIdx.loop x p stop h (i + 1)) ≤ stop
Theorem: SizedArray.findIdx_loop_le
Proof state before:
α : Type u
n : Nat
x : SizedArray α n
p : α → Bool
stop : Nat
h : stop ≤ n
i : Nat
hi : i < stop
⊢ (bif p x[i] then i else findIdx.loop x p stop h (i + 1)) ≤ stop
Tactic:
match p (x[i]'(trans (r:=LT.lt) (s:=LE.le) hi h)) with
| true => exact Nat.le_of_lt hi
| false => exact findIdx_loop_le x p stop h (i+1)
Proof state after:
no goals
Theorem: SizedArray.findIdx_loop_le
Proof state before:
α : Type u
n : Nat
x : SizedArray α n
p : α → Bool
stop : Nat
h : stop ≤ n
i : Nat
hi : i < stop
⊢ (bif true then i else findIdx.loop x p stop h (i + 1)) ≤ stop
Tactic:
exact Nat.le_of_lt hi
Proof state after:
no goals
Theorem: SizedArray.findIdx_loop_le
Proof state before:
α : Type u
n : Nat
x : SizedArray α n
p : α → Bool
stop : Nat
h : stop ≤ n
i : Nat
hi : i < stop
⊢ (bif false then i else findIdx.loop x p stop h (i + 1)) ≤ stop
Tactic:
exact findIdx_loop_le x p stop h (i+1)
Proof state after:
no goals
Theorem: SizedArray.findIdx_loop_le
Proof state before:
α : Type u
n : Nat
x : SizedArray α n
p : α → Bool
stop : Nat
h : stop ≤ n
i : Nat
hi : ¬i < stop
⊢ (if hi : i < stop then
      let_fun this := (_ : i < n);
      bif p x[i] then i else findIdx.loop x p stop h (i + 1)
    else stop) ≤
    stop
Tactic:
rewrite [dif_neg hi]
Proof state after:
α : Type u
n : Nat
x : SizedArray α n
p : α → Bool
stop : Nat
h : stop ≤ n
i : Nat
hi : ¬i < stop
⊢ stop ≤ stop
Theorem: SizedArray.findIdx_loop_le
Proof state before:
α : Type u
n : Nat
x : SizedArray α n
p : α → Bool
stop : Nat
h : stop ≤ n
i : Nat
hi : ¬i < stop
⊢ stop ≤ stop
Tactic:
exact .refl
Proof state after:
no goals
Theorem: SizedArray.findIdx_loop_ge
Proof state before:
α : Type u
n : Nat
x : SizedArray α n
p : α → Bool
stop : Nat
h : stop ≤ n
i : Nat
hi : i ≤ stop
⊢ findIdx.loop x p stop h i ≥ i
Tactic:
unfold findIdx.loop
Proof state after:
α : Type u
n : Nat
x : SizedArray α n
p : α → Bool
stop : Nat
h : stop ≤ n
i : Nat
hi : i ≤ stop
⊢ (if hi : i < stop then
      let_fun this := (_ : i < n);
      bif p x[i] then i else findIdx.loop x p stop h (i + 1)
    else stop) ≥
    i
Theorem: SizedArray.findIdx_loop_ge
Proof state before:
α : Type u
n : Nat
x : SizedArray α n
p : α → Bool
stop : Nat
h : stop ≤ n
i : Nat
hi : i ≤ stop
⊢ (if hi : i < stop then
      let_fun this := (_ : i < n);
      bif p x[i] then i else findIdx.loop x p stop h (i + 1)
    else stop) ≥
    i
Tactic:
if hi : i < stop then
  rewrite [dif_pos hi]; dsimp
  match p (x[i]'(trans (r:=LT.lt) (s:=LE.le) hi h)) with
  | true => exact Nat.le.refl
  | false =>
    apply Nat.le_of_succ_le
    exact findIdx_loop_ge x p stop h (i+1) hi
else
  rewrite [dif_neg hi]; assumption
Proof state after:
no goals
Theorem: SizedArray.findIdx_loop_ge
Proof state before:
α : Type u
n : Nat
x : SizedArray α n
p : α → Bool
stop : Nat
h : stop ≤ n
i : Nat
hi✝ : i ≤ stop
hi : i < stop
⊢ (if hi : i < stop then
      let_fun this := (_ : i < n);
      bif p x[i] then i else findIdx.loop x p stop h (i + 1)
    else stop) ≥
    i
Tactic:
rewrite [dif_pos hi]
Proof state after:
α : Type u
n : Nat
x : SizedArray α n
p : α → Bool
stop : Nat
h : stop ≤ n
i : Nat
hi✝ : i ≤ stop
hi : i < stop
⊢ (let_fun this := (_ : i < n);
    bif p x[i] then i else findIdx.loop x p stop h (i + 1)) ≥
    i
Theorem: SizedArray.findIdx_loop_ge
Proof state before:
α : Type u
n : Nat
x : SizedArray α n
p : α → Bool
stop : Nat
h : stop ≤ n
i : Nat
hi✝ : i ≤ stop
hi : i < stop
⊢ (let_fun this := (_ : i < n);
    bif p x[i] then i else findIdx.loop x p stop h (i + 1)) ≥
    i
Tactic:
dsimp
Proof state after:
α : Type u
n : Nat
x : SizedArray α n
p : α → Bool
stop : Nat
h : stop ≤ n
i : Nat
hi✝ : i ≤ stop
hi : i < stop
⊢ (bif p x[i] then i else findIdx.loop x p stop h (i + 1)) ≥ i
Theorem: SizedArray.findIdx_loop_ge
Proof state before:
α : Type u
n : Nat
x : SizedArray α n
p : α → Bool
stop : Nat
h : stop ≤ n
i : Nat
hi✝ : i ≤ stop
hi : i < stop
⊢ (bif p x[i] then i else findIdx.loop x p stop h (i + 1)) ≥ i
Tactic:
match p (x[i]'(trans (r:=LT.lt) (s:=LE.le) hi h)) with
| true => exact Nat.le.refl
| false =>
  apply Nat.le_of_succ_le
  exact findIdx_loop_ge x p stop h (i+1) hi
Proof state after:
no goals
Theorem: SizedArray.findIdx_loop_ge
Proof state before:
α : Type u
n : Nat
x : SizedArray α n
p : α → Bool
stop : Nat
h : stop ≤ n
i : Nat
hi✝ : i ≤ stop
hi : i < stop
⊢ (bif true then i else findIdx.loop x p stop h (i + 1)) ≥ i
Tactic:
exact Nat.le.refl
Proof state after:
no goals
Theorem: SizedArray.findIdx_loop_ge
Proof state before:
α : Type u
n : Nat
x : SizedArray α n
p : α → Bool
stop : Nat
h : stop ≤ n
i : Nat
hi✝ : i ≤ stop
hi : i < stop
⊢ (bif false then i else findIdx.loop x p stop h (i + 1)) ≥ i
Tactic:
apply Nat.le_of_succ_le
Proof state after:
case h
α : Type u
n : Nat
x : SizedArray α n
p : α → Bool
stop : Nat
h : stop ≤ n
i : Nat
hi✝ : i ≤ stop
hi : i < stop
⊢ Nat.succ i ≤ bif false then i else findIdx.loop x p stop h (i + 1)
Theorem: SizedArray.findIdx_loop_ge
Proof state before:
case h
α : Type u
n : Nat
x : SizedArray α n
p : α → Bool
stop : Nat
h : stop ≤ n
i : Nat
hi✝ : i ≤ stop
hi : i < stop
⊢ Nat.succ i ≤ bif false then i else findIdx.loop x p stop h (i + 1)
Tactic:
exact findIdx_loop_ge x p stop h (i+1) hi
Proof state after:
no goals
Theorem: SizedArray.findIdx_loop_ge
Proof state before:
α : Type u
n : Nat
x : SizedArray α n
p : α → Bool
stop : Nat
h : stop ≤ n
i : Nat
hi✝ : i ≤ stop
hi : ¬i < stop
⊢ (if hi : i < stop then
      let_fun this := (_ : i < n);
      bif p x[i] then i else findIdx.loop x p stop h (i + 1)
    else stop) ≥
    i
Tactic:
rewrite [dif_neg hi]
Proof state after:
α : Type u
n : Nat
x : SizedArray α n
p : α → Bool
stop : Nat
h : stop ≤ n
i : Nat
hi✝ : i ≤ stop
hi : ¬i < stop
⊢ stop ≥ i
Theorem: SizedArray.findIdx_loop_ge
Proof state before:
α : Type u
n : Nat
x : SizedArray α n
p : α → Bool
stop : Nat
h : stop ≤ n
i : Nat
hi✝ : i ≤ stop
hi : ¬i < stop
⊢ stop ≥ i
Tactic:
assumption
Proof state after:
no goals
Theorem: SizedArray.get_findIdx_loop
Proof state before:
α : Type u
n : Nat
x : SizedArray α n
p : α → Bool
stop : Nat
hstop : stop ≤ n
i : Nat
h : findIdx.loop x p stop hstop i < stop
x✝ : findIdx.loop x p stop hstop i < n
⊢ p x[findIdx.loop x p stop hstop i] = true
Tactic:
unfold findIdx.loop at h ⊢
Proof state after:
α : Type u
n : Nat
x : SizedArray α n
p : α → Bool
stop : Nat
hstop : stop ≤ n
i : Nat
x✝ : findIdx.loop x p stop hstop i < n
h :
  (if hi : i < stop then
      let_fun this := (_ : i < n);
      bif p x[i] then i else findIdx.loop x p stop hstop (i + 1)
    else stop) <
    stop
⊢ p
      x[if hi : i < stop then
          let_fun this := (_ : i < n);
          bif p x[i] then i else findIdx.loop x p stop hstop (i + 1)
        else stop] =
    true
Theorem: SizedArray.get_findIdx_loop
Proof state before:
α : Type u
n : Nat
x : SizedArray α n
p : α → Bool
stop : Nat
hstop : stop ≤ n
i : Nat
x✝ : findIdx.loop x p stop hstop i < n
h :
  (if hi : i < stop then
      let_fun this := (_ : i < n);
      bif p x[i] then i else findIdx.loop x p stop hstop (i + 1)
    else stop) <
    stop
⊢ p
      x[if hi : i < stop then
          let_fun this := (_ : i < n);
          bif p x[i] then i else findIdx.loop x p stop hstop (i + 1)
        else stop] =
    true
Tactic:
if hi : i < stop then
  rewrite [dif_pos hi] at h
  rewrite [getElem_eq rfl (dif_pos hi)]
  dsimp at *
  if hp : p (x[i]'(trans (r:=LT.lt) (s:=LE.le) hi hstop)) = true then
    rewrite [getElem_eq rfl (by rw [hp, cond_true])]
    exact hp
  else
    have hp := Bool.eq_false_iff.mpr hp
    rewrite [getElem_eq rfl (by rw [hp, cond_false])]
    rewrite [hp, cond_false] at h
    exact get_findIdx_loop x p stop hstop (i+1) h
else
  rewrite [dif_neg hi] at h
  exact absurd h stop.lt_irrefl
Proof state after:
no goals
Theorem: SizedArray.get_findIdx_loop
Proof state before:
α : Type u
n : Nat
x : SizedArray α n
p : α → Bool
stop : Nat
hstop : stop ≤ n
i : Nat
x✝ : findIdx.loop x p stop hstop i < n
h :
  (if hi : i < stop then
      let_fun this := (_ : i < n);
      bif p x[i] then i else findIdx.loop x p stop hstop (i + 1)
    else stop) <
    stop
hi : i < stop
⊢ p
      x[if hi : i < stop then
          let_fun this := (_ : i < n);
          bif p x[i] then i else findIdx.loop x p stop hstop (i + 1)
        else stop] =
    true
Tactic:
rewrite [dif_pos hi] at h
Proof state after:
α : Type u
n : Nat
x : SizedArray α n
p : α → Bool
stop : Nat
hstop : stop ≤ n
i : Nat
x✝ : findIdx.loop x p stop hstop i < n
hi : i < stop
h :
  (let_fun this := (_ : i < n);
    bif p x[i] then i else findIdx.loop x p stop hstop (i + 1)) <
    stop
⊢ p
      x[if hi : i < stop then
          let_fun this := (_ : i < n);
          bif p x[i] then i else findIdx.loop x p stop hstop (i + 1)
        else stop] =
    true
Theorem: SizedArray.get_findIdx_loop
Proof state before:
α : Type u
n : Nat
x : SizedArray α n
p : α → Bool
stop : Nat
hstop : stop ≤ n
i : Nat
x✝ : findIdx.loop x p stop hstop i < n
hi : i < stop
h :
  (let_fun this := (_ : i < n);
    bif p x[i] then i else findIdx.loop x p stop hstop (i + 1)) <
    stop
⊢ p
      x[if hi : i < stop then
          let_fun this := (_ : i < n);
          bif p x[i] then i else findIdx.loop x p stop hstop (i + 1)
        else stop] =
    true
Tactic:
rewrite [getElem_eq rfl (dif_pos hi)]
Proof state after:
α : Type u
n : Nat
x : SizedArray α n
p : α → Bool
stop : Nat
hstop : stop ≤ n
i : Nat
x✝ : findIdx.loop x p stop hstop i < n
hi : i < stop
h :
  (let_fun this := (_ : i < n);
    bif p x[i] then i else findIdx.loop x p stop hstop (i + 1)) <
    stop
⊢ p
      x[let_fun this := (_ : i < n);
        bif p x[i] then i else findIdx.loop x p stop hstop (i + 1)] =
    true
Theorem: SizedArray.get_findIdx_loop
Proof state before:
α : Type u
n : Nat
x : SizedArray α n
p : α → Bool
stop : Nat
hstop : stop ≤ n
i : Nat
x✝ : findIdx.loop x p stop hstop i < n
hi : i < stop
h :
  (let_fun this := (_ : i < n);
    bif p x[i] then i else findIdx.loop x p stop hstop (i + 1)) <
    stop
⊢ p
      x[let_fun this := (_ : i < n);
        bif p x[i] then i else findIdx.loop x p stop hstop (i + 1)] =
    true
Tactic:
dsimp at *
Proof state after:
α : Type u
n : Nat
x : SizedArray α n
p : α → Bool
stop : Nat
hstop : stop ≤ n
i : Nat
x✝ : findIdx.loop x p stop hstop i < n
hi : i < stop
h : (bif p x[i] then i else findIdx.loop x p stop hstop (i + 1)) < stop
⊢ p x[bif p x[i] then i else findIdx.loop x p stop hstop (i + 1)] = true
Theorem: SizedArray.get_findIdx_loop
Proof state before:
α : Type u
n : Nat
x : SizedArray α n
p : α → Bool
stop : Nat
hstop : stop ≤ n
i : Nat
x✝ : findIdx.loop x p stop hstop i < n
hi : i < stop
h : (bif p x[i] then i else findIdx.loop x p stop hstop (i + 1)) < stop
⊢ p x[bif p x[i] then i else findIdx.loop x p stop hstop (i + 1)] = true
Tactic:
if hp : p (x[i]'(trans (r:=LT.lt) (s:=LE.le) hi hstop)) = true then
  rewrite [getElem_eq rfl (by rw [hp, cond_true])]
  exact hp
else
  have hp := Bool.eq_false_iff.mpr hp
  rewrite [getElem_eq rfl (by rw [hp, cond_false])]
  rewrite [hp, cond_false] at h
  exact get_findIdx_loop x p stop hstop (i+1) h
Proof state after:
no goals
Theorem: SizedArray.get_findIdx_loop
Proof state before:
α : Type u
n : Nat
x : SizedArray α n
p : α → Bool
stop : Nat
hstop : stop ≤ n
i : Nat
x✝ : findIdx.loop x p stop hstop i < n
hi : i < stop
h : (bif p x[i] then i else findIdx.loop x p stop hstop (i + 1)) < stop
hp : p x[i] = true
⊢ p x[bif p x[i] then i else findIdx.loop x p stop hstop (i + 1)] = true
Tactic:
rewrite [getElem_eq rfl (by rw [hp, cond_true])]
Proof state after:
α : Type u
n : Nat
x : SizedArray α n
p : α → Bool
stop : Nat
hstop : stop ≤ n
i : Nat
x✝ : findIdx.loop x p stop hstop i < n
hi : i < stop
h : (bif p x[i] then i else findIdx.loop x p stop hstop (i + 1)) < stop
hp : p x[i] = true
⊢ p x[i] = true
Theorem: SizedArray.get_findIdx_loop
Proof state before:
α : Type u
n : Nat
x : SizedArray α n
p : α → Bool
stop : Nat
hstop : stop ≤ n
i : Nat
x✝ : findIdx.loop x p stop hstop i < n
hi : i < stop
h : (bif p x[i] then i else findIdx.loop x p stop hstop (i + 1)) < stop
hp : p x[i] = true
⊢ p x[i] = true
Tactic:
exact hp
Proof state after:
no goals
Theorem: SizedArray.get_findIdx_loop
Proof state before:
α : Type u
n : Nat
x : SizedArray α n
p : α → Bool
stop : Nat
hstop : stop ≤ n
i : Nat
x✝ : findIdx.loop x p stop hstop i < n
hi : i < stop
h : (bif p x[i] then i else findIdx.loop x p stop hstop (i + 1)) < stop
hp : p x[i] = true
⊢ (bif p x[i] then i else findIdx.loop x p stop hstop (i + 1)) = ?m.160149
Tactic:
rw [hp, cond_true]
Proof state after:
no goals
Theorem: SizedArray.get_findIdx_loop
Proof state before:
α : Type u
n : Nat
x : SizedArray α n
p : α → Bool
stop : Nat
hstop : stop ≤ n
i : Nat
x✝ : findIdx.loop x p stop hstop i < n
hi : i < stop
h : (bif p x[i] then i else findIdx.loop x p stop hstop (i + 1)) < stop
hp : ¬p x[i] = true
⊢ p x[bif p x[i] then i else findIdx.loop x p stop hstop (i + 1)] = true
Tactic:
have hp := Bool.eq_false_iff.mpr hp
Proof state after:
α : Type u
n : Nat
x : SizedArray α n
p : α → Bool
stop : Nat
hstop : stop ≤ n
i : Nat
x✝ : findIdx.loop x p stop hstop i < n
hi : i < stop
h : (bif p x[i] then i else findIdx.loop x p stop hstop (i + 1)) < stop
hp✝ : ¬p x[i] = true
hp : p x[i] = false
⊢ p x[bif p x[i] then i else findIdx.loop x p stop hstop (i + 1)] = true
Theorem: SizedArray.get_findIdx_loop
Proof state before:
α : Type u
n : Nat
x : SizedArray α n
p : α → Bool
stop : Nat
hstop : stop ≤ n
i : Nat
x✝ : findIdx.loop x p stop hstop i < n
hi : i < stop
h : (bif p x[i] then i else findIdx.loop x p stop hstop (i + 1)) < stop
hp✝ : ¬p x[i] = true
hp : p x[i] = false
⊢ p x[bif p x[i] then i else findIdx.loop x p stop hstop (i + 1)] = true
Tactic:
rewrite [getElem_eq rfl (by rw [hp, cond_false])]
Proof state after:
α : Type u
n : Nat
x : SizedArray α n
p : α → Bool
stop : Nat
hstop : stop ≤ n
i : Nat
x✝ : findIdx.loop x p stop hstop i < n
hi : i < stop
h : (bif p x[i] then i else findIdx.loop x p stop hstop (i + 1)) < stop
hp✝ : ¬p x[i] = true
hp : p x[i] = false
⊢ p x[findIdx.loop x p stop hstop (i + 1)] = true
Theorem: SizedArray.get_findIdx_loop
Proof state before:
α : Type u
n : Nat
x : SizedArray α n
p : α → Bool
stop : Nat
hstop : stop ≤ n
i : Nat
x✝ : findIdx.loop x p stop hstop i < n
hi : i < stop
h : (bif p x[i] then i else findIdx.loop x p stop hstop (i + 1)) < stop
hp✝ : ¬p x[i] = true
hp : p x[i] = false
⊢ p x[findIdx.loop x p stop hstop (i + 1)] = true
Tactic:
rewrite [hp, cond_false] at h
Proof state after:
α : Type u
n : Nat
x : SizedArray α n
p : α → Bool
stop : Nat
hstop : stop ≤ n
i : Nat
x✝ : findIdx.loop x p stop hstop i < n
hi : i < stop
h : findIdx.loop x p stop hstop (i + 1) < stop
hp✝ : ¬p x[i] = true
hp : p x[i] = false
⊢ p x[findIdx.loop x p stop hstop (i + 1)] = true
Theorem: SizedArray.get_findIdx_loop
Proof state before:
α : Type u
n : Nat
x : SizedArray α n
p : α → Bool
stop : Nat
hstop : stop ≤ n
i : Nat
x✝ : findIdx.loop x p stop hstop i < n
hi : i < stop
h : findIdx.loop x p stop hstop (i + 1) < stop
hp✝ : ¬p x[i] = true
hp : p x[i] = false
⊢ p x[findIdx.loop x p stop hstop (i + 1)] = true
Tactic:
exact get_findIdx_loop x p stop hstop (i+1) h
Proof state after:
no goals
Theorem: SizedArray.get_findIdx_loop
Proof state before:
α : Type u
n : Nat
x : SizedArray α n
p : α → Bool
stop : Nat
hstop : stop ≤ n
i : Nat
x✝ : findIdx.loop x p stop hstop i < n
hi : i < stop
h : (bif p x[i] then i else findIdx.loop x p stop hstop (i + 1)) < stop
hp✝ : ¬p x[i] = true
hp : p x[i] = false
⊢ (bif p x[i] then i else findIdx.loop x p stop hstop (i + 1)) = ?m.160313
Tactic:
rw [hp, cond_false]
Proof state after:
no goals
Theorem: SizedArray.get_findIdx_loop
Proof state before:
α : Type u
n : Nat
x : SizedArray α n
p : α → Bool
stop : Nat
hstop : stop ≤ n
i : Nat
x✝ : findIdx.loop x p stop hstop i < n
h :
  (if hi : i < stop then
      let_fun this := (_ : i < n);
      bif p x[i] then i else findIdx.loop x p stop hstop (i + 1)
    else stop) <
    stop
hi : ¬i < stop
⊢ p
      x[if hi : i < stop then
          let_fun this := (_ : i < n);
          bif p x[i] then i else findIdx.loop x p stop hstop (i + 1)
        else stop] =
    true
Tactic:
rewrite [dif_neg hi] at h
Proof state after:
α : Type u
n : Nat
x : SizedArray α n
p : α → Bool
stop : Nat
hstop : stop ≤ n
i : Nat
x✝ : findIdx.loop x p stop hstop i < n
h : stop < stop
hi : ¬i < stop
⊢ p
      x[if hi : i < stop then
          let_fun this := (_ : i < n);
          bif p x[i] then i else findIdx.loop x p stop hstop (i + 1)
        else stop] =
    true
Theorem: SizedArray.get_findIdx_loop
Proof state before:
α : Type u
n : Nat
x : SizedArray α n
p : α → Bool
stop : Nat
hstop : stop ≤ n
i : Nat
x✝ : findIdx.loop x p stop hstop i < n
h : stop < stop
hi : ¬i < stop
⊢ p
      x[if hi : i < stop then
          let_fun this := (_ : i < n);
          bif p x[i] then i else findIdx.loop x p stop hstop (i + 1)
        else stop] =
    true
Tactic:
exact absurd h stop.lt_irrefl
Proof state after:
no goals
Theorem: SizedArray.get_findIdx_loop_of_lt
Proof state before:
α : Type u
n : Nat
x : SizedArray α n
p : α → Bool
stop : Nat
h : stop ≤ n
i k : Nat
hk : k ≥ i
hk' : k < findIdx.loop x p stop h i
x✝ : k < n
⊢ p x[k] = false
Tactic:
have hkstop : k < stop :=
  trans (r:=LT.lt) (s:=LE.le) hk' <| findIdx_loop_le x p stop h i
Proof state after:
α : Type u
n : Nat
x : SizedArray α n
p : α → Bool
stop : Nat
h : stop ≤ n
i k : Nat
hk : k ≥ i
hk' : k < findIdx.loop x p stop h i
x✝ : k < n
hkstop : k < stop
⊢ p x[k] = false
Theorem: SizedArray.get_findIdx_loop_of_lt
Proof state before:
α : Type u
n : Nat
x : SizedArray α n
p : α → Bool
stop : Nat
h : stop ≤ n
i k : Nat
hk : k ≥ i
hk' : k < findIdx.loop x p stop h i
x✝ : k < n
hkstop : k < stop
⊢ p x[k] = false
Tactic:
have histop : i < stop := trans hk hkstop
Proof state after:
α : Type u
n : Nat
x : SizedArray α n
p : α → Bool
stop : Nat
h : stop ≤ n
i k : Nat
hk : k ≥ i
hk' : k < findIdx.loop x p stop h i
x✝ : k < n
hkstop : k < stop
histop : i < stop
⊢ p x[k] = false
Theorem: SizedArray.get_findIdx_loop_of_lt
Proof state before:
α : Type u
n : Nat
x : SizedArray α n
p : α → Bool
stop : Nat
h : stop ≤ n
i k : Nat
hk : k ≥ i
hk' : k < findIdx.loop x p stop h i
x✝ : k < n
hkstop : k < stop
histop : i < stop
⊢ p x[k] = false
Tactic:
conv at hk' =>
  unfold findIdx.loop; rw [dif_pos histop]; dsimp
Proof state after:
α : Type u
n : Nat
x : SizedArray α n
p : α → Bool
stop : Nat
h : stop ≤ n
i k : Nat
hk : k ≥ i
x✝ : k < n
hkstop : k < stop
histop : i < stop
hk' : k < bif p x[i] then i else findIdx.loop x p stop h (i + 1)
⊢ p x[k] = false
Theorem: SizedArray.get_findIdx_loop_of_lt
Proof state before:
α : Type u
n : Nat
x : SizedArray α n
p : α → Bool
stop : Nat
h : stop ≤ n
i k : Nat
hk : k ≥ i
x✝ : k < n
hkstop : k < stop
histop : i < stop
hk' : k < bif p x[i] then i else findIdx.loop x p stop h (i + 1)
⊢ p x[k] = false
Tactic:
match hpi : p (x[i]'(trans (r:=LT.lt) (s:=LE.le) histop h)) with
| true =>
  rewrite [hpi, cond_true] at hk'
  exact absurd hk' <| Nat.not_lt_of_le hk
| false =>
  rewrite [hpi, cond_false] at hk'
  cases Nat.eq_or_lt_of_le hk with
  | inl heq => exact heq ▸ hpi
  | inr hlt => exact get_findIdx_loop_of_lt x p stop h (i+1) k hlt hk'
Proof state after:
no goals