internlm/Lean-Github huggingface dataset:
Theorem: Array.anyPairM_loop_cons_succ
Proof state before:
α : Type u
β : Type v
m : Type → Type v
inst✝ : Monad m
a : α
x : Array α
p : α → α → m Bool
stop : Nat
h : stop ≤ size x
i j : Nat
hij : i < j
hj : ¬j < stop
⊢ (if i + 1 < stop + 1 then
      anyPairM.loop (cons a x) p (stop + 1) (_ : Nat.succ stop ≤ Nat.succ (List.length x.data)) (i + 1 + 1) (i + 1 + 2)
        (_ : i + 1 + 1 < Nat.succ (i + 1 + 1))
    else pure false) =
    if i < stop then anyPairM.loop x p stop h (i + 1) (i + 2) (_ : i + 1 < Nat.succ (i + 1)) else pure false
Tactic:
if hi : i < stop then
  rewrite [if_pos (Nat.succ_lt_succ hi), if_pos hi]
  exact anyPairM_loop_cons_succ a x p h (i+1).lt_succ_self
else
  rw [if_neg (fun h' => hi (Nat.lt_of_succ_lt_succ h')), if_neg hi]
Proof state after:
no goals
Theorem: Array.anyPairM_loop_cons_succ
Proof state before:
α : Type u
β : Type v
m : Type → Type v
inst✝ : Monad m
a : α
x : Array α
p : α → α → m Bool
stop : Nat
h : stop ≤ size x
i j : Nat
hij : i < j
hj : ¬j < stop
hi : i < stop
⊢ (if i + 1 < stop + 1 then
      anyPairM.loop (cons a x) p (stop + 1) (_ : Nat.succ stop ≤ Nat.succ (List.length x.data)) (i + 1 + 1) (i + 1 + 2)
        (_ : i + 1 + 1 < Nat.succ (i + 1 + 1))
    else pure false) =
    if i < stop then anyPairM.loop x p stop h (i + 1) (i + 2) (_ : i + 1 < Nat.succ (i + 1)) else pure false
Tactic:
rewrite [if_pos (Nat.succ_lt_succ hi), if_pos hi]
Proof state after:
α : Type u
β : Type v
m : Type → Type v
inst✝ : Monad m
a : α
x : Array α
p : α → α → m Bool
stop : Nat
h : stop ≤ size x
i j : Nat
hij : i < j
hj : ¬j < stop
hi : i < stop
⊢ anyPairM.loop (cons a x) p (stop + 1) (_ : Nat.succ stop ≤ Nat.succ (List.length x.data)) (i + 1 + 1) (i + 1 + 2)
      (_ : i + 1 + 1 < Nat.succ (i + 1 + 1)) =
    anyPairM.loop x p stop h (i + 1) (i + 2) (_ : i + 1 < Nat.succ (i + 1))
Theorem: Array.anyPairM_loop_cons_succ
Proof state before:
α : Type u
β : Type v
m : Type → Type v
inst✝ : Monad m
a : α
x : Array α
p : α → α → m Bool
stop : Nat
h : stop ≤ size x
i j : Nat
hij : i < j
hj : ¬j < stop
hi : i < stop
⊢ anyPairM.loop (cons a x) p (stop + 1) (_ : Nat.succ stop ≤ Nat.succ (List.length x.data)) (i + 1 + 1) (i + 1 + 2)
      (_ : i + 1 + 1 < Nat.succ (i + 1 + 1)) =
    anyPairM.loop x p stop h (i + 1) (i + 2) (_ : i + 1 < Nat.succ (i + 1))
