internlm/Lean-Github huggingface dataset:
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.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)
Tactic:
rfl
Proof state after:
no goals
Theorem: Etch.Verification.Stream.fold_wf_invalid
Proof state before:
ι : Type
α : Type u_2
a b s✝ : Stream ι α
inst✝¹ : Preorder ι
β : Sort u_1
f : β → ι → α → β
s : Stream ι α
inst✝ : IsBounded s
q : s.σ
acc : β
h : ¬s.valid q = true
⊢ fold_wf f s q acc = 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 : s.σ
acc : β
h : ¬s.valid q = true
⊢ (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) =
    acc
Theorem: Etch.Verification.Stream.fold_wf_invalid
Proof state before:
ι : Type
α : Type u_2
a b s✝ : Stream ι α
inst✝¹ : Preorder ι
β : Sort u_1
f : β → ι → α → β
s : Stream ι α
inst✝ : IsBounded s
q : s.σ
acc : β
h : ¬s.valid q = true
⊢ (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) =
    acc
Tactic:
simp [h]
Proof state after:
no goals
Theorem: Etch.Verification.Stream.map_isMonotonic
Proof state before:
ι : Type
inst✝ : LinearOrder ι
α : Type u_1
β : Type u_2
s : Stream ι α
f : α → β
⊢ IsMonotonic (map f s) ↔ IsMonotonic s
Tactic:
rfl
Proof state after:
no goals
Theorem: Etch.Verification.Stream.map_isStrictMono
Proof state before:
ι : Type
inst✝ : LinearOrder ι
α : Type u_1
β : Type u_2
s : Stream ι α
f : α → β
⊢ IsStrictMono (map f s) ↔ IsStrictMono s
Tactic:
rfl
Proof state after:
no goals
Theorem: Etch.Verification.Stream.isMonotonic_iff
Proof state before:
ι : Type
inst✝ : LinearOrder ι
α : Type u_1
s : Stream ι α
⊢ IsMonotonic s ↔
    ∀ (q : { x // s.valid x = true }) (i : Lex (ι × Bool)) (hq : s.valid (s.seek q i) = true),
      s.index q ≤ s.index { val := s.seek q i, property := hq }
Tactic:
constructor
Proof state after:
case mp
ι : Type
inst✝ : LinearOrder ι
α : Type u_1
s : Stream ι α
⊢ IsMonotonic s →
    ∀ (q : { x // s.valid x = true }) (i : Lex (ι × Bool)) (hq : s.valid (s.seek q i) = true),
      s.index q ≤ s.index { val := s.seek q i, property := hq }

case mpr
ι : Type
inst✝ : LinearOrder ι
α : Type u_1
s : Stream ι α
⊢ (∀ (q : { x // s.valid x = true }) (i : Lex (ι × Bool)) (hq : s.valid (s.seek q i) = true),
      s.index q ≤ s.index { val := s.seek q i, property := hq }) →
    IsMonotonic s
Theorem: Etch.Verification.Stream.isMonotonic_iff
Proof state before:
case mp
ι : Type
inst✝ : LinearOrder ι
α : Type u_1
s : Stream ι α
⊢ IsMonotonic s →
    ∀ (q : { x // s.valid x = true }) (i : Lex (ι × Bool)) (hq : s.valid (s.seek q i) = true),
      s.index q ≤ s.index { val := s.seek q i, property := hq }
Tactic:
intro h q i hq
Proof state after:
case mp
ι : Type
inst✝ : LinearOrder ι
α : Type u_1
s : Stream ι α
h : IsMonotonic s
q : { x // s.valid x = true }
i : Lex (ι × Bool)
hq : s.valid (s.seek q i) = true
⊢ s.index q ≤ s.index { val := s.seek q i, property := hq }
Theorem: Etch.Verification.Stream.isMonotonic_iff
Proof state before:
case mp
ι : Type
inst✝ : LinearOrder ι
α : Type u_1
s : Stream ι α
h : IsMonotonic s
q : { x // s.valid x = true }
i : Lex (ι × Bool)
hq : s.valid (s.seek q i) = true
⊢ s.index q ≤ s.index { val := s.seek q i, property := hq }
Tactic:
simpa [index'_val' _ hq] using h q i
Proof state after:
no goals
Theorem: Etch.Verification.Stream.isMonotonic_iff
Proof state before:
case mpr
ι : Type
inst✝ : LinearOrder ι
α : Type u_1
s : Stream ι α
⊢ (∀ (q : { x // s.valid x = true }) (i : Lex (ι × Bool)) (hq : s.valid (s.seek q i) = true),
      s.index q ≤ s.index { val := s.seek q i, property := hq }) →
    IsMonotonic s
Tactic:
intro h q i
Proof state after:
case mpr
ι : Type
inst✝ : LinearOrder ι
α : Type u_1
s : Stream ι α
h :
  ∀ (q : { x // s.valid x = true }) (i : Lex (ι × Bool)) (hq : s.valid (s.seek q i) = true),
    s.index q ≤ s.index { val := s.seek q i, property := hq }
q : { q // s.valid q = true }
i : Lex (ι × Bool)
⊢ index' s ↑q ≤ index' s (s.seek q i)
Theorem: Etch.Verification.Stream.isMonotonic_iff
Proof state before:
case mpr
ι : Type
inst✝ : LinearOrder ι
α : Type u_1
s : Stream ι α
h :
  ∀ (q : { x // s.valid x = true }) (i : Lex (ι × Bool)) (hq : s.valid (s.seek q i) = true),
    s.index q ≤ s.index { val := s.seek q i, property := hq }
q : { q // s.valid q = true }
i : Lex (ι × Bool)
⊢ index' s ↑q ≤ index' s (s.seek q i)
Tactic:
by_cases hq' : s.valid (s.seek q i)
Proof state after:
case pos
ι : Type
inst✝ : LinearOrder ι
α : Type u_1
s : Stream ι α
h :
  ∀ (q : { x // s.valid x = true }) (i : Lex (ι × Bool)) (hq : s.valid (s.seek q i) = true),
    s.index q ≤ s.index { val := s.seek q i, property := hq }
q : { q // s.valid q = true }
i : Lex (ι × Bool)
hq' : s.valid (s.seek q i) = true
⊢ index' s ↑q ≤ index' s (s.seek q i)

case neg
ι : Type
inst✝ : LinearOrder ι
α : Type u_1
s : Stream ι α
h :
  ∀ (q : { x // s.valid x = true }) (i : Lex (ι × Bool)) (hq : s.valid (s.seek q i) = true),
    s.index q ≤ s.index { val := s.seek q i, property := hq }
q : { q // s.valid q = true }
i : Lex (ι × Bool)
hq' : ¬s.valid (s.seek q i) = true
⊢ index' s ↑q ≤ index' s (s.seek q i)
Theorem: Etch.Verification.Stream.isMonotonic_iff
Proof state before:
case pos
ι : Type
inst✝ : LinearOrder ι
α : Type u_1
s : Stream ι α
h :
  ∀ (q : { x // s.valid x = true }) (i : Lex (ι × Bool)) (hq : s.valid (s.seek q i) = true),
    s.index q ≤ s.index { val := s.seek q i, property := hq }
q : { q // s.valid q = true }
i : Lex (ι × Bool)
hq' : s.valid (s.seek q i) = true
⊢ index' s ↑q ≤ index' s (s.seek q i)
Tactic:
simpa [index'_val' _ hq'] using h q i hq'
Proof state after:
no goals
Theorem: Etch.Verification.Stream.isMonotonic_iff
Proof state before:
case neg
ι : Type
inst✝ : LinearOrder ι
α : Type u_1
s : Stream ι α
h :
  ∀ (q : { x // s.valid x = true }) (i : Lex (ι × Bool)) (hq : s.valid (s.seek q i) = true),
    s.index q ≤ s.index { val := s.seek q i, property := hq }
q : { q // s.valid q = true }
i : Lex (ι × Bool)
hq' : ¬s.valid (s.seek q i) = true
⊢ index' s ↑q ≤ index' s (s.seek q i)
Tactic:
rw [Bool.not_eq_true] at hq'
Proof state after:
case neg
ι : Type
inst✝ : LinearOrder ι
α : Type u_1
s : Stream ι α
h :
  ∀ (q : { x // s.valid x = true }) (i : Lex (ι × Bool)) (hq : s.valid (s.seek q i) = true),
    s.index q ≤ s.index { val := s.seek q i, property := hq }
q : { q // s.valid q = true }
i : Lex (ι × Bool)
hq' : s.valid (s.seek q i) = false
⊢ index' s ↑q ≤ index' s (s.seek q i)
Theorem: Etch.Verification.Stream.isMonotonic_iff
Proof state before:
case neg
ι : Type
inst✝ : LinearOrder ι
α : Type u_1
s : Stream ι α
h :
  ∀ (q : { x // s.valid x = true }) (i : Lex (ι × Bool)) (hq : s.valid (s.seek q i) = true),
    s.index q ≤ s.index { val := s.seek q i, property := hq }
q : { q // s.valid q = true }
i : Lex (ι × Bool)
hq' : s.valid (s.seek q i) = false
⊢ index' s ↑q ≤ index' s (s.seek q i)
Tactic:
rw [Stream.index'_invalid hq']
Proof state after:
case neg
ι : Type
inst✝ : LinearOrder ι
α : Type u_1
s : Stream ι α
h :
  ∀ (q : { x // s.valid x = true }) (i : Lex (ι × Bool)) (hq : s.valid (s.seek q i) = true),
    s.index q ≤ s.index { val := s.seek q i, property := hq }
q : { q // s.valid q = true }
i : Lex (ι × Bool)
hq' : s.valid (s.seek q i) = false
⊢ index' s ↑q ≤ ⊤
Theorem: Etch.Verification.Stream.isMonotonic_iff
Proof state before:
case neg
ι : Type
inst✝ : LinearOrder ι
α : Type u_1
s : Stream ι α
h :
  ∀ (q : { x // s.valid x = true }) (i : Lex (ι × Bool)) (hq : s.valid (s.seek q i) = true),
    s.index q ≤ s.index { val := s.seek q i, property := hq }
q : { q // s.valid q = true }
i : Lex (ι × Bool)
hq' : s.valid (s.seek q i) = false
⊢ index' s ↑q ≤ ⊤
Tactic:
exact le_top
Proof state after:
no goals
Theorem: Etch.Verification.Stream.IsMonotonic.index_le_index_advance
Proof state before:
ι : Type
inst✝ : LinearOrder ι
α : Type u_1
s : Stream ι α
h : IsMonotonic s
q : s.σ
⊢ index' s q ≤ index' s (advance s q)
Tactic:
by_cases H : s.valid q
Proof state after:
case pos
ι : Type
inst✝ : LinearOrder ι
α : Type u_1
s : Stream ι α
h : IsMonotonic s
q : s.σ
H : s.valid q = true
⊢ index' s q ≤ index' s (advance s q)

case neg
ι : Type
inst✝ : LinearOrder ι
α : Type u_1
s : Stream ι α
h : IsMonotonic s
q : s.σ
H : ¬s.valid q = true
⊢ index' s q ≤ index' s (advance s q)
Theorem: Etch.Verification.Stream.IsMonotonic.index_le_index_advance
Proof state before:
case pos
ι : Type
inst✝ : LinearOrder ι
α : Type u_1
s : Stream ι α
h : IsMonotonic s
q : s.σ
H : s.valid q = true
⊢ index' s q ≤ index' s (advance s q)

case neg
ι : Type
inst✝ : LinearOrder ι
α : Type u_1
s : Stream ι α
h : IsMonotonic s
q : s.σ
H : ¬s.valid q = true
⊢ index' s q ≤ index' s (advance s q)
Tactic:
swap
Proof state after:
case neg
ι : Type
inst✝ : LinearOrder ι
α : Type u_1
s : Stream ι α
h : IsMonotonic s
q : s.σ
H : ¬s.valid q = true
⊢ index' s q ≤ index' s (advance s q)

case pos
ι : Type
inst✝ : LinearOrder ι
α : Type u_1
s : Stream ι α
h : IsMonotonic s
q : s.σ
H : s.valid q = true
⊢ index' s q ≤ index' s (advance s q)
Theorem: Etch.Verification.Stream.IsMonotonic.index_le_index_advance
Proof state before:
case neg
ι : Type
inst✝ : LinearOrder ι
α : Type u_1
s : Stream ι α
h : IsMonotonic s
q : s.σ
H : ¬s.valid q = true
⊢ index' s q ≤ index' s (advance s q)
Tactic:
simp [H]
Proof state after:
no goals
Theorem: Etch.Verification.Stream.IsMonotonic.index_le_index_advance
Proof state before:
case pos
ι : Type
inst✝ : LinearOrder ι
α : Type u_1
s : Stream ι α
h : IsMonotonic s
q : s.σ
H : s.valid q = true
⊢ index' s q ≤ index' s (advance s q)
Tactic:
simp only [Stream.advance, H, dif_pos]
Proof state after:
case pos
ι : Type
inst✝ : LinearOrder ι
α : Type u_1
s : Stream ι α
h : IsMonotonic s
q : s.σ
H : s.valid q = true
⊢ index' s q ≤ index' s (s.seek { val := q, property := ⋯ } (toOrder s { val := q, property := ⋯ }))
Theorem: Etch.Verification.Stream.IsMonotonic.index_le_index_advance
Proof state before:
case pos
ι : Type
inst✝ : LinearOrder ι
α : Type u_1
s : Stream ι α
h : IsMonotonic s
q : s.σ
H : s.valid q = true
⊢ index' s q ≤ index' s (s.seek { val := q, property := ⋯ } (toOrder s { val := q, property := ⋯ }))
Tactic:
apply h
Proof state after:
no goals
Theorem: Etch.Verification.Stream.IsMonotonic.index_le_of_mem_support
Proof state before:
ι : Type
inst✝² : LinearOrder ι
α : Type u_1
inst✝¹ : AddZeroClass α
s : Stream ι α
inst✝ : IsBounded s
hs : IsMonotonic s
q : s.σ
⊢ ∀ (i : ι), (eval s q) i ≠ 0 → index' s q ≤ ↑i
Tactic:
simp only [← Finsupp.mem_support_iff]
Proof state after:
ι : Type
inst✝² : LinearOrder ι
α : Type u_1
inst✝¹ : AddZeroClass α
s : Stream ι α
inst✝ : IsBounded s
hs : IsMonotonic s
q : s.σ
⊢ ∀ i ∈ (eval s q).support, index' s q ≤ ↑i
Theorem: Etch.Verification.Stream.IsMonotonic.index_le_of_mem_support
Proof state before:
ι : Type
inst✝² : LinearOrder ι
α : Type u_1
inst✝¹ : AddZeroClass α
s : Stream ι α
inst✝ : IsBounded s
hs : IsMonotonic s
q : s.σ
⊢ ∀ i ∈ (eval s q).support, index' s q ≤ ↑i
Tactic:
apply s.wf.induction q
Proof state after:
ι : Type
inst✝² : LinearOrder ι
α : Type u_1
inst✝¹ : AddZeroClass α
s : Stream ι α
inst✝ : IsBounded s
hs : IsMonotonic s
q : s.σ
⊢ ∀ (x : s.σ),
    (∀ (y : s.σ), WfRel s y x → ∀ i ∈ (eval s y).support, index' s y ≤ ↑i) → ∀ i ∈ (eval s x).support, index' s x ≤ ↑i
Theorem: Etch.Verification.Stream.IsMonotonic.index_le_of_mem_support
Proof state before:
ι : Type
inst✝² : LinearOrder ι
α : Type u_1
inst✝¹ : AddZeroClass α
s : Stream ι α
inst✝ : IsBounded s
hs : IsMonotonic s
q : s.σ
⊢ ∀ (x : s.σ),
    (∀ (y : s.σ), WfRel s y x → ∀ i ∈ (eval s y).support, index' s y ≤ ↑i) → ∀ i ∈ (eval s x).support, index' s x ≤ ↑i
Tactic:
clear q
Proof state after:
ι : Type
inst✝² : LinearOrder ι
α : Type u_1
inst✝¹ : AddZeroClass α
s : Stream ι α
inst✝ : IsBounded s
hs : IsMonotonic s
⊢ ∀ (x : s.σ),
    (∀ (y : s.σ), WfRel s y x → ∀ i ∈ (eval s y).support, index' s y ≤ ↑i) → ∀ i ∈ (eval s x).support, index' s x ≤ ↑i
Theorem: Etch.Verification.Stream.IsMonotonic.index_le_of_mem_support
Proof state before:
ι : Type
inst✝² : LinearOrder ι
α : Type u_1
inst✝¹ : AddZeroClass α
s : Stream ι α
inst✝ : IsBounded s
hs : IsMonotonic s
⊢ ∀ (x : s.σ),
    (∀ (y : s.σ), WfRel s y x → ∀ i ∈ (eval s y).support, index' s y ≤ ↑i) → ∀ i ∈ (eval s x).support, index' s x ≤ ↑i
Tactic:
intro q ih i hi
Proof state after:
ι : Type
inst✝² : LinearOrder ι
α : Type u_1
inst✝¹ : AddZeroClass α
s : Stream ι α
inst✝ : IsBounded s
hs : IsMonotonic s
q : s.σ
ih : ∀ (y : s.σ), WfRel s y q → ∀ i ∈ (eval s y).support, index' s y ≤ ↑i
i : ι
hi : i ∈ (eval s q).support
⊢ index' s q ≤ ↑i
Theorem: Etch.Verification.Stream.IsMonotonic.index_le_of_mem_support
Proof state before:
ι : Type
inst✝² : LinearOrder ι
α : Type u_1
inst✝¹ : AddZeroClass α
s : Stream ι α
inst✝ : IsBounded s
hs : IsMonotonic s
q : s.σ
ih : ∀ (y : s.σ), WfRel s y q → ∀ i ∈ (eval s y).support, index' s y ≤ ↑i
i : ι
hi : i ∈ (eval s q).support
⊢ index' s q ≤ ↑i
Tactic:
by_cases H : s.valid q
Proof state after:
case pos
ι : Type
inst✝² : LinearOrder ι
α : Type u_1
inst✝¹ : AddZeroClass α
s : Stream ι α
inst✝ : IsBounded s
hs : IsMonotonic s
q : s.σ
ih : ∀ (y : s.σ), WfRel s y q → ∀ i ∈ (eval s y).support, index' s y ≤ ↑i
i : ι
hi : i ∈ (eval s q).support
H : s.valid q = true
⊢ index' s q ≤ ↑i

case neg
ι : Type
inst✝² : LinearOrder ι
α : Type u_1
inst✝¹ : AddZeroClass α
s : Stream ι α
inst✝ : IsBounded s
hs : IsMonotonic s
q : s.σ
ih : ∀ (y : s.σ), WfRel s y q → ∀ i ∈ (eval s y).support, index' s y ≤ ↑i
i : ι
hi : i ∈ (eval s q).support
H : ¬s.valid q = true
⊢ index' s q ≤ ↑i
Theorem: Etch.Verification.Stream.IsMonotonic.index_le_of_mem_support
Proof state before:
case pos
ι : Type
inst✝² : LinearOrder ι
α : Type u_1
inst✝¹ : AddZeroClass α
s : Stream ι α
inst✝ : IsBounded s
hs : IsMonotonic s
q : s.σ
ih : ∀ (y : s.σ), WfRel s y q → ∀ i ∈ (eval s y).support, index' s y ≤ ↑i
i : ι
hi : i ∈ (eval s q).support
H : s.valid q = true
⊢ index' s q ≤ ↑i

case neg
ι : Type
inst✝² : LinearOrder ι
α : Type u_1
inst✝¹ : AddZeroClass α
s : Stream ι α
inst✝ : IsBounded s
hs : IsMonotonic s
q : s.σ
ih : ∀ (y : s.σ), WfRel s y q → ∀ i ∈ (eval s y).support, index' s y ≤ ↑i
i : ι
hi : i ∈ (eval s q).support
H : ¬s.valid q = true
⊢ index' s q ≤ ↑i
Tactic:
swap
Proof state after:
case neg
ι : Type
inst✝² : LinearOrder ι
α : Type u_1
inst✝¹ : AddZeroClass α
s : Stream ι α
inst✝ : IsBounded s
hs : IsMonotonic s
q : s.σ
ih : ∀ (y : s.σ), WfRel s y q → ∀ i ∈ (eval s y).support, index' s y ≤ ↑i
i : ι
hi : i ∈ (eval s q).support
H : ¬s.valid q = true
⊢ index' s q ≤ ↑i

case pos
ι : Type
inst✝² : LinearOrder ι
α : Type u_1
inst✝¹ : AddZeroClass α
s : Stream ι α
inst✝ : IsBounded s
hs : IsMonotonic s
q : s.σ
ih : ∀ (y : s.σ), WfRel s y q → ∀ i ∈ (eval s y).support, index' s y ≤ ↑i
i : ι
hi : i ∈ (eval s q).support
H : s.valid q = true
⊢ index' s q ≤ ↑i
Theorem: Etch.Verification.Stream.IsMonotonic.index_le_of_mem_support
Proof state before:
case neg
ι : Type
inst✝² : LinearOrder ι
α : Type u_1
inst✝¹ : AddZeroClass α
s : Stream ι α
inst✝ : IsBounded s
hs : IsMonotonic s
q : s.σ
ih : ∀ (y : s.σ), WfRel s y q → ∀ i ∈ (eval s y).support, index' s y ≤ ↑i
i : ι
hi : i ∈ (eval s q).support
H : ¬s.valid q = true
⊢ index' s q ≤ ↑i
Tactic:
simp [H] at hi
Proof state after:
no goals
Theorem: Etch.Verification.Stream.IsMonotonic.index_le_of_mem_support
Proof state before:
case pos
ι : Type
inst✝² : LinearOrder ι
α : Type u_1
inst✝¹ : AddZeroClass α
s : Stream ι α
inst✝ : IsBounded s
hs : IsMonotonic s
q : s.σ
ih : ∀ (y : s.σ), WfRel s y q → ∀ i ∈ (eval s y).support, index' s y ≤ ↑i
i : ι
hi : i ∈ (eval s q).support
H : s.valid q = true
⊢ index' s q ≤ ↑i
Tactic:
rw [s.eval_valid ⟨_, H⟩] at hi
Proof state after:
case pos
ι : Type
inst✝² : LinearOrder ι
α : Type u_1
inst✝¹ : AddZeroClass α
s : Stream ι α
inst✝ : IsBounded s
hs : IsMonotonic s
q : s.σ
ih : ∀ (y : s.σ), WfRel s y q → ∀ i ∈ (eval s y).support, index' s y ≤ ↑i
i : ι
H : s.valid q = true
hi : i ∈ (eval₀ s { val := q, property := H } + eval s (advance s ↑{ val := q, property := H })).support
⊢ index' s q ≤ ↑i
Theorem: Etch.Verification.Stream.IsMonotonic.index_le_of_mem_support
Proof state before:
case pos
ι : Type
inst✝² : LinearOrder ι
α : Type u_1
inst✝¹ : AddZeroClass α
s : Stream ι α
inst✝ : IsBounded s
hs : IsMonotonic s
q : s.σ
ih : ∀ (y : s.σ), WfRel s y q → ∀ i ∈ (eval s y).support, index' s y ≤ ↑i
i : ι
H : s.valid q = true
hi : i ∈ (eval₀ s { val := q, property := H } + eval s (advance s ↑{ val := q, property := H })).support
⊢ index' s q ≤ ↑i
Tactic:
rcases Finset.mem_union.mp (Finsupp.support_add hi) with hi | hi
Proof state after:
case pos.inl
ι : Type
inst✝² : LinearOrder ι
α : Type u_1
inst✝¹ : AddZeroClass α
s : Stream ι α
inst✝ : IsBounded s
hs : IsMonotonic s
q : s.σ
ih : ∀ (y : s.σ), WfRel s y q → ∀ i ∈ (eval s y).support, index' s y ≤ ↑i
i : ι
H : s.valid q = true
hi✝ : i ∈ (eval₀ s { val := q, property := H } + eval s (advance s ↑{ val := q, property := H })).support
hi : i ∈ (eval₀ s { val := q, property := H }).support
⊢ index' s q ≤ ↑i

case pos.inr
ι : Type
inst✝² : LinearOrder ι
α : Type u_1
inst✝¹ : AddZeroClass α
s : Stream ι α
inst✝ : IsBounded s
hs : IsMonotonic s
q : s.σ
ih : ∀ (y : s.σ), WfRel s y q → ∀ i ∈ (eval s y).support, index' s y ≤ ↑i
i : ι
H : s.valid q = true
hi✝ : i ∈ (eval₀ s { val := q, property := H } + eval s (advance s ↑{ val := q, property := H })).support
hi : i ∈ (eval s (advance s ↑{ val := q, property := H })).support
⊢ index' s q ≤ ↑i
Theorem: Etch.Verification.Stream.IsMonotonic.index_le_of_mem_support
Proof state before:
case pos.inl
ι : Type
inst✝² : LinearOrder ι
α : Type u_1
inst✝¹ : AddZeroClass α
s : Stream ι α
inst✝ : IsBounded s
hs : IsMonotonic s
q : s.σ
ih : ∀ (y : s.σ), WfRel s y q → ∀ i ∈ (eval s y).support, index' s y ≤ ↑i
i : ι
H : s.valid q = true
hi✝ : i ∈ (eval₀ s { val := q, property := H } + eval s (advance s ↑{ val := q, property := H })).support
hi : i ∈ (eval₀ s { val := q, property := H }).support
⊢ index' s q ≤ ↑i
Tactic:
rw [Finset.mem_singleton.mp (s.eval₀_support ⟨_, H⟩ hi)]
Proof state after:
case pos.inl
ι : Type
inst✝² : LinearOrder ι
α : Type u_1
inst✝¹ : AddZeroClass α
s : Stream ι α
inst✝ : IsBounded s
hs : IsMonotonic s
q : s.σ
ih : ∀ (y : s.σ), WfRel s y q → ∀ i ∈ (eval s y).support, index' s y ≤ ↑i
i : ι
H : s.valid q = true
hi✝ : i ∈ (eval₀ s { val := q, property := H } + eval s (advance s ↑{ val := q, property := H })).support
hi : i ∈ (eval₀ s { val := q, property := H }).support
⊢ index' s q ≤ ↑(s.index { val := q, property := H })
Theorem: Etch.Verification.Stream.IsMonotonic.index_le_of_mem_support
Proof state before:
case pos.inl
ι : Type
inst✝² : LinearOrder ι
α : Type u_1
inst✝¹ : AddZeroClass α
s : Stream ι α
inst✝ : IsBounded s
hs : IsMonotonic s
q : s.σ
ih : ∀ (y : s.σ), WfRel s y q → ∀ i ∈ (eval s y).support, index' s y ≤ ↑i
i : ι
H : s.valid q = true
hi✝ : i ∈ (eval₀ s { val := q, property := H } + eval s (advance s ↑{ val := q, property := H })).support
hi : i ∈ (eval₀ s { val := q, property := H }).support
⊢ index' s q ≤ ↑(s.index { val := q, property := H })
Tactic:
exact le_of_eq (Stream.index'_val' _ _)
Proof state after:
no goals
Theorem: Etch.Verification.Stream.IsMonotonic.index_le_of_mem_support
Proof state before:
case pos.inr
ι : Type
inst✝² : LinearOrder ι
α : Type u_1
inst✝¹ : AddZeroClass α
s : Stream ι α
inst✝ : IsBounded s
hs : IsMonotonic s
q : s.σ
ih : ∀ (y : s.σ), WfRel s y q → ∀ i ∈ (eval s y).support, index' s y ≤ ↑i
i : ι
H : s.valid q = true
hi✝ : i ∈ (eval₀ s { val := q, property := H } + eval s (advance s ↑{ val := q, property := H })).support
hi : i ∈ (eval s (advance s ↑{ val := q, property := H })).support
⊢ index' s q ≤ ↑i
Tactic:
exact (hs.index_le_index_advance q).trans (ih (s.advance q) (s.next_wf ⟨q, H⟩) i hi)
Proof state after:
no goals
Theorem: Etch.Verification.Stream.IsMonotonic.eq_zero_of_lt_index
Proof state before:
ι : Type
inst✝² : LinearOrder ι
α : Type u_1
inst✝¹ : AddZeroClass α
s : Stream ι α
inst✝ : IsBounded s
hs : IsMonotonic s
q : s.σ
i : ι
⊢ ↑i < index' s q → (eval s q) i = 0
Tactic:
contrapose!
Proof state after:
ι : Type
inst✝² : LinearOrder ι
α : Type u_1
inst✝¹ : AddZeroClass α
s : Stream ι α
inst✝ : IsBounded s
hs : IsMonotonic s
q : s.σ
i : ι
⊢ (eval s q) i ≠ 0 → index' s q ≤ ↑i
Theorem: Etch.Verification.Stream.IsMonotonic.eq_zero_of_lt_index
Proof state before:
ι : Type
inst✝² : LinearOrder ι
α : Type u_1
inst✝¹ : AddZeroClass α
s : Stream ι α
inst✝ : IsBounded s
hs : IsMonotonic s
q : s.σ
i : ι
⊢ (eval s q) i ≠ 0 → index' s q ≤ ↑i
Tactic:
exact hs.index_le_of_mem_support i
Proof state after:
no goals
Theorem: Etch.Verification.Stream.IsMonotonic.eq_empty_of_lt_index
Proof state before:
ι : Type
inst✝¹ : LinearOrder ι
α : Type u_1
s : Stream ι α
inst✝ : IsBounded s
hs : IsMonotonic s
q : s.σ
i : ι
⊢ ↑i < index' s q → (evalMultiset s q) i = 0
Tactic:
contrapose!
Proof state after:
ι : Type
inst✝¹ : LinearOrder ι
α : Type u_1
s : Stream ι α
inst✝ : IsBounded s
hs : IsMonotonic s
q : s.σ
i : ι
⊢ (evalMultiset s q) i ≠ 0 → index' s q ≤ ↑i
Theorem: Etch.Verification.Stream.IsMonotonic.eq_empty_of_lt_index
Proof state before:
ι : Type
inst✝¹ : LinearOrder ι
α : Type u_1
s : Stream ι α
inst✝ : IsBounded s
hs : IsMonotonic s
q : s.σ
i : ι
⊢ (evalMultiset s q) i ≠ 0 → index' s q ≤ ↑i
Tactic:
exact hs.index_le_of_nonempty_multiset i
Proof state after:
no goals
Theorem: Etch.Verification.Stream.IsStrictMono.lt'
Proof state before:
ι : Type
inst✝ : LinearOrder ι
α : Type u_1
s : Stream ι α
hs : IsStrictMono s
q : { q // s.valid q = true }
i : StreamOrder ι
H : toOrder s q ≤ i
hr : s.ready q = true
⊢ ↑(s.index q) < index' s (s.seek q i)
Tactic:
simpa using hs.lt H hr
Proof state after:
no goals
Theorem: Etch.Verification.Stream.IsStrictMono.advance_ne
Proof state before:
ι : Type
inst✝ : LinearOrder ι
α : Type u_1
s : Stream ι α
hs : IsStrictMono s
q : { q // s.valid q = true }
hr : s.ready q = true
⊢ index' s ↑q ≠ index' s (advance s ↑q)
Tactic:
rw [Stream.advance_val]
Proof state after:
ι : Type
inst✝ : LinearOrder ι
α : Type u_1
s : Stream ι α
hs : IsStrictMono s
q : { q // s.valid q = true }
hr : s.ready q = true
⊢ index' s ↑q ≠ index' s (s.seek q (toOrder s q))
Theorem: Etch.Verification.Stream.IsStrictMono.advance_ne
Proof state before:
ι : Type
inst✝ : LinearOrder ι
α : Type u_1
s : Stream ι α
hs : IsStrictMono s
q : { q // s.valid q = true }
hr : s.ready q = true
⊢ index' s ↑q ≠ index' s (s.seek q (toOrder s q))
Tactic:
exact hs.2 q _ rfl.le hr
Proof state after:
no goals