internlm/Lean-Github huggingface dataset:
Theorem: Etch.Verification.Stream.eval_map
Proof state before:
case pos
ι : Type
α : Type u_2
a b s✝ : Stream ι α
inst✝³ : Preorder ι
β : Type u_1
inst✝² : AddCommMonoid α
inst✝¹ : AddCommMonoid β
f : α →+ β
s : Stream ι α
inst✝ : IsBounded s
q : s.σ
ih : ∀ (y : s.σ), WfRel s y q → eval (map (⇑f) s) y = (Finsupp.mapRange.addMonoidHom f) (eval s y)
hq : s.valid q = true
⊢ eval₀ (map (⇑f) s) { val := q, property := hq } + eval (map (⇑f) s) (advance (map (⇑f) s) q) =
    Finsupp.mapRange ⇑f ⋯ (eval₀ s { val := q, property := hq }) + Finsupp.mapRange ⇑f ⋯ (eval s (advance s q))
Tactic:
congr 1
Proof state after:
case pos.e_a
ι : Type
α : Type u_2
a b s✝ : Stream ι α
inst✝³ : Preorder ι
β : Type u_1
inst✝² : AddCommMonoid α
inst✝¹ : AddCommMonoid β
f : α →+ β
s : Stream ι α
inst✝ : IsBounded s
q : s.σ
ih : ∀ (y : s.σ), WfRel s y q → eval (map (⇑f) s) y = (Finsupp.mapRange.addMonoidHom f) (eval s y)
hq : s.valid q = true
⊢ eval₀ (map (⇑f) s) { val := q, property := hq } = Finsupp.mapRange ⇑f ⋯ (eval₀ s { val := q, property := hq })

case pos.e_a
ι : Type
α : Type u_2
a b s✝ : Stream ι α
inst✝³ : Preorder ι
β : Type u_1
inst✝² : AddCommMonoid α
inst✝¹ : AddCommMonoid β
f : α →+ β
s : Stream ι α
inst✝ : IsBounded s
q : s.σ
ih : ∀ (y : s.σ), WfRel s y q → eval (map (⇑f) s) y = (Finsupp.mapRange.addMonoidHom f) (eval s y)
hq : s.valid q = true
⊢ eval (map (⇑f) s) (advance (map (⇑f) s) q) = Finsupp.mapRange ⇑f ⋯ (eval s (advance s q))
Theorem: Etch.Verification.Stream.eval_map
Proof state before:
case pos.e_a
ι : Type
α : Type u_2
a b s✝ : Stream ι α
inst✝³ : Preorder ι
β : Type u_1
inst✝² : AddCommMonoid α
inst✝¹ : AddCommMonoid β
f : α →+ β
s : Stream ι α
inst✝ : IsBounded s
q : s.σ
ih : ∀ (y : s.σ), WfRel s y q → eval (map (⇑f) s) y = (Finsupp.mapRange.addMonoidHom f) (eval s y)
hq : s.valid q = true
⊢ eval₀ (map (⇑f) s) { val := q, property := hq } = Finsupp.mapRange ⇑f ⋯ (eval₀ s { val := q, property := hq })
Tactic:
rw [Stream.eval₀_map]
Proof state after:
no goals
Theorem: Etch.Verification.Stream.eval_map
Proof state before:
case pos.e_a
ι : Type
α : Type u_2
a b s✝ : Stream ι α
inst✝³ : Preorder ι
β : Type u_1
inst✝² : AddCommMonoid α
inst✝¹ : AddCommMonoid β
f : α →+ β
s : Stream ι α
inst✝ : IsBounded s
q : s.σ
ih : ∀ (y : s.σ), WfRel s y q → eval (map (⇑f) s) y = (Finsupp.mapRange.addMonoidHom f) (eval s y)
hq : s.valid q = true
⊢ eval (map (⇑f) s) (advance (map (⇑f) s) q) = Finsupp.mapRange ⇑f ⋯ (eval s (advance s q))
Tactic:
exact ih (s.advance q) (s.next_wf ⟨q, hq⟩)
Proof state after:
no goals
Theorem: Etch.Verification.Stream.eval_map_apply
Proof state before:
ι : Type
α : Type u_2
a b s✝ : Stream ι α
inst✝³ : Preorder ι
β : Type u_1
inst✝² : AddCommMonoid α
inst✝¹ : AddCommMonoid β
f : α →+ β
s : Stream ι α
inst✝ : IsBounded s
q : s.σ
i : ι
⊢ (eval (map (⇑f) s) q) i = f ((eval s q) i)
Tactic:
rw [Stream.eval_map, Finsupp.mapRange.addMonoidHom_apply, Finsupp.mapRange_apply]
Proof state after:
no goals
Theorem: Etch.Verification.Stream.evalMultiset_sum
Proof state before:
ι : Type
α : Type u_1
a b s✝ : Stream ι α
inst✝² : Preorder ι
inst✝¹ : AddCommMonoid α
s : Stream ι α
inst✝ : IsBounded s
q : s.σ
i : ι
⊢ Multiset.sum ((evalMultiset s q) i) = (eval s q) i
Tactic:
have h₁ : (s |> (Stream.map fun x => {x}) |> Stream.map Multiset.sum).eval = s.eval := by
  dsimp only [Stream.map_map]
  rw [Stream.eval_map_id]
  ext; simp