Tactic:
exact anyPairM_loop_cons_succ a x p h (i+1).lt_succ_self
Proof state after:
no goals
Theorem: Array.anyPairM_loop_cons_succ
Proof state before:
α : Type u
β : Type v
m : Type → Type v
inst✝ : Monad m
a : α
x : Array α
p : α → α → m Bool
stop : Nat
h : stop ≤ size x
i j : Nat
hij : i < j
hj : ¬j < stop
hi : ¬i < stop
⊢ (if i + 1 < stop + 1 then
      anyPairM.loop (cons a x) p (stop + 1) (_ : Nat.succ stop ≤ Nat.succ (List.length x.data)) (i + 1 + 1) (i + 1 + 2)
        (_ : i + 1 + 1 < Nat.succ (i + 1 + 1))
    else pure false) =
    if i < stop then anyPairM.loop x p stop h (i + 1) (i + 2) (_ : i + 1 < Nat.succ (i + 1)) else pure false
Tactic:
rw [if_neg (fun h' => hi (Nat.lt_of_succ_lt_succ h')), if_neg hi]
Proof state after:
no goals
Theorem: Array.anyPairM_loop_cons_zero
Proof state before:
α : Type u
β : Type v
m : Type → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
a : α
x : Array α
p : α → α → m Bool
stop : Nat
h : stop ≤ size x
j : Nat
⊢ anyPairM.loop (cons a x) p (stop + 1) (_ : Nat.succ stop ≤ Nat.succ (List.length x.data)) 0 (j + 1)
      (_ : 0 < Nat.succ j) =
    do
    let b ← anyM (p a) x j stop
    if b = true then pure true else anyPairM.loop x p stop h 0 1 Nat.zero_lt_one
Tactic:
conv => lhs; unfold anyPairM.loop
Proof state after:
α : Type u
β : Type v
m : Type → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
a : α
x : Array α
p : α → α → m Bool
stop : Nat
h : stop ≤ size x
j : Nat
⊢ (if hj : j + 1 < stop + 1 then
      let_fun this := (_ : 0 < size (cons a x));
      let_fun this_1 := (_ : j + 1 < size (cons a x));
      do
      let __do_lift ← p (cons a x)[0] (cons a x)[j + 1]
      if __do_lift = true then pure true
        else
          anyPairM.loop (cons a x) p (stop + 1) (_ : Nat.succ stop ≤ Nat.succ (List.length x.data)) 0 (j + 1 + 1)
            (_ : 0 < Nat.succ (j + 1))
    else
      if 0 < stop + 1 then
        anyPairM.loop (cons a x) p (stop + 1) (_ : Nat.succ stop ≤ Nat.succ (List.length x.data)) (0 + 1) (0 + 2)
          (_ : 0 + 1 < Nat.succ (0 + 1))
      else pure false) =
    do
    let b ← anyM (p a) x j stop
    if b = true then pure true else anyPairM.loop x p stop h 0 1 Nat.zero_lt_one
Theorem: Array.anyPairM_loop_cons_zero
Proof state before:
α : Type u
β : Type v
m : Type → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
a : α
x : Array α
p : α → α → m Bool
stop : Nat
h : stop ≤ size x
j : Nat
⊢ (if hj : j + 1 < stop + 1 then
      let_fun this := (_ : 0 < size (cons a x));
      let_fun this_1 := (_ : j + 1 < size (cons a x));
      do
      let __do_lift ← p (cons a x)[0] (cons a x)[j + 1]
      if __do_lift = true then pure true
        else
          anyPairM.loop (cons a x) p (stop + 1) (_ : Nat.succ stop ≤ Nat.succ (List.length x.data)) 0 (j + 1 + 1)
            (_ : 0 < Nat.succ (j + 1))
    else
      if 0 < stop + 1 then
        anyPairM.loop (cons a x) p (stop + 1) (_ : Nat.succ stop ≤ Nat.succ (List.length x.data)) (0 + 1) (0 + 2)
          (_ : 0 + 1 < Nat.succ (0 + 1))
      else pure false) =
    do
    let b ← anyM (p a) x j stop
    if b = true then pure true else anyPairM.loop x p stop h 0 1 Nat.zero_lt_one
