internlm/Lean-Github huggingface dataset:
Theorem: Etch.Verification.Stream.LawfulOfStream.get_fold
Proof state before:
ι : Type
inst✝⁹ : LinearOrder ι
α : Type u_1
β : Type u_2
m : Type u_3
γ : Type u_4
inst✝⁸ : Zero α
inst✝⁷ : Zero β
inst✝⁶ : Zero m
inst✝⁵ : AddCommMonoid γ
inst✝⁴ : EvalToFinsupp α γ
inst✝³ : EvalToFinsupp β γ
inst✝² : LawfulOfStream α β γ
inst✝¹ : LawfulModifiable ι β m
s : Stream ι α
inst✝ : IsBounded s
i : ι
q : s.σ
ih :
  ∀ (y : s.σ),
    WfRel s y q →
      ∀ (b : m),
        evalFinsupp (Readable.get (fold_wf Modifiable.update (map OfStream.eval s) y b) i) =
          evalFinsupp (Readable.get b i) + (eval (map (⇑evalFinsupp) s) y) i
b : m
⊢ evalFinsupp (Readable.get (fold_wf Modifiable.update (map OfStream.eval s) q b) i) =
    evalFinsupp (Readable.get b i) + (eval (map (⇑evalFinsupp) s) q) i
Tactic:
by_cases hv : s.valid q
Proof state after:
case pos
ι : Type
inst✝⁹ : LinearOrder ι
α : Type u_1
β : Type u_2
m : Type u_3
γ : Type u_4
inst✝⁸ : Zero α
inst✝⁷ : Zero β
inst✝⁶ : Zero m
inst✝⁵ : AddCommMonoid γ
inst✝⁴ : EvalToFinsupp α γ
inst✝³ : EvalToFinsupp β γ
inst✝² : LawfulOfStream α β γ
inst✝¹ : LawfulModifiable ι β m
s : Stream ι α
inst✝ : IsBounded s
i : ι
q : s.σ
ih :
  ∀ (y : s.σ),
    WfRel s y q →
      ∀ (b : m),
        evalFinsupp (Readable.get (fold_wf Modifiable.update (map OfStream.eval s) y b) i) =
          evalFinsupp (Readable.get b i) + (eval (map (⇑evalFinsupp) s) y) i
b : m
hv : s.valid q = true
⊢ evalFinsupp (Readable.get (fold_wf Modifiable.update (map OfStream.eval s) q b) i) =
    evalFinsupp (Readable.get b i) + (eval (map (⇑evalFinsupp) s) q) i

case neg
ι : Type
inst✝⁹ : LinearOrder ι
α : Type u_1
β : Type u_2
m : Type u_3
γ : Type u_4
inst✝⁸ : Zero α
inst✝⁷ : Zero β
inst✝⁶ : Zero m
inst✝⁵ : AddCommMonoid γ
inst✝⁴ : EvalToFinsupp α γ
inst✝³ : EvalToFinsupp β γ
inst✝² : LawfulOfStream α β γ
inst✝¹ : LawfulModifiable ι β m
s : Stream ι α
inst✝ : IsBounded s
i : ι
q : s.σ
ih :
  ∀ (y : s.σ),
    WfRel s y q →
      ∀ (b : m),
        evalFinsupp (Readable.get (fold_wf Modifiable.update (map OfStream.eval s) y b) i) =
          evalFinsupp (Readable.get b i) + (eval (map (⇑evalFinsupp) s) y) i
b : m
hv : ¬s.valid q = true
⊢ evalFinsupp (Readable.get (fold_wf Modifiable.update (map OfStream.eval s) q b) i) =
    evalFinsupp (Readable.get b i) + (eval (map (⇑evalFinsupp) s) q) i
Theorem: Etch.Verification.Stream.LawfulOfStream.get_fold
Proof state before:
case pos
ι : Type
inst✝⁹ : LinearOrder ι
α : Type u_1
β : Type u_2
m : Type u_3
γ : Type u_4
inst✝⁸ : Zero α
inst✝⁷ : Zero β
inst✝⁶ : Zero m
inst✝⁵ : AddCommMonoid γ
inst✝⁴ : EvalToFinsupp α γ
inst✝³ : EvalToFinsupp β γ
inst✝² : LawfulOfStream α β γ
inst✝¹ : LawfulModifiable ι β m
s : Stream ι α
inst✝ : IsBounded s
i : ι
q : s.σ
ih :
  ∀ (y : s.σ),
    WfRel s y q →
      ∀ (b : m),
        evalFinsupp (Readable.get (fold_wf Modifiable.update (map OfStream.eval s) y b) i) =
          evalFinsupp (Readable.get b i) + (eval (map (⇑evalFinsupp) s) y) i
