Theorem: Etch.Verification.Stream.isMonotonic_iff (Etch/StreamFusion/Proofs/StreamProof.lean)

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
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

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
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 }

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
State after:
no goals

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
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)

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)
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)

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'
State after:
no goals

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'
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)

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']
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 ≤ ⊤

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
State after:
no goals