Tactic:
conv => rhs; dsimp [anyM]; rewrite [dif_pos h]; unfold anyM.loop
Proof state after:
α : Type u
β : Type v
m : Type → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
a : α
x : Array α
p : α → α → m Bool
stop : Nat
h : stop ≤ size x
j : Nat
⊢ (if hj : j + 1 < stop + 1 then
      let_fun this := (_ : 0 < size (cons a x));
      let_fun this_1 := (_ : j + 1 < size (cons a x));
      do
      let __do_lift ← p (cons a x)[0] (cons a x)[j + 1]
      if __do_lift = true then pure true
        else
          anyPairM.loop (cons a x) p (stop + 1) (_ : Nat.succ stop ≤ Nat.succ (List.length x.data)) 0 (j + 1 + 1)
            (_ : 0 < Nat.succ (j + 1))
    else
      if 0 < stop + 1 then
        anyPairM.loop (cons a x) p (stop + 1) (_ : Nat.succ stop ≤ Nat.succ (List.length x.data)) (0 + 1) (0 + 2)
          (_ : 0 + 1 < Nat.succ (0 + 1))
      else pure false) =
    do
    let b ←
      if hlt : j < stop then
          let_fun this := (_ : j < size x);
          do
          let __do_lift ← p a x[j]
          if __do_lift = true then pure true else anyM.loop (p a) x stop h (j + 1)
        else pure false
    if b = true then pure true else anyPairM.loop x p stop h 0 1 Nat.zero_lt_one
Theorem: Array.anyPairM_loop_cons_zero
Proof state before:
α : Type u
β : Type v
m : Type → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
a : α
x : Array α
p : α → α → m Bool
stop : Nat
h : stop ≤ size x
j : Nat
⊢ (if hj : j + 1 < stop + 1 then
      let_fun this := (_ : 0 < size (cons a x));
      let_fun this_1 := (_ : j + 1 < size (cons a x));
      do
      let __do_lift ← p (cons a x)[0] (cons a x)[j + 1]
      if __do_lift = true then pure true
        else
          anyPairM.loop (cons a x) p (stop + 1) (_ : Nat.succ stop ≤ Nat.succ (List.length x.data)) 0 (j + 1 + 1)
            (_ : 0 < Nat.succ (j + 1))
    else
      if 0 < stop + 1 then
        anyPairM.loop (cons a x) p (stop + 1) (_ : Nat.succ stop ≤ Nat.succ (List.length x.data)) (0 + 1) (0 + 2)
          (_ : 0 + 1 < Nat.succ (0 + 1))
      else pure false) =
    do
    let b ←
      if hlt : j < stop then
          let_fun this := (_ : j < size x);
          do
          let __do_lift ← p a x[j]
          if __do_lift = true then pure true else anyM.loop (p a) x stop h (j + 1)
        else pure false
    if b = true then pure true else anyPairM.loop x p stop h 0 1 Nat.zero_lt_one
Tactic:
simp only [if_pos stop.zero_lt_succ]
Proof state after:
α : Type u
β : Type v
m : Type → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
a : α
x : Array α
p : α → α → m Bool
stop : Nat
h : stop ≤ size x
j : Nat
⊢ (if h_1 : j + 1 < stop + 1 then do
      let __do_lift ← p (cons a x)[0] (cons a x)[j + 1]
      if __do_lift = true then pure true
        else
          anyPairM.loop (cons a x) p (stop + 1) (_ : Nat.succ stop ≤ Nat.succ (List.length x.data)) 0 (j + 1 + 1)
            (_ : 0 < Nat.succ (j + 1))
    else
      anyPairM.loop (cons a x) p (stop + 1) (_ : Nat.succ stop ≤ Nat.succ (List.length x.data)) (0 + 1) (0 + 2)
        (_ : 0 + 1 < Nat.succ (0 + 1))) =
    do
    let b ←
      if h_1 : j < stop then do
          let __do_lift ← p a x[j]
          if __do_lift = true then pure true else anyM.loop (p a) x stop h (j + 1)
        else pure false
    if b = true then pure true else anyPairM.loop x p stop h 0 1 Nat.zero_lt_one
