Theorem: Etch.Verification.Stream.IsBounded.imap (Etch/StreamFusion/Proofs/Imap.lean)

State before:
ι ι' : Type
inst✝² : LinearOrder ι
inst✝¹ : LinearOrder ι'
α : Type u_1
s : Stream ι α
inst✝ : IsBounded s
f : ι → ι'
g : ι → ι' → ι
hfg : ∀ (i : ι) (j : ι'), compareOfLessAndEq j (f i) = compareOfLessAndEq (g i j) i
⊢ IsBounded (imap_general f g s)
Tactic:
refine ⟨s.wfRel, ?_⟩
State after:
ι ι' : Type
inst✝² : LinearOrder ι
inst✝¹ : LinearOrder ι'
α : Type u_1
s : Stream ι α
inst✝ : IsBounded s
f : ι → ι'
g : ι → ι' → ι
hfg : ∀ (i : ι) (j : ι'), compareOfLessAndEq j (f i) = compareOfLessAndEq (g i j) i
⊢ ∀ (q : { x // (imap_general f g s).valid x = true }) (i : Lex (ι' × Bool)),
    WellFoundedRelation.rel ((imap_general f g s).seek q i) ↑q ∨
      i < toOrder (imap_general f g s) q ∧ (imap_general f g s).seek q i = ↑q

State before:
ι ι' : Type
inst✝² : LinearOrder ι
inst✝¹ : LinearOrder ι'
α : Type u_1
s : Stream ι α
inst✝ : IsBounded s
f : ι → ι'
g : ι → ι' → ι
hfg : ∀ (i : ι) (j : ι'), compareOfLessAndEq j (f i) = compareOfLessAndEq (g i j) i
⊢ ∀ (q : { x // (imap_general f g s).valid x = true }) (i : Lex (ι' × Bool)),
    WellFoundedRelation.rel ((imap_general f g s).seek q i) ↑q ∨
      i < toOrder (imap_general f g s) q ∧ (imap_general f g s).seek q i = ↑q
Tactic:
rintro q ⟨j, b⟩
State after:
case mk
ι ι' : Type
inst✝² : LinearOrder ι
inst✝¹ : LinearOrder ι'
α : Type u_1
s : Stream ι α
inst✝ : IsBounded s
f : ι → ι'
g : ι → ι' → ι
hfg : ∀ (i : ι) (j : ι'), compareOfLessAndEq j (f i) = compareOfLessAndEq (g i j) i
q : { x // (imap_general f g s).valid x = true }
j : ι'
b : Bool
⊢ WellFoundedRelation.rel ((imap_general f g s).seek q (j, b)) ↑q ∨
    (j, b) < toOrder (imap_general f g s) q ∧ (imap_general f g s).seek q (j, b) = ↑q

State before:
case mk
ι ι' : Type
inst✝² : LinearOrder ι
inst✝¹ : LinearOrder ι'
α : Type u_1
s : Stream ι α
inst✝ : IsBounded s
f : ι → ι'
g : ι → ι' → ι
hfg : ∀ (i : ι) (j : ι'), compareOfLessAndEq j (f i) = compareOfLessAndEq (g i j) i
q : { x // (imap_general f g s).valid x = true }
j : ι'
b : Bool
⊢ WellFoundedRelation.rel ((imap_general f g s).seek q (j, b)) ↑q ∨
    (j, b) < toOrder (imap_general f g s) q ∧ (imap_general f g s).seek q (j, b) = ↑q
Tactic:
refine (s.wf_valid q (g (s.index q) j, b)).imp_right (And.imp_left ?_)
State after:
case mk
ι ι' : Type
inst✝² : LinearOrder ι
inst✝¹ : LinearOrder ι'
α : Type u_1
s : Stream ι α
inst✝ : IsBounded s
f : ι → ι'
g : ι → ι' → ι
hfg : ∀ (i : ι) (j : ι'), compareOfLessAndEq j (f i) = compareOfLessAndEq (g i j) i
q : { x // (imap_general f g s).valid x = true }
j : ι'
b : Bool
⊢ (g (s.index q) j, b) < toOrder s q → (j, b) < toOrder (imap_general f g s) q

State before:
case mk
ι ι' : Type
inst✝² : LinearOrder ι
inst✝¹ : LinearOrder ι'
α : Type u_1
s : Stream ι α
inst✝ : IsBounded s
f : ι → ι'
g : ι → ι' → ι
hfg : ∀ (i : ι) (j : ι'), compareOfLessAndEq j (f i) = compareOfLessAndEq (g i j) i
q : { x // (imap_general f g s).valid x = true }
j : ι'
b : Bool
⊢ (g (s.index q) j, b) < toOrder s q → (j, b) < toOrder (imap_general f g s) q
Tactic:
dsimp [toOrder]
State after:
case mk
ι ι' : Type
inst✝² : LinearOrder ι
inst✝¹ : LinearOrder ι'
α : Type u_1
s : Stream ι α
inst✝ : IsBounded s
f : ι → ι'
g : ι → ι' → ι
hfg : ∀ (i : ι) (j : ι'), compareOfLessAndEq j (f i) = compareOfLessAndEq (g i j) i
q : { x // (imap_general f g s).valid x = true }
j : ι'
b : Bool
⊢ (g (s.index q) j, b) < (s.index q, s.ready q) → (j, b) < (f (s.index q), s.ready q)

State before:
case mk
ι ι' : Type
inst✝² : LinearOrder ι
inst✝¹ : LinearOrder ι'
α : Type u_1
s : Stream ι α
inst✝ : IsBounded s
f : ι → ι'
g : ι → ι' → ι
hfg : ∀ (i : ι) (j : ι'), compareOfLessAndEq j (f i) = compareOfLessAndEq (g i j) i
q : { x // (imap_general f g s).valid x = true }
j : ι'
b : Bool
⊢ (g (s.index q) j, b) < (s.index q, s.ready q) → (j, b) < (f (s.index q), s.ready q)
Tactic:
convert id
State after:
case h'.a
ι ι' : Type
inst✝² : LinearOrder ι
inst✝¹ : LinearOrder ι'
α : Type u_1
s : Stream ι α
inst✝ : IsBounded s
f : ι → ι'
g : ι → ι' → ι
hfg : ∀ (i : ι) (j : ι'), compareOfLessAndEq j (f i) = compareOfLessAndEq (g i j) i
q : { x // (imap_general f g s).valid x = true }
j : ι'
b : Bool
a✝ : (g (s.index q) j, b) < (s.index q, s.ready q)
⊢ (j, b) < (f (s.index q), s.ready q) ↔ (g (s.index q) j, b) < (s.index q, s.ready q)

State before:
case h'.a
ι ι' : Type
inst✝² : LinearOrder ι
inst✝¹ : LinearOrder ι'
α : Type u_1
s : Stream ι α
inst✝ : IsBounded s
f : ι → ι'
g : ι → ι' → ι
hfg : ∀ (i : ι) (j : ι'), compareOfLessAndEq j (f i) = compareOfLessAndEq (g i j) i
q : { x // (imap_general f g s).valid x = true }
j : ι'
b : Bool
a✝ : (g (s.index q) j, b) < (s.index q, s.ready q)
⊢ (j, b) < (f (s.index q), s.ready q) ↔ (g (s.index q) j, b) < (s.index q, s.ready q)
Tactic:
simp only [Prod.Lex.lt_iff', ← lt_iff_of_eq_compare (hfg (s.index q) j),
  eq_iff_of_eq_compare (hfg (s.index q) j)]
State after:
no goals