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

State before:
ι ι' : Type
inst✝³ : LinearOrder ι
inst✝² : LinearOrder ι'
α : Type u_1
s : Stream ι α
inst✝¹ : AddZeroClass α
inst✝ : IsLawful s
f : ι → ι'
g : ι → ι' → ι
hf : Monotone f
hg : ∀ (j : ι'), Monotone fun x => g x j
hfg : ∀ (i : ι) (j : ι'), compareOfLessAndEq j (f i) = compareOfLessAndEq (g i j) i
⊢ IsLawful (imap_general f g s)
Tactic:
haveI : IsBounded (s.imap_general f g) := IsBounded.imap s f g hfg
State after:
ι ι' : Type
inst✝³ : LinearOrder ι
inst✝² : LinearOrder ι'
α : Type u_1
s : Stream ι α
inst✝¹ : AddZeroClass α
inst✝ : IsLawful s
f : ι → ι'
g : ι → ι' → ι
hf : Monotone f
hg : ∀ (j : ι'), Monotone fun x => g x j
hfg : ∀ (i : ι) (j : ι'), compareOfLessAndEq j (f i) = compareOfLessAndEq (g i j) i
this : IsBounded (imap_general f g s)
⊢ IsLawful (imap_general f g s)

State before:
ι ι' : Type
inst✝³ : LinearOrder ι
inst✝² : LinearOrder ι'
α : Type u_1
s : Stream ι α
inst✝¹ : AddZeroClass α
inst✝ : IsLawful s
f : ι → ι'
g : ι → ι' → ι
hf : Monotone f
hg : ∀ (j : ι'), Monotone fun x => g x j
hfg : ∀ (i : ι) (j : ι'), compareOfLessAndEq j (f i) = compareOfLessAndEq (g i j) i
this : IsBounded (imap_general f g s)
⊢ IsLawful (imap_general f g s)
Tactic:
refine ⟨s.mono.imap g hf, ?_⟩
State after:
ι ι' : Type
inst✝³ : LinearOrder ι
inst✝² : LinearOrder ι'
α : Type u_1
s : Stream ι α
inst✝¹ : AddZeroClass α
inst✝ : IsLawful s
f : ι → ι'
g : ι → ι' → ι
hf : Monotone f
hg : ∀ (j : ι'), Monotone fun x => g x j
hfg : ∀ (i : ι) (j : ι'), compareOfLessAndEq j (f i) = compareOfLessAndEq (g i j) i
this : IsBounded (imap_general f g s)
⊢ ∀ (q : { x // (imap_general f g s).valid x = true }) (i : StreamOrder ι') (j : ι'),
    i ≤ (j, false) →
      (evalMultiset (imap_general f g s) ((imap_general f g s).seek q i)) j = (evalMultiset (imap_general f g s) ↑q) j

State before:
ι ι' : Type
inst✝³ : LinearOrder ι
inst✝² : LinearOrder ι'
α : Type u_1
s : Stream ι α
inst✝¹ : AddZeroClass α
inst✝ : IsLawful s
f : ι → ι'
g : ι → ι' → ι
hf : Monotone f
hg : ∀ (j : ι'), Monotone fun x => g x j
hfg : ∀ (i : ι) (j : ι'), compareOfLessAndEq j (f i) = compareOfLessAndEq (g i j) i
this : IsBounded (imap_general f g s)
⊢ ∀ (q : { x // (imap_general f g s).valid x = true }) (i : StreamOrder ι') (j : ι'),
    i ≤ (j, false) →
      (evalMultiset (imap_general f g s) ((imap_general f g s).seek q i)) j = (evalMultiset (imap_general f g s) ↑q) j
Tactic:
rintro q ⟨j₁, b⟩ j₂ hj
State after:
case mk
ι ι' : Type
inst✝³ : LinearOrder ι
inst✝² : LinearOrder ι'
α : Type u_1
s : Stream ι α
inst✝¹ : AddZeroClass α
inst✝ : IsLawful s
f : ι → ι'
g : ι → ι' → ι
hf : Monotone f
hg : ∀ (j : ι'), Monotone fun x => g x j
hfg : ∀ (i : ι) (j : ι'), compareOfLessAndEq j (f i) = compareOfLessAndEq (g i j) i
this : IsBounded (imap_general f g s)
q : { x // (imap_general f g s).valid x = true }
j₁ : ι'
b : Bool
j₂ : ι'
hj : (j₁, b) ≤ (j₂, false)
⊢ (evalMultiset (imap_general f g s) ((imap_general f g s).seek q (j₁, b))) j₂ =
    (evalMultiset (imap_general f g s) ↑q) j₂

State before:
case mk
ι ι' : Type
inst✝³ : LinearOrder ι
inst✝² : LinearOrder ι'
α : Type u_1
s : Stream ι α
inst✝¹ : AddZeroClass α
inst✝ : IsLawful s
f : ι → ι'
g : ι → ι' → ι
hf : Monotone f
hg : ∀ (j : ι'), Monotone fun x => g x j
hfg : ∀ (i : ι) (j : ι'), compareOfLessAndEq j (f i) = compareOfLessAndEq (g i j) i
this : IsBounded (imap_general f g s)
q : { x // (imap_general f g s).valid x = true }
j₁ : ι'
b : Bool
j₂ : ι'
hj : (j₁, b) ≤ (j₂, false)
⊢ (evalMultiset (imap_general f g s) ((imap_general f g s).seek q (j₁, b))) j₂ =
    (evalMultiset (imap_general f g s) ↑q) j₂
Tactic:
dsimp only [imap_general_seek, imap_general_σ, imap_general_valid]
State after:
case mk
ι ι' : Type
inst✝³ : LinearOrder ι
inst✝² : LinearOrder ι'
α : Type u_1
s : Stream ι α
inst✝¹ : AddZeroClass α
inst✝ : IsLawful s
f : ι → ι'
g : ι → ι' → ι
hf : Monotone f
hg : ∀ (j : ι'), Monotone fun x => g x j
hfg : ∀ (i : ι) (j : ι'), compareOfLessAndEq j (f i) = compareOfLessAndEq (g i j) i
this : IsBounded (imap_general f g s)
q : { x // (imap_general f g s).valid x = true }
j₁ : ι'
b : Bool
j₂ : ι'
hj : (j₁, b) ≤ (j₂, false)
⊢ (evalMultiset (imap_general f g s) (s.seek q (g (s.index q) j₁, b))) j₂ = (evalMultiset (imap_general f g s) ↑q) j₂

State before:
case mk
ι ι' : Type
inst✝³ : LinearOrder ι
inst✝² : LinearOrder ι'
α : Type u_1
s : Stream ι α
inst✝¹ : AddZeroClass α
inst✝ : IsLawful s
f : ι → ι'
g : ι → ι' → ι
hf : Monotone f
hg : ∀ (j : ι'), Monotone fun x => g x j
hfg : ∀ (i : ι) (j : ι'), compareOfLessAndEq j (f i) = compareOfLessAndEq (g i j) i
this : IsBounded (imap_general f g s)
q : { x // (imap_general f g s).valid x = true }
j₁ : ι'
b : Bool
j₂ : ι'
hj : (j₁, b) ≤ (j₂, false)
⊢ (evalMultiset (imap_general f g s) (s.seek q (g (s.index q) j₁, b))) j₂ = (evalMultiset (imap_general f g s) ↑q) j₂
Tactic:
dsimp at q
State after:
case mk
ι ι' : Type
inst✝³ : LinearOrder ι
inst✝² : LinearOrder ι'
α : Type u_1
s : Stream ι α
inst✝¹ : AddZeroClass α
inst✝ : IsLawful s
f : ι → ι'
g : ι → ι' → ι
hf : Monotone f
hg : ∀ (j : ι'), Monotone fun x => g x j
hfg : ∀ (i : ι) (j : ι'), compareOfLessAndEq j (f i) = compareOfLessAndEq (g i j) i
this : IsBounded (imap_general f g s)
q : { x // s.valid x = true }
j₁ : ι'
b : Bool
j₂ : ι'
hj : (j₁, b) ≤ (j₂, false)
⊢ (evalMultiset (imap_general f g s) (s.seek q (g (s.index q) j₁, b))) j₂ = (evalMultiset (imap_general f g s) ↑q) j₂

State before:
case mk
ι ι' : Type
inst✝³ : LinearOrder ι
inst✝² : LinearOrder ι'
α : Type u_1
s : Stream ι α
inst✝¹ : AddZeroClass α
inst✝ : IsLawful s
f : ι → ι'
g : ι → ι' → ι
hf : Monotone f
hg : ∀ (j : ι'), Monotone fun x => g x j
hfg : ∀ (i : ι) (j : ι'), compareOfLessAndEq j (f i) = compareOfLessAndEq (g i j) i
this : IsBounded (imap_general f g s)
q : { x // s.valid x = true }
j₁ : ι'
b : Bool
j₂ : ι'
hj : (j₁, b) ≤ (j₂, false)
⊢ (evalMultiset (imap_general f g s) (s.seek q (g (s.index q) j₁, b))) j₂ = (evalMultiset (imap_general f g s) ↑q) j₂
Tactic:
suffices ∀ i, f i = j₂ → s.eval (s.seek q (g (s.index q) j₁, b)) i = s.eval q i by sorry
State after:
case mk
ι ι' : Type
inst✝³ : LinearOrder ι
inst✝² : LinearOrder ι'
α : Type u_1
s : Stream ι α
inst✝¹ : AddZeroClass α
inst✝ : IsLawful s
f : ι → ι'
g : ι → ι' → ι
hf : Monotone f
hg : ∀ (j : ι'), Monotone fun x => g x j
hfg : ∀ (i : ι) (j : ι'), compareOfLessAndEq j (f i) = compareOfLessAndEq (g i j) i
this : IsBounded (imap_general f g s)
q : { x // s.valid x = true }
j₁ : ι'
b : Bool
j₂ : ι'
hj : (j₁, b) ≤ (j₂, false)
⊢ ∀ (i : ι), f i = j₂ → (eval s (s.seek q (g (s.index q) j₁, b))) i = (eval s ↑q) i

State before:
case mk
ι ι' : Type
inst✝³ : LinearOrder ι
inst✝² : LinearOrder ι'
α : Type u_1
s : Stream ι α
inst✝¹ : AddZeroClass α
inst✝ : IsLawful s
f : ι → ι'
g : ι → ι' → ι
hf : Monotone f
hg : ∀ (j : ι'), Monotone fun x => g x j
hfg : ∀ (i : ι) (j : ι'), compareOfLessAndEq j (f i) = compareOfLessAndEq (g i j) i
this : IsBounded (imap_general f g s)
q : { x // s.valid x = true }
j₁ : ι'
b : Bool
j₂ : ι'
hj : (j₁, b) ≤ (j₂, false)
⊢ ∀ (i : ι), f i = j₂ → (eval s (s.seek q (g (s.index q) j₁, b))) i = (eval s ↑q) i
Tactic:
rintro i rfl
State after:
case mk
ι ι' : Type
inst✝³ : LinearOrder ι
inst✝² : LinearOrder ι'
α : Type u_1
s : Stream ι α
inst✝¹ : AddZeroClass α
inst✝ : IsLawful s
f : ι → ι'
g : ι → ι' → ι
hf : Monotone f
hg : ∀ (j : ι'), Monotone fun x => g x j
hfg : ∀ (i : ι) (j : ι'), compareOfLessAndEq j (f i) = compareOfLessAndEq (g i j) i
this : IsBounded (imap_general f g s)
q : { x // s.valid x = true }
j₁ : ι'
b : Bool
i : ι
hj : (j₁, b) ≤ (f i, false)
⊢ (eval s (s.seek q (g (s.index q) j₁, b))) i = (eval s ↑q) i

State before:
case mk
ι ι' : Type
inst✝³ : LinearOrder ι
inst✝² : LinearOrder ι'
α : Type u_1
s : Stream ι α
inst✝¹ : AddZeroClass α
inst✝ : IsLawful s
f : ι → ι'
g : ι → ι' → ι
hf : Monotone f
hg : ∀ (j : ι'), Monotone fun x => g x j
hfg : ∀ (i : ι) (j : ι'), compareOfLessAndEq j (f i) = compareOfLessAndEq (g i j) i
this : IsBounded (imap_general f g s)
q : { x // s.valid x = true }
j₁ : ι'
b : Bool
i : ι
hj : (j₁, b) ≤ (f i, false)
⊢ (eval s (s.seek q (g (s.index q) j₁, b))) i = (eval s ↑q) i
Tactic:
by_cases le : s.index q ≤ i
State after:
case pos
ι ι' : Type
inst✝³ : LinearOrder ι
inst✝² : LinearOrder ι'
α : Type u_1
s : Stream ι α
inst✝¹ : AddZeroClass α
inst✝ : IsLawful s
f : ι → ι'
g : ι → ι' → ι
hf : Monotone f
hg : ∀ (j : ι'), Monotone fun x => g x j
hfg : ∀ (i : ι) (j : ι'), compareOfLessAndEq j (f i) = compareOfLessAndEq (g i j) i
this : IsBounded (imap_general f g s)
q : { x // s.valid x = true }
j₁ : ι'
b : Bool
i : ι
hj : (j₁, b) ≤ (f i, false)
le : s.index q ≤ i
⊢ (eval s (s.seek q (g (s.index q) j₁, b))) i = (eval s ↑q) i

case neg
ι ι' : Type
inst✝³ : LinearOrder ι
inst✝² : LinearOrder ι'
α : Type u_1
s : Stream ι α
inst✝¹ : AddZeroClass α
inst✝ : IsLawful s
f : ι → ι'
g : ι → ι' → ι
hf : Monotone f
hg : ∀ (j : ι'), Monotone fun x => g x j
hfg : ∀ (i : ι) (j : ι'), compareOfLessAndEq j (f i) = compareOfLessAndEq (g i j) i
this : IsBounded (imap_general f g s)
q : { x // s.valid x = true }
j₁ : ι'
b : Bool
i : ι
hj : (j₁, b) ≤ (f i, false)
le : ¬s.index q ≤ i
⊢ (eval s (s.seek q (g (s.index q) j₁, b))) i = (eval s ↑q) i

State before:
ι ι' : Type
inst✝³ : LinearOrder ι
inst✝² : LinearOrder ι'
α : Type u_1
s : Stream ι α
inst✝¹ : AddZeroClass α
inst✝ : IsLawful s
f : ι → ι'
g : ι → ι' → ι
hf : Monotone f
hg : ∀ (j : ι'), Monotone fun x => g x j
hfg : ∀ (i : ι) (j : ι'), compareOfLessAndEq j (f i) = compareOfLessAndEq (g i j) i
this✝ : IsBounded (imap_general f g s)
q : { x // s.valid x = true }
j₁ : ι'
b : Bool
j₂ : ι'
hj : (j₁, b) ≤ (j₂, false)
this : ∀ (i : ι), f i = j₂ → (eval s (s.seek q (g (s.index q) j₁, b))) i = (eval s ↑q) i
⊢ (evalMultiset (imap_general f g s) (s.seek q (g (s.index q) j₁, b))) j₂ = (evalMultiset (imap_general f g s) ↑q) j₂
Tactic:
sorry
State after:
no goals

State before:
case neg
ι ι' : Type
inst✝³ : LinearOrder ι
inst✝² : LinearOrder ι'
α : Type u_1
s : Stream ι α
inst✝¹ : AddZeroClass α
inst✝ : IsLawful s
f : ι → ι'
g : ι → ι' → ι
hf : Monotone f
hg : ∀ (j : ι'), Monotone fun x => g x j
hfg : ∀ (i : ι) (j : ι'), compareOfLessAndEq j (f i) = compareOfLessAndEq (g i j) i
this : IsBounded (imap_general f g s)
q : { x // s.valid x = true }
j₁ : ι'
b : Bool
i : ι
hj : (j₁, b) ≤ (f i, false)
le : ¬s.index q ≤ i
⊢ (eval s (s.seek q (g (s.index q) j₁, b))) i = (eval s ↑q) i
Tactic:
rw [s.mono.eq_zero_of_lt_index, s.mono.eq_zero_of_lt_index]
State after:
case neg.a
ι ι' : Type
inst✝³ : LinearOrder ι
inst✝² : LinearOrder ι'
α : Type u_1
s : Stream ι α
inst✝¹ : AddZeroClass α
inst✝ : IsLawful s
f : ι → ι'
g : ι → ι' → ι
hf : Monotone f
hg : ∀ (j : ι'), Monotone fun x => g x j
hfg : ∀ (i : ι) (j : ι'), compareOfLessAndEq j (f i) = compareOfLessAndEq (g i j) i
this : IsBounded (imap_general f g s)
q : { x // s.valid x = true }
j₁ : ι'
b : Bool
i : ι
hj : (j₁, b) ≤ (f i, false)
le : ¬s.index q ≤ i
⊢ ↑i < index' s ↑q

case neg.a
ι ι' : Type
inst✝³ : LinearOrder ι
inst✝² : LinearOrder ι'
α : Type u_1
s : Stream ι α
inst✝¹ : AddZeroClass α
inst✝ : IsLawful s
f : ι → ι'
g : ι → ι' → ι
hf : Monotone f
hg : ∀ (j : ι'), Monotone fun x => g x j
hfg : ∀ (i : ι) (j : ι'), compareOfLessAndEq j (f i) = compareOfLessAndEq (g i j) i
this : IsBounded (imap_general f g s)
q : { x // s.valid x = true }
j₁ : ι'
b : Bool
i : ι
hj : (j₁, b) ≤ (f i, false)
le : ¬s.index q ≤ i
⊢ ↑i < index' s (s.seek q (g (s.index q) j₁, b))

State before:
case neg.a
ι ι' : Type
inst✝³ : LinearOrder ι
inst✝² : LinearOrder ι'
α : Type u_1
s : Stream ι α
inst✝¹ : AddZeroClass α
inst✝ : IsLawful s
f : ι → ι'
g : ι → ι' → ι
hf : Monotone f
hg : ∀ (j : ι'), Monotone fun x => g x j
hfg : ∀ (i : ι) (j : ι'), compareOfLessAndEq j (f i) = compareOfLessAndEq (g i j) i
this : IsBounded (imap_general f g s)
q : { x // s.valid x = true }
j₁ : ι'
b : Bool
i : ι
hj : (j₁, b) ≤ (f i, false)
le : ¬s.index q ≤ i
⊢ ↑i < index' s ↑q
Tactic:
simpa using le
State after:
no goals

State before:
case neg.a
ι ι' : Type
inst✝³ : LinearOrder ι
inst✝² : LinearOrder ι'
α : Type u_1
s : Stream ι α
inst✝¹ : AddZeroClass α
inst✝ : IsLawful s
f : ι → ι'
g : ι → ι' → ι
hf : Monotone f
hg : ∀ (j : ι'), Monotone fun x => g x j
hfg : ∀ (i : ι) (j : ι'), compareOfLessAndEq j (f i) = compareOfLessAndEq (g i j) i
this : IsBounded (imap_general f g s)
q : { x // s.valid x = true }
j₁ : ι'
b : Bool
i : ι
hj : (j₁, b) ≤ (f i, false)
le : ¬s.index q ≤ i
⊢ ↑i < index' s (s.seek q (g (s.index q) j₁, b))
Tactic:
refine lt_of_lt_of_le ?_ (s.mono q _)
State after:
case neg.a
ι ι' : Type
inst✝³ : LinearOrder ι
inst✝² : LinearOrder ι'
α : Type u_1
s : Stream ι α
inst✝¹ : AddZeroClass α
inst✝ : IsLawful s
f : ι → ι'
g : ι → ι' → ι
hf : Monotone f
hg : ∀ (j : ι'), Monotone fun x => g x j
hfg : ∀ (i : ι) (j : ι'), compareOfLessAndEq j (f i) = compareOfLessAndEq (g i j) i
this : IsBounded (imap_general f g s)
q : { x // s.valid x = true }
j₁ : ι'
b : Bool
i : ι
hj : (j₁, b) ≤ (f i, false)
le : ¬s.index q ≤ i
⊢ ↑i < index' s ↑q