Theorem: Array.anyPairM_loop_cons_zero
Proof state before:
α : Type u
β : Type v
m : Type → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
a : α
x : Array α
p : α → α → m Bool
stop : Nat
h : stop ≤ size x
j : Nat
⊢ (if h_1 : j + 1 < stop + 1 then do
      let __do_lift ← p (cons a x)[0] (cons a x)[j + 1]
      if __do_lift = true then pure true
        else
          anyPairM.loop (cons a x) p (stop + 1) (_ : Nat.succ stop ≤ Nat.succ (List.length x.data)) 0 (j + 1 + 1)
            (_ : 0 < Nat.succ (j + 1))
    else
      anyPairM.loop (cons a x) p (stop + 1) (_ : Nat.succ stop ≤ Nat.succ (List.length x.data)) (0 + 1) (0 + 2)
        (_ : 0 + 1 < Nat.succ (0 + 1))) =
    do
    let b ←
      if h_1 : j < stop then do
          let __do_lift ← p a x[j]
          if __do_lift = true then pure true else anyM.loop (p a) x stop h (j + 1)
        else pure false
    if b = true then pure true else anyPairM.loop x p stop h 0 1 Nat.zero_lt_one
Tactic:
if hj : j < stop then
  simp only [dif_pos (Nat.succ_lt_succ hj), dif_pos hj]
  simp only [getElem_cons_zero, getElem_cons_succ, bind_assoc]
  apply bind_congr; intro b
  match b with
  | true => simp only [ite_true, pure_bind]
  | false =>
    simp only [ite_false]
    rewrite [anyPairM_loop_cons_zero a x p h (j+1)]
    conv => lhs; lhs; dsimp [anyM]; rw [dif_pos h]
else
  simp only [dif_neg (fun h' => hj (Nat.lt_of_succ_lt_succ h')), dif_neg hj]
  rewrite [anyPairM_loop_cons_succ a x p h Nat.zero_lt_one]
  simp only [pure_bind, ite_false]
Proof state after:
no goals
Theorem: Array.anyPairM_loop_cons_zero
Proof state before:
α : Type u
β : Type v
m : Type → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
a : α
x : Array α
p : α → α → m Bool
stop : Nat
h : stop ≤ size x
j : Nat
hj : j < stop
⊢ (if h_1 : j + 1 < stop + 1 then do
      let __do_lift ← p (cons a x)[0] (cons a x)[j + 1]
      if __do_lift = true then pure true
        else
          anyPairM.loop (cons a x) p (stop + 1) (_ : Nat.succ stop ≤ Nat.succ (List.length x.data)) 0 (j + 1 + 1)
            (_ : 0 < Nat.succ (j + 1))
    else
      anyPairM.loop (cons a x) p (stop + 1) (_ : Nat.succ stop ≤ Nat.succ (List.length x.data)) (0 + 1) (0 + 2)
        (_ : 0 + 1 < Nat.succ (0 + 1))) =
    do
    let b ←
      if h_1 : j < stop then do
          let __do_lift ← p a x[j]
          if __do_lift = true then pure true else anyM.loop (p a) x stop h (j + 1)
        else pure false
    if b = true then pure true else anyPairM.loop x p stop h 0 1 Nat.zero_lt_one
Tactic:
simp only [dif_pos (Nat.succ_lt_succ hj), dif_pos hj]
Proof state after:
α : Type u
β : Type v
m : Type → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
a : α
x : Array α
p : α → α → m Bool
stop : Nat
h : stop ≤ size x
j : Nat
hj : j < stop
⊢ (do
      let __do_lift ← p (cons a x)[0] (cons a x)[j + 1]
      if __do_lift = true then pure true
        else
          anyPairM.loop (cons a x) p (stop + 1) (_ : Nat.succ stop ≤ Nat.succ (List.length x.data)) 0 (j + 1 + 1)
            (_ : 0 < Nat.succ (j + 1))) =
    do
    let b ←
      do
        let __do_lift ← p a x[j]
        if __do_lift = true then pure true else anyM.loop (p a) x stop h (j + 1)
    if b = true then pure true else anyPairM.loop x p stop h 0 1 Nat.zero_lt_one
