Theorem: Etch.Verification.Stream.fold_wf_invalid (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 : s.σ
acc : β
h : ¬s.valid q = true
⊢ fold_wf f s q acc = 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 : s.σ
acc : β
h : ¬s.valid q = true
⊢ (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) =
    acc

State before:
ι : Type
α : Type u_2
a b s✝ : Stream ι α
inst✝¹ : Preorder ι
β : Sort u_1
f : β → ι → α → β
s : Stream ι α
inst✝ : IsBounded s
q : s.σ
acc : β
h : ¬s.valid q = true
⊢ (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) =
    acc
Tactic:
simp [h]
State after:
no goals