b : m
hv : s.valid q = true
⊢ evalFinsupp (Readable.get (fold_wf Modifiable.update (map OfStream.eval s) q b) i) =
    evalFinsupp (Readable.get b i) + (eval (map (⇑evalFinsupp) s) q) i
Tactic:
revert ih
Proof state after:
case pos
ι : Type
inst✝⁹ : LinearOrder ι
α : Type u_1
β : Type u_2
m : Type u_3
γ : Type u_4
inst✝⁸ : Zero α
inst✝⁷ : Zero β
inst✝⁶ : Zero m
inst✝⁵ : AddCommMonoid γ
inst✝⁴ : EvalToFinsupp α γ
inst✝³ : EvalToFinsupp β γ
inst✝² : LawfulOfStream α β γ
inst✝¹ : LawfulModifiable ι β m
s : Stream ι α
inst✝ : IsBounded s
i : ι
q : s.σ
b : m
hv : s.valid q = true
⊢ (∀ (y : s.σ),
      WfRel s y q →
        ∀ (b : m),
          evalFinsupp (Readable.get (fold_wf Modifiable.update (map OfStream.eval s) y b) i) =
            evalFinsupp (Readable.get b i) + (eval (map (⇑evalFinsupp) s) y) i) →
    evalFinsupp (Readable.get (fold_wf Modifiable.update (map OfStream.eval s) q b) i) =
      evalFinsupp (Readable.get b i) + (eval (map (⇑evalFinsupp) s) q) i
Theorem: Etch.Verification.Stream.LawfulOfStream.get_fold
Proof state before:
case pos
ι : Type
inst✝⁹ : LinearOrder ι
α : Type u_1
β : Type u_2
m : Type u_3
γ : Type u_4
inst✝⁸ : Zero α
inst✝⁷ : Zero β
inst✝⁶ : Zero m
inst✝⁵ : AddCommMonoid γ
inst✝⁴ : EvalToFinsupp α γ
inst✝³ : EvalToFinsupp β γ
inst✝² : LawfulOfStream α β γ
inst✝¹ : LawfulModifiable ι β m
s : Stream ι α
inst✝ : IsBounded s
i : ι
q : s.σ
b : m
hv : s.valid q = true
⊢ (∀ (y : s.σ),
      WfRel s y q →
        ∀ (b : m),
          evalFinsupp (Readable.get (fold_wf Modifiable.update (map OfStream.eval s) y b) i) =
            evalFinsupp (Readable.get b i) + (eval (map (⇑evalFinsupp) s) y) i) →
    evalFinsupp (Readable.get (fold_wf Modifiable.update (map OfStream.eval s) q b) i) =
      evalFinsupp (Readable.get b i) + (eval (map (⇑evalFinsupp) s) q) i