Theorem: Array.anyPairM_loop_cons_zero
Proof state before:
α : Type u
β : Type v
m : Type → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
a : α
x : Array α
p : α → α → m Bool
stop : Nat
h : stop ≤ size x
j : Nat
hj : j < stop
⊢ (do
      let __do_lift ← p (cons a x)[0] (cons a x)[j + 1]
      if __do_lift = true then pure true
        else
          anyPairM.loop (cons a x) p (stop + 1) (_ : Nat.succ stop ≤ Nat.succ (List.length x.data)) 0 (j + 1 + 1)
            (_ : 0 < Nat.succ (j + 1))) =
    do
    let b ←
      do
        let __do_lift ← p a x[j]
        if __do_lift = true then pure true else anyM.loop (p a) x stop h (j + 1)
    if b = true then pure true else anyPairM.loop x p stop h 0 1 Nat.zero_lt_one
Tactic:
simp only [getElem_cons_zero, getElem_cons_succ, bind_assoc]
Proof state after:
α : Type u
β : Type v
m : Type → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
a : α
x : Array α
p : α → α → m Bool
stop : Nat
h : stop ≤ size x
j : Nat
hj : j < stop
⊢ (do
      let __do_lift ← p a x[j]
      if __do_lift = true then pure true
        else
          anyPairM.loop (cons a x) p (stop + 1) (_ : Nat.succ stop ≤ Nat.succ (List.length x.data)) 0 (j + 1 + 1)
            (_ : 0 < Nat.succ (j + 1))) =
    do
    let x_1 ← p a x[j]
    let b ← if x_1 = true then pure true else anyM.loop (p a) x stop h (j + 1)
    if b = true then pure true else anyPairM.loop x p stop h 0 1 Nat.zero_lt_one
Theorem: Array.anyPairM_loop_cons_zero
Proof state before:
α : Type u
β : Type v
m : Type → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
a : α
x : Array α
p : α → α → m Bool
stop : Nat
h : stop ≤ size x
j : Nat
hj : j < stop
⊢ (do
      let __do_lift ← p a x[j]
      if __do_lift = true then pure true
        else
          anyPairM.loop (cons a x) p (stop + 1) (_ : Nat.succ stop ≤ Nat.succ (List.length x.data)) 0 (j + 1 + 1)
            (_ : 0 < Nat.succ (j + 1))) =
    do
    let x_1 ← p a x[j]
    let b ← if x_1 = true then pure true else anyM.loop (p a) x stop h (j + 1)
    if b = true then pure true else anyPairM.loop x p stop h 0 1 Nat.zero_lt_one
Tactic:
apply bind_congr
Proof state after:
case h
α : Type u
β : Type v
m : Type → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
a : α
x : Array α
p : α → α → m Bool
stop : Nat
h : stop ≤ size x
j : Nat
hj : j < stop
⊢ ∀ (a_1 : Bool),
    (if a_1 = true then pure true
      else
        anyPairM.loop (cons a x) p (stop + 1) (_ : Nat.succ stop ≤ Nat.succ (List.length x.data)) 0 (j + 1 + 1)
          (_ : 0 < Nat.succ (j + 1))) =
      do
      let b ← if a_1 = true then pure true else anyM.loop (p a) x stop h (j + 1)
      if b = true then pure true else anyPairM.loop x p stop h 0 1 Nat.zero_lt_one
Theorem: Array.anyPairM_loop_cons_zero
Proof state before:
case h
α : Type u
β : Type v
m : Type → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
a : α
x : Array α
p : α → α → m Bool
stop : Nat
h : stop ≤ size x
j : Nat
hj : j < stop
⊢ ∀ (a_1 : Bool),
    (if a_1 = true then pure true
      else
        anyPairM.loop (cons a x) p (stop + 1) (_ : Nat.succ stop ≤ Nat.succ (List.length x.data)) 0 (j + 1 + 1)
          (_ : 0 < Nat.succ (j + 1))) =
      do
      let b ← if a_1 = true then pure true else anyM.loop (p a) x stop h (j + 1)
      if b = true then pure true else anyPairM.loop x p stop h 0 1 Nat.zero_lt_one
