internlm/Lean-Github huggingface dataset:
Theorem: LeanColls.Fold.bind_fold_pure
Proof state before:
case intro.intro.cons
C : Type u_3
τ : Type u_4
inst✝⁵ : Fold C τ
inst✝⁴ : LeanColls.ToList C τ
inst✝³ : ToList C τ
m : Type u_1 → Type u_2
α : Type u_1
inst✝² : ToList C τ
inst✝¹ : Monad m
inst✝ : LawfulMonad m
ma : m α
c : C
f : α → τ → m α
L : List τ
hd : τ
tl : List τ
ih :
  (do
      let x ← ma
      List.foldr
          (fun t acc => do
            let acc ← acc
            f acc t)
          (pure x) tl) =
    List.foldr
      (fun t acc => do
        let acc ← acc
        f acc t)
      ma tl
⊢ (do
      let x ← ma
      let acc ←
        List.foldr
            (fun t acc => do
              let acc ← acc
              f acc t)
            (pure x) tl
      f acc hd) =
    do
    let acc ←
      do
        let x ← ma
        List.foldr
            (fun t acc => do
              let acc ← acc
              f acc t)
            (pure x) tl
    f acc hd
Tactic:
simp
Proof state after:
no goals
Theorem: LeanColls.Fold.any_eq_any_toList
Proof state before:
C : Type u_1
τ : Type u_2
inst✝⁴ : Fold C τ
inst✝³ : LeanColls.ToList C τ
inst✝² : ToList C τ
inst✝¹ : LeanColls.ToList C τ
inst✝ : ToList C τ
f : τ → Bool
c : C
⊢ any f c = (toList c).any f
Tactic:
unfold any
Proof state after:
C : Type u_1
τ : Type u_2
inst✝⁴ : Fold C τ
inst✝³ : LeanColls.ToList C τ
inst✝² : ToList C τ
inst✝¹ : LeanColls.ToList C τ
inst✝ : ToList C τ
f : τ → Bool
c : C
⊢ (match foldM c (fun x x => if f x = true then Except.error () else Except.ok ()) () with
    | Except.ok PUnit.unit => false
    | Except.error PUnit.unit => true) =
    (toList c).any f
Theorem: LeanColls.Fold.any_eq_any_toList
Proof state before:
C : Type u_1
τ : Type u_2
inst✝⁴ : Fold C τ
inst✝³ : LeanColls.ToList C τ
inst✝² : ToList C τ
inst✝¹ : LeanColls.ToList C τ
inst✝ : ToList C τ
f : τ → Bool
c : C
⊢ (match foldM c (fun x x => if f x = true then Except.error () else Except.ok ()) () with
    | Except.ok PUnit.unit => false
    | Except.error PUnit.unit => true) =
    (toList c).any f
Tactic:
generalize hf' : (fun _ _ => _) = f'
Proof state after:
C : Type u_1
τ : Type u_2
inst✝⁴ : Fold C τ
inst✝³ : LeanColls.ToList C τ
inst✝² : ToList C τ
inst✝¹ : LeanColls.ToList C τ
inst✝ : ToList C τ
f : τ → Bool
c : C
f' : Unit → τ → Except Unit Unit
hf' : (fun x x => if f x = true then Except.error () else Except.ok ()) = f'
⊢ (match foldM c f' () with
    | Except.ok PUnit.unit => false
    | Except.error PUnit.unit => true) =
    (toList c).any f