Tactic:
refine Subtype.with_prop (fun t => s.valid t) q hv ?_
Proof state after:
case pos
ι : Type
inst✝⁹ : LinearOrder ι
α : Type u_1
β : Type u_2
m : Type u_3
γ : Type u_4
inst✝⁸ : Zero α
inst✝⁷ : Zero β
inst✝⁶ : Zero m
inst✝⁵ : AddCommMonoid γ
inst✝⁴ : EvalToFinsupp α γ
inst✝³ : EvalToFinsupp β γ
inst✝² : LawfulOfStream α β γ
inst✝¹ : LawfulModifiable ι β m
s : Stream ι α
inst✝ : IsBounded s
i : ι
q : s.σ
b : m
hv : s.valid q = true
⊢ ∀ (x : { t // s.valid t = true }),
    (∀ (y : s.σ),
        WfRel s y ↑x →
          ∀ (b : m),
            evalFinsupp (Readable.get (fold_wf Modifiable.update (map OfStream.eval s) y b) i) =
              evalFinsupp (Readable.get b i) + (eval (map (⇑evalFinsupp) s) y) i) →
      evalFinsupp (Readable.get (fold_wf Modifiable.update (map OfStream.eval s) (↑x) b) i) =
        evalFinsupp (Readable.get b i) + (eval (map (⇑evalFinsupp) s) ↑x) i
Theorem: Etch.Verification.Stream.LawfulOfStream.get_fold
Proof state before:
case pos
ι : Type
inst✝⁹ : LinearOrder ι
α : Type u_1
β : Type u_2
m : Type u_3
γ : Type u_4
inst✝⁸ : Zero α
inst✝⁷ : Zero β
inst✝⁶ : Zero m
inst✝⁵ : AddCommMonoid γ
inst✝⁴ : EvalToFinsupp α γ
inst✝³ : EvalToFinsupp β γ
inst✝² : LawfulOfStream α β γ
inst✝¹ : LawfulModifiable ι β m
s : Stream ι α
inst✝ : IsBounded s
i : ι
q : s.σ
b : m
hv : s.valid q = true
⊢ ∀ (x : { t // s.valid t = true }),
    (∀ (y : s.σ),
        WfRel s y ↑x →
          ∀ (b : m),
            evalFinsupp (Readable.get (fold_wf Modifiable.update (map OfStream.eval s) y b) i) =
              evalFinsupp (Readable.get b i) + (eval (map (⇑evalFinsupp) s) y) i) →
      evalFinsupp (Readable.get (fold_wf Modifiable.update (map OfStream.eval s) (↑x) b) i) =
        evalFinsupp (Readable.get b i) + (eval (map (⇑evalFinsupp) s) ↑x) i
Tactic:
clear q hv
Proof state after:
case pos
ι : Type
inst✝⁹ : LinearOrder ι
α : Type u_1
β : Type u_2
m : Type u_3
γ : Type u_4
inst✝⁸ : Zero α
inst✝⁷ : Zero β
inst✝⁶ : Zero m
inst✝⁵ : AddCommMonoid γ
inst✝⁴ : EvalToFinsupp α γ
inst✝³ : EvalToFinsupp β γ
inst✝² : LawfulOfStream α β γ
inst✝¹ : LawfulModifiable ι β m
s : Stream ι α
inst✝ : IsBounded s
i : ι
b : m
⊢ ∀ (x : { t // s.valid t = true }),
    (∀ (y : s.σ),
        WfRel s y ↑x →
          ∀ (b : m),
            evalFinsupp (Readable.get (fold_wf Modifiable.update (map OfStream.eval s) y b) i) =
              evalFinsupp (Readable.get b i) + (eval (map (⇑evalFinsupp) s) y) i) →
      evalFinsupp (Readable.get (fold_wf Modifiable.update (map OfStream.eval s) (↑x) b) i) =
        evalFinsupp (Readable.get b i) + (eval (map (⇑evalFinsupp) s) ↑x) i
Theorem: Etch.Verification.Stream.LawfulOfStream.get_fold
Proof state before:
case pos
ι : Type
inst✝⁹ : LinearOrder ι
α : Type u_1
β : Type u_2
m : Type u_3
γ : Type u_4
inst✝⁸ : Zero α
inst✝⁷ : Zero β
inst✝⁶ : Zero m
inst✝⁵ : AddCommMonoid γ
inst✝⁴ : EvalToFinsupp α γ
inst✝³ : EvalToFinsupp β γ
inst✝² : LawfulOfStream α β γ
inst✝¹ : LawfulModifiable ι β m
s : Stream ι α
inst✝ : IsBounded s
i : ι
b : m
⊢ ∀ (x : { t // s.valid t = true }),
    (∀ (y : s.σ),
        WfRel s y ↑x →
          ∀ (b : m),
            evalFinsupp (Readable.get (fold_wf Modifiable.update (map OfStream.eval s) y b) i) =
              evalFinsupp (Readable.get b i) + (eval (map (⇑evalFinsupp) s) y) i) →
      evalFinsupp (Readable.get (fold_wf Modifiable.update (map OfStream.eval s) (↑x) b) i) =
        evalFinsupp (Readable.get b i) + (eval (map (⇑evalFinsupp) s) ↑x) i
Tactic:
intro q ih
Proof state after:
case pos
ι : Type
inst✝⁹ : LinearOrder ι
α : Type u_1
β : Type u_2
m : Type u_3
γ : Type u_4
inst✝⁸ : Zero α
inst✝⁷ : Zero β
inst✝⁶ : Zero m
inst✝⁵ : AddCommMonoid γ
inst✝⁴ : EvalToFinsupp α γ
inst✝³ : EvalToFinsupp β γ
inst✝² : LawfulOfStream α β γ
inst✝¹ : LawfulModifiable ι β m
s : Stream ι α
inst✝ : IsBounded s
i : ι
b : m
q : { t // s.valid t = true }
ih :
  ∀ (y : s.σ),
    WfRel s y ↑q →
      ∀ (b : m),
        evalFinsupp (Readable.get (fold_wf Modifiable.update (map OfStream.eval s) y b) i) =
          evalFinsupp (Readable.get b i) + (eval (map (⇑evalFinsupp) s) y) i
⊢ evalFinsupp (Readable.get (fold_wf Modifiable.update (map OfStream.eval s) (↑q) b) i) =
    evalFinsupp (Readable.get b i) + (eval (map (⇑evalFinsupp) s) ↑q) i
Theorem: Etch.Verification.Stream.LawfulOfStream.get_fold
Proof state before:
case pos
ι : Type
inst✝⁹ : LinearOrder ι
α : Type u_1
β : Type u_2
m : Type u_3
γ : Type u_4
inst✝⁸ : Zero α
inst✝⁷ : Zero β
inst✝⁶ : Zero m
inst✝⁵ : AddCommMonoid γ
inst✝⁴ : EvalToFinsupp α γ
inst✝³ : EvalToFinsupp β γ
inst✝² : LawfulOfStream α β γ
inst✝¹ : LawfulModifiable ι β m
s : Stream ι α
inst✝ : IsBounded s
i : ι
b : m
q : { t // s.valid t = true }
ih :
  ∀ (y : s.σ),
    WfRel s y ↑q →
      ∀ (b : m),
        evalFinsupp (Readable.get (fold_wf Modifiable.update (map OfStream.eval s) y b) i) =
          evalFinsupp (Readable.get b i) + (eval (map (⇑evalFinsupp) s) y) i
⊢ evalFinsupp (Readable.get (fold_wf Modifiable.update (map OfStream.eval s) (↑q) b) i) =
    evalFinsupp (Readable.get b i) + (eval (map (⇑evalFinsupp) s) ↑q) i
Tactic:
rw [Stream.fold_wf_spec, Stream.eval_valid, Stream.eval₀]
Proof state after:
case pos
ι : Type
inst✝⁹ : LinearOrder ι
α : Type u_1
β : Type u_2
m : Type u_3
γ : Type u_4
inst✝⁸ : Zero α
inst✝⁷ : Zero β
inst✝⁶ : Zero m
inst✝⁵ : AddCommMonoid γ
inst✝⁴ : EvalToFinsupp α γ
inst✝³ : EvalToFinsupp β γ
inst✝² : LawfulOfStream α β γ
inst✝¹ : LawfulModifiable ι β m
s : Stream ι α
inst✝ : IsBounded s
i : ι
b : m
q : { t // s.valid t = true }
ih :
  ∀ (y : s.σ),
    WfRel s y ↑q →
      ∀ (b : m),
        evalFinsupp (Readable.get (fold_wf Modifiable.update (map OfStream.eval s) y b) i) =
          evalFinsupp (Readable.get b i) + (eval (map (⇑evalFinsupp) s) y) i
⊢ evalFinsupp
      (Readable.get
        (fold_wf Modifiable.update (map OfStream.eval s) (advance (map OfStream.eval s) ↑q)
          (if hr : (map OfStream.eval s).ready q = true then
            Modifiable.update b ((map OfStream.eval s).index q)
              ((map OfStream.eval s).value { val := q, property := hr })
          else b))
        i) =
    evalFinsupp (Readable.get b i) +
      ((if h₂ : (map (⇑evalFinsupp) s).ready q = true then
            fun₀ | (map (⇑evalFinsupp) s).index q => (map (⇑evalFinsupp) s).value { val := q, property := h₂ }
          else 0) +
          eval (map (⇑evalFinsupp) s) (advance (map (⇑evalFinsupp) s) ↑q))
        i
Theorem: Etch.Verification.Stream.LawfulOfStream.get_fold
Proof state before:
case pos
ι : Type
inst✝⁹ : LinearOrder ι
α : Type u_1
β : Type u_2
m : Type u_3
γ : Type u_4
inst✝⁸ : Zero α
inst✝⁷ : Zero β
inst✝⁶ : Zero m
inst✝⁵ : AddCommMonoid γ
inst✝⁴ : EvalToFinsupp α γ
inst✝³ : EvalToFinsupp β γ
inst✝² : LawfulOfStream α β γ
inst✝¹ : LawfulModifiable ι β m
s : Stream ι α
inst✝ : IsBounded s
i : ι
b : m
q : { t // s.valid t = true }
ih :
  ∀ (y : s.σ),
    WfRel s y ↑q →
      ∀ (b : m),
        evalFinsupp (Readable.get (fold_wf Modifiable.update (map OfStream.eval s) y b) i) =
          evalFinsupp (Readable.get b i) + (eval (map (⇑evalFinsupp) s) y) i
⊢ evalFinsupp
      (Readable.get
        (fold_wf Modifiable.update (map OfStream.eval s) (advance (map OfStream.eval s) ↑q)
          (if hr : (map OfStream.eval s).ready q = true then
            Modifiable.update b ((map OfStream.eval s).index q)
              ((map OfStream.eval s).value { val := q, property := hr })
          else b))
        i) =
    evalFinsupp (Readable.get b i) +
      ((if h₂ : (map (⇑evalFinsupp) s).ready q = true then
            fun₀ | (map (⇑evalFinsupp) s).index q => (map (⇑evalFinsupp) s).value { val := q, property := h₂ }
          else 0) +
          eval (map (⇑evalFinsupp) s) (advance (map (⇑evalFinsupp) s) ↑q))
        i
Tactic:
dsimp only [map_σ, map_valid, map_ready, map_index, map_value, Finsupp.coe_add, Pi.add_apply]
Proof state after:
case pos
ι : Type
inst✝⁹ : LinearOrder ι
α : Type u_1
β : Type u_2
m : Type u_3
γ : Type u_4
inst✝⁸ : Zero α
inst✝⁷ : Zero β
inst✝⁶ : Zero m
inst✝⁵ : AddCommMonoid γ
inst✝⁴ : EvalToFinsupp α γ
inst✝³ : EvalToFinsupp β γ
inst✝² : LawfulOfStream α β γ
inst✝¹ : LawfulModifiable ι β m
s : Stream ι α
inst✝ : IsBounded s
i : ι
b : m
q : { t // s.valid t = true }
ih :
  ∀ (y : s.σ),
    WfRel s y ↑q →
      ∀ (b : m),
        evalFinsupp (Readable.get (fold_wf Modifiable.update (map OfStream.eval s) y b) i) =
          evalFinsupp (Readable.get b i) + (eval (map (⇑evalFinsupp) s) y) i
⊢ evalFinsupp
      (Readable.get
        (fold_wf Modifiable.update (map OfStream.eval s) (advance (map OfStream.eval s) ↑q)
          (if hr : s.ready q = true then
            Modifiable.update b (s.index q) (OfStream.eval (s.value { val := q, property := hr }))
          else b))
        i) =
    evalFinsupp (Readable.get b i) +
      ((if h₂ : s.ready q = true then fun₀ | s.index q => evalFinsupp (s.value { val := q, property := h₂ }) else 0) i +
        (eval (map (⇑evalFinsupp) s) (advance (map (⇑evalFinsupp) s) ↑q)) i)
Theorem: Etch.Verification.Stream.LawfulOfStream.get_fold
Proof state before:
case pos
ι : Type
inst✝⁹ : LinearOrder ι
α : Type u_1
β : Type u_2
m : Type u_3
γ : Type u_4
inst✝⁸ : Zero α
inst✝⁷ : Zero β
inst✝⁶ : Zero m
inst✝⁵ : AddCommMonoid γ
inst✝⁴ : EvalToFinsupp α γ
inst✝³ : EvalToFinsupp β γ
inst✝² : LawfulOfStream α β γ
inst✝¹ : LawfulModifiable ι β m
s : Stream ι α
inst✝ : IsBounded s
i : ι
b : m
q : { t // s.valid t = true }
ih :
  ∀ (y : s.σ),
    WfRel s y ↑q →
      ∀ (b : m),
        evalFinsupp (Readable.get (fold_wf Modifiable.update (map OfStream.eval s) y b) i) =
          evalFinsupp (Readable.get b i) + (eval (map (⇑evalFinsupp) s) y) i
⊢ evalFinsupp
      (Readable.get
        (fold_wf Modifiable.update (map OfStream.eval s) (advance (map OfStream.eval s) ↑q)
          (if hr : s.ready q = true then
            Modifiable.update b (s.index q) (OfStream.eval (s.value { val := q, property := hr }))
          else b))
        i) =
    evalFinsupp (Readable.get b i) +
      ((if h₂ : s.ready q = true then fun₀ | s.index q => evalFinsupp (s.value { val := q, property := h₂ }) else 0) i +
        (eval (map (⇑evalFinsupp) s) (advance (map (⇑evalFinsupp) s) ↑q)) i)
Tactic:
simp only [advance_val, map_seek, map_toOrder]
Proof state after:
case pos
ι : Type
inst✝⁹ : LinearOrder ι
α : Type u_1
β : Type u_2
m : Type u_3
γ : Type u_4
inst✝⁸ : Zero α
inst✝⁷ : Zero β
inst✝⁶ : Zero m
inst✝⁵ : AddCommMonoid γ
inst✝⁴ : EvalToFinsupp α γ
inst✝³ : EvalToFinsupp β γ
inst✝² : LawfulOfStream α β γ
inst✝¹ : LawfulModifiable ι β m
s : Stream ι α
inst✝ : IsBounded s
i : ι
b : m
q : { t // s.valid t = true }
ih :
  ∀ (y : s.σ),
    WfRel s y ↑q →
      ∀ (b : m),
        evalFinsupp (Readable.get (fold_wf Modifiable.update (map OfStream.eval s) y b) i) =
          evalFinsupp (Readable.get b i) + (eval (map (⇑evalFinsupp) s) y) i
⊢ evalFinsupp
      (Readable.get
        (fold_wf Modifiable.update (map OfStream.eval s) (s.seek q (toOrder s q))
          (if hr : s.ready q = true then
            Modifiable.update b (s.index q) (OfStream.eval (s.value { val := q, property := hr }))
          else b))
        i) =
    evalFinsupp (Readable.get b i) +
      ((if h₂ : s.ready q = true then fun₀ | s.index q => evalFinsupp (s.value { val := q, property := h₂ }) else 0) i +
        (eval (map (⇑evalFinsupp) s) (s.seek q (toOrder s q))) i)
Theorem: Etch.Verification.Stream.LawfulOfStream.get_fold
Proof state before:
case pos
ι : Type
inst✝⁹ : LinearOrder ι
α : Type u_1
β : Type u_2
m : Type u_3
γ : Type u_4
inst✝⁸ : Zero α
inst✝⁷ : Zero β
inst✝⁶ : Zero m
inst✝⁵ : AddCommMonoid γ
inst✝⁴ : EvalToFinsupp α γ
inst✝³ : EvalToFinsupp β γ
inst✝² : LawfulOfStream α β γ
inst✝¹ : LawfulModifiable ι β m
s : Stream ι α
inst✝ : IsBounded s
i : ι
b : m
q : { t // s.valid t = true }
ih :
  ∀ (y : s.σ),
    WfRel s y ↑q →
      ∀ (b : m),
        evalFinsupp (Readable.get (fold_wf Modifiable.update (map OfStream.eval s) y b) i) =
          evalFinsupp (Readable.get b i) + (eval (map (⇑evalFinsupp) s) y) i
⊢ evalFinsupp
      (Readable.get
        (fold_wf Modifiable.update (map OfStream.eval s) (s.seek q (toOrder s q))
          (if hr : s.ready q = true then
            Modifiable.update b (s.index q) (OfStream.eval (s.value { val := q, property := hr }))
          else b))
        i) =
    evalFinsupp (Readable.get b i) +
      ((if h₂ : s.ready q = true then fun₀ | s.index q => evalFinsupp (s.value { val := q, property := h₂ }) else 0) i +
        (eval (map (⇑evalFinsupp) s) (s.seek q (toOrder s q))) i)
Tactic:
rw [ih]
Proof state after:
case pos
ι : Type
inst✝⁹ : LinearOrder ι
α : Type u_1
β : Type u_2
m : Type u_3
γ : Type u_4
inst✝⁸ : Zero α
inst✝⁷ : Zero β
inst✝⁶ : Zero m
inst✝⁵ : AddCommMonoid γ
inst✝⁴ : EvalToFinsupp α γ
inst✝³ : EvalToFinsupp β γ
inst✝² : LawfulOfStream α β γ
inst✝¹ : LawfulModifiable ι β m
s : Stream ι α
inst✝ : IsBounded s
i : ι
b : m
q : { t // s.valid t = true }
ih :
  ∀ (y : s.σ),
    WfRel s y ↑q →
      ∀ (b : m),
        evalFinsupp (Readable.get (fold_wf Modifiable.update (map OfStream.eval s) y b) i) =
          evalFinsupp (Readable.get b i) + (eval (map (⇑evalFinsupp) s) y) i
⊢ evalFinsupp
        (Readable.get
          (if hr : s.ready q = true then
            Modifiable.update b (s.index q) (OfStream.eval (s.value { val := q, property := hr }))
          else b)
          i) +
      (eval (map (⇑evalFinsupp) s) (s.seek q (toOrder s q))) i =
    evalFinsupp (Readable.get b i) +
      ((if h₂ : s.ready q = true then fun₀ | s.index q => evalFinsupp (s.value { val := q, property := h₂ }) else 0) i +
        (eval (map (⇑evalFinsupp) s) (s.seek q (toOrder s q))) i)

case pos.a
ι : Type
inst✝⁹ : LinearOrder ι
α : Type u_1
β : Type u_2
m : Type u_3
γ : Type u_4
inst✝⁸ : Zero α
inst✝⁷ : Zero β
inst✝⁶ : Zero m
inst✝⁵ : AddCommMonoid γ
inst✝⁴ : EvalToFinsupp α γ
inst✝³ : EvalToFinsupp β γ
inst✝² : LawfulOfStream α β γ
inst✝¹ : LawfulModifiable ι β m
s : Stream ι α
inst✝ : IsBounded s
i : ι
b : m
q : { t // s.valid t = true }
ih :
  ∀ (y : s.σ),
    WfRel s y ↑q →
      ∀ (b : m),
        evalFinsupp (Readable.get (fold_wf Modifiable.update (map OfStream.eval s) y b) i) =
          evalFinsupp (Readable.get b i) + (eval (map (⇑evalFinsupp) s) y) i
⊢ WfRel s (s.seek q (toOrder s q)) ↑q
Theorem: Etch.Verification.Stream.LawfulOfStream.get_fold
Proof state before:
case pos
ι : Type
inst✝⁹ : LinearOrder ι
α : Type u_1
β : Type u_2
m : Type u_3
γ : Type u_4
inst✝⁸ : Zero α
inst✝⁷ : Zero β
inst✝⁶ : Zero m
inst✝⁵ : AddCommMonoid γ
inst✝⁴ : EvalToFinsupp α γ
inst✝³ : EvalToFinsupp β γ
inst✝² : LawfulOfStream α β γ
inst✝¹ : LawfulModifiable ι β m
s : Stream ι α
inst✝ : IsBounded s
i : ι
b : m
q : { t // s.valid t = true }
ih :
  ∀ (y : s.σ),
    WfRel s y ↑q →
      ∀ (b : m),
        evalFinsupp (Readable.get (fold_wf Modifiable.update (map OfStream.eval s) y b) i) =
          evalFinsupp (Readable.get b i) + (eval (map (⇑evalFinsupp) s) y) i
hr : s.ready q = true
⊢ evalFinsupp
        (Readable.get (Modifiable.update b (s.index q) (OfStream.eval (s.value { val := q, property := hr }))) i) +
      (eval (map (⇑evalFinsupp) s) (s.seek q (toOrder s q))) i =
    evalFinsupp (Readable.get b i) +
      ((fun₀ | s.index q => evalFinsupp (s.value { val := q, property := hr })) i +
        (eval (map (⇑evalFinsupp) s) (s.seek q (toOrder s q))) i)
Tactic:
rw [Finsupp.single_apply, LawfulModifiable.get_update']
Proof state after:
case pos
ι : Type
inst✝⁹ : LinearOrder ι
α : Type u_1
β : Type u_2
m : Type u_3
γ : Type u_4
inst✝⁸ : Zero α
inst✝⁷ : Zero β
inst✝⁶ : Zero m
inst✝⁵ : AddCommMonoid γ
inst✝⁴ : EvalToFinsupp α γ
inst✝³ : EvalToFinsupp β γ
inst✝² : LawfulOfStream α β γ
inst✝¹ : LawfulModifiable ι β m
s : Stream ι α
inst✝ : IsBounded s
i : ι
b : m
q : { t // s.valid t = true }
ih :
  ∀ (y : s.σ),
    WfRel s y ↑q →
      ∀ (b : m),
        evalFinsupp (Readable.get (fold_wf Modifiable.update (map OfStream.eval s) y b) i) =
          evalFinsupp (Readable.get b i) + (eval (map (⇑evalFinsupp) s) y) i
hr : s.ready q = true
⊢ evalFinsupp
        (if s.index q = i then OfStream.eval (s.value { val := q, property := hr }) (Readable.get b i)
        else Readable.get b i) +
      (eval (map (⇑evalFinsupp) s) (s.seek q (toOrder s q))) i =
    evalFinsupp (Readable.get b i) +
      ((if s.index q = i then evalFinsupp (s.value { val := q, property := hr }) else 0) +
        (eval (map (⇑evalFinsupp) s) (s.seek q (toOrder s q))) i)
Theorem: Etch.Verification.Stream.LawfulOfStream.get_fold
Proof state before:
case pos
ι : Type
inst✝⁹ : LinearOrder ι
α : Type u_1
β : Type u_2
m : Type u_3
γ : Type u_4
inst✝⁸ : Zero α
inst✝⁷ : Zero β
inst✝⁶ : Zero m
inst✝⁵ : AddCommMonoid γ
inst✝⁴ : EvalToFinsupp α γ
inst✝³ : EvalToFinsupp β γ
inst✝² : LawfulOfStream α β γ
inst✝¹ : LawfulModifiable ι β m
s : Stream ι α
inst✝ : IsBounded s
i : ι
b : m
q : { t // s.valid t = true }
ih :
  ∀ (y : s.σ),
    WfRel s y ↑q →
      ∀ (b : m),
        evalFinsupp (Readable.get (fold_wf Modifiable.update (map OfStream.eval s) y b) i) =
          evalFinsupp (Readable.get b i) + (eval (map (⇑evalFinsupp) s) y) i
hr : s.ready q = true
⊢ evalFinsupp
        (if s.index q = i then OfStream.eval (s.value { val := q, property := hr }) (Readable.get b i)
        else Readable.get b i) +
      (eval (map (⇑evalFinsupp) s) (s.seek q (toOrder s q))) i =
    evalFinsupp (Readable.get b i) +
      ((if s.index q = i then evalFinsupp (s.value { val := q, property := hr }) else 0) +
        (eval (map (⇑evalFinsupp) s) (s.seek q (toOrder s q))) i)
Tactic:
split_ifs with heq
Proof state after:
case pos
ι : Type
inst✝⁹ : LinearOrder ι
α : Type u_1
β : Type u_2
m : Type u_3
γ : Type u_4
inst✝⁸ : Zero α
inst✝⁷ : Zero β
inst✝⁶ : Zero m
inst✝⁵ : AddCommMonoid γ
inst✝⁴ : EvalToFinsupp α γ
inst✝³ : EvalToFinsupp β γ
inst✝² : LawfulOfStream α β γ
inst✝¹ : LawfulModifiable ι β m
s : Stream ι α
inst✝ : IsBounded s
i : ι
b : m
q : { t // s.valid t = true }
ih :
  ∀ (y : s.σ),
    WfRel s y ↑q →
      ∀ (b : m),
        evalFinsupp (Readable.get (fold_wf Modifiable.update (map OfStream.eval s) y b) i) =
          evalFinsupp (Readable.get b i) + (eval (map (⇑evalFinsupp) s) y) i
hr : s.ready q = true
heq : s.index q = i
⊢ evalFinsupp (OfStream.eval (s.value { val := q, property := hr }) (Readable.get b i)) +
      (eval (map (⇑evalFinsupp) s) (s.seek q (toOrder s q))) i =
    evalFinsupp (Readable.get b i) +
      (evalFinsupp (s.value { val := q, property := hr }) + (eval (map (⇑evalFinsupp) s) (s.seek q (toOrder s q))) i)

case neg
ι : Type
inst✝⁹ : LinearOrder ι
α : Type u_1
β : Type u_2
m : Type u_3
γ : Type u_4
inst✝⁸ : Zero α
inst✝⁷ : Zero β
inst✝⁶ : Zero m
inst✝⁵ : AddCommMonoid γ
inst✝⁴ : EvalToFinsupp α γ
inst✝³ : EvalToFinsupp β γ
inst✝² : LawfulOfStream α β γ
inst✝¹ : LawfulModifiable ι β m
s : Stream ι α
inst✝ : IsBounded s
i : ι
b : m
q : { t // s.valid t = true }
ih :
  ∀ (y : s.σ),
    WfRel s y ↑q →
      ∀ (b : m),
        evalFinsupp (Readable.get (fold_wf Modifiable.update (map OfStream.eval s) y b) i) =
          evalFinsupp (Readable.get b i) + (eval (map (⇑evalFinsupp) s) y) i
hr : s.ready q = true
heq : ¬s.index q = i
⊢ evalFinsupp (Readable.get b i) + (eval (map (⇑evalFinsupp) s) (s.seek q (toOrder s q))) i =
    evalFinsupp (Readable.get b i) + (0 + (eval (map (⇑evalFinsupp) s) (s.seek q (toOrder s q))) i)