Tactic:
intro b
Proof state after:
case h
α : Type u
β : Type v
m : Type → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
a : α
x : Array α
p : α → α → m Bool
stop : Nat
h : stop ≤ size x
j : Nat
hj : j < stop
b : Bool
⊢ (if b = true then pure true
    else
      anyPairM.loop (cons a x) p (stop + 1) (_ : Nat.succ stop ≤ Nat.succ (List.length x.data)) 0 (j + 1 + 1)
        (_ : 0 < Nat.succ (j + 1))) =
    do
    let b ← if b = true then pure true else anyM.loop (p a) x stop h (j + 1)
    if b = true then pure true else anyPairM.loop x p stop h 0 1 Nat.zero_lt_one
Theorem: Array.anyPairM_loop_cons_zero
Proof state before:
case h
α : Type u
β : Type v
m : Type → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
a : α
x : Array α
p : α → α → m Bool
stop : Nat
h : stop ≤ size x
j : Nat
hj : j < stop
b : Bool
⊢ (if b = true then pure true
    else
      anyPairM.loop (cons a x) p (stop + 1) (_ : Nat.succ stop ≤ Nat.succ (List.length x.data)) 0 (j + 1 + 1)
        (_ : 0 < Nat.succ (j + 1))) =
    do
    let b ← if b = true then pure true else anyM.loop (p a) x stop h (j + 1)
    if b = true then pure true else anyPairM.loop x p stop h 0 1 Nat.zero_lt_one
Tactic:
match b with
| true => simp only [ite_true, pure_bind]
| false =>
  simp only [ite_false]
  rewrite [anyPairM_loop_cons_zero a x p h (j+1)]
  conv => lhs; lhs; dsimp [anyM]; rw [dif_pos h]
Proof state after:
no goals
Theorem: Array.anyPairM_loop_cons_zero
Proof state before:
α : Type u
β : Type v
m : Type → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
a : α
x : Array α
p : α → α → m Bool
stop : Nat
h : stop ≤ size x
j : Nat
hj : j < stop
b : Bool
⊢ (if true = true then pure true
    else
      anyPairM.loop (cons a x) p (stop + 1) (_ : Nat.succ stop ≤ Nat.succ (List.length x.data)) 0 (j + 1 + 1)
        (_ : 0 < Nat.succ (j + 1))) =
    do
    let b ← if true = true then pure true else anyM.loop (p a) x stop h (j + 1)
    if b = true then pure true else anyPairM.loop x p stop h 0 1 Nat.zero_lt_one
Tactic:
simp only [ite_true, pure_bind]
Proof state after:
no goals
Theorem: Array.anyPairM_loop_cons_zero
Proof state before:
α : Type u
β : Type v
m : Type → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
a : α
x : Array α
p : α → α → m Bool
stop : Nat
h : stop ≤ size x
j : Nat
hj : j < stop
b : Bool
⊢ (if false = true then pure true
    else
      anyPairM.loop (cons a x) p (stop + 1) (_ : Nat.succ stop ≤ Nat.succ (List.length x.data)) 0 (j + 1 + 1)
        (_ : 0 < Nat.succ (j + 1))) =
    do
    let b ← if false = true then pure true else anyM.loop (p a) x stop h (j + 1)
    if b = true then pure true else anyPairM.loop x p stop h 0 1 Nat.zero_lt_one
