internlm/Lean-Github huggingface dataset:
Theorem: Etch.Verification.Stream.IsStrictMono.spec
Proof state before:
ι : Type
inst✝ : LinearOrder ι
α : Type u_1
s : Stream ι α
hs : IsStrictMono s
q : { q // s.valid q = true }
i : StreamOrder ι
hi : toOrder s q ≤ i
⊢ (toOrder' s ↑q).1 ≤ (index' s (s.seek q i), false).1
Tactic:
simpa using hs.1 q i
Proof state after:
no goals
Theorem: Etch.Verification.Stream.IsStrictMono.spec
Proof state before:
ι : Type
inst✝ : LinearOrder ι
α : Type u_1
s : Stream ι α
hs : IsStrictMono s
q : { q // s.valid q = true }
i : StreamOrder ι
hi : toOrder s q ≤ i
⊢ (toOrder' s ↑q).1 = (index' s (s.seek q i), false).1 → (toOrder' s ↑q).2 ≤ (index' s (s.seek q i), false).2
Tactic:
simp
Proof state after:
ι : Type
inst✝ : LinearOrder ι
α : Type u_1
s : Stream ι α
hs : IsStrictMono s
q : { q // s.valid q = true }
i : StreamOrder ι
hi : toOrder s q ≤ i
⊢ ↑(s.index q) = index' s (s.seek q i) → s.ready q = false
Theorem: Etch.Verification.Stream.IsStrictMono.spec
Proof state before:
ι : Type
inst✝ : LinearOrder ι
α : Type u_1
s : Stream ι α
hs : IsStrictMono s
q : { q // s.valid q = true }
i : StreamOrder ι
hi : toOrder s q ≤ i
⊢ ↑(s.index q) = index' s (s.seek q i) → s.ready q = false
Tactic:
contrapose
Proof state after:
ι : Type
inst✝ : LinearOrder ι
α : Type u_1
s : Stream ι α
hs : IsStrictMono s
q : { q // s.valid q = true }
i : StreamOrder ι
hi : toOrder s q ≤ i
⊢ ¬s.ready q = false → ¬↑(s.index q) = index' s (s.seek q i)
Theorem: Etch.Verification.Stream.IsStrictMono.spec
Proof state before:
ι : Type
inst✝ : LinearOrder ι
α : Type u_1
s : Stream ι α
hs : IsStrictMono s
q : { q // s.valid q = true }
i : StreamOrder ι
hi : toOrder s q ≤ i
⊢ ¬s.ready q = false → ¬↑(s.index q) = index' s (s.seek q i)
Tactic:
simpa using hs.2 q i hi
Proof state after:
no goals
Theorem: Etch.Verification.Stream.IsStrictMono.index_le_of_mem_support
Proof state before:
ι : Type
inst✝² : LinearOrder ι
α : Type u_1
inst✝¹ : AddZeroClass α
s : Stream ι α
inst✝ : IsBounded s
hs : IsStrictMono s
q : { q // s.valid q = true }
i : StreamOrder ι
hi : toOrder s q ≤ i
j : ι
hj : (eval s (s.seek q i)) j ≠ 0
⊢ coeLex (toOrder s q) ≤ coeLex (j, false)
Tactic:
rw [← Stream.coeLex_toOrder]
Proof state after:
ι : Type
inst✝² : LinearOrder ι
α : Type u_1
inst✝¹ : AddZeroClass α
s : Stream ι α
inst✝ : IsBounded s
hs : IsStrictMono s
q : { q // s.valid q = true }
i : StreamOrder ι
hi : toOrder s q ≤ i
j : ι
hj : (eval s (s.seek q i)) j ≠ 0
⊢ toOrder' s ↑q ≤ coeLex (j, false)
Theorem: Etch.Verification.Stream.IsStrictMono.index_le_of_mem_support
Proof state before:
ι : Type
inst✝² : LinearOrder ι
α : Type u_1
inst✝¹ : AddZeroClass α
s : Stream ι α
inst✝ : IsBounded s
hs : IsStrictMono s
q : { q // s.valid q = true }
i : StreamOrder ι
hi : toOrder s q ≤ i
j : ι
hj : (eval s (s.seek q i)) j ≠ 0
⊢ toOrder' s ↑q ≤ coeLex (j, false)
Tactic:
refine (hs.spec q hi).trans ?_
Proof state after:
ι : Type
inst✝² : LinearOrder ι
α : Type u_1
inst✝¹ : AddZeroClass α
s : Stream ι α
inst✝ : IsBounded s
hs : IsStrictMono s
q : { q // s.valid q = true }
i : StreamOrder ι
hi : toOrder s q ≤ i
j : ι
hj : (eval s (s.seek q i)) j ≠ 0
⊢ (index' s (s.seek q i), false) ≤ coeLex (j, false)
Theorem: Etch.Verification.Stream.IsStrictMono.index_le_of_mem_support
Proof state before:
ι : Type
inst✝² : LinearOrder ι
α : Type u_1
inst✝¹ : AddZeroClass α
s : Stream ι α
inst✝ : IsBounded s
hs : IsStrictMono s
q : { q // s.valid q = true }
i : StreamOrder ι
hi : toOrder s q ≤ i
j : ι
hj : (eval s (s.seek q i)) j ≠ 0
⊢ (index' s (s.seek q i), false) ≤ coeLex (j, false)
Tactic:
simpa using hs.1.index_le_of_mem_support j hj
Proof state after:
no goals
Theorem: Etch.Verification.Stream.IsStrictMono.eq_zero_of_lt_index
Proof state before:
ι : Type
inst✝² : LinearOrder ι
α : Type u_1
inst✝¹ : AddZeroClass α
s : Stream ι α
inst✝ : IsBounded s
hs : IsStrictMono s
q : { q // s.valid q = true }
i : StreamOrder ι
hi : toOrder s q ≤ i
j : ι
⊢ (j, false) < toOrder s q → (eval s (s.seek q i)) j = 0
Tactic:
contrapose
Proof state after:
ι : Type
inst✝² : LinearOrder ι
α : Type u_1
inst✝¹ : AddZeroClass α
s : Stream ι α
inst✝ : IsBounded s
hs : IsStrictMono s
q : { q // s.valid q = true }
i : StreamOrder ι
hi : toOrder s q ≤ i
j : ι
⊢ ¬(eval s (s.seek q i)) j = 0 → ¬(j, false) < toOrder s q
Theorem: Etch.Verification.Stream.IsStrictMono.eq_zero_of_lt_index
Proof state before:
ι : Type
inst✝² : LinearOrder ι
α : Type u_1
inst✝¹ : AddZeroClass α
s : Stream ι α
inst✝ : IsBounded s
hs : IsStrictMono s
q : { q // s.valid q = true }
i : StreamOrder ι
hi : toOrder s q ≤ i
j : ι
⊢ ¬(eval s (s.seek q i)) j = 0 → ¬(j, false) < toOrder s q
Tactic:
simpa using hs.index_le_of_mem_support q hi j
Proof state after:
no goals
Theorem: Etch.Verification.fst_lt_of_lt_of_lt
Proof state before:
ι : Type ?u.114137
inst✝¹ : LinearOrder ι
α : Type u_1
inst✝ : Preorder α
x y : Lex (α × Bool)
z : α
h₁ : x < y
h₂ : y < (z, false)
⊢ (z, false).2 ≤ x.2
Tactic:
simp
Proof state after:
no goals
Theorem: Etch.Verification.fst_lt_of_lt_of_lt
Proof state before:
ι : Type ?u.114137
inst✝¹ : LinearOrder ι
α : Type u_1
inst✝ : Preorder α
x : Lex (α × Bool)
y z : α
h₁ : x < (y, true)
h₂ : (y, true) < (z, true)
⊢ y < (z, true).1
Tactic:
simpa using h₂
Proof state after:
no goals
Theorem: Etch.Verification.fst_lt_of_lt_of_lt
Proof state before:
ι : Type ?u.114137
inst✝¹ : LinearOrder ι
α : Type u_1
inst✝ : Preorder α
x : Lex (α × Bool)
y z : α
h₁ : x < (y, false)
h₂ : (y, false) < (z, true)
⊢ (y, false).2 ≤ x.2
Tactic:
simp
Proof state after:
no goals
Theorem: Etch.Verification.Stream.IsStrictMono.eval_seek_eq_zero
Proof state before:
ι : Type
inst✝² : LinearOrder ι
α : Type u_1
inst✝¹ : AddZeroClass α
s : Stream ι α
inst✝ : IsBounded s
hs : IsStrictMono s
q : { q // s.valid q = true }
i : StreamOrder ι
j : ι
h₁ : (j, false) < i
h₂ : i ≤ toOrder s q
⊢ (eval s (s.seek q i)) j = 0
Tactic:
rcases eq_or_lt_of_le h₂ with h₂ | h₂
Proof state after:
case inl
ι : Type
inst✝² : LinearOrder ι
α : Type u_1
inst✝¹ : AddZeroClass α
s : Stream ι α
inst✝ : IsBounded s
hs : IsStrictMono s
q : { q // s.valid q = true }
i : StreamOrder ι
j : ι
h₁ : (j, false) < i
h₂✝ : i ≤ toOrder s q
h₂ : i = toOrder s q
⊢ (eval s (s.seek q i)) j = 0

case inr
ι : Type
inst✝² : LinearOrder ι
α : Type u_1
inst✝¹ : AddZeroClass α
s : Stream ι α
inst✝ : IsBounded s
hs : IsStrictMono s
q : { q // s.valid q = true }
i : StreamOrder ι
j : ι
h₁ : (j, false) < i
h₂✝ : i ≤ toOrder s q
h₂ : i < toOrder s q
⊢ (eval s (s.seek q i)) j = 0
Theorem: Etch.Verification.Stream.IsStrictMono.eval_seek_eq_zero
Proof state before:
case inl
ι : Type
inst✝² : LinearOrder ι
α : Type u_1
inst✝¹ : AddZeroClass α
s : Stream ι α
inst✝ : IsBounded s
hs : IsStrictMono s
q : { q // s.valid q = true }
i : StreamOrder ι
j : ι
h₁ : (j, false) < i
h₂✝ : i ≤ toOrder s q
h₂ : i = toOrder s q
⊢ (eval s (s.seek q i)) j = 0
Tactic:
refine hs.eq_zero_of_lt_index _ h₂.symm.le _ ?_
Proof state after:
case inl
ι : Type
inst✝² : LinearOrder ι
α : Type u_1
inst✝¹ : AddZeroClass α
s : Stream ι α
inst✝ : IsBounded s
hs : IsStrictMono s
q : { q // s.valid q = true }
i : StreamOrder ι
j : ι
h₁ : (j, false) < i
h₂✝ : i ≤ toOrder s q
h₂ : i = toOrder s q
⊢ (j, false) < toOrder s q
Theorem: Etch.Verification.Stream.IsStrictMono.eval_seek_eq_zero
Proof state before:
case inl
ι : Type
inst✝² : LinearOrder ι
α : Type u_1
inst✝¹ : AddZeroClass α
s : Stream ι α
inst✝ : IsBounded s
hs : IsStrictMono s
q : { q // s.valid q = true }
i : StreamOrder ι
j : ι
h₁ : (j, false) < i
h₂✝ : i ≤ toOrder s q
h₂ : i = toOrder s q
⊢ (j, false) < toOrder s q
Tactic:
rwa [← h₂]
Proof state after:
no goals
Theorem: Etch.Verification.Stream.IsStrictMono.eval_seek_eq_zero
Proof state before:
case inr
ι : Type
inst✝² : LinearOrder ι
α : Type u_1
inst✝¹ : AddZeroClass α
s : Stream ι α
inst✝ : IsBounded s
hs : IsStrictMono s
q : { q // s.valid q = true }
i : StreamOrder ι
j : ι
h₁ : (j, false) < i
h₂✝ : i ≤ toOrder s q
h₂ : i < toOrder s q
⊢ (eval s (s.seek q i)) j = 0
Tactic:
apply hs.1.eq_zero_of_lt_index
Proof state after:
case inr.a
ι : Type
inst✝² : LinearOrder ι
α : Type u_1
inst✝¹ : AddZeroClass α
s : Stream ι α
inst✝ : IsBounded s
hs : IsStrictMono s
q : { q // s.valid q = true }
i : StreamOrder ι
j : ι
h₁ : (j, false) < i
h₂✝ : i ≤ toOrder s q
h₂ : i < toOrder s q
⊢ ↑j < index' s (s.seek q i)
Theorem: Etch.Verification.Stream.IsStrictMono.eval_seek_eq_zero
Proof state before:
case inr.a
ι : Type
inst✝² : LinearOrder ι
α : Type u_1
inst✝¹ : AddZeroClass α
s : Stream ι α
inst✝ : IsBounded s
hs : IsStrictMono s
q : { q // s.valid q = true }
i : StreamOrder ι
j : ι
h₁ : (j, false) < i
h₂✝ : i ≤ toOrder s q
h₂ : i < toOrder s q
⊢ ↑j < index' s (s.seek q i)
Tactic:
refine lt_of_lt_of_le ?_ (hs.1 _ _)
Proof state after:
case inr.a
ι : Type
inst✝² : LinearOrder ι
α : Type u_1
inst✝¹ : AddZeroClass α
s : Stream ι α
inst✝ : IsBounded s
hs : IsStrictMono s
q : { q // s.valid q = true }
i : StreamOrder ι
j : ι
h₁ : (j, false) < i
h₂✝ : i ≤ toOrder s q
h₂ : i < toOrder s q
⊢ ↑j < index' s ↑q
Theorem: Etch.Verification.Stream.IsStrictMono.eval_seek_eq_zero
Proof state before:
case inr.a
ι : Type
inst✝² : LinearOrder ι
α : Type u_1
inst✝¹ : AddZeroClass α
s : Stream ι α
inst✝ : IsBounded s
hs : IsStrictMono s
q : { q // s.valid q = true }
i : StreamOrder ι
j : ι
h₁ : (j, false) < i
h₂✝ : i ≤ toOrder s q
h₂ : i < toOrder s q
⊢ ↑j < index' s ↑q
Tactic:
simpa using fst_lt_of_lt_of_lt h₁ h₂
Proof state after:
no goals
Theorem: Etch.Verification.Stream.IsStrictMono.eval₀_eq_eval_filter
Proof state before:
ι : Type
inst✝² : LinearOrder ι
α : Type u_1
inst✝¹ : AddCommMonoid α
s : Stream ι α
inst✝ : IsBounded s
hs : IsStrictMono s
q : { q // s.valid q = true }
⊢ eval₀ s q = Finsupp.filter (fun i => (i, false) < toOrder s q) (eval s ↑q)
Tactic:
rw [s.eval_valid, Finsupp.filter_add]
Proof state after:
ι : Type
inst✝² : LinearOrder ι
α : Type u_1
inst✝¹ : AddCommMonoid α
s : Stream ι α
inst✝ : IsBounded s
hs : IsStrictMono s
q : { q // s.valid q = true }
⊢ eval₀ s q =
    Finsupp.filter (fun i => (i, false) < toOrder s q) (eval₀ s q) +
      Finsupp.filter (fun i => (i, false) < toOrder s q) (eval s (advance s ↑q))
Theorem: Etch.Verification.Stream.IsStrictMono.eval₀_eq_eval_filter
Proof state before:
ι : Type
inst✝² : LinearOrder ι
α : Type u_1
inst✝¹ : AddCommMonoid α
s : Stream ι α
inst✝ : IsBounded s
hs : IsStrictMono s
q : { q // s.valid q = true }
⊢ eval₀ s q =
    Finsupp.filter (fun i => (i, false) < toOrder s q) (eval₀ s q) +
      Finsupp.filter (fun i => (i, false) < toOrder s q) (eval s (advance s ↑q))
Tactic:
convert (add_zero (M := ι →₀ α) _).symm
Proof state after:
case h.e'_3.h.e'_5
ι : Type
inst✝² : LinearOrder ι
α : Type u_1
inst✝¹ : AddCommMonoid α
s : Stream ι α
inst✝ : IsBounded s
hs : IsStrictMono s
q : { q // s.valid q = true }
⊢ Finsupp.filter (fun i => (i, false) < toOrder s q) (eval₀ s q) = eval₀ s q

case h.e'_3.h.e'_6
ι : Type
inst✝² : LinearOrder ι
α : Type u_1
inst✝¹ : AddCommMonoid α
s : Stream ι α
inst✝ : IsBounded s
hs : IsStrictMono s
q : { q // s.valid q = true }
⊢ Finsupp.filter (fun i => (i, false) < toOrder s q) (eval s (advance s ↑q)) = 0
Theorem: Etch.Verification.Stream.IsStrictMono.eval₀_eq_eval_filter
Proof state before:
case h.e'_3.h.e'_5
ι : Type
inst✝² : LinearOrder ι
α : Type u_1
inst✝¹ : AddCommMonoid α
s : Stream ι α
inst✝ : IsBounded s
hs : IsStrictMono s
q : { q // s.valid q = true }
⊢ Finsupp.filter (fun i => (i, false) < toOrder s q) (eval₀ s q) = eval₀ s q
Tactic:
rw [Finsupp.filter_eq_self_iff]
Proof state after:
case h.e'_3.h.e'_5
ι : Type
inst✝² : LinearOrder ι
α : Type u_1
inst✝¹ : AddCommMonoid α
s : Stream ι α
inst✝ : IsBounded s
hs : IsStrictMono s
q : { q // s.valid q = true }
⊢ ∀ (x : ι), (eval₀ s q) x ≠ 0 → (x, false) < toOrder s q
Theorem: Etch.Verification.Stream.IsStrictMono.eval₀_eq_eval_filter
Proof state before:
case h.e'_3.h.e'_5
ι : Type
inst✝² : LinearOrder ι
α : Type u_1
inst✝¹ : AddCommMonoid α
s : Stream ι α
inst✝ : IsBounded s
hs : IsStrictMono s
q : { q // s.valid q = true }
⊢ ∀ (x : ι), (eval₀ s q) x ≠ 0 → (x, false) < toOrder s q
Tactic:
intro i hi
Proof state after:
case h.e'_3.h.e'_5
ι : Type
inst✝² : LinearOrder ι
α : Type u_1
inst✝¹ : AddCommMonoid α
s : Stream ι α
inst✝ : IsBounded s
hs : IsStrictMono s
q : { q // s.valid q = true }
i : ι
hi : (eval₀ s q) i ≠ 0
⊢ (i, false) < toOrder s q
Theorem: Etch.Verification.Stream.IsStrictMono.eval₀_eq_eval_filter
Proof state before:
case h.e'_3.h.e'_5
ι : Type
inst✝² : LinearOrder ι
α : Type u_1
inst✝¹ : AddCommMonoid α
s : Stream ι α
inst✝ : IsBounded s
hs : IsStrictMono s
q : { q // s.valid q = true }
i : ι
hi : (eval₀ s q) i ≠ 0
⊢ (i, false) < toOrder s q
Tactic:
rw [s.eval₀_support' q hi]
Proof state after:
case h.e'_3.h.e'_5
ι : Type
inst✝² : LinearOrder ι
α : Type u_1
inst✝¹ : AddCommMonoid α
s : Stream ι α
inst✝ : IsBounded s
hs : IsStrictMono s
q : { q // s.valid q = true }
i : ι
hi : (eval₀ s q) i ≠ 0
⊢ (i, false) < (i, true)
Theorem: Etch.Verification.Stream.IsStrictMono.eval₀_eq_eval_filter
Proof state before:
case h.e'_3.h.e'_5
ι : Type
inst✝² : LinearOrder ι
α : Type u_1
inst✝¹ : AddCommMonoid α
s : Stream ι α
inst✝ : IsBounded s
hs : IsStrictMono s
q : { q // s.valid q = true }
i : ι
hi : (eval₀ s q) i ≠ 0
⊢ (i, false) < (i, true)
Tactic:
simp
Proof state after:
no goals
Theorem: Etch.Verification.Stream.IsStrictMono.eval₀_eq_eval_filter
Proof state before:
case h.e'_3.h.e'_6
ι : Type
inst✝² : LinearOrder ι
α : Type u_1
inst✝¹ : AddCommMonoid α
s : Stream ι α
inst✝ : IsBounded s
hs : IsStrictMono s
q : { q // s.valid q = true }
⊢ Finsupp.filter (fun i => (i, false) < toOrder s q) (eval s (advance s ↑q)) = 0
Tactic:
rw [Finsupp.filter_eq_zero_iff]
Proof state after:
case h.e'_3.h.e'_6
ι : Type
inst✝² : LinearOrder ι
α : Type u_1
inst✝¹ : AddCommMonoid α
s : Stream ι α
inst✝ : IsBounded s
hs : IsStrictMono s
q : { q // s.valid q = true }
⊢ ∀ (x : ι), (x, false) < toOrder s q → (eval s (advance s ↑q)) x = 0
Theorem: Etch.Verification.Stream.IsStrictMono.eval₀_eq_eval_filter
Proof state before:
case h.e'_3.h.e'_6
ι : Type
inst✝² : LinearOrder ι
α : Type u_1
inst✝¹ : AddCommMonoid α
s : Stream ι α
inst✝ : IsBounded s
hs : IsStrictMono s
q : { q // s.valid q = true }
⊢ ∀ (x : ι), (x, false) < toOrder s q → (eval s (advance s ↑q)) x = 0
Tactic:
intro i hi
Proof state after:
case h.e'_3.h.e'_6
ι : Type
inst✝² : LinearOrder ι
α : Type u_1
inst✝¹ : AddCommMonoid α
s : Stream ι α
inst✝ : IsBounded s
hs : IsStrictMono s
q : { q // s.valid q = true }
i : ι
hi : (i, false) < toOrder s q
⊢ (eval s (advance s ↑q)) i = 0
Theorem: Etch.Verification.Stream.IsStrictMono.eval₀_eq_eval_filter
Proof state before:
case h.e'_3.h.e'_6
ι : Type
inst✝² : LinearOrder ι
α : Type u_1
inst✝¹ : AddCommMonoid α
s : Stream ι α
inst✝ : IsBounded s
hs : IsStrictMono s
q : { q // s.valid q = true }
i : ι
hi : (i, false) < toOrder s q
⊢ (eval s (advance s ↑q)) i = 0
Tactic:
rw [Stream.advance_val]
Proof state after:
case h.e'_3.h.e'_6
ι : Type
inst✝² : LinearOrder ι
α : Type u_1
inst✝¹ : AddCommMonoid α
s : Stream ι α
inst✝ : IsBounded s
hs : IsStrictMono s
q : { q // s.valid q = true }
i : ι
hi : (i, false) < toOrder s q
⊢ (eval s (s.seek q (toOrder s q))) i = 0
Theorem: Etch.Verification.Stream.IsStrictMono.eval₀_eq_eval_filter
Proof state before:
case h.e'_3.h.e'_6
ι : Type
inst✝² : LinearOrder ι
α : Type u_1
inst✝¹ : AddCommMonoid α
s : Stream ι α
inst✝ : IsBounded s
hs : IsStrictMono s
q : { q // s.valid q = true }
i : ι
hi : (i, false) < toOrder s q
⊢ (eval s (s.seek q (toOrder s q))) i = 0
Tactic:
exact hs.eq_zero_of_lt_index q rfl.le i hi
Proof state after:
no goals
Theorem: Etch.Verification.Stream.evalOption_zero
Proof state before:
ι : Type
inst✝ : LinearOrder ι
α : Type u_1
q : 0.σ
i : ι
⊢ evalOption 0 q i = none
Tactic:
simp [Stream.evalOption]
Proof state after:
no goals
Theorem: Etch.Verification.Stream.evalOption_invalid
Proof state before:
ι : Type
inst✝¹ : LinearOrder ι
α : Type u_1
s : Stream ι α
inst✝ : IsBounded s
q : s.σ
i : ι
h : ¬s.valid q = true
⊢ evalOption s q i = none
Tactic:
simp [Stream.evalOption, h]
Proof state after:
no goals
Theorem: Etch.Verification.Stream.IsStrictMono.evalMultiset_advance_of_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
⊢ (evalMultiset s (advance s ↑q)) (s.index q) = 0
Tactic:
apply h.1.eq_empty_of_lt_index
Proof state after:
case a
ι : 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
⊢ ↑(s.index q) < index' s (advance s ↑q)
Theorem: Etch.Verification.Stream.IsStrictMono.evalMultiset_advance_of_ready
Proof state before:
case a
ι : 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
⊢ ↑(s.index q) < index' s (advance s ↑q)
Tactic:
rw [advance_val]
Proof state after:
case a
ι : 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
⊢ ↑(s.index q) < index' s (s.seek q (toOrder s q))
Theorem: Etch.Verification.Stream.IsStrictMono.evalMultiset_advance_of_ready
Proof state before:
case a
ι : 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
⊢ ↑(s.index q) < index' s (s.seek q (toOrder s q))
Tactic:
exact h.lt' rfl.le hr
Proof state after:
no goals
Theorem: Etch.Verification.Stream.IsStrictMono.evalMultiset_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
⊢ (evalMultiset s ↑q) (s.index q) = {s.value { val := q, property := hr }}
Tactic:
simp [h.evalMultiset_advance_of_ready hr, hr, -advance_val]
Proof state after:
no goals
Theorem: Etch.Verification.Stream.IsStrictMono.evalMultiset_length_le
Proof state before:
ι : Type
inst✝¹ : LinearOrder ι
α : Type u_1
s : Stream ι α
inst✝ : IsBounded s
h : IsStrictMono s
q : s.σ
i : ι
⊢ Multiset.card ((evalMultiset s q) i) ≤ 1
Tactic:
apply s.wf.induction q
Proof state after:
ι : Type
inst✝¹ : LinearOrder ι
α : Type u_1
s : Stream ι α
inst✝ : IsBounded s
h : IsStrictMono s
q : s.σ
i : ι
⊢ ∀ (x : s.σ),
    (∀ (y : s.σ), WfRel s y x → Multiset.card ((evalMultiset s y) i) ≤ 1) → Multiset.card ((evalMultiset s x) i) ≤ 1
Theorem: Etch.Verification.Stream.IsStrictMono.evalMultiset_length_le
Proof state before:
ι : Type
inst✝¹ : LinearOrder ι
α : Type u_1
s : Stream ι α
inst✝ : IsBounded s
h : IsStrictMono s
q : s.σ
i : ι
⊢ ∀ (x : s.σ),
    (∀ (y : s.σ), WfRel s y x → Multiset.card ((evalMultiset s y) i) ≤ 1) → Multiset.card ((evalMultiset s x) i) ≤ 1
Tactic:
clear q
Proof state after:
ι : Type
inst✝¹ : LinearOrder ι
α : Type u_1
s : Stream ι α
inst✝ : IsBounded s
h : IsStrictMono s
i : ι
⊢ ∀ (x : s.σ),
    (∀ (y : s.σ), WfRel s y x → Multiset.card ((evalMultiset s y) i) ≤ 1) → Multiset.card ((evalMultiset s x) i) ≤ 1
Theorem: Etch.Verification.Stream.IsStrictMono.evalMultiset_length_le
Proof state before:
ι : Type
inst✝¹ : LinearOrder ι
α : Type u_1
s : Stream ι α
inst✝ : IsBounded s
h : IsStrictMono s
i : ι
⊢ ∀ (x : s.σ),
    (∀ (y : s.σ), WfRel s y x → Multiset.card ((evalMultiset s y) i) ≤ 1) → Multiset.card ((evalMultiset s x) i) ≤ 1
Tactic:
intro q ih
Proof state after:
ι : 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
⊢ Multiset.card ((evalMultiset s q) i) ≤ 1
Theorem: Etch.Verification.Stream.IsStrictMono.evalMultiset_length_le
Proof state before:
ι : 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
⊢ Multiset.card ((evalMultiset s q) i) ≤ 1
Tactic:
by_cases hq : s.valid q
Proof state after:
case pos
ι : 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
⊢ Multiset.card ((evalMultiset s q) i) ≤ 1

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
⊢ Multiset.card ((evalMultiset s q) i) ≤ 1
Theorem: Etch.Verification.Stream.IsStrictMono.evalMultiset_length_le
Proof state before:
case pos
ι : 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
⊢ Multiset.card ((evalMultiset s q) i) ≤ 1

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
⊢ Multiset.card ((evalMultiset s q) i) ≤ 1
Tactic:
swap
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
⊢ Multiset.card ((evalMultiset s q) i) ≤ 1

case pos
ι : 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
⊢ Multiset.card ((evalMultiset s q) i) ≤ 1
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
⊢ Multiset.card ((evalMultiset s q) i) ≤ 1
Tactic:
simp [hq]
Proof state after:
no goals
Theorem: Etch.Verification.Stream.IsStrictMono.evalMultiset_length_le
Proof state before:
case pos
ι : 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
⊢ Multiset.card ((evalMultiset s q) i) ≤ 1
Tactic:
by_cases hr : s.ready ⟨q, hq⟩ ∧ s.index ⟨q, hq⟩ = i
Proof state after:
case pos
ι : 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

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
Theorem: Etch.Verification.Stream.IsStrictMono.evalMultiset_length_le
Proof state before:
case pos
ι : 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 [← hr.2, h.evalMultiset_ready hr.1, Multiset.card_singleton]
Proof state after:
no goals