Theorem: LeanColls.Fold.any_eq_any_toList
Proof state before:
C : Type u_1
τ : Type u_2
inst✝⁴ : Fold C τ
inst✝³ : LeanColls.ToList C τ
inst✝² : ToList C τ
inst✝¹ : LeanColls.ToList C τ
inst✝ : ToList C τ
f : τ → Bool
c : C
f' : Unit → τ → Except Unit Unit
hf' : (fun x x => if f x = true then Except.error () else Except.ok ()) = f'
⊢ foldM c f' () = Except.error () ↔ (toList c).any f = true
Tactic:
rw [ToList.foldM_eq_fold]
Proof state after:
C : Type u_1
τ : Type u_2
inst✝⁴ : Fold C τ
inst✝³ : LeanColls.ToList C τ
inst✝² : ToList C τ
inst✝¹ : LeanColls.ToList C τ
inst✝ : ToList C τ
f : τ → Bool
c : C
f' : Unit → τ → Except Unit Unit
hf' : (fun x x => if f x = true then Except.error () else Except.ok ()) = f'
⊢ fold c
        (fun acc x => do
          let x_1 ← acc
          f' x_1 x)
        (pure ()) =
      Except.error () ↔
    (toList c).any f = true
Theorem: LeanColls.Fold.any_eq_any_toList
Proof state before:
C : Type u_1
τ : Type u_2
inst✝⁴ : Fold C τ
inst✝³ : LeanColls.ToList C τ
inst✝² : ToList C τ
inst✝¹ : LeanColls.ToList C τ
inst✝ : ToList C τ
f : τ → Bool
c : C
f' : Unit → τ → Except Unit Unit
hf' : (fun x x => if f x = true then Except.error () else Except.ok ()) = f'
⊢ fold c
        (fun acc x => do
          let x_1 ← acc
          f' x_1 x)
        (pure ()) =
      Except.error () ↔
    (toList c).any f = true
Tactic:
have ⟨L,perm,h⟩ := ToList.fold_eq_fold_toList c
Proof state after:
C : Type u_1
τ : Type u_2
inst✝⁴ : Fold C τ
inst✝³ : LeanColls.ToList C τ
inst✝² : ToList C τ
inst✝¹ : LeanColls.ToList C τ
inst✝ : ToList C τ
f : τ → Bool
c : C
f' : Unit → τ → Except Unit Unit
hf' : (fun x x => if f x = true then Except.error () else Except.ok ()) = f'
L : List τ
perm : L.Perm (toList c)
h : ∀ {β : Type} (f : β → τ → β) (init : β), fold c f init = List.foldl f init L
⊢ fold c
        (fun acc x => do
          let x_1 ← acc
          f' x_1 x)
        (pure ()) =
      Except.error () ↔
    (toList c).any f = true
Theorem: LeanColls.Fold.any_eq_any_toList
Proof state before:
C : Type u_1
τ : Type u_2
inst✝⁴ : Fold C τ
inst✝³ : LeanColls.ToList C τ
inst✝² : ToList C τ
inst✝¹ : LeanColls.ToList C τ
inst✝ : ToList C τ
f : τ → Bool
c : C
f' : Unit → τ → Except Unit Unit
hf' : (fun x x => if f x = true then Except.error () else Except.ok ()) = f'
L : List τ
perm : L.Perm (toList c)
h : ∀ {β : Type} (f : β → τ → β) (init : β), fold c f init = List.foldl f init L
⊢ fold c
        (fun acc x => do
          let x_1 ← acc
          f' x_1 x)
        (pure ()) =
      Except.error () ↔
    (toList c).any f = true
Tactic:
rw [h]
Proof state after:
C : Type u_1
τ : Type u_2
inst✝⁴ : Fold C τ
inst✝³ : LeanColls.ToList C τ
inst✝² : ToList C τ
inst✝¹ : LeanColls.ToList C τ
inst✝ : ToList C τ
f : τ → Bool
c : C
f' : Unit → τ → Except Unit Unit
hf' : (fun x x => if f x = true then Except.error () else Except.ok ()) = f'
L : List τ
perm : L.Perm (toList c)
h : ∀ {β : Type} (f : β → τ → β) (init : β), fold c f init = List.foldl f init L
⊢ List.foldl
        (fun acc x => do
          let x_1 ← acc
          f' x_1 x)
        (pure ()) L =
      Except.error () ↔
    (toList c).any f = true
Theorem: LeanColls.Fold.any_eq_any_toList
Proof state before:
C : Type u_1
τ : Type u_2
inst✝⁴ : Fold C τ
inst✝³ : LeanColls.ToList C τ
inst✝² : ToList C τ
inst✝¹ : LeanColls.ToList C τ
inst✝ : ToList C τ
f : τ → Bool
c : C
f' : Unit → τ → Except Unit Unit
hf' : (fun x x => if f x = true then Except.error () else Except.ok ()) = f'
L : List τ
perm : L.Perm (toList c)
h : ∀ {β : Type} (f : β → τ → β) (init : β), fold c f init = List.foldl f init L
⊢ List.foldl
        (fun acc x => do
          let x_1 ← acc
          f' x_1 x)
        (pure ()) L =
      Except.error () ↔
    (toList c).any f = true
Tactic:
clear h
Proof state after:
C : Type u_1
τ : Type u_2
inst✝⁴ : Fold C τ
inst✝³ : LeanColls.ToList C τ
inst✝² : ToList C τ
inst✝¹ : LeanColls.ToList C τ
inst✝ : ToList C τ
f : τ → Bool
c : C
f' : Unit → τ → Except Unit Unit
hf' : (fun x x => if f x = true then Except.error () else Except.ok ()) = f'
L : List τ
perm : L.Perm (toList c)
⊢ List.foldl
        (fun acc x => do
          let x_1 ← acc
          f' x_1 x)
        (pure ()) L =
      Except.error () ↔
    (toList c).any f = true
Theorem: LeanColls.Fold.any_eq_any_toList
Proof state before:
C : Type u_1
τ : Type u_2
inst✝⁴ : Fold C τ
inst✝³ : LeanColls.ToList C τ
inst✝² : ToList C τ
inst✝¹ : LeanColls.ToList C τ
inst✝ : ToList C τ
f : τ → Bool
c : C
f' : Unit → τ → Except Unit Unit
hf' : (fun x x => if f x = true then Except.error () else Except.ok ()) = f'
L : List τ
perm : L.Perm (toList c)
⊢ List.foldl
        (fun acc x => do
          let x_1 ← acc
          f' x_1 x)
        (pure ()) L =
      Except.error () ↔
    (toList c).any f = true
Tactic:
simp_rw [List.any_eq_true, ← perm.mem_iff]
Proof state after:
C : Type u_1
τ : Type u_2
inst✝⁴ : Fold C τ
inst✝³ : LeanColls.ToList C τ
inst✝² : ToList C τ
inst✝¹ : LeanColls.ToList C τ
inst✝ : ToList C τ
f : τ → Bool
c : C
f' : Unit → τ → Except Unit Unit
hf' : (fun x x => if f x = true then Except.error () else Except.ok ()) = f'
L : List τ
perm : L.Perm (toList c)
⊢ List.foldl
        (fun acc x => do
          let x_1 ← acc
          f' x_1 x)
        (pure ()) L =
      Except.error () ↔
    ∃ x ∈ L, f x = true
Theorem: LeanColls.Fold.any_eq_any_toList
Proof state before:
C : Type u_1
τ : Type u_2
inst✝⁴ : Fold C τ
inst✝³ : LeanColls.ToList C τ
inst✝² : ToList C τ
inst✝¹ : LeanColls.ToList C τ
inst✝ : ToList C τ
f : τ → Bool
c : C
f' : Unit → τ → Except Unit Unit
hf' : (fun x x => if f x = true then Except.error () else Except.ok ()) = f'
L : List τ
perm : L.Perm (toList c)
⊢ List.foldl
        (fun acc x => do
          let x_1 ← acc
          f' x_1 x)
        (pure ()) L =
      Except.error () ↔
    ∃ x ∈ L, f x = true
Tactic:
clear perm c
Proof state after:
C : Type u_1
τ : Type u_2
inst✝⁴ : Fold C τ
inst✝³ : LeanColls.ToList C τ
inst✝² : ToList C τ
inst✝¹ : LeanColls.ToList C τ
inst✝ : ToList C τ
f : τ → Bool
f' : Unit → τ → Except Unit Unit
hf' : (fun x x => if f x = true then Except.error () else Except.ok ()) = f'
L : List τ
⊢ List.foldl
        (fun acc x => do
          let x_1 ← acc
          f' x_1 x)
        (pure ()) L =
      Except.error () ↔
    ∃ x ∈ L, f x = true
Theorem: LeanColls.Fold.any_eq_any_toList
Proof state before:
C : Type u_1
τ : Type u_2
inst✝⁴ : Fold C τ
inst✝³ : LeanColls.ToList C τ
inst✝² : ToList C τ
inst✝¹ : LeanColls.ToList C τ
inst✝ : ToList C τ
f : τ → Bool
f' : Unit → τ → Except Unit Unit
hf' : (fun x x => if f x = true then Except.error () else Except.ok ()) = f'
L : List τ
⊢ List.foldl
        (fun acc x => do
          let x_1 ← acc
          f' x_1 x)
        (pure ()) L =
      Except.error () ↔
    ∃ x ∈ L, f x = true
Tactic:
subst hf'
Proof state after:
C : Type u_1
τ : Type u_2
inst✝⁴ : Fold C τ
inst✝³ : LeanColls.ToList C τ
inst✝² : ToList C τ
inst✝¹ : LeanColls.ToList C τ
inst✝ : ToList C τ
f : τ → Bool
L : List τ
⊢ List.foldl
        (fun acc x => do
          let x_1 ← acc
          (fun x x => if f x = true then Except.error () else Except.ok ()) x_1 x)
        (pure ()) L =
      Except.error () ↔
    ∃ x ∈ L, f x = true
Theorem: LeanColls.Fold.any_eq_any_toList
Proof state before:
C : Type u_1
τ : Type u_2
inst✝⁴ : Fold C τ
inst✝³ : LeanColls.ToList C τ
inst✝² : ToList C τ
inst✝¹ : LeanColls.ToList C τ
inst✝ : ToList C τ
f : τ → Bool
L : List τ
⊢ List.foldl
        (fun acc x => do
          let x_1 ← acc
          (fun x x => if f x = true then Except.error () else Except.ok ()) x_1 x)
        (pure ()) L =
      Except.error () ↔
    ∃ x ∈ L, f x = true
Tactic:
rw [← List.foldlM_eq_foldl]
Proof state after:
C : Type u_1
τ : Type u_2
inst✝⁴ : Fold C τ
inst✝³ : LeanColls.ToList C τ
inst✝² : ToList C τ
inst✝¹ : LeanColls.ToList C τ
inst✝ : ToList C τ
f : τ → Bool
L : List τ
⊢ List.foldlM (fun x x_1 => (fun x x => if f x = true then Except.error () else Except.ok ()) x x_1) () L =
      Except.error () ↔
    ∃ x ∈ L, f x = true
Theorem: LeanColls.Fold.any_eq_any_toList
Proof state before:
C : Type u_1
τ : Type u_2
inst✝⁴ : Fold C τ
inst✝³ : LeanColls.ToList C τ
inst✝² : ToList C τ
inst✝¹ : LeanColls.ToList C τ
inst✝ : ToList C τ
f : τ → Bool
L : List τ
⊢ List.foldlM (fun x x_1 => (fun x x => if f x = true then Except.error () else Except.ok ()) x x_1) () L =
      Except.error () ↔
    ∃ x ∈ L, f x = true
Tactic:
induction L with
| nil => simp_all [pure, Except.pure]
| cons hd tl ih =>
  simp [bind, Except.bind]
  by_cases f hd = true <;> simp_all
Proof state after:
no goals
Theorem: LeanColls.Fold.any_eq_any_toList
Proof state before:
C : Type u_1
τ : Type u_2
inst✝⁴ : Fold C τ
inst✝³ : LeanColls.ToList C τ
inst✝² : ToList C τ
inst✝¹ : LeanColls.ToList C τ
inst✝ : ToList C τ
f : τ → Bool
c : C
f' : Unit → τ → Except Unit Unit
hf' : (fun x x => if f x = true then Except.error () else Except.ok ()) = f'
this : foldM c f' () = Except.error () ↔ (toList c).any f = true
⊢ (match foldM c f' () with
    | Except.ok PUnit.unit => false
    | Except.error PUnit.unit => true) =
    (toList c).any f
Tactic:
rw [eq_comm]
Proof state after:
C : Type u_1
τ : Type u_2
inst✝⁴ : Fold C τ
inst✝³ : LeanColls.ToList C τ
inst✝² : ToList C τ
inst✝¹ : LeanColls.ToList C τ
inst✝ : ToList C τ
f : τ → Bool
c : C
f' : Unit → τ → Except Unit Unit
hf' : (fun x x => if f x = true then Except.error () else Except.ok ()) = f'
this : foldM c f' () = Except.error () ↔ (toList c).any f = true
⊢ (toList c).any f =
    match foldM c f' () with
    | Except.ok PUnit.unit => false
    | Except.error PUnit.unit => true
Theorem: LeanColls.Fold.any_eq_any_toList
Proof state before:
C : Type u_1
τ : Type u_2
inst✝⁴ : Fold C τ
inst✝³ : LeanColls.ToList C τ
inst✝² : ToList C τ
inst✝¹ : LeanColls.ToList C τ
inst✝ : ToList C τ
f : τ → Bool
c : C
f' : Unit → τ → Except Unit Unit
hf' : (fun x x => if f x = true then Except.error () else Except.ok ()) = f'
this : foldM c f' () = Except.error () ↔ (toList c).any f = true
⊢ (toList c).any f =
    match foldM c f' () with
    | Except.ok PUnit.unit => false
    | Except.error PUnit.unit => true
Tactic:
split
Proof state after:
case h_1
C : Type u_1
τ : Type u_2
inst✝⁴ : Fold C τ
inst✝³ : LeanColls.ToList C τ
inst✝² : ToList C τ
inst✝¹ : LeanColls.ToList C τ
inst✝ : ToList C τ
f : τ → Bool
c : C
f' : Unit → τ → Except Unit Unit
hf' : (fun x x => if f x = true then Except.error () else Except.ok ()) = f'
this : foldM c f' () = Except.error () ↔ (toList c).any f = true
x✝ : Except Unit Unit
heq✝ : foldM c f' () = Except.ok PUnit.unit
⊢ (toList c).any f = false

case h_2
C : Type u_1
τ : Type u_2
inst✝⁴ : Fold C τ
inst✝³ : LeanColls.ToList C τ
inst✝² : ToList C τ
inst✝¹ : LeanColls.ToList C τ
inst✝ : ToList C τ
f : τ → Bool
c : C
f' : Unit → τ → Except Unit Unit
hf' : (fun x x => if f x = true then Except.error () else Except.ok ()) = f'
this : foldM c f' () = Except.error () ↔ (toList c).any f = true
x✝ : Except Unit Unit
heq✝ : foldM c f' () = Except.error PUnit.unit
⊢ (toList c).any f = true
Theorem: LeanColls.Fold.any_eq_any_toList
Proof state before:
case h_1
C : Type u_1
τ : Type u_2
inst✝⁴ : Fold C τ
inst✝³ : LeanColls.ToList C τ
inst✝² : ToList C τ
inst✝¹ : LeanColls.ToList C τ
inst✝ : ToList C τ
f : τ → Bool
c : C
f' : Unit → τ → Except Unit Unit
hf' : (fun x x => if f x = true then Except.error () else Except.ok ()) = f'
this : foldM c f' () = Except.error () ↔ (toList c).any f = true
x✝ : Except Unit Unit
heq✝ : foldM c f' () = Except.ok PUnit.unit
⊢ (toList c).any f = false
Tactic:
rw [Bool.eq_false_iff]
Proof state after:
case h_1
C : Type u_1
τ : Type u_2
inst✝⁴ : Fold C τ
inst✝³ : LeanColls.ToList C τ
inst✝² : ToList C τ
inst✝¹ : LeanColls.ToList C τ
inst✝ : ToList C τ
f : τ → Bool
c : C
f' : Unit → τ → Except Unit Unit
hf' : (fun x x => if f x = true then Except.error () else Except.ok ()) = f'
this : foldM c f' () = Except.error () ↔ (toList c).any f = true
x✝ : Except Unit Unit
heq✝ : foldM c f' () = Except.ok PUnit.unit
⊢ (toList c).any f ≠ true
Theorem: LeanColls.Fold.any_eq_any_toList
Proof state before:
case h_1
C : Type u_1
τ : Type u_2
inst✝⁴ : Fold C τ
inst✝³ : LeanColls.ToList C τ
inst✝² : ToList C τ
inst✝¹ : LeanColls.ToList C τ
inst✝ : ToList C τ
f : τ → Bool
c : C
f' : Unit → τ → Except Unit Unit
hf' : (fun x x => if f x = true then Except.error () else Except.ok ()) = f'
this : foldM c f' () = Except.error () ↔ (toList c).any f = true
x✝ : Except Unit Unit
heq✝ : foldM c f' () = Except.ok PUnit.unit
⊢ (toList c).any f ≠ true
Tactic:
aesop
Proof state after:
no goals
Theorem: LeanColls.Fold.any_eq_any_toList
Proof state before:
case h_2
C : Type u_1
τ : Type u_2
inst✝⁴ : Fold C τ
inst✝³ : LeanColls.ToList C τ
inst✝² : ToList C τ
inst✝¹ : LeanColls.ToList C τ
inst✝ : ToList C τ
f : τ → Bool
c : C
f' : Unit → τ → Except Unit Unit
hf' : (fun x x => if f x = true then Except.error () else Except.ok ()) = f'
this : foldM c f' () = Except.error () ↔ (toList c).any f = true
x✝ : Except Unit Unit
heq✝ : foldM c f' () = Except.error PUnit.unit
⊢ (toList c).any f = true
Tactic:
aesop
Proof state after:
no goals
Theorem: LeanColls.Fold.any_eq_any_toList
Proof state before:
case nil
C : Type u_1
τ : Type u_2
inst✝⁴ : Fold C τ
inst✝³ : LeanColls.ToList C τ
inst✝² : ToList C τ
inst✝¹ : LeanColls.ToList C τ
inst✝ : ToList C τ
f : τ → Bool
⊢ List.foldlM (fun x x_1 => (fun x x => if f x = true then Except.error () else Except.ok ()) x x_1) () [] =
      Except.error () ↔
    ∃ x ∈ [], f x = true
Tactic:
simp_all [pure, Except.pure]
Proof state after:
no goals
Theorem: LeanColls.Fold.any_eq_any_toList
Proof state before:
case cons
C : Type u_1
τ : Type u_2
inst✝⁴ : Fold C τ
inst✝³ : LeanColls.ToList C τ
inst✝² : ToList C τ
inst✝¹ : LeanColls.ToList C τ
inst✝ : ToList C τ
f : τ → Bool
hd : τ
tl : List τ
ih :
  List.foldlM (fun x x_1 => (fun x x => if f x = true then Except.error () else Except.ok ()) x x_1) () tl =
      Except.error () ↔
    ∃ x ∈ tl, f x = true
⊢ List.foldlM (fun x x_1 => (fun x x => if f x = true then Except.error () else Except.ok ()) x x_1) () (hd :: tl) =
      Except.error () ↔
    ∃ x ∈ hd :: tl, f x = true
Tactic:
simp [bind, Except.bind]
Proof state after:
case cons
C : Type u_1
τ : Type u_2
inst✝⁴ : Fold C τ
inst✝³ : LeanColls.ToList C τ
inst✝² : ToList C τ
inst✝¹ : LeanColls.ToList C τ
inst✝ : ToList C τ
f : τ → Bool
hd : τ
tl : List τ
ih :
  List.foldlM (fun x x_1 => (fun x x => if f x = true then Except.error () else Except.ok ()) x x_1) () tl =
      Except.error () ↔
    ∃ x ∈ tl, f x = true
⊢ (match if f hd = true then Except.error () else Except.ok () with
      | Except.error err => Except.error err
      | Except.ok v => List.foldlM (fun x x => if f x = true then Except.error () else Except.ok ()) v tl) =
      Except.error () ↔
    f hd = true ∨ ∃ a ∈ tl, f a = true
Theorem: LeanColls.Fold.any_eq_any_toList
Proof state before:
case cons
C : Type u_1
τ : Type u_2
inst✝⁴ : Fold C τ
inst✝³ : LeanColls.ToList C τ
inst✝² : ToList C τ
inst✝¹ : LeanColls.ToList C τ
inst✝ : ToList C τ
f : τ → Bool
hd : τ
tl : List τ
ih :
  List.foldlM (fun x x_1 => (fun x x => if f x = true then Except.error () else Except.ok ()) x x_1) () tl =
      Except.error () ↔
    ∃ x ∈ tl, f x = true
⊢ (match if f hd = true then Except.error () else Except.ok () with
      | Except.error err => Except.error err
      | Except.ok v => List.foldlM (fun x x => if f x = true then Except.error () else Except.ok ()) v tl) =
      Except.error () ↔
    f hd = true ∨ ∃ a ∈ tl, f a = true
Tactic:
by_cases f hd = true <;> simp_all
Proof state after:
no goals
Theorem: LeanColls.Fold.all_eq_all_toList
Proof state before:
C : Type u_1
τ : Type u_2
inst✝⁴ : Fold C τ
inst✝³ : LeanColls.ToList C τ
inst✝² : ToList C τ
inst✝¹ : LeanColls.ToList C τ
inst✝ : ToList C τ
f : τ → Bool
c : C
⊢ all f c = (toList c).all f
Tactic:
unfold all
Proof state after:
C : Type u_1
τ : Type u_2
inst✝⁴ : Fold C τ
inst✝³ : LeanColls.ToList C τ
inst✝² : ToList C τ
inst✝¹ : LeanColls.ToList C τ
inst✝ : ToList C τ
f : τ → Bool
c : C
⊢ (match foldM c (fun x x => if f x = true then Except.ok () else Except.error ()) () with
    | Except.ok PUnit.unit => true
    | Except.error PUnit.unit => false) =
    (toList c).all f
Theorem: LeanColls.Fold.all_eq_all_toList
Proof state before:
C : Type u_1
τ : Type u_2
inst✝⁴ : Fold C τ
inst✝³ : LeanColls.ToList C τ
inst✝² : ToList C τ
inst✝¹ : LeanColls.ToList C τ
inst✝ : ToList C τ
f : τ → Bool
c : C
⊢ (match foldM c (fun x x => if f x = true then Except.ok () else Except.error ()) () with
    | Except.ok PUnit.unit => true
    | Except.error PUnit.unit => false) =
    (toList c).all f
Tactic:
generalize hf' : (fun _ _ => _) = f'
Proof state after:
C : Type u_1
τ : Type u_2
inst✝⁴ : Fold C τ
inst✝³ : LeanColls.ToList C τ
inst✝² : ToList C τ
inst✝¹ : LeanColls.ToList C τ
inst✝ : ToList C τ
f : τ → Bool
c : C
f' : Unit → τ → Except Unit Unit
hf' : (fun x x => if f x = true then Except.ok () else Except.error ()) = f'
⊢ (match foldM c f' () with
    | Except.ok PUnit.unit => true
    | Except.error PUnit.unit => false) =
    (toList c).all f
Theorem: LeanColls.Fold.all_eq_all_toList
Proof state before:
C : Type u_1
τ : Type u_2
inst✝⁴ : Fold C τ
inst✝³ : LeanColls.ToList C τ
inst✝² : ToList C τ
inst✝¹ : LeanColls.ToList C τ
inst✝ : ToList C τ
f : τ → Bool
c : C
f' : Unit → τ → Except Unit Unit
hf' : (fun x x => if f x = true then Except.ok () else Except.error ()) = f'
⊢ foldM c f' () = Except.ok () ↔ (toList c).all f = true
Tactic:
rw [ToList.foldM_eq_fold]
Proof state after:
C : Type u_1
τ : Type u_2
inst✝⁴ : Fold C τ
inst✝³ : LeanColls.ToList C τ
inst✝² : ToList C τ
inst✝¹ : LeanColls.ToList C τ
inst✝ : ToList C τ
f : τ → Bool
c : C
f' : Unit → τ → Except Unit Unit
hf' : (fun x x => if f x = true then Except.ok () else Except.error ()) = f'
⊢ fold c
        (fun acc x => do
          let x_1 ← acc
          f' x_1 x)
        (pure ()) =
      Except.ok () ↔
    (toList c).all f = true
Theorem: LeanColls.Fold.all_eq_all_toList
Proof state before:
C : Type u_1
τ : Type u_2
inst✝⁴ : Fold C τ
inst✝³ : LeanColls.ToList C τ
inst✝² : ToList C τ
inst✝¹ : LeanColls.ToList C τ
inst✝ : ToList C τ
f : τ → Bool
c : C
f' : Unit → τ → Except Unit Unit
hf' : (fun x x => if f x = true then Except.ok () else Except.error ()) = f'
⊢ fold c
        (fun acc x => do
          let x_1 ← acc
          f' x_1 x)
        (pure ()) =
      Except.ok () ↔
    (toList c).all f = true
Tactic:
have ⟨L,perm,h⟩ := ToList.fold_eq_fold_toList c
Proof state after:
C : Type u_1
τ : Type u_2
inst✝⁴ : Fold C τ
inst✝³ : LeanColls.ToList C τ
inst✝² : ToList C τ
inst✝¹ : LeanColls.ToList C τ
inst✝ : ToList C τ
f : τ → Bool
c : C
f' : Unit → τ → Except Unit Unit
hf' : (fun x x => if f x = true then Except.ok () else Except.error ()) = f'
L : List τ
perm : L.Perm (toList c)
h : ∀ {β : Type} (f : β → τ → β) (init : β), fold c f init = List.foldl f init L
⊢ fold c
        (fun acc x => do
          let x_1 ← acc
          f' x_1 x)
        (pure ()) =
      Except.ok () ↔
    (toList c).all f = true
Theorem: LeanColls.Fold.all_eq_all_toList
Proof state before:
C : Type u_1
τ : Type u_2
inst✝⁴ : Fold C τ
inst✝³ : LeanColls.ToList C τ
inst✝² : ToList C τ
inst✝¹ : LeanColls.ToList C τ
inst✝ : ToList C τ
f : τ → Bool
c : C
f' : Unit → τ → Except Unit Unit
hf' : (fun x x => if f x = true then Except.ok () else Except.error ()) = f'
L : List τ
perm : L.Perm (toList c)
h : ∀ {β : Type} (f : β → τ → β) (init : β), fold c f init = List.foldl f init L
⊢ fold c
        (fun acc x => do
          let x_1 ← acc
          f' x_1 x)
        (pure ()) =
      Except.ok () ↔
    (toList c).all f = true
Tactic:
rw [h]
Proof state after:
C : Type u_1
τ : Type u_2
inst✝⁴ : Fold C τ
inst✝³ : LeanColls.ToList C τ
inst✝² : ToList C τ
inst✝¹ : LeanColls.ToList C τ
inst✝ : ToList C τ
f : τ → Bool
c : C
f' : Unit → τ → Except Unit Unit
hf' : (fun x x => if f x = true then Except.ok () else Except.error ()) = f'
L : List τ
perm : L.Perm (toList c)
h : ∀ {β : Type} (f : β → τ → β) (init : β), fold c f init = List.foldl f init L
⊢ List.foldl
        (fun acc x => do
          let x_1 ← acc
          f' x_1 x)
        (pure ()) L =
      Except.ok () ↔
    (toList c).all f = true
Theorem: LeanColls.Fold.all_eq_all_toList
Proof state before:
C : Type u_1
τ : Type u_2
inst✝⁴ : Fold C τ
inst✝³ : LeanColls.ToList C τ
inst✝² : ToList C τ
inst✝¹ : LeanColls.ToList C τ
inst✝ : ToList C τ
f : τ → Bool
c : C
f' : Unit → τ → Except Unit Unit
hf' : (fun x x => if f x = true then Except.ok () else Except.error ()) = f'
L : List τ
perm : L.Perm (toList c)
h : ∀ {β : Type} (f : β → τ → β) (init : β), fold c f init = List.foldl f init L
⊢ List.foldl
        (fun acc x => do
          let x_1 ← acc
          f' x_1 x)
        (pure ()) L =
      Except.ok () ↔
    (toList c).all f = true
Tactic:
clear h
Proof state after:
C : Type u_1
τ : Type u_2
inst✝⁴ : Fold C τ
inst✝³ : LeanColls.ToList C τ
inst✝² : ToList C τ
inst✝¹ : LeanColls.ToList C τ
inst✝ : ToList C τ
f : τ → Bool
c : C
f' : Unit → τ → Except Unit Unit
hf' : (fun x x => if f x = true then Except.ok () else Except.error ()) = f'
L : List τ
perm : L.Perm (toList c)
⊢ List.foldl
        (fun acc x => do
          let x_1 ← acc
          f' x_1 x)
        (pure ()) L =
      Except.ok () ↔
    (toList c).all f = true