Tactic:
simp only [ite_false]
Proof state after:
α : Type u
β : Type v
m : Type → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
a : α
x : Array α
p : α → α → m Bool
stop : Nat
h : stop ≤ size x
j : Nat
hj : j < stop
b : Bool
⊢ anyPairM.loop (cons a x) p (stop + 1) (_ : Nat.succ stop ≤ Nat.succ (List.length x.data)) 0 (j + 1 + 1)
      (_ : 0 < Nat.succ (j + 1)) =
    do
    let b ← anyM.loop (p a) x stop h (j + 1)
    if b = true then pure true else anyPairM.loop x p stop h 0 1 Nat.zero_lt_one
Theorem: Array.anyPairM_loop_cons_zero
Proof state before:
α : Type u
β : Type v
m : Type → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
a : α
x : Array α
p : α → α → m Bool
stop : Nat
h : stop ≤ size x
j : Nat
hj : j < stop
b : Bool
⊢ anyPairM.loop (cons a x) p (stop + 1) (_ : Nat.succ stop ≤ Nat.succ (List.length x.data)) 0 (j + 1 + 1)
      (_ : 0 < Nat.succ (j + 1)) =
    do
    let b ← anyM.loop (p a) x stop h (j + 1)
    if b = true then pure true else anyPairM.loop x p stop h 0 1 Nat.zero_lt_one
Tactic:
rewrite [anyPairM_loop_cons_zero a x p h (j+1)]
Proof state after:
α : Type u
β : Type v
m : Type → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
a : α
x : Array α
p : α → α → m Bool
stop : Nat
h : stop ≤ size x
j : Nat
hj : j < stop
b : Bool
⊢ (do
      let b ← anyM (p a) x (j + 1) stop
      if b = true then pure true else anyPairM.loop x p stop h 0 1 Nat.zero_lt_one) =
    do
    let b ← anyM.loop (p a) x stop h (j + 1)
    if b = true then pure true else anyPairM.loop x p stop h 0 1 Nat.zero_lt_one
Theorem: Array.anyPairM_loop_cons_zero
Proof state before:
α : Type u
β : Type v
m : Type → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
a : α
x : Array α
p : α → α → m Bool
stop : Nat
h : stop ≤ size x
j : Nat
hj : j < stop
b : Bool
⊢ (do
      let b ← anyM (p a) x (j + 1) stop
      if b = true then pure true else anyPairM.loop x p stop h 0 1 Nat.zero_lt_one) =
    do
    let b ← anyM.loop (p a) x stop h (j + 1)
    if b = true then pure true else anyPairM.loop x p stop h 0 1 Nat.zero_lt_one
Tactic:
conv => lhs; lhs; dsimp [anyM]; rw [dif_pos h]
Proof state after:
no goals
Theorem: Array.anyPairM_loop_cons_zero
Proof state before:
α : Type u
β : Type v
m : Type → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
a : α
x : Array α
p : α → α → m Bool
stop : Nat
h : stop ≤ size x
j : Nat
hj : ¬j < stop
⊢ (if h_1 : j + 1 < stop + 1 then do
      let __do_lift ← p (cons a x)[0] (cons a x)[j + 1]
      if __do_lift = true then pure true
        else
          anyPairM.loop (cons a x) p (stop + 1) (_ : Nat.succ stop ≤ Nat.succ (List.length x.data)) 0 (j + 1 + 1)
            (_ : 0 < Nat.succ (j + 1))
    else
      anyPairM.loop (cons a x) p (stop + 1) (_ : Nat.succ stop ≤ Nat.succ (List.length x.data)) (0 + 1) (0 + 2)
        (_ : 0 + 1 < Nat.succ (0 + 1))) =
    do
    let b ←
      if h_1 : j < stop then do
          let __do_lift ← p a x[j]
          if __do_lift = true then pure true else anyM.loop (p a) x stop h (j + 1)
        else pure false
    if b = true then pure true else anyPairM.loop x p stop h 0 1 Nat.zero_lt_one