Proof state after:
ι : Type
α : Type u_1
a b s✝ : Stream ι α
inst✝² : Preorder ι
inst✝¹ : AddCommMonoid α
s : Stream ι α
inst✝ : IsBounded s
q : s.σ
i : ι
h₁ : eval (map Multiset.sum (map (fun x => {x}) s)) = eval s
⊢ Multiset.sum ((evalMultiset s q) i) = (eval s q) i
Theorem: Etch.Verification.Stream.evalMultiset_sum
Proof state before:
ι : Type
α : Type u_1
a b s✝ : Stream ι α
inst✝² : Preorder ι
inst✝¹ : AddCommMonoid α
s : Stream ι α
inst✝ : IsBounded s
q : s.σ
i : ι
h₁ : eval (map Multiset.sum (map (fun x => {x}) s)) = eval s
⊢ Multiset.sum ((evalMultiset s q) i) = (eval s q) i
Tactic:
have h₂ : (s.evalMultiset q i).sum = (s |> (Stream.map fun x => {x}) |> Stream.map Multiset.sumAddMonoidHom).eval q i := by
  rw [Stream.eval_map_apply]
  rfl
Proof state after:
ι : Type
α : Type u_1
a b s✝ : Stream ι α
inst✝² : Preorder ι
inst✝¹ : AddCommMonoid α
s : Stream ι α
inst✝ : IsBounded s
q : s.σ
i : ι
h₁ : eval (map Multiset.sum (map (fun x => {x}) s)) = eval s
h₂ : Multiset.sum ((evalMultiset s q) i) = (eval (map (⇑Multiset.sumAddMonoidHom) (map (fun x => {x}) s)) q) i
⊢ Multiset.sum ((evalMultiset s q) i) = (eval s q) i
Theorem: Etch.Verification.Stream.evalMultiset_sum
Proof state before:
ι : Type
α : Type u_1
a b s✝ : Stream ι α
inst✝² : Preorder ι
inst✝¹ : AddCommMonoid α
s : Stream ι α
inst✝ : IsBounded s
q : s.σ
i : ι
h₁ : eval (map Multiset.sum (map (fun x => {x}) s)) = eval s
h₂ : Multiset.sum ((evalMultiset s q) i) = (eval (map (⇑Multiset.sumAddMonoidHom) (map (fun x => {x}) s)) q) i
⊢ Multiset.sum ((evalMultiset s q) i) = (eval s q) i
Tactic:
rw [Multiset.coe_sumAddMonoidHom] at h₂
Proof state after:
ι : Type
α : Type u_1
a b s✝ : Stream ι α
inst✝² : Preorder ι
inst✝¹ : AddCommMonoid α
s : Stream ι α
inst✝ : IsBounded s
q : s.σ
i : ι
h₁ : eval (map Multiset.sum (map (fun x => {x}) s)) = eval s
h₂ : Multiset.sum ((evalMultiset s q) i) = (eval (map Multiset.sum (map (fun x => {x}) s)) q) i
⊢ Multiset.sum ((evalMultiset s q) i) = (eval s q) i
Theorem: Etch.Verification.Stream.evalMultiset_sum
Proof state before:
ι : Type
α : Type u_1
a b s✝ : Stream ι α
inst✝² : Preorder ι
inst✝¹ : AddCommMonoid α
s : Stream ι α
inst✝ : IsBounded s
q : s.σ
i : ι
h₁ : eval (map Multiset.sum (map (fun x => {x}) s)) = eval s
h₂ : Multiset.sum ((evalMultiset s q) i) = (eval (map Multiset.sum (map (fun x => {x}) s)) q) i
⊢ Multiset.sum ((evalMultiset s q) i) = (eval s q) i
Tactic:
rw [h₂, h₁]
Proof state after:
no goals
Theorem: Etch.Verification.Stream.evalMultiset_sum
Proof state before:
ι : Type
α : Type u_1
a b s✝ : Stream ι α
inst✝² : Preorder ι
inst✝¹ : AddCommMonoid α
s : Stream ι α
inst✝ : IsBounded s
q : s.σ
i : ι
⊢ eval (map Multiset.sum (map (fun x => {x}) s)) = eval s
Tactic:
dsimp only [Stream.map_map]
Proof state after:
ι : Type
α : Type u_1
a b s✝ : Stream ι α
inst✝² : Preorder ι
inst✝¹ : AddCommMonoid α
s : Stream ι α
inst✝ : IsBounded s
q : s.σ
i : ι
⊢ eval (map (Multiset.sum ∘ fun x => {x}) s) = eval s
Theorem: Etch.Verification.Stream.evalMultiset_sum
Proof state before:
ι : Type
α : Type u_1
a b s✝ : Stream ι α
inst✝² : Preorder ι
inst✝¹ : AddCommMonoid α
s : Stream ι α
inst✝ : IsBounded s
q : s.σ
i : ι
⊢ eval (map (Multiset.sum ∘ fun x => {x}) s) = eval s
Tactic:
rw [Stream.eval_map_id]
Proof state after:
case hf
ι : Type
α : Type u_1
a b s✝ : Stream ι α
inst✝² : Preorder ι
inst✝¹ : AddCommMonoid α
s : Stream ι α
inst✝ : IsBounded s
q : s.σ
i : ι
⊢ (Multiset.sum ∘ fun x => {x}) = id
Theorem: Etch.Verification.Stream.evalMultiset_sum
Proof state before:
case hf
ι : Type
α : Type u_1
a b s✝ : Stream ι α
inst✝² : Preorder ι
inst✝¹ : AddCommMonoid α
s : Stream ι α
inst✝ : IsBounded s
q : s.σ
i : ι
⊢ (Multiset.sum ∘ fun x => {x}) = id
Tactic:
ext
Proof state after:
case hf.h
ι : Type
α : Type u_1
a b s✝ : Stream ι α
inst✝² : Preorder ι
inst✝¹ : AddCommMonoid α
s : Stream ι α
inst✝ : IsBounded s
q : s.σ
i : ι
x✝ : α
⊢ (Multiset.sum ∘ fun x => {x}) x✝ = id x✝
Theorem: Etch.Verification.Stream.evalMultiset_sum
Proof state before:
case hf.h
ι : Type
α : Type u_1
a b s✝ : Stream ι α
inst✝² : Preorder ι
inst✝¹ : AddCommMonoid α
s : Stream ι α
inst✝ : IsBounded s
q : s.σ
i : ι
x✝ : α
⊢ (Multiset.sum ∘ fun x => {x}) x✝ = id x✝
Tactic:
simp
Proof state after:
no goals
Theorem: Etch.Verification.Stream.evalMultiset_sum
Proof state before:
ι : Type
α : Type u_1
a b s✝ : Stream ι α
inst✝² : Preorder ι
inst✝¹ : AddCommMonoid α
s : Stream ι α
inst✝ : IsBounded s
q : s.σ
i : ι
h₁ : eval (map Multiset.sum (map (fun x => {x}) s)) = eval s
⊢ Multiset.sum ((evalMultiset s q) i) = (eval (map (⇑Multiset.sumAddMonoidHom) (map (fun x => {x}) s)) q) i
Tactic:
rw [Stream.eval_map_apply]
Proof state after:
ι : Type
α : Type u_1
a b s✝ : Stream ι α
inst✝² : Preorder ι
inst✝¹ : AddCommMonoid α
s : Stream ι α
inst✝ : IsBounded s
q : s.σ
i : ι
h₁ : eval (map Multiset.sum (map (fun x => {x}) s)) = eval s
⊢ Multiset.sum ((evalMultiset s q) i) = Multiset.sumAddMonoidHom ((eval (map (fun x => {x}) s) q) i)
Theorem: Etch.Verification.Stream.evalMultiset_sum
Proof state before:
ι : Type
α : Type u_1
a b s✝ : Stream ι α
inst✝² : Preorder ι
inst✝¹ : AddCommMonoid α
s : Stream ι α
inst✝ : IsBounded s
q : s.σ
i : ι
h₁ : eval (map Multiset.sum (map (fun x => {x}) s)) = eval s
⊢ Multiset.sum ((evalMultiset s q) i) = Multiset.sumAddMonoidHom ((eval (map (fun x => {x}) s) q) i)
Tactic:
rfl
Proof state after:
no goals
Theorem: Etch.Verification.Stream.evalMultiset_zero
Proof state before:
ι : Type
α : Type u_1
a b s : Stream ι α
inst✝ : Preorder ι
q : 0.σ
i : ι
⊢ (evalMultiset 0 q) i = 0
Tactic:
simp [Stream.evalMultiset]
Proof state after:
no goals
Theorem: Etch.Verification.Stream.evalMultiset_invalid
Proof state before:
ι : Type
α : Type u_1
a b s✝ : Stream ι α
inst✝¹ : Preorder ι
s : Stream ι α
inst✝ : IsBounded s
q : s.σ
h : ¬s.valid q = true
i : ι
⊢ (evalMultiset s q) i = 0
Tactic:
simp [Stream.evalMultiset, h]
Proof state after:
no goals
Theorem: Etch.Verification.Stream.evalMultiset_ready
Proof state before:
ι : Type
α : Type u_1
a b s✝ : Stream ι α
inst✝¹ : Preorder ι
s : Stream ι α
inst✝ : IsBounded s
q : { q // s.valid q = true }
hr : s.ready q = true
⊢ (evalMultiset s ↑q) (s.index q) =
    insert (s.value { val := q, property := hr }) ((evalMultiset s (advance s ↑q)) (s.index q))
Tactic:
simp [Stream.evalMultiset, Stream.eval₀, hr]
Proof state after:
no goals
Theorem: Etch.Verification.Stream.evalMultiset_not_ready
Proof state before:
ι : Type
α : Type u_1
a b s✝ : Stream ι α
inst✝¹ : Preorder ι
s : Stream ι α
inst✝ : IsBounded s
q : { q // s.valid q = true }
i : ι
hr : ¬s.ready q = true ∨ s.index q ≠ i
⊢ (evalMultiset s ↑q) i = (evalMultiset s (advance s ↑q)) i
Tactic:
suffices (s.map fun x => ({x} : Multiset α)).eval₀ q i = 0 by
  simpa [Stream.evalMultiset]
Proof state after:
ι : Type
α : Type u_1
a b s✝ : Stream ι α
inst✝¹ : Preorder ι
s : Stream ι α
inst✝ : IsBounded s
q : { q // s.valid q = true }
i : ι
hr : ¬s.ready q = true ∨ s.index q ≠ i
⊢ (eval₀ (map (fun x => {x}) s) q) i = 0
Theorem: Etch.Verification.Stream.evalMultiset_not_ready
Proof state before:
ι : Type
α : Type u_1
a b s✝ : Stream ι α
inst✝¹ : Preorder ι
s : Stream ι α
inst✝ : IsBounded s
q : { q // s.valid q = true }
i : ι
hr : ¬s.ready q = true ∨ s.index q ≠ i
this : (eval₀ (map (fun x => {x}) s) q) i = 0
⊢ (evalMultiset s ↑q) i = (evalMultiset s (advance s ↑q)) i
Tactic:
simpa [Stream.evalMultiset]
Proof state after:
no goals
Theorem: Etch.Verification.Stream.evalMultiset_not_ready
Proof state before:
case inl
ι : Type
α : Type u_1
a b s✝ : Stream ι α
inst✝¹ : Preorder ι
s : Stream ι α
inst✝ : IsBounded s
q : { q // s.valid q = true }
i : ι
hr : ¬s.ready q = true
⊢ (eval₀ (map (fun x => {x}) s) q) i = 0
Tactic:
simp [Stream.eval₀, hr]
Proof state after:
no goals
Theorem: Etch.Verification.Stream.evalMultiset_not_ready
Proof state before:
case inr
ι : Type
α : Type u_1
a b s✝ : Stream ι α
inst✝¹ : Preorder ι
s : Stream ι α
inst✝ : IsBounded s
q : { q // s.valid q = true }
i : ι
hr : s.index q ≠ i
⊢ (eval₀ (map (fun x => {x}) s) q) i = 0
Tactic:
simp only [Stream.eval₀]
Proof state after:
case inr
ι : Type
α : Type u_1
a b s✝ : Stream ι α
inst✝¹ : Preorder ι
s : Stream ι α
inst✝ : IsBounded s
q : { q // s.valid q = true }
i : ι
hr : s.index q ≠ i
⊢ (if h₂ : (map (fun x => {x}) s).ready q = true then
        fun₀ | (map (fun x => {x}) s).index q => (map (fun x => {x}) s).value { val := q, property := h₂ }
      else 0)
      i =
    0
Theorem: Etch.Verification.Stream.evalMultiset_not_ready
Proof state before:
case inr
ι : Type
α : Type u_1
a b s✝ : Stream ι α
inst✝¹ : Preorder ι
s : Stream ι α
inst✝ : IsBounded s
q : { q // s.valid q = true }
i : ι
hr : s.index q ≠ i
⊢ (if h₂ : (map (fun x => {x}) s).ready q = true then
        fun₀ | (map (fun x => {x}) s).index q => (map (fun x => {x}) s).value { val := q, property := h₂ }
      else 0)
      i =
    0
Tactic:
split_ifs
Proof state after:
case pos
ι : Type
α : Type u_1
a b s✝ : Stream ι α
inst✝¹ : Preorder ι
s : Stream ι α
inst✝ : IsBounded s
q : { q // s.valid q = true }
i : ι
hr : s.index q ≠ i
h✝ : (map (fun x => {x}) s).ready q = true
⊢ (fun₀ | (map (fun x => {x}) s).index q => (map (fun x => {x}) s).value { val := q, property := h✝ }) i = 0

case neg
ι : Type
α : Type u_1
a b s✝ : Stream ι α
inst✝¹ : Preorder ι
s : Stream ι α
inst✝ : IsBounded s
q : { q // s.valid q = true }
i : ι
hr : s.index q ≠ i
h✝ : ¬(map (fun x => {x}) s).ready q = true
⊢ 0 i = 0
Theorem: Etch.Verification.Stream.evalMultiset_not_ready
Proof state before:
case pos
ι : Type
α : Type u_1
a b s✝ : Stream ι α
inst✝¹ : Preorder ι
s : Stream ι α
inst✝ : IsBounded s
q : { q // s.valid q = true }
i : ι
hr : s.index q ≠ i
h✝ : (map (fun x => {x}) s).ready q = true
⊢ (fun₀ | (map (fun x => {x}) s).index q => (map (fun x => {x}) s).value { val := q, property := h✝ }) i = 0

case neg
ι : Type
α : Type u_1
a b s✝ : Stream ι α
inst✝¹ : Preorder ι
s : Stream ι α
inst✝ : IsBounded s
q : { q // s.valid q = true }
i : ι
hr : s.index q ≠ i
h✝ : ¬(map (fun x => {x}) s).ready q = true
⊢ 0 i = 0
Tactic:
swap
Proof state after:
case neg
ι : Type
α : Type u_1
a b s✝ : Stream ι α
inst✝¹ : Preorder ι
s : Stream ι α
inst✝ : IsBounded s
q : { q // s.valid q = true }
i : ι
hr : s.index q ≠ i
h✝ : ¬(map (fun x => {x}) s).ready q = true
⊢ 0 i = 0

case pos
ι : Type
α : Type u_1
a b s✝ : Stream ι α
inst✝¹ : Preorder ι
s : Stream ι α
inst✝ : IsBounded s
q : { q // s.valid q = true }
i : ι
hr : s.index q ≠ i
h✝ : (map (fun x => {x}) s).ready q = true
⊢ (fun₀ | (map (fun x => {x}) s).index q => (map (fun x => {x}) s).value { val := q, property := h✝ }) i = 0
Theorem: Etch.Verification.Stream.evalMultiset_not_ready
Proof state before:
case pos
ι : Type
α : Type u_1
a b s✝ : Stream ι α
inst✝¹ : Preorder ι
s : Stream ι α
inst✝ : IsBounded s
q : { q // s.valid q = true }
i : ι
hr : s.index q ≠ i
h✝ : (map (fun x => {x}) s).ready q = true
⊢ (fun₀ | (map (fun x => {x}) s).index q => (map (fun x => {x}) s).value { val := q, property := h✝ }) i = 0
Tactic:
simp [hr]
Proof state after:
no goals
Theorem: Etch.Verification.Stream.evalMultiset_not_ready
Proof state before:
case neg
ι : Type
α : Type u_1
a b s✝ : Stream ι α
inst✝¹ : Preorder ι
s : Stream ι α
inst✝ : IsBounded s
q : { q // s.valid q = true }
i : ι
hr : s.index q ≠ i
h✝ : ¬(map (fun x => {x}) s).ready q = true
⊢ 0 i = 0
Tactic:
rfl
Proof state after:
no goals
Theorem: Etch.Verification.Stream.not_ready_of_toOrder_lt
Proof state before:
ι✝ : Type
α : Type u_1
a b s✝ : Stream ι✝ α
inst✝¹ : Preorder ι✝
ι : Type
inst✝ : PartialOrder ι
s : Stream ι α
i : ι
q : { q // s.valid q = true }
h : toOrder s q < (i, true)
⊢ ¬s.ready q = true ∨ s.index q ≠ i
Tactic:
simp only [toOrder, Prod.Lex.lt_iff', lt_true_iff] at h
Proof state after:
ι✝ : Type
α : Type u_1
a b s✝ : Stream ι✝ α
inst✝¹ : Preorder ι✝
ι : Type
inst✝ : PartialOrder ι
s : Stream ι α
i : ι
q : { q // s.valid q = true }
h : s.index q < i ∨ s.index q = i ∧ s.ready q = false
⊢ ¬s.ready q = true ∨ s.index q ≠ i
Theorem: Etch.Verification.Stream.not_ready_of_toOrder_lt
Proof state before:
ι✝ : Type
α : Type u_1
a b s✝ : Stream ι✝ α
inst✝¹ : Preorder ι✝
ι : Type
inst✝ : PartialOrder ι
s : Stream ι α
i : ι
q : { q // s.valid q = true }
h : s.index q < i ∨ s.index q = i ∧ s.ready q = false
⊢ ¬s.ready q = true ∨ s.index q ≠ i
Tactic:
exact h.symm.imp (by simp) ne_of_lt
Proof state after:
no goals
Theorem: Etch.Verification.Stream.not_ready_of_toOrder_lt
Proof state before:
ι✝ : Type
α : Type u_1
a b s✝ : Stream ι✝ α
inst✝¹ : Preorder ι✝
ι : Type
inst✝ : PartialOrder ι
s : Stream ι α
i : ι
q : { q // s.valid q = true }
h : s.index q < i ∨ s.index q = i ∧ s.ready q = false
⊢ s.index q = i ∧ s.ready q = false → ¬s.ready q = true
Tactic:
simp
Proof state after:
no goals
Theorem: Etch.Verification.Stream.eval₀_support
Proof state before:
ι : Type
α : Type u_1
a b s✝ : Stream ι α
inst✝² : Preorder ι
inst✝¹ : Zero α
s : Stream ι α
inst✝ : IsBounded s
x : { q // s.valid q = true }
⊢ (eval₀ s x).support ⊆ {s.index x}
Tactic:
rw [Stream.eval₀]
Proof state after:
ι : Type
α : Type u_1
a b s✝ : Stream ι α
inst✝² : Preorder ι
inst✝¹ : Zero α
s : Stream ι α
inst✝ : IsBounded s
x : { q // s.valid q = true }
⊢ (if h₂ : s.ready x = true then fun₀ | s.index x => s.value { val := x, property := h₂ } else 0).support ⊆ {s.index x}
Theorem: Etch.Verification.Stream.eval₀_support
Proof state before:
ι : Type
α : Type u_1
a b s✝ : Stream ι α
inst✝² : Preorder ι
inst✝¹ : Zero α
s : Stream ι α
inst✝ : IsBounded s
x : { q // s.valid q = true }
⊢ (if h₂ : s.ready x = true then fun₀ | s.index x => s.value { val := x, property := h₂ } else 0).support ⊆ {s.index x}
Tactic:
split_ifs
Proof state after:
case pos
ι : Type
α : Type u_1
a b s✝ : Stream ι α
inst✝² : Preorder ι
inst✝¹ : Zero α
s : Stream ι α
inst✝ : IsBounded s
x : { q // s.valid q = true }
h✝ : s.ready x = true
⊢ (fun₀ | s.index x => s.value { val := x, property := h✝ }).support ⊆ {s.index x}

case neg
ι : Type
α : Type u_1
a b s✝ : Stream ι α
inst✝² : Preorder ι
inst✝¹ : Zero α
s : Stream ι α
inst✝ : IsBounded s
x : { q // s.valid q = true }
h✝ : ¬s.ready x = true
⊢ 0.support ⊆ {s.index x}
Theorem: Etch.Verification.Stream.eval₀_support
Proof state before:
case pos
ι : Type
α : Type u_1
a b s✝ : Stream ι α
inst✝² : Preorder ι
inst✝¹ : Zero α
s : Stream ι α
inst✝ : IsBounded s
x : { q // s.valid q = true }
h✝ : s.ready x = true
⊢ (fun₀ | s.index x => s.value { val := x, property := h✝ }).support ⊆ {s.index x}
Tactic:
exact Finsupp.support_single_subset
Proof state after:
no goals
Theorem: Etch.Verification.Stream.eval₀_support
Proof state before:
case neg
ι : Type
α : Type u_1
a b s✝ : Stream ι α
inst✝² : Preorder ι
inst✝¹ : Zero α
s : Stream ι α
inst✝ : IsBounded s
x : { q // s.valid q = true }
h✝ : ¬s.ready x = true
⊢ 0.support ⊆ {s.index x}
Tactic:
simp
Proof state after:
no goals
Theorem: Etch.Verification.Stream.eval₀_support'
Proof state before:
ι : Type
α : Type u_1
a b s✝ : Stream ι α
inst✝² : Preorder ι
inst✝¹ : Zero α
s : Stream ι α
inst✝ : IsBounded s
x : { q // s.valid q = true }
i : ι
h₂ : (eval₀ s x) i ≠ 0
⊢ toOrder s x = (i, true)
Tactic:
obtain rfl := Finset.eq_of_mem_singleton (s.eval₀_support x (Finsupp.mem_support_iff.mpr h₂))
Proof state after:
ι : Type
α : Type u_1
a b s✝ : Stream ι α
inst✝² : Preorder ι
inst✝¹ : Zero α
s : Stream ι α
inst✝ : IsBounded s
x : { q // s.valid q = true }
h₂ : (eval₀ s x) (s.index x) ≠ 0
⊢ toOrder s x = (s.index x, true)
Theorem: Etch.Verification.Stream.eval₀_support'
Proof state before:
ι : Type
α : Type u_1
a b s✝ : Stream ι α
inst✝² : Preorder ι
inst✝¹ : Zero α
s : Stream ι α
inst✝ : IsBounded s
x : { q // s.valid q = true }
h₂ : (eval₀ s x) (s.index x) ≠ 0
⊢ toOrder s x = (s.index x, true)
Tactic:
rw [Stream.eval₀] at h₂
Proof state after:
ι : Type
α : Type u_1
a b s✝ : Stream ι α
inst✝² : Preorder ι
inst✝¹ : Zero α
s : Stream ι α
inst✝ : IsBounded s
x : { q // s.valid q = true }
h₂ : (if h₂ : s.ready x = true then fun₀ | s.index x => s.value { val := x, property := h₂ } else 0) (s.index x) ≠ 0
⊢ toOrder s x = (s.index x, true)
Theorem: Etch.Verification.Stream.eval₀_support'
Proof state before:
ι : Type
α : Type u_1
a b s✝ : Stream ι α
inst✝² : Preorder ι
inst✝¹ : Zero α
s : Stream ι α
inst✝ : IsBounded s
x : { q // s.valid q = true }
h₂ : (if h₂ : s.ready x = true then fun₀ | s.index x => s.value { val := x, property := h₂ } else 0) (s.index x) ≠ 0
⊢ toOrder s x = (s.index x, true)
Tactic:
split_ifs at h₂ with hr
Proof state after:
case pos
ι : Type
α : Type u_1
a b s✝ : Stream ι α
inst✝² : Preorder ι
inst✝¹ : Zero α
s : Stream ι α
inst✝ : IsBounded s
x : { q // s.valid q = true }
hr : s.ready x = true
h₂ : (fun₀ | s.index x => s.value { val := x, property := hr }) (s.index x) ≠ 0
⊢ toOrder s x = (s.index x, true)

case neg
ι : Type
α : Type u_1
a b s✝ : Stream ι α
inst✝² : Preorder ι
inst✝¹ : Zero α
s : Stream ι α
inst✝ : IsBounded s
x : { q // s.valid q = true }
hr : ¬s.ready x = true
h₂ : 0 (s.index x) ≠ 0
⊢ toOrder s x = (s.index x, true)
Theorem: Etch.Verification.Stream.eval₀_support'
Proof state before:
case pos
ι : Type
α : Type u_1
a b s✝ : Stream ι α
inst✝² : Preorder ι
inst✝¹ : Zero α
s : Stream ι α
inst✝ : IsBounded s
x : { q // s.valid q = true }
hr : s.ready x = true
h₂ : (fun₀ | s.index x => s.value { val := x, property := hr }) (s.index x) ≠ 0
⊢ toOrder s x = (s.index x, true)
Tactic:
simp [Stream.toOrder, hr]
Proof state after:
no goals
Theorem: Etch.Verification.Stream.eval₀_support'
Proof state before:
case neg
ι : Type
α : Type u_1
a b s✝ : Stream ι α
inst✝² : Preorder ι
inst✝¹ : Zero α
s : Stream ι α
inst✝ : IsBounded s
x : { q // s.valid q = true }
hr : ¬s.ready x = true
h₂ : 0 (s.index x) ≠ 0
⊢ toOrder s x = (s.index x, true)
Tactic:
simp at h₂
Proof state after:
no goals
Theorem: Etch.Verification.Stream.fold_wf_spec
Proof 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]
Proof 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)
Theorem: Etch.Verification.Stream.fold_wf_spec
Proof 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]
Proof 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)