internlm/Lean-Github huggingface dataset:
Theorem: Etch.Verification.Stream.map_zero
Proof state before:
case value
ι : Type
α : Type u_2
a b s : Stream ι α
β : Type u_1
f : α → β
⊢ (map f 0).value = 0.value
Tactic:
funext ⟨q, h⟩
Proof state after:
case value.h
ι : Type
α : Type u_2
a b s : Stream ι α
β : Type u_1
f : α → β
q : { x // (map f 0).valid x = true }
h : (map f 0).ready q = true
⊢ (map f 0).value { val := q, property := h } = 0.value { val := q, property := h }
Theorem: Etch.Verification.Stream.map_zero
Proof state before:
case value.h
ι : Type
α : Type u_2
a b s : Stream ι α
β : Type u_1
f : α → β
q : { x // (map f 0).valid x = true }
h : (map f 0).ready q = true
⊢ (map f 0).value { val := q, property := h } = 0.value { val := q, property := h }
Tactic:
cases h
Proof state after:
no goals
Theorem: Etch.Verification.Stream.map_zero
Proof state before:
case ready
ι : Type
α : Type u_2
a b s : Stream ι α
β : Type u_1
f : α → β
⊢ HEq (map f 0).ready 0.ready
Tactic:
rfl
Proof state after:
no goals
Theorem: Etch.Verification.Stream.ready'_val
Proof state before:
ι : Type
α : Type u_1
a b s : Stream ι α
x : { q // s.valid q = true }
⊢ ready' s ↑x ↔ s.ready x = true
Tactic:
simp [Stream.ready', x.prop]
Proof state after:
no goals
Theorem: Etch.Verification.coeLex_le_iff
Proof state before:
ι : Type
α : Type ?u.4823
a b s : Stream ι α
inst✝ : Preorder ι
x y : StreamOrder ι
⊢ coeLex x ≤ coeLex y ↔ x ≤ y
Tactic:
simp [Prod.Lex.le_iff']
Proof state after:
no goals
Theorem: Etch.Verification.coeLex_lt_iff
Proof state before:
ι : Type
α : Type ?u.6775
a b s : Stream ι α
inst✝ : Preorder ι
x y : StreamOrder ι
⊢ coeLex x < coeLex y ↔ x < y
Tactic:
simp [Prod.Lex.lt_iff']
Proof state after:
no goals
Theorem: Etch.Verification.coeLex_injective
Proof state before:
ι : Type
α : Type ?u.7590
a b s : Stream ι α
x₁ : ι
y₁ : Bool
x₂ : ι
y₂ : Bool
⊢ coeLex (x₁, y₁) = coeLex (x₂, y₂) → (x₁, y₁) = (x₂, y₂)
Tactic:
rw [Prod.mk.injEq .., Prod.mk.injEq ..]
Proof state after:
ι : Type
α : Type ?u.7590
a b s : Stream ι α
x₁ : ι
y₁ : Bool
x₂ : ι
y₂ : Bool
⊢ ↑(x₁, y₁).1 = ↑(x₂, y₂).1 ∧ (x₁, y₁).2 = (x₂, y₂).2 → x₁ = x₂ ∧ y₁ = y₂
Theorem: Etch.Verification.coeLex_injective
Proof state before:
ι : Type
α : Type ?u.7590
a b s : Stream ι α
x₁ : ι
y₁ : Bool
x₂ : ι
y₂ : Bool
⊢ ↑(x₁, y₁).1 = ↑(x₂, y₂).1 ∧ (x₁, y₁).2 = (x₂, y₂).2 → x₁ = x₂ ∧ y₁ = y₂
Tactic:
simp
Proof state after:
no goals
Theorem: Etch.Verification.Stream.index'_invalid
Proof state before:
ι : Type
α : Type u_1
a b s : Stream ι α
x : s.σ
h : s.valid x = false
⊢ ¬s.valid x = true
Tactic:
simpa
Proof state after:
no goals
Theorem: Etch.Verification.Stream.toOrder'_val
Proof state before:
ι : Type
α : Type u_1
a b s : Stream ι α
q : { q // s.valid q = true }
⊢ toOrder' s ↑q = (index' s ↑q, s.ready q)
Tactic:
simp [Stream.toOrder']
Proof state after:
no goals
Theorem: Etch.Verification.Stream.coeLex_toOrder
Proof state before:
ι : Type
α : Type u_1
a b s : Stream ι α
q : { q // s.valid q = true }
⊢ toOrder' s ↑q = coeLex (toOrder s q)
Tactic:
simp [coeLex, Stream.toOrder'_val]
Proof state after:
no goals
Theorem: Etch.Verification.Stream.toOrder'_val_snd
Proof state before:
ι : Type
α : Type u_1
a b s : Stream ι α
q : { q // s.valid q = true }
⊢ (toOrder' s ↑q).2 = s.ready q
Tactic:
simp [Stream.toOrder'_val]
Proof state after:
no goals
Theorem: Etch.Verification.Stream.index'_lt_top_iff
Proof state before:
ι : Type
α : Type u_1
a b s : Stream ι α
inst✝ : Preorder ι
q : s.σ
⊢ index' s q < ⊤ ↔ s.valid q = true
Tactic:
rw [Stream.index']
Proof state after:
ι : Type
α : Type u_1
a b s : Stream ι α
inst✝ : Preorder ι
q : s.σ
⊢ (if h : s.valid q = true then ↑(s.index { val := q, property := h }) else ⊤) < ⊤ ↔ s.valid q = true
Theorem: Etch.Verification.Stream.index'_lt_top_iff
Proof state before:
ι : Type
α : Type u_1
a b s : Stream ι α
inst✝ : Preorder ι
q : s.σ
⊢ (if h : s.valid q = true then ↑(s.index { val := q, property := h }) else ⊤) < ⊤ ↔ s.valid q = true
Tactic:
split_ifs
Proof state after:
case pos
ι : Type
α : Type u_1
a b s : Stream ι α
inst✝ : Preorder ι
q : s.σ
h✝ : s.valid q = true
⊢ ↑(s.index { val := q, property := h✝ }) < ⊤ ↔ s.valid q = true

case neg
ι : Type
α : Type u_1
a b s : Stream ι α
inst✝ : Preorder ι
q : s.σ
h✝ : ¬s.valid q = true
⊢ ⊤ < ⊤ ↔ s.valid q = true
Theorem: Etch.Verification.Stream.index'_lt_top_iff
Proof state before:
case pos
ι : Type
α : Type u_1
a b s : Stream ι α
inst✝ : Preorder ι
q : s.σ
h✝ : s.valid q = true
⊢ ↑(s.index { val := q, property := h✝ }) < ⊤ ↔ s.valid q = true
Tactic:
simpa [WithTop.coe_lt_top]
Proof state after:
no goals
Theorem: Etch.Verification.Stream.index'_lt_top_iff
Proof state before:
case neg
ι : Type
α : Type u_1
a b s : Stream ι α
inst✝ : Preorder ι
q : s.σ
h✝ : ¬s.valid q = true
⊢ ⊤ < ⊤ ↔ s.valid q = true
Tactic:
simp [*]
Proof state after:
no goals
Theorem: Etch.Verification.Stream.get_index'
Proof state before:
ι : Type
α : Type ?u.13400
a b s : Stream ι α
inst✝ : PartialOrder ι
x : s.σ
h : Option.isSome (index' s x) = true
⊢ s.valid x = true
Tactic:
simpa using h
Proof state after:
no goals
Theorem: Etch.Verification.Stream.get_index'
Proof state before:
ι : Type
α : Type u_1
a b s : Stream ι α
inst✝ : PartialOrder ι
x : s.σ
h : Option.isSome (index' s x) = true
⊢ Option.get (index' s x) h = s.index { val := x, property := ⋯ }
Tactic:
generalize_proofs hq
Proof state after:
ι : Type
α : Type u_1
a b s : Stream ι α
inst✝ : PartialOrder ι
x : s.σ
h : Option.isSome (index' s x) = true
hq : s.valid x = true
⊢ Option.get (index' s x) h = s.index { val := x, property := hq }
Theorem: Etch.Verification.Stream.get_index'
Proof state before:
ι : Type
α : Type u_1
a b s : Stream ι α
inst✝ : PartialOrder ι
x : s.σ
h : Option.isSome (index' s x) = true
hq : s.valid x = true
⊢ Option.get (index' s x) h = s.index { val := x, property := hq }
Tactic:
simp_rw [Stream.index', hq, Option.get]
Proof state after:
no goals
Theorem: Etch.Verification.wf_valid_iff
Proof state before:
ι : Type
α : Type u_1
a b s : Stream ι α
inst✝ : Preorder ι
wf_rel : s.σ → s.σ → Prop
q : { x // s.valid x = true }
i : Lex (ι × Bool)
⊢ wf_rel (s.seek q i) ↑q ∨ i < Stream.toOrder s q ∧ s.seek q i = ↑q ↔
    wf_rel (Stream.seek' s (↑q) i) ↑q ∨ coeLex i < Stream.toOrder' s ↑q ∧ Stream.seek' s (↑q) i = ↑q
Tactic:
simp only [Stream.seek'_val q.prop, Stream.coeLex_toOrder, coeLex_lt_iff]
Proof state after:
no goals
Theorem: Etch.Verification.IsBounded.mk'
Proof state before:
ι : Type
α : Type u_1
a b s : Stream ι α
inst✝ : Preorder ι
h :
  ∃ wf_rel,
    ∀ (q : s.σ) (i : StreamOrder ι),
      WellFoundedRelation.rel (Stream.seek' s q i) q ∨ coeLex i < Stream.toOrder' s q ∧ Stream.seek' s q i = q
⊢ ∃ wf_rel,
    ∀ (q : { x // s.valid x = true }) (i : Lex (ι × Bool)),
      WellFoundedRelation.rel (s.seek q i) ↑q ∨ i < Stream.toOrder s q ∧ s.seek q i = ↑q
Tactic:
simp only [wf_valid_iff]
Proof state after:
ι : Type
α : Type u_1
a b s : Stream ι α
inst✝ : Preorder ι
h :
  ∃ wf_rel,
    ∀ (q : s.σ) (i : StreamOrder ι),
      WellFoundedRelation.rel (Stream.seek' s q i) q ∨ coeLex i < Stream.toOrder' s q ∧ Stream.seek' s q i = q
⊢ ∃ wf_rel,
    ∀ (q : { x // s.valid x = true }) (i : Lex (ι × Bool)),
      WellFoundedRelation.rel (Stream.seek' s (↑q) i) ↑q ∨ coeLex i < Stream.toOrder' s ↑q ∧ Stream.seek' s (↑q) i = ↑q
Theorem: Etch.Verification.IsBounded.mk'
Proof state before:
ι : Type
α : Type u_1
a b s : Stream ι α
inst✝ : Preorder ι
h :
  ∃ wf_rel,
    ∀ (q : s.σ) (i : StreamOrder ι),
      WellFoundedRelation.rel (Stream.seek' s q i) q ∨ coeLex i < Stream.toOrder' s q ∧ Stream.seek' s q i = q
⊢ ∃ wf_rel,
    ∀ (q : { x // s.valid x = true }) (i : Lex (ι × Bool)),
      WellFoundedRelation.rel (Stream.seek' s (↑q) i) ↑q ∨ coeLex i < Stream.toOrder' s ↑q ∧ Stream.seek' s (↑q) i = ↑q
Tactic:
rcases h with ⟨wfr, hr⟩
Proof state after:
case intro
ι : Type
α : Type u_1
a b s : Stream ι α
inst✝ : Preorder ι
wfr : WellFoundedRelation s.σ
hr :
  ∀ (q : s.σ) (i : StreamOrder ι),
    WellFoundedRelation.rel (Stream.seek' s q i) q ∨ coeLex i < Stream.toOrder' s q ∧ Stream.seek' s q i = q
⊢ ∃ wf_rel,
    ∀ (q : { x // s.valid x = true }) (i : Lex (ι × Bool)),
      WellFoundedRelation.rel (Stream.seek' s (↑q) i) ↑q ∨ coeLex i < Stream.toOrder' s ↑q ∧ Stream.seek' s (↑q) i = ↑q
Theorem: Etch.Verification.IsBounded.mk'
Proof state before:
case intro
ι : Type
α : Type u_1
a b s : Stream ι α
inst✝ : Preorder ι
wfr : WellFoundedRelation s.σ
hr :
  ∀ (q : s.σ) (i : StreamOrder ι),
    WellFoundedRelation.rel (Stream.seek' s q i) q ∨ coeLex i < Stream.toOrder' s q ∧ Stream.seek' s q i = q
⊢ ∃ wf_rel,
    ∀ (q : { x // s.valid x = true }) (i : Lex (ι × Bool)),
      WellFoundedRelation.rel (Stream.seek' s (↑q) i) ↑q ∨ coeLex i < Stream.toOrder' s ↑q ∧ Stream.seek' s (↑q) i = ↑q
Tactic:
exact ⟨wfr, fun q i => hr q i⟩
Proof state after:
no goals
Theorem: Etch.Verification.Stream.wf_valid'
Proof state before:
ι : Type
α : Type u_1
a b s : Stream ι α
inst✝¹ : Preorder ι
inst✝ : IsBounded s
q : s.σ
i : StreamOrder ι
hq : s.valid q = true
⊢ WfRel s (seek' s q i) q ∨ coeLex i < toOrder' s q ∧ seek' s q i = q
Tactic:
rw [← wf_valid_iff (q := ⟨q, hq⟩)]
Proof state after:
ι : Type
α : Type u_1
a b s : Stream ι α
inst✝¹ : Preorder ι
inst✝ : IsBounded s
q : s.σ
i : StreamOrder ι
hq : s.valid q = true
⊢ WfRel s (s.seek { val := q, property := hq } i) ↑{ val := q, property := hq } ∨
    i < toOrder s { val := q, property := hq } ∧ s.seek { val := q, property := hq } i = ↑{ val := q, property := hq }
Theorem: Etch.Verification.Stream.wf_valid'
Proof state before:
ι : Type
α : Type u_1
a b s : Stream ι α
inst✝¹ : Preorder ι
inst✝ : IsBounded s
q : s.σ
i : StreamOrder ι
hq : s.valid q = true
⊢ WfRel s (s.seek { val := q, property := hq } i) ↑{ val := q, property := hq } ∨
    i < toOrder s { val := q, property := hq } ∧ s.seek { val := q, property := hq } i = ↑{ val := q, property := hq }
Tactic:
exact s.wf_valid ⟨q, hq⟩ i
Proof state after:
no goals
Theorem: Etch.Verification.Stream.wf_valid'
Proof state before:
ι : Type
α : Type u_1
a b s : Stream ι α
inst✝¹ : Preorder ι
inst✝ : IsBounded s
q : s.σ
i : StreamOrder ι
hq : ¬s.valid q = true
⊢ WfRel s (seek' s q i) q ∨ coeLex i < toOrder' s q ∧ seek' s q i = q
Tactic:
right
Proof state after:
case h
ι : Type
α : Type u_1
a b s : Stream ι α
inst✝¹ : Preorder ι
inst✝ : IsBounded s
q : s.σ
i : StreamOrder ι
hq : ¬s.valid q = true
⊢ coeLex i < toOrder' s q ∧ seek' s q i = q
Theorem: Etch.Verification.Stream.wf_valid'
Proof state before:
case h
ι : Type
α : Type u_1
a b s : Stream ι α
inst✝¹ : Preorder ι
inst✝ : IsBounded s
q : s.σ
i : StreamOrder ι
hq : ¬s.valid q = true
⊢ coeLex i < toOrder' s q ∧ seek' s q i = q
Tactic:
constructor
Proof state after:
case h.left
ι : Type
α : Type u_1
a b s : Stream ι α
inst✝¹ : Preorder ι
inst✝ : IsBounded s
q : s.σ
i : StreamOrder ι
hq : ¬s.valid q = true
⊢ coeLex i < toOrder' s q

case h.right
ι : Type
α : Type u_1
a b s : Stream ι α
inst✝¹ : Preorder ι
inst✝ : IsBounded s
q : s.σ
i : StreamOrder ι
hq : ¬s.valid q = true
⊢ seek' s q i = q
Theorem: Etch.Verification.Stream.wf_valid'
Proof state before:
case h.left
ι : Type
α : Type u_1
a b s : Stream ι α
inst✝¹ : Preorder ι
inst✝ : IsBounded s
q : s.σ
i : StreamOrder ι
hq : ¬s.valid q = true
⊢ coeLex i < toOrder' s q
Tactic:
rw [Prod.Lex.lt_iff']
Proof state after:
case h.left
ι : Type
α : Type u_1
a b s : Stream ι α
inst✝¹ : Preorder ι
inst✝ : IsBounded s
q : s.σ
i : StreamOrder ι
hq : ¬s.valid q = true
⊢ (coeLex i).1 < (toOrder' s q).1 ∨ (coeLex i).1 = (toOrder' s q).1 ∧ (coeLex i).2 < (toOrder' s q).2
Theorem: Etch.Verification.Stream.wf_valid'
Proof state before:
case h.left
ι : Type
α : Type u_1
a b s : Stream ι α
inst✝¹ : Preorder ι
inst✝ : IsBounded s
q : s.σ
i : StreamOrder ι
hq : ¬s.valid q = true
⊢ (coeLex i).1 < (toOrder' s q).1 ∨ (coeLex i).1 = (toOrder' s q).1 ∧ (coeLex i).2 < (toOrder' s q).2
Tactic:
left
Proof state after:
case h.left.h
ι : Type
α : Type u_1
a b s : Stream ι α
inst✝¹ : Preorder ι
inst✝ : IsBounded s
q : s.σ
i : StreamOrder ι
hq : ¬s.valid q = true
⊢ (coeLex i).1 < (toOrder' s q).1
Theorem: Etch.Verification.Stream.wf_valid'
Proof state before:
case h.left.h
ι : Type
α : Type u_1
a b s : Stream ι α
inst✝¹ : Preorder ι
inst✝ : IsBounded s
q : s.σ
i : StreamOrder ι
hq : ¬s.valid q = true
⊢ (coeLex i).1 < (toOrder' s q).1
Tactic:
simp [hq]
Proof state after:
no goals
Theorem: Etch.Verification.Stream.wf_valid'
Proof state before:
case h.right
ι : Type
α : Type u_1
a b s : Stream ι α
inst✝¹ : Preorder ι
inst✝ : IsBounded s
q : s.σ
i : StreamOrder ι
hq : ¬s.valid q = true
⊢ seek' s q i = q
Tactic:
simp [hq]
Proof state after:
no goals
Theorem: Etch.Verification.Stream.next_wf
Proof state before:
ι : Type
α : Type u_1
a b s : Stream ι α
inst✝¹ : Preorder ι
inst✝ : IsBounded s
q : { q // s.valid q = true }
⊢ WfRel s (advance s ↑q) ↑q
Tactic:
rw [Stream.advance_val]
Proof state after:
ι : Type
α : Type u_1
a b s : Stream ι α
inst✝¹ : Preorder ι
inst✝ : IsBounded s
q : { q // s.valid q = true }
⊢ WfRel s (s.seek q (toOrder s q)) ↑q
Theorem: Etch.Verification.Stream.next_wf
Proof state before:
ι : Type
α : Type u_1
a b s : Stream ι α
inst✝¹ : Preorder ι
inst✝ : IsBounded s
q : { q // s.valid q = true }
⊢ WfRel s (s.seek q (toOrder s q)) ↑q
Tactic:
exact s.progress rfl.le
Proof state after:
no goals
Theorem: Etch.Verification.Stream.eval_zero
Proof state before:
ι : Type
α : Type u_1
a b s : Stream ι α
inst✝¹ : Preorder ι
inst✝ : AddZeroClass α
⊢ eval 0 = 0
Tactic:
ext
Proof state after:
case h.h
ι : Type
α : Type u_1
a b s : Stream ι α
inst✝¹ : Preorder ι
inst✝ : AddZeroClass α
x✝ : 0.σ
a✝ : ι
⊢ (eval 0 x✝) a✝ = (0 x✝) a✝
Theorem: Etch.Verification.Stream.eval_zero
Proof state before:
case h.h
ι : Type
α : Type u_1
a b s : Stream ι α
inst✝¹ : Preorder ι
inst✝ : AddZeroClass α
x✝ : 0.σ
a✝ : ι
⊢ (eval 0 x✝) a✝ = (0 x✝) a✝
Tactic:
rw [Stream.eval]
Proof state after:
case h.h
ι : Type
α : Type u_1
a b s : Stream ι α
inst✝¹ : Preorder ι
inst✝ : AddZeroClass α
x✝ : 0.σ
a✝ : ι
⊢ (if h : 0.valid x✝ = true then
        let_fun this := ⋯;
        eval₀ 0 { val := x✝, property := h } + eval 0 (advance 0 x✝)
      else 0)
      a✝ =
    (0 x✝) a✝
Theorem: Etch.Verification.Stream.eval_zero
Proof state before:
case h.h
ι : Type
α : Type u_1
a b s : Stream ι α
inst✝¹ : Preorder ι
inst✝ : AddZeroClass α
x✝ : 0.σ
a✝ : ι
⊢ (if h : 0.valid x✝ = true then
        let_fun this := ⋯;
        eval₀ 0 { val := x✝, property := h } + eval 0 (advance 0 x✝)
      else 0)
      a✝ =
    (0 x✝) a✝
Tactic:
simp
Proof state after:
no goals
Theorem: Etch.Verification.Stream.eval_invalid
Proof state before:
ι : Type
α : Type u_1
a b s✝ : Stream ι α
inst✝² : Preorder ι
inst✝¹ : AddZeroClass α
s : Stream ι α
inst✝ : IsBounded s
q : s.σ
h : ¬s.valid q = true
⊢ eval s q = 0
Tactic:
rwa [Stream.eval, dif_neg]
Proof state after:
no goals
Theorem: Etch.Verification.Stream.eval_valid
Proof state before:
ι : Type
α : Type u_1
a b s✝ : Stream ι α
inst✝² : Preorder ι
inst✝¹ : AddZeroClass α
s : Stream ι α
inst✝ : IsBounded s
q : { q // s.valid q = true }
⊢ eval s ↑q = eval₀ s q + eval s (advance s ↑q)
Tactic:
rw [Stream.eval, dif_pos]
Proof state after:
no goals
Theorem: Etch.Verification.Stream.eval_map_id
Proof state before:
ι : Type
α : Type u_1
a b s✝ : Stream ι α
inst✝² : Preorder ι
inst✝¹ : AddZeroClass α
f : α → α
hf : f = id
s : Stream ι α
inst✝ : IsBounded s
⊢ eval (map f s) = eval s
Tactic:
subst f
Proof state after:
ι : Type
α : Type u_1
a b s✝ : Stream ι α
inst✝² : Preorder ι
inst✝¹ : AddZeroClass α
s : Stream ι α
inst✝ : IsBounded s
⊢ eval (map id s) = eval s
Theorem: Etch.Verification.Stream.eval_map_id
Proof state before:
ι : Type
α : Type u_1
a b s✝ : Stream ι α
inst✝² : Preorder ι
inst✝¹ : AddZeroClass α
s : Stream ι α
inst✝ : IsBounded s
⊢ eval (map id s) = eval s
Tactic:
rfl
Proof state after:
no goals
Theorem: Etch.Verification.Stream.eval_map
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.σ
⊢ eval (map (⇑f) s) q = (Finsupp.mapRange.addMonoidHom f) (eval s q)
Tactic:
apply s.wf.induction q
Proof state after:
ι : 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.σ
⊢ ∀ (x : s.σ),
    (∀ (y : s.σ), WfRel s y x → eval (map (⇑f) s) y = (Finsupp.mapRange.addMonoidHom f) (eval s y)) →
      eval (map (⇑f) s) x = (Finsupp.mapRange.addMonoidHom f) (eval s x)
Theorem: Etch.Verification.Stream.eval_map
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.σ
⊢ ∀ (x : s.σ),
    (∀ (y : s.σ), WfRel s y x → eval (map (⇑f) s) y = (Finsupp.mapRange.addMonoidHom f) (eval s y)) →
      eval (map (⇑f) s) x = (Finsupp.mapRange.addMonoidHom f) (eval s x)
Tactic:
clear q
Proof state after:
ι : Type
α : Type u_2
a b s✝ : Stream ι α
inst✝³ : Preorder ι
β : Type u_1
inst✝² : AddCommMonoid α
inst✝¹ : AddCommMonoid β
f : α →+ β
s : Stream ι α
inst✝ : IsBounded s
⊢ ∀ (x : s.σ),
    (∀ (y : s.σ), WfRel s y x → eval (map (⇑f) s) y = (Finsupp.mapRange.addMonoidHom f) (eval s y)) →
      eval (map (⇑f) s) x = (Finsupp.mapRange.addMonoidHom f) (eval s x)
Theorem: Etch.Verification.Stream.eval_map
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
⊢ ∀ (x : s.σ),
    (∀ (y : s.σ), WfRel s y x → eval (map (⇑f) s) y = (Finsupp.mapRange.addMonoidHom f) (eval s y)) →
      eval (map (⇑f) s) x = (Finsupp.mapRange.addMonoidHom f) (eval s x)
Tactic:
intro q ih
Proof state after:
ι : 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)
⊢ eval (map (⇑f) s) q = (Finsupp.mapRange.addMonoidHom f) (eval s q)
Theorem: Etch.Verification.Stream.eval_map
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.σ
ih : ∀ (y : s.σ), WfRel s y q → eval (map (⇑f) s) y = (Finsupp.mapRange.addMonoidHom f) (eval s y)
⊢ eval (map (⇑f) s) q = (Finsupp.mapRange.addMonoidHom f) (eval s q)
Tactic:
by_cases hq : s.valid q
Proof state after:
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) q = (Finsupp.mapRange.addMonoidHom f) (eval s q)

case neg
ι : 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) q = (Finsupp.mapRange.addMonoidHom f) (eval s q)
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) q = (Finsupp.mapRange.addMonoidHom f) (eval s q)

case neg
ι : 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) q = (Finsupp.mapRange.addMonoidHom f) (eval s q)
Tactic:
swap
Proof state after:
case neg
ι : 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) q = (Finsupp.mapRange.addMonoidHom f) (eval s q)

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) q = (Finsupp.mapRange.addMonoidHom f) (eval s q)
Theorem: Etch.Verification.Stream.eval_map
Proof state before:
case neg
ι : 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) q = (Finsupp.mapRange.addMonoidHom f) (eval s q)
Tactic:
rw [Stream.eval_invalid, Stream.eval_invalid] <;> simp [hq]
Proof state after:
no goals
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) q = (Finsupp.mapRange.addMonoidHom f) (eval s q)
Tactic:
rw [s.eval_valid ⟨_, hq⟩, (s.map f).eval_valid ⟨_, hq⟩]
Proof state after:
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) ↑{ val := q, property := hq }) =
    (Finsupp.mapRange.addMonoidHom f)
      (eval₀ s { val := q, property := hq } + eval s (advance s ↑{ val := q, property := hq }))
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) ↑{ val := q, property := hq }) =
    (Finsupp.mapRange.addMonoidHom f)
      (eval₀ s { val := q, property := hq } + eval s (advance s ↑{ val := q, property := hq }))
Tactic:
simp only [map_σ, map_valid, map_add, Finsupp.mapRange.addMonoidHom_apply]
Proof state after:
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))