Tactic:
simp only [dif_neg (fun h' => hj (Nat.lt_of_succ_lt_succ h')), dif_neg hj]
Proof state after:
α : Type u
β : Type v
m : Type → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
a : α
x : Array α
p : α → α → m Bool
stop : Nat
h : stop ≤ size x
j : Nat
hj : ¬j < stop
⊢ anyPairM.loop (cons a x) p (stop + 1) (_ : Nat.succ stop ≤ Nat.succ (List.length x.data)) (0 + 1) (0 + 2)
      (_ : 0 + 1 < Nat.succ (0 + 1)) =
    do
    let b ← pure false
    if b = true then pure true else anyPairM.loop x p stop h 0 1 Nat.zero_lt_one
Theorem: Array.anyPairM_loop_cons_zero
Proof state before:
α : Type u
β : Type v
m : Type → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
a : α
x : Array α
p : α → α → m Bool
stop : Nat
h : stop ≤ size x
j : Nat
hj : ¬j < stop
⊢ anyPairM.loop (cons a x) p (stop + 1) (_ : Nat.succ stop ≤ Nat.succ (List.length x.data)) (0 + 1) (0 + 2)
      (_ : 0 + 1 < Nat.succ (0 + 1)) =
    do
    let b ← pure false
    if b = true then pure true else anyPairM.loop x p stop h 0 1 Nat.zero_lt_one
Tactic:
rewrite [anyPairM_loop_cons_succ a x p h Nat.zero_lt_one]
Proof state after:
α : Type u
β : Type v
m : Type → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
a : α
x : Array α
p : α → α → m Bool
stop : Nat
h : stop ≤ size x
j : Nat
hj : ¬j < stop
⊢ anyPairM.loop x p stop h 0 1 Nat.zero_lt_one = do
    let b ← pure false
    if b = true then pure true else anyPairM.loop x p stop h 0 1 Nat.zero_lt_one
Theorem: Array.anyPairM_loop_cons_zero
Proof state before:
α : Type u
β : Type v
m : Type → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
a : α
x : Array α
p : α → α → m Bool
stop : Nat
h : stop ≤ size x
j : Nat
hj : ¬j < stop
⊢ anyPairM.loop x p stop h 0 1 Nat.zero_lt_one = do
    let b ← pure false
    if b = true then pure true else anyPairM.loop x p stop h 0 1 Nat.zero_lt_one
Tactic:
simp only [pure_bind, ite_false]
Proof state after:
no goals
Theorem: Array.anyPairM_empty
Proof state before:
α : Type u
β : Type v
m : Type → Type v
inst✝ : Monad m
p : α → α → m Bool
start stop : Nat
⊢ anyPairM #[] p start stop = pure false
Tactic:
dsimp [anyPairM]
Proof state after:
α : Type u
β : Type v
m : Type → Type v
inst✝ : Monad m
p : α → α → m Bool
start stop : Nat
⊢ (if h : stop ≤ size #[] then anyPairM.loop #[] p stop h start (start + 1) (_ : start < Nat.succ start)
    else
      anyPairM.loop #[] p (size #[]) (_ : Nat.le (size #[]) (size #[])) start (start + 1)
        (_ : start < Nat.succ start)) =
    pure false
Theorem: Array.anyPairM_empty
Proof state before:
α : Type u
β : Type v
m : Type → Type v
inst✝ : Monad m
p : α → α → m Bool
start stop : Nat
⊢ (if h : stop ≤ size #[] then anyPairM.loop #[] p stop h start (start + 1) (_ : start < Nat.succ start)
    else
      anyPairM.loop #[] p (size #[]) (_ : Nat.le (size #[]) (size #[])) start (start + 1)
        (_ : start < Nat.succ start)) =
    pure false
Tactic:
simp only [size_toArray, List.length_nil]
Proof state after:
α : Type u
β : Type v
m : Type → Type v
inst✝ : Monad m
p : α → α → m Bool
start stop : Nat
⊢ (if h : stop ≤ 0 then anyPairM.loop #[] p stop (_ : stop ≤ size #[]) start (start + 1) (_ : start < Nat.succ start)
    else anyPairM.loop #[] p 0 (_ : 0 ≤ size #[]) start (start + 1) (_ : start < Nat.succ start)) =
    pure false