Theorem: Etch.Verification.Stream.fold_wf_spec (Etch/StreamFusion/Proofs/StreamProof.lean)

State before:
ι : Type
α : Type u_2
a b s✝ : Stream ι α
inst✝¹ : Preorder ι
β : Sort u_1
f : β → ι → α → β
s : Stream ι α
inst✝ : IsBounded s
q : { q // s.valid q = true }
acc : β
⊢ fold_wf f s (↑q) acc =
    fold_wf f s (advance s ↑q)
      (if hr : s.ready q = true then f acc (s.index q) (s.value { val := q, property := hr }) else acc)
Tactic:
rw [Stream.fold_wf, fold_wf.go]
State after:
ι : Type
α : Type u_2
a b s✝ : Stream ι α
inst✝¹ : Preorder ι
β : Sort u_1
f : β → ι → α → β
s : Stream ι α
inst✝ : IsBounded s
q : { q // s.valid q = true }
acc : β
⊢ (if hv : s.valid ↑q = true then
      let i := s.index { val := ↑q, property := hv };
      let hr := s.ready { val := ↑q, property := hv };
      let q' := next s { val := ↑q, property := hv } i hr;
      let acc' :=
        if hr : hr = true then f acc i (s.value { val := { val := ↑q, property := hv }, property := hr }) else acc;
      fold_wf.go s f s.valid (fun q h => s.ready { val := q, property := h })
        (fun q h => s.index { val := q, property := h })
        (fun q v r => s.value { val := { val := q, property := v }, property := r }) (next s) ⋯ acc' q'
    else acc) =
    fold_wf f s (advance s ↑q)
      (if hr : s.ready q = true then f acc (s.index q) (s.value { val := q, property := hr }) else acc)

State before:
ι : Type
α : Type u_2
a b s✝ : Stream ι α
inst✝¹ : Preorder ι
β : Sort u_1
f : β → ι → α → β
s : Stream ι α
inst✝ : IsBounded s
q : { q // s.valid q = true }
acc : β
⊢ (if hv : s.valid ↑q = true then
      let i := s.index { val := ↑q, property := hv };
      let hr := s.ready { val := ↑q, property := hv };
      let q' := next s { val := ↑q, property := hv } i hr;
      let acc' :=
        if hr : hr = true then f acc i (s.value { val := { val := ↑q, property := hv }, property := hr }) else acc;
      fold_wf.go s f s.valid (fun q h => s.ready { val := q, property := h })
        (fun q h => s.index { val := q, property := h })
        (fun q v r => s.value { val := { val := q, property := v }, property := r }) (next s) ⋯ acc' q'
    else acc) =
    fold_wf f s (advance s ↑q)
      (if hr : s.ready q = true then f acc (s.index q) (s.value { val := q, property := hr }) else acc)
Tactic:
simp only [q.prop, Subtype.coe_eta, dite_true, advance_val]
State after:
ι : Type
α : Type u_2
a b s✝ : Stream ι α
inst✝¹ : Preorder ι
β : Sort u_1
f : β → ι → α → β
s : Stream ι α
inst✝ : IsBounded s
q : { q // s.valid q = true }
acc : β
⊢ fold_wf.go s f s.valid (fun q h => s.ready { val := q, property := h })
      (fun q h => s.index { val := q, property := h })
      (fun q v r => s.value { val := { val := q, property := v }, property := r }) (next s) ⋯
      (if h : s.ready q = true then f acc (s.index q) (s.value { val := q, property := ⋯ }) else acc)
      (next s q (s.index q) (s.ready q)) =
    fold_wf f s (s.seek q (toOrder s q))
      (if hr : s.ready q = true then f acc (s.index q) (s.value { val := q, property := hr }) else acc)

State before:
ι : Type
α : Type u_2
a b s✝ : Stream ι α
inst✝¹ : Preorder ι
β : Sort u_1
f : β → ι → α → β
s : Stream ι α
inst✝ : IsBounded s
q : { q // s.valid q = true }
acc : β
⊢ fold_wf.go s f s.valid (fun q h => s.ready { val := q, property := h })
      (fun q h => s.index { val := q, property := h })
      (fun q v r => s.value { val := { val := q, property := v }, property := r }) (next s) ⋯
      (if h : s.ready q = true then f acc (s.index q) (s.value { val := q, property := ⋯ }) else acc)
      (next s q (s.index q) (s.ready q)) =
    fold_wf f s (s.seek q (toOrder s q))
      (if hr : s.ready q = true then f acc (s.index q) (s.value { val := q, property := hr }) else acc)
Tactic:
rfl
State after:
no goals