internlm/Lean-Github huggingface dataset:
Theorem: Etch.Verification.Stream.IsStrictMono.evalMultiset_length_le
Proof state before:
case neg
ι : Type
inst✝¹ : LinearOrder ι
α : Type u_1
s : Stream ι α
inst✝ : IsBounded s
h : IsStrictMono s
i : ι
q : s.σ
ih : ∀ (y : s.σ), WfRel s y q → Multiset.card ((evalMultiset s y) i) ≤ 1
hq : s.valid q = true
hr : ¬(s.ready { val := q, property := hq } = true ∧ s.index { val := q, property := hq } = i)
⊢ Multiset.card ((evalMultiset s q) i) ≤ 1
Tactic:
rw [Stream.evalMultiset_not_ready (q := ⟨q, hq⟩)]
Proof state after:
case neg
ι : Type
inst✝¹ : LinearOrder ι
α : Type u_1
s : Stream ι α
inst✝ : IsBounded s
h : IsStrictMono s
i : ι
q : s.σ
ih : ∀ (y : s.σ), WfRel s y q → Multiset.card ((evalMultiset s y) i) ≤ 1
hq : s.valid q = true
hr : ¬(s.ready { val := q, property := hq } = true ∧ s.index { val := q, property := hq } = i)
⊢ Multiset.card ((evalMultiset s (advance s ↑{ val := q, property := hq })) i) ≤ 1

