Theorem: LeanColls.Fold.all_eq_all_toList (LeanColls/Classes/Ops/Fold.lean)

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
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

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'
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

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]
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

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
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

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]
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

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
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

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)
⊢ List.foldl
        (fun acc x => do
          let x_1 ← acc
          f' x_1 x)
        (pure ()) L =
      Except.ok () ↔
    (toList c).all f = true
Tactic:
simp_rw [List.all_eq_true, ← perm.mem_iff]
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 () ↔
    ∀ x ∈ L, f x = true

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)
⊢ List.foldl
        (fun acc x => do
          let x_1 ← acc
          f' x_1 x)
        (pure ()) L =
      Except.ok () ↔
    ∀ x ∈ L, f x = true
Tactic:
clear perm c
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.ok () else Except.error ()) = f'
L : List τ
⊢ List.foldl
        (fun acc x => do
          let x_1 ← acc
          f' x_1 x)
        (pure ()) L =
      Except.ok () ↔
    ∀ x ∈ L, f x = true

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.ok () else Except.error ()) = f'
L : List τ
⊢ List.foldl
        (fun acc x => do
          let x_1 ← acc
          f' x_1 x)
        (pure ()) L =
      Except.ok () ↔
    ∀ x ∈ L, f x = true
Tactic:
subst hf'
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.ok () else Except.error ()) x_1 x)
        (pure ()) L =
      Except.ok () ↔
    ∀ x ∈ L, f x = true

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.ok () else Except.error ()) x_1 x)
        (pure ()) L =
      Except.ok () ↔
    ∀ x ∈ L, f x = true
Tactic:
rw [← List.foldlM_eq_foldl]
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.ok () else Except.error ()) x x_1) () L =
      Except.ok () ↔
    ∀ x ∈ L, f x = true

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.ok () else Except.error ()) x x_1) () L =
      Except.ok () ↔
    ∀ 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
State after:
no goals

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'
this : foldM c f' () = Except.ok () ↔ (toList c).all f = true
⊢ (match foldM c f' () with
    | Except.ok PUnit.unit => true
    | Except.error PUnit.unit => false) =
    (toList c).all f
Tactic:
rw [eq_comm]
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'
this : foldM c f' () = Except.ok () ↔ (toList c).all f = true
⊢ (toList c).all f =
    match foldM c f' () with
    | Except.ok PUnit.unit => true
    | Except.error PUnit.unit => false

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'
this : foldM c f' () = Except.ok () ↔ (toList c).all f = true
⊢ (toList c).all f =
    match foldM c f' () with
    | Except.ok PUnit.unit => true
    | Except.error PUnit.unit => false
Tactic:
split
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.ok () else Except.error ()) = f'
this : foldM c f' () = Except.ok () ↔ (toList c).all f = true
x✝ : Except Unit Unit
heq✝ : foldM c f' () = Except.ok PUnit.unit
⊢ (toList c).all f = true

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.ok () else Except.error ()) = f'
this : foldM c f' () = Except.ok () ↔ (toList c).all f = true
x✝ : Except Unit Unit
heq✝ : foldM c f' () = Except.error PUnit.unit
⊢ (toList c).all f = false

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.ok () else Except.error ()) = f'
this : foldM c f' () = Except.ok () ↔ (toList c).all f = true
x✝ : Except Unit Unit
heq✝ : foldM c f' () = Except.ok PUnit.unit
⊢ (toList c).all f = true
Tactic:
aesop
State after:
no goals

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.ok () else Except.error ()) = f'
this : foldM c f' () = Except.ok () ↔ (toList c).all f = true
x✝ : Except Unit Unit
heq✝ : foldM c f' () = Except.error PUnit.unit
⊢ (toList c).all f = false
Tactic:
rw [Bool.eq_false_iff]
State after:
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.ok () else Except.error ()) = f'
this : foldM c f' () = Except.ok () ↔ (toList c).all f = true
x✝ : Except Unit Unit
heq✝ : foldM c f' () = Except.error PUnit.unit
⊢ (toList c).all f ≠ true

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.ok () else Except.error ()) = f'
this : foldM c f' () = Except.ok () ↔ (toList c).all f = true
x✝ : Except Unit Unit
heq✝ : foldM c f' () = Except.error PUnit.unit
⊢ (toList c).all f ≠ true
Tactic:
aesop
State after:
no goals

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.ok () else Except.error ()) x x_1) () [] =
      Except.ok () ↔
    ∀ x ∈ [], f x = true
Tactic:
simp_all [pure, Except.pure]
State after:
no goals

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.ok () else Except.error ()) x x_1) () tl =
      Except.ok () ↔
    ∀ x ∈ tl, f x = true
⊢ List.foldlM (fun x x_1 => (fun x x => if f x = true then Except.ok () else Except.error ()) x x_1) () (hd :: tl) =
      Except.ok () ↔
    ∀ x ∈ hd :: tl, f x = true
Tactic:
simp [bind, Except.bind]
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.ok () else Except.error ()) x x_1) () tl =
      Except.ok () ↔
    ∀ x ∈ tl, f x = true
⊢ (match if f hd = true then Except.ok () else Except.error () with
      | Except.error err => Except.error err
      | Except.ok v => List.foldlM (fun x x => if f x = true then Except.ok () else Except.error ()) v tl) =
      Except.ok () ↔
    f hd = true ∧ ∀ a ∈ tl, f a = true

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.ok () else Except.error ()) x x_1) () tl =
      Except.ok () ↔
    ∀ x ∈ tl, f x = true
⊢ (match if f hd = true then Except.ok () else Except.error () with
      | Except.error err => Except.error err
      | Except.ok v => List.foldlM (fun x x => if f x = true then Except.ok () else Except.error ()) v tl) =
      Except.ok () ↔
    f hd = true ∧ ∀ a ∈ tl, f a = true
Tactic:
by_cases f hd = true <;> simp_all
State after:
no goals