case neg.hr
ι : Type
inst✝¹ : LinearOrder ι
α : Type u_1
s : Stream ι α
inst✝ : IsBounded s
h : IsStrictMono s
i : ι
q : s.σ
ih : ∀ (y : s.σ), WfRel s y q → Multiset.card ((evalMultiset s y) i) ≤ 1
hq : s.valid q = true
hr : ¬(s.ready { val := q, property := hq } = true ∧ s.index { val := q, property := hq } = i)
⊢ ¬s.ready { val := q, property := hq } = true ∨ s.index { val := q, property := hq } ≠ i
Theorem: Etch.Verification.Stream.IsStrictMono.evalMultiset_length_le
Proof state before:
case neg
ι : Type
inst✝¹ : LinearOrder ι
α : Type u_1
s : Stream ι α
inst✝ : IsBounded s
h : IsStrictMono s
i : ι
q : s.σ
ih : ∀ (y : s.σ), WfRel s y q → Multiset.card ((evalMultiset s y) i) ≤ 1
hq : s.valid q = true
hr : ¬(s.ready { val := q, property := hq } = true ∧ s.index { val := q, property := hq } = i)
⊢ Multiset.card ((evalMultiset s (advance s ↑{ val := q, property := hq })) i) ≤ 1
Tactic:
apply ih
Proof state after:
case neg.a
ι : Type
inst✝¹ : LinearOrder ι
α : Type u_1
s : Stream ι α
inst✝ : IsBounded s
h : IsStrictMono s
i : ι
q : s.σ
ih : ∀ (y : s.σ), WfRel s y q → Multiset.card ((evalMultiset s y) i) ≤ 1
hq : s.valid q = true
hr : ¬(s.ready { val := q, property := hq } = true ∧ s.index { val := q, property := hq } = i)
⊢ WfRel s (advance s ↑{ val := q, property := hq }) q
Theorem: Etch.Verification.Stream.IsStrictMono.evalMultiset_length_le
Proof state before:
case neg.a
ι : Type
inst✝¹ : LinearOrder ι
α : Type u_1
s : Stream ι α
inst✝ : IsBounded s
h : IsStrictMono s
i : ι
q : s.σ
ih : ∀ (y : s.σ), WfRel s y q → Multiset.card ((evalMultiset s y) i) ≤ 1
hq : s.valid q = true
hr : ¬(s.ready { val := q, property := hq } = true ∧ s.index { val := q, property := hq } = i)
⊢ WfRel s (advance s ↑{ val := q, property := hq }) q
Tactic:
exact s.next_wf ⟨q, hq⟩
Proof state after:
no goals
Theorem: Etch.Verification.Stream.IsStrictMono.evalMultiset_length_le
Proof state before:
case neg.hr
ι : Type
inst✝¹ : LinearOrder ι
α : Type u_1
s : Stream ι α
inst✝ : IsBounded s
h : IsStrictMono s
i : ι
q : s.σ
ih : ∀ (y : s.σ), WfRel s y q → Multiset.card ((evalMultiset s y) i) ≤ 1
hq : s.valid q = true
hr : ¬(s.ready { val := q, property := hq } = true ∧ s.index { val := q, property := hq } = i)
⊢ ¬s.ready { val := q, property := hq } = true ∨ s.index { val := q, property := hq } ≠ i
Tactic:
exact not_and_or.mp hr
Proof state after:
no goals
Theorem: Etch.Verification.Stream.IsStrictMono.evalOption_ready
Proof state before:
ι : Type
inst✝¹ : LinearOrder ι
α : Type u_1
s : Stream ι α
inst✝ : IsBounded s
h : IsStrictMono s
q : { q // s.valid q = true }
hr : s.ready q = true
⊢ evalOption s (↑q) (s.index q) = some (s.value { val := q, property := hr })
Tactic:
simp [evalOption, h.evalMultiset_ready hr]
Proof state after:
no goals
Theorem: Etch.Verification.Stream.evalOption_not_ready
Proof state before:
ι : Type
inst✝¹ : LinearOrder ι
α : Type u_1
s : Stream ι α
inst✝ : IsBounded s
q : { q // s.valid q = true }
i : ι
hr : ¬s.ready q = true ∨ s.index q ≠ i
⊢ evalOption s (↑q) i = evalOption s (advance s ↑q) i
Tactic:
simp only [Stream.evalOption]
Proof state after:
ι : Type
inst✝¹ : LinearOrder ι
α : Type u_1
s : Stream ι α
inst✝ : IsBounded s
q : { q // s.valid q = true }
i : ι
hr : ¬s.ready q = true ∨ s.index q ≠ i
⊢ Multiset.get ((evalMultiset s ↑q) i) = Multiset.get ((evalMultiset s (advance s ↑q)) i)
Theorem: Etch.Verification.Stream.evalOption_not_ready
Proof state before:
ι : Type
inst✝¹ : LinearOrder ι
α : Type u_1
s : Stream ι α
inst✝ : IsBounded s
q : { q // s.valid q = true }
i : ι
hr : ¬s.ready q = true ∨ s.index q ≠ i
⊢ Multiset.get ((evalMultiset s ↑q) i) = Multiset.get ((evalMultiset s (advance s ↑q)) i)
Tactic:
rw [s.evalMultiset_not_ready q i hr]
Proof state after:
no goals
Theorem: Etch.Verification.Stream.IsStrictMono.evalOption_eq_iff
Proof state before:
ι : Type
inst✝¹ : LinearOrder ι
α : Type u_1
s : Stream ι α
inst✝ : IsBounded s
hs : IsStrictMono s
q : s.σ
i : ι
x✝ : 0 ≤ 1
H : Multiset.card ((evalMultiset s q) i) = 0
⊢ (∀ (a : α), evalOption s q i = some a ↔ (evalMultiset s q) i = {a}) ∧
    (evalOption s q i = none ↔ (evalMultiset s q) i = 0)
Tactic:
rw [Multiset.card_eq_zero] at H
Proof state after:
ι : Type
inst✝¹ : LinearOrder ι
α : Type u_1
s : Stream ι α
inst✝ : IsBounded s
hs : IsStrictMono s
q : s.σ
i : ι
x✝ : 0 ≤ 1
H : (evalMultiset s q) i = 0
⊢ (∀ (a : α), evalOption s q i = some a ↔ (evalMultiset s q) i = {a}) ∧
    (evalOption s q i = none ↔ (evalMultiset s q) i = 0)
Theorem: Etch.Verification.Stream.IsStrictMono.evalOption_eq_iff
Proof state before:
ι : Type
inst✝¹ : LinearOrder ι
α : Type u_1
s : Stream ι α
inst✝ : IsBounded s
hs : IsStrictMono s
q : s.σ
i : ι
x✝ : 0 ≤ 1
H : (evalMultiset s q) i = 0
⊢ (∀ (a : α), evalOption s q i = some a ↔ (evalMultiset s q) i = {a}) ∧
    (evalOption s q i = none ↔ (evalMultiset s q) i = 0)
Tactic:
simp [H, evalOption]
Proof state after:
no goals
Theorem: Etch.Verification.Stream.IsStrictMono.evalOption_eq_iff
Proof state before:
ι : Type
inst✝¹ : LinearOrder ι
α : Type u_1
s : Stream ι α
inst✝ : IsBounded s
hs : IsStrictMono s
q : s.σ
i : ι
x✝ : 1 ≤ 1
H : Multiset.card ((evalMultiset s q) i) = 1
⊢ (∀ (a : α), evalOption s q i = some a ↔ (evalMultiset s q) i = {a}) ∧
    (evalOption s q i = none ↔ (evalMultiset s q) i = 0)
Tactic:
rw [Multiset.card_eq_one] at H
Proof state after:
ι : Type
inst✝¹ : LinearOrder ι
α : Type u_1
s : Stream ι α
inst✝ : IsBounded s
hs : IsStrictMono s
q : s.σ
i : ι
x✝ : 1 ≤ 1
H : ∃ a, (evalMultiset s q) i = {a}
⊢ (∀ (a : α), evalOption s q i = some a ↔ (evalMultiset s q) i = {a}) ∧
    (evalOption s q i = none ↔ (evalMultiset s q) i = 0)
Theorem: Etch.Verification.Stream.IsStrictMono.evalOption_eq_iff
Proof state before:
ι : Type
inst✝¹ : LinearOrder ι
α : Type u_1
s : Stream ι α
inst✝ : IsBounded s
hs : IsStrictMono s
q : s.σ
i : ι
x✝ : 1 ≤ 1
H : ∃ a, (evalMultiset s q) i = {a}
⊢ (∀ (a : α), evalOption s q i = some a ↔ (evalMultiset s q) i = {a}) ∧
    (evalOption s q i = none ↔ (evalMultiset s q) i = 0)
Tactic:
rcases H with ⟨a', ha'⟩
Proof state after:
case intro
ι : Type
inst✝¹ : LinearOrder ι
α : Type u_1
s : Stream ι α
inst✝ : IsBounded s
hs : IsStrictMono s
q : s.σ
i : ι
x✝ : 1 ≤ 1
a' : α
ha' : (evalMultiset s q) i = {a'}
⊢ (∀ (a : α), evalOption s q i = some a ↔ (evalMultiset s q) i = {a}) ∧
    (evalOption s q i = none ↔ (evalMultiset s q) i = 0)
Theorem: Etch.Verification.Stream.IsStrictMono.evalOption_eq_iff
Proof state before:
case intro
ι : Type
inst✝¹ : LinearOrder ι
α : Type u_1
s : Stream ι α
inst✝ : IsBounded s
hs : IsStrictMono s
q : s.σ
i : ι
x✝ : 1 ≤ 1
a' : α
ha' : (evalMultiset s q) i = {a'}
⊢ (∀ (a : α), evalOption s q i = some a ↔ (evalMultiset s q) i = {a}) ∧
    (evalOption s q i = none ↔ (evalMultiset s q) i = 0)
Tactic:
simp [evalOption, ha']
Proof state after:
no goals
Theorem: Etch.Verification.Stream.IsStrictMono.evalMultiset_eq_evalOption
Proof state before:
ι : Type
inst✝¹ : LinearOrder ι
α : Type u_1
s : Stream ι α
inst✝ : IsBounded s
hs : IsStrictMono s
q : s.σ
i : ι
⊢ (evalMultiset s q) i = Option.getD (Option.map (fun x => {x}) (evalOption s q i)) 0
Tactic:
cases h : s.evalOption q i <;>
simpa [(hs.evalOption_eq_iff (q := q)).1, (hs.evalOption_eq_iff (q := q)).2] using h
Proof state after:
no goals
Theorem: Etch.Verification.Stream.seek_spec
Proof state before:
ι : Type
inst✝¹ : LinearOrder ι
α : Type u_1
s : Stream ι α
inst✝ : IsLawful s
q : { q // s.valid q = true }
i : StreamOrder ι
⊢ Finsupp.filter (fun j => i ≤ (j, false)) (evalMultiset s (s.seek q i)) =
    Finsupp.filter (fun j => i ≤ (j, false)) (evalMultiset s ↑q)
Tactic:
rw [Finsupp.filter_ext_iff]
Proof state after:
ι : Type
inst✝¹ : LinearOrder ι
α : Type u_1
s : Stream ι α
inst✝ : IsLawful s
q : { q // s.valid q = true }
i : StreamOrder ι
⊢ ∀ (a : ι), i ≤ (a, false) → (evalMultiset s (s.seek q i)) a = (evalMultiset s ↑q) a
Theorem: Etch.Verification.Stream.seek_spec
Proof state before:
ι : Type
inst✝¹ : LinearOrder ι
α : Type u_1
s : Stream ι α
inst✝ : IsLawful s
q : { q // s.valid q = true }
i : StreamOrder ι
⊢ ∀ (a : ι), i ≤ (a, false) → (evalMultiset s (s.seek q i)) a = (evalMultiset s ↑q) a
Tactic:
exact IsLawful.seek_spec q i
Proof state after:
no goals
Theorem: Etch.Verification.Stream.seek_lt_toOrder
Proof state before:
ι : Type
inst✝¹ : LinearOrder ι
α : Type u_1
s : Stream ι α
inst✝ : IsLawful s
q : { q // s.valid q = true }
i : StreamOrder ι
hi : i < toOrder s q
⊢ evalMultiset s (s.seek q i) = evalMultiset s ↑q
Tactic:
ext j
Proof state after:
case h
ι : Type
inst✝¹ : LinearOrder ι
α : Type u_1
s : Stream ι α
inst✝ : IsLawful s
q : { q // s.valid q = true }
i : StreamOrder ι
hi : i < toOrder s q
j : ι
⊢ (evalMultiset s (s.seek q i)) j = (evalMultiset s ↑q) j
Theorem: Etch.Verification.Stream.seek_lt_toOrder
Proof state before:
case h
ι : Type
inst✝¹ : LinearOrder ι
α : Type u_1
s : Stream ι α
inst✝ : IsLawful s
q : { q // s.valid q = true }
i : StreamOrder ι
hi : i < toOrder s q
j : ι
⊢ (evalMultiset s (s.seek q i)) j = (evalMultiset s ↑q) j
Tactic:
by_cases H : s.toOrder q ≤ (j, true)
Proof state after:
case pos
ι : Type
inst✝¹ : LinearOrder ι
α : Type u_1
s : Stream ι α
inst✝ : IsLawful s
q : { q // s.valid q = true }
i : StreamOrder ι
hi : i < toOrder s q
j : ι
H : toOrder s q ≤ (j, true)
⊢ (evalMultiset s (s.seek q i)) j = (evalMultiset s ↑q) j

case neg
ι : Type
inst✝¹ : LinearOrder ι
α : Type u_1
s : Stream ι α
inst✝ : IsLawful s
q : { q // s.valid q = true }
i : StreamOrder ι
hi : i < toOrder s q
j : ι
H : ¬toOrder s q ≤ (j, true)
⊢ (evalMultiset s (s.seek q i)) j = (evalMultiset s ↑q) j
Theorem: Etch.Verification.Stream.seek_lt_toOrder
Proof state before:
case neg
ι : Type
inst✝¹ : LinearOrder ι
α : Type u_1
s : Stream ι α
inst✝ : IsLawful s
q : { q // s.valid q = true }
i : StreamOrder ι
hi : i < toOrder s q
j : ι
H : ¬toOrder s q ≤ (j, true)
⊢ (evalMultiset s (s.seek q i)) j = (evalMultiset s ↑q) j
Tactic:
have : ↑j < s.index' q := by
  simpa using fst_lt_of_lt_of_lt (show (j, false) <ₗ (j, true) by simp) (not_le.mp H)
Proof state after:
case neg
ι : Type
inst✝¹ : LinearOrder ι
α : Type u_1
s : Stream ι α
inst✝ : IsLawful s
q : { q // s.valid q = true }
i : StreamOrder ι
hi : i < toOrder s q
j : ι
H : ¬toOrder s q ≤ (j, true)
this : ↑j < index' s ↑q
⊢ (evalMultiset s (s.seek q i)) j = (evalMultiset s ↑q) j
Theorem: Etch.Verification.Stream.seek_lt_toOrder
Proof state before:
case neg
ι : Type
inst✝¹ : LinearOrder ι
α : Type u_1
s : Stream ι α
inst✝ : IsLawful s
q : { q // s.valid q = true }
i : StreamOrder ι
hi : i < toOrder s q
j : ι
H : ¬toOrder s q ≤ (j, true)
this : ↑j < index' s ↑q
⊢ (evalMultiset s (s.seek q i)) j = (evalMultiset s ↑q) j
Tactic:
rw [s.mono.eq_empty_of_lt_index j this,
  s.mono.eq_empty_of_lt_index _ (this.trans_le (s.mono q i))]
Proof state after:
no goals
Theorem: Etch.Verification.Stream.seek_lt_toOrder
Proof state before:
case pos
ι : Type
inst✝¹ : LinearOrder ι
α : Type u_1
s : Stream ι α
inst✝ : IsLawful s
q : { q // s.valid q = true }
i : StreamOrder ι
hi : i < toOrder s q
j : ι
H : toOrder s q ≤ (j, true)
⊢ (evalMultiset s (s.seek q i)) j = (evalMultiset s ↑q) j
Tactic:
rw [IsLawful.seek_spec q]
Proof state after:
case pos.a
ι : Type
inst✝¹ : LinearOrder ι
α : Type u_1
s : Stream ι α
inst✝ : IsLawful s
q : { q // s.valid q = true }
i : StreamOrder ι
hi : i < toOrder s q
j : ι
H : toOrder s q ≤ (j, true)
⊢ i ≤ (j, false)
Theorem: Etch.Verification.Stream.seek_lt_toOrder
Proof state before:
case pos.a
ι : Type
inst✝¹ : LinearOrder ι
α : Type u_1
s : Stream ι α
inst✝ : IsLawful s
q : { q // s.valid q = true }
i : StreamOrder ι
hi : i < toOrder s q
j : ι
H : toOrder s q ≤ (j, true)
⊢ i ≤ (j, false)
Tactic:
simpa [Prod.Lex.lt_iff'', Prod.Lex.le_iff''] using lt_of_lt_of_le hi H
Proof state after:
no goals
Theorem: Etch.Verification.Stream.seek_lt_toOrder
Proof state before:
ι : Type
inst✝¹ : LinearOrder ι
α : Type u_1
s : Stream ι α
inst✝ : IsLawful s
q : { q // s.valid q = true }
i : StreamOrder ι
hi : i < toOrder s q
j : ι
H : ¬toOrder s q ≤ (j, true)
⊢ ↑j < index' s ↑q
Tactic:
simpa using fst_lt_of_lt_of_lt (show (j, false) <ₗ (j, true) by simp) (not_le.mp H)
Proof state after:
no goals
Theorem: Etch.Verification.Stream.seek_lt_toOrder
Proof state before:
ι : Type
inst✝¹ : LinearOrder ι
α : Type u_1
s : Stream ι α
inst✝ : IsLawful s
q : { q // s.valid q = true }
i : StreamOrder ι
hi : i < toOrder s q
j : ι
H : ¬toOrder s q ≤ (j, true)
⊢ (j, false) < (j, true)
Tactic:
simp
Proof state after:
no goals
Theorem: Etch.Verification.Stream.eval_seek_eq_of_false
Proof state before:
ι : Type
inst✝¹ : LinearOrder ι
α : Type u_1
s : Stream ι α
inst✝ : IsLawful s
q : { q // s.valid q = true }
⊢ evalMultiset s (s.seek q (s.index q, false)) = evalMultiset s ↑q
Tactic:
by_cases hr : s.ready q
Proof state after:
case pos
ι : Type
inst✝¹ : LinearOrder ι
α : Type u_1
s : Stream ι α
inst✝ : IsLawful s
q : { q // s.valid q = true }
hr : s.ready q = true
⊢ evalMultiset s (s.seek q (s.index q, false)) = evalMultiset s ↑q

case neg
ι : Type
inst✝¹ : LinearOrder ι
α : Type u_1
s : Stream ι α
inst✝ : IsLawful s
q : { q // s.valid q = true }
hr : ¬s.ready q = true
⊢ evalMultiset s (s.seek q (s.index q, false)) = evalMultiset s ↑q
Theorem: Etch.Verification.Stream.eval_seek_eq_of_false
Proof state before:
case neg
ι : Type
inst✝¹ : LinearOrder ι
α : Type u_1
s : Stream ι α
inst✝ : IsLawful s
q : { q // s.valid q = true }
hr : ¬s.ready q = true
⊢ evalMultiset s (s.seek q (s.index q, false)) = evalMultiset s ↑q
Tactic:
. ext i
  simp [s.evalMultiset_not_ready q i (.inl hr), Stream.toOrder, hr]
Proof state after:
no goals
Theorem: Etch.Verification.Stream.eval_seek_eq_of_false
Proof state before:
case pos
ι : Type
inst✝¹ : LinearOrder ι
α : Type u_1
s : Stream ι α
inst✝ : IsLawful s
q : { q // s.valid q = true }
hr : s.ready q = true
⊢ evalMultiset s (s.seek q (s.index q, false)) = evalMultiset s ↑q
Tactic:
apply Stream.seek_lt_toOrder
Proof state after:
case pos.hi
ι : Type
inst✝¹ : LinearOrder ι
α : Type u_1
s : Stream ι α
inst✝ : IsLawful s
q : { q // s.valid q = true }
hr : s.ready q = true
⊢ (s.index q, false) < toOrder s q
Theorem: Etch.Verification.Stream.eval_seek_eq_of_false
Proof state before:
case pos.hi
ι : Type
inst✝¹ : LinearOrder ι
α : Type u_1
s : Stream ι α
inst✝ : IsLawful s
q : { q // s.valid q = true }
hr : s.ready q = true
⊢ (s.index q, false) < toOrder s q
Tactic:
simp [Stream.toOrder, hr]
Proof state after:
no goals
Theorem: Etch.Verification.Stream.eval_seek_eq_of_false
Proof state before:
case neg
ι : Type
inst✝¹ : LinearOrder ι
α : Type u_1
s : Stream ι α
inst✝ : IsLawful s
q : { q // s.valid q = true }
hr : ¬s.ready q = true
⊢ evalMultiset s (s.seek q (s.index q, false)) = evalMultiset s ↑q
Tactic:
ext i
Proof state after:
case neg.h
ι : Type
inst✝¹ : LinearOrder ι
α : Type u_1
s : Stream ι α
inst✝ : IsLawful s
q : { q // s.valid q = true }
hr : ¬s.ready q = true
i : ι
⊢ (evalMultiset s (s.seek q (s.index q, false))) i = (evalMultiset s ↑q) i
Theorem: Etch.Verification.Stream.eval_seek_eq_of_false
Proof state before:
case neg.h
ι : Type
inst✝¹ : LinearOrder ι
α : Type u_1
s : Stream ι α
inst✝ : IsLawful s
q : { q // s.valid q = true }
hr : ¬s.ready q = true
i : ι
⊢ (evalMultiset s (s.seek q (s.index q, false))) i = (evalMultiset s ↑q) i
Tactic:
simp [s.evalMultiset_not_ready q i (.inl hr), Stream.toOrder, hr]
Proof state after:
no goals
Theorem: Etch.Verification.Stream.bothand_spec
Proof state before:
⊢ ∀ (x y : Bool), bothand x y = (x && y)
Tactic:
decide
Proof state after:
no goals
Theorem: Etch.Verification.Stream.LawfulModifiable.get_update'
Proof state before:
ι : Type
inst✝⁴ : LinearOrder ι
β : Type u_1
m : Type u_2
α : Type u_3
inst✝³ : Zero β
inst✝² : Zero m
inst✝¹ : DecidableEq α
m₀ : m
x t : α
v : β → β
inst✝ : LawfulModifiable α β m
⊢ Readable.get (Modifiable.update m₀ x v) t = if x = t then v (Readable.get m₀ t) else Readable.get m₀ t
Tactic:
split_ifs with h
Proof state after:
case pos
ι : Type
inst✝⁴ : LinearOrder ι
β : Type u_1
m : Type u_2
α : Type u_3
inst✝³ : Zero β
inst✝² : Zero m
inst✝¹ : DecidableEq α
m₀ : m
x t : α
v : β → β
inst✝ : LawfulModifiable α β m
h : x = t
⊢ Readable.get (Modifiable.update m₀ x v) t = v (Readable.get m₀ t)

case neg
ι : Type
inst✝⁴ : LinearOrder ι
β : Type u_1
m : Type u_2
α : Type u_3
inst✝³ : Zero β
inst✝² : Zero m
inst✝¹ : DecidableEq α
m₀ : m
x t : α
v : β → β
inst✝ : LawfulModifiable α β m
h : ¬x = t
⊢ Readable.get (Modifiable.update m₀ x v) t = Readable.get m₀ t
Theorem: Etch.Verification.Stream.LawfulModifiable.get_update'
Proof state before:
case pos
ι : Type
inst✝⁴ : LinearOrder ι
β : Type u_1
m : Type u_2
α : Type u_3
inst✝³ : Zero β
inst✝² : Zero m
inst✝¹ : DecidableEq α
m₀ : m
x t : α
v : β → β
inst✝ : LawfulModifiable α β m
h : x = t
⊢ Readable.get (Modifiable.update m₀ x v) t = v (Readable.get m₀ t)
Tactic:
rw [← h, LawfulModifiable.get_update]
Proof state after:
no goals
Theorem: Etch.Verification.Stream.LawfulModifiable.get_update'
Proof state before:
case neg
ι : Type
inst✝⁴ : LinearOrder ι
β : Type u_1
m : Type u_2
α : Type u_3
inst✝³ : Zero β
inst✝² : Zero m
inst✝¹ : DecidableEq α
m₀ : m
x t : α
v : β → β
inst✝ : LawfulModifiable α β m
h : ¬x = t
⊢ Readable.get (Modifiable.update m₀ x v) t = Readable.get m₀ t
Tactic:
rw [LawfulModifiable.get_update_ne _ _ _ _ h]
Proof state after:
no goals
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
q : s.σ
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:
apply s.wf.induction q
Proof state after:
ι : 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
q : s.σ
i : ι
⊢ ∀ (x : s.σ),
    (∀ (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) →
      ∀ (b : m),
        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:
ι : 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
q : s.σ
i : ι
⊢ ∀ (x : s.σ),
    (∀ (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) →
      ∀ (b : m),
        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
Proof state after:
ι : 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 : ι
⊢ ∀ (x : s.σ),
    (∀ (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) →
      ∀ (b : m),
        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:
ι : 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 : ι
⊢ ∀ (x : s.σ),
    (∀ (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) →
      ∀ (b : m),
        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 b
Proof state after:
ι : 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