internlm/Lean-Github huggingface dataset:
Theorem: Etch.Verification.Stream.IsMonotonic.imap
Proof state before:
case mk
ι ι' : Type
inst✝¹ : LinearOrder ι
inst✝ : LinearOrder ι'
α : Type u_1
s : Stream ι α
hs : IsMonotonic s
f : ι → ι'
g : ι → ι' → ι
hf : Monotone f
q : { x // (imap_general f g s).valid x = true }
i : ι'
b : Bool
hq : (imap_general f g s).valid ((imap_general f g s).seek q (i, b)) = true
⊢ (imap_general f g s).index q ≤
    (imap_general f g s).index { val := (imap_general f g s).seek q (i, b), property := hq }
Tactic:
dsimp at q hq ⊢
Proof state after:
case mk
ι ι' : Type
inst✝¹ : LinearOrder ι
inst✝ : LinearOrder ι'
α : Type u_1
s : Stream ι α
hs : IsMonotonic s
f : ι → ι'
g : ι → ι' → ι
hf : Monotone f
q : { x // s.valid x = true }
i : ι'
b : Bool
hq : s.valid (s.seek q (g (s.index q) i, b)) = true
⊢ f (s.index q) ≤ f (s.index { val := s.seek q (g (s.index q) i, b), property := hq })
Theorem: Etch.Verification.Stream.IsMonotonic.imap
Proof state before:
case mk
ι ι' : Type
inst✝¹ : LinearOrder ι
inst✝ : LinearOrder ι'
α : Type u_1
s : Stream ι α
hs : IsMonotonic s
f : ι → ι'
g : ι → ι' → ι
hf : Monotone f
q : { x // s.valid x = true }
i : ι'
b : Bool
hq : s.valid (s.seek q (g (s.index q) i, b)) = true
⊢ f (s.index q) ≤ f (s.index { val := s.seek q (g (s.index q) i, b), property := hq })
Tactic:
apply hf
Proof state after:
case mk.a
ι ι' : Type
inst✝¹ : LinearOrder ι
inst✝ : LinearOrder ι'
α : Type u_1
s : Stream ι α
hs : IsMonotonic s
f : ι → ι'
g : ι → ι' → ι
hf : Monotone f
q : { x // s.valid x = true }
i : ι'
b : Bool
hq : s.valid (s.seek q (g (s.index q) i, b)) = true
⊢ s.index q ≤ s.index { val := s.seek q (g (s.index q) i, b), property := hq }
Theorem: Etch.Verification.Stream.IsMonotonic.imap
Proof state before:
case mk.a
ι ι' : Type
inst✝¹ : LinearOrder ι
inst✝ : LinearOrder ι'
α : Type u_1
s : Stream ι α
hs : IsMonotonic s
f : ι → ι'
g : ι → ι' → ι
hf : Monotone f
q : { x // s.valid x = true }
i : ι'
b : Bool
hq : s.valid (s.seek q (g (s.index q) i, b)) = true
⊢ s.index q ≤ s.index { val := s.seek q (g (s.index q) i, b), property := hq }
Tactic:
apply Stream.isMonotonic_iff.mp hs q
Proof state after:
no goals
Theorem: Etch.Verification.Stream.IsLawful.imap
Proof 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
Proof 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)
Theorem: Etch.Verification.Stream.IsLawful.imap
Proof 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, ?_⟩
Proof 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
Theorem: Etch.Verification.Stream.IsLawful.imap
Proof 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
Proof 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₂
Theorem: Etch.Verification.Stream.IsLawful.imap
Proof 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]
Proof 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₂
Theorem: Etch.Verification.Stream.IsLawful.imap
Proof 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
Proof 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₂
Theorem: Etch.Verification.Stream.IsLawful.imap
Proof 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
Proof 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
Theorem: Etch.Verification.Stream.IsLawful.imap
Proof 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
Proof 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
Theorem: Etch.Verification.Stream.IsLawful.imap
Proof 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
Proof 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
Theorem: Etch.Verification.Stream.IsLawful.imap
Proof 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
Proof state after:
no goals
Theorem: Etch.Verification.Stream.IsLawful.imap
Proof 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]
Proof 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))
Theorem: Etch.Verification.Stream.IsLawful.imap
Proof 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
Proof state after:
no goals
Theorem: Etch.Verification.Stream.IsLawful.imap
Proof 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 _)
Proof 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
Theorem: Etch.Verification.Stream.mul.ready.order_eq
Proof state before:
ι : Type
inst✝ : LinearOrder ι
α : Type u
β : Type v
a : Stream ι α
b : Stream ι β
q : { p // valid a b p = true }
h : ready a b q = true
⊢ toOrder a (valid.fst q) = toOrder b (valid.snd q)
Tactic:
dsimp only [Stream.toOrder]
Proof state after:
ι : Type
inst✝ : LinearOrder ι
α : Type u
β : Type v
a : Stream ι α
b : Stream ι β
q : { p // valid a b p = true }
h : ready a b q = true
⊢ (a.index (valid.fst q), a.ready (valid.fst q)) = (b.index (valid.snd q), b.ready (valid.snd q))
Theorem: Etch.Verification.Stream.mul.ready.order_eq
Proof state before:
ι : Type
inst✝ : LinearOrder ι
α : Type u
β : Type v
a : Stream ι α
b : Stream ι β
q : { p // valid a b p = true }
h : ready a b q = true
⊢ (a.index (valid.fst q), a.ready (valid.fst q)) = (b.index (valid.snd q), b.ready (valid.snd q))
Tactic:
aesop
Proof state after:
no goals
Theorem: Etch.Verification.Stream.order_eq_of_zip_ready
Proof state before:
ι : Type
inst✝ : LinearOrder ι
α : Type u
β : Type v
a : Stream ι α
b : Stream ι β
q : { p // mul.valid a b p = true }
h : mul.ready a b q = true
⊢ toOrder a (mul.valid.fst q) = toOrder (zip a b) q ∧ toOrder b (mul.valid.snd q) = toOrder (zip a b) q
Tactic:
dsimp only [Stream.toOrder]
Proof state after:
ι : Type
inst✝ : LinearOrder ι
α : Type u
β : Type v
a : Stream ι α
b : Stream ι β
q : { p // mul.valid a b p = true }
h : mul.ready a b q = true
⊢ (a.index (mul.valid.fst q), a.ready (mul.valid.fst q)) = ((zip a b).index q, (zip a b).ready q) ∧
    (b.index (mul.valid.snd q), b.ready (mul.valid.snd q)) = ((zip a b).index q, (zip a b).ready q)
Theorem: Etch.Verification.Stream.order_eq_of_zip_ready
Proof state before:
ι : Type
inst✝ : LinearOrder ι
α : Type u
β : Type v
a : Stream ι α
b : Stream ι β
q : { p // mul.valid a b p = true }
h : mul.ready a b q = true
⊢ (a.index (mul.valid.fst q), a.ready (mul.valid.fst q)) = ((zip a b).index q, (zip a b).ready q) ∧
    (b.index (mul.valid.snd q), b.ready (mul.valid.snd q)) = ((zip a b).index q, (zip a b).ready q)
Tactic:
aesop
Proof state after:
no goals
Theorem: Etch.Verification.Stream.zip_index'
Proof state before:
ι : Type
inst✝ : LinearOrder ι
α : Type u
β : Type v
a : Stream ι α
b : Stream ι β
q : (zip a b).σ
⊢ index' (zip a b) q = max (index' a q.1) (index' b q.2)
Tactic:
rw [Stream.index']
Proof state after:
ι : Type
inst✝ : LinearOrder ι
α : Type u
β : Type v
a : Stream ι α
b : Stream ι β
q : (zip a b).σ
⊢ (if h : (zip a b).valid q = true then ↑((zip a b).index { val := q, property := h }) else ⊤) =
    max (index' a q.1) (index' b q.2)
Theorem: Etch.Verification.Stream.zip_index'
Proof state before:
ι : Type
inst✝ : LinearOrder ι
α : Type u
β : Type v
a : Stream ι α
b : Stream ι β
q : (zip a b).σ
⊢ (if h : (zip a b).valid q = true then ↑((zip a b).index { val := q, property := h }) else ⊤) =
    max (index' a q.1) (index' b q.2)
Tactic:
split_ifs with h
Proof state after:
case pos
ι : Type
inst✝ : LinearOrder ι
α : Type u
β : Type v
a : Stream ι α
b : Stream ι β
q : (zip a b).σ
h : (zip a b).valid q = true
⊢ ↑((zip a b).index { val := q, property := h }) = max (index' a q.1) (index' b q.2)

case neg
ι : Type
inst✝ : LinearOrder ι
α : Type u
β : Type v
a : Stream ι α
b : Stream ι β
q : (zip a b).σ
h : ¬(zip a b).valid q = true
⊢ ⊤ = max (index' a q.1) (index' b q.2)
Theorem: Etch.Verification.Stream.zip_index'
Proof state before:
case pos
ι : Type
inst✝ : LinearOrder ι
α : Type u
β : Type v
a : Stream ι α
b : Stream ι β
q : (zip a b).σ
h : (zip a b).valid q = true
⊢ ↑((zip a b).index { val := q, property := h }) = max (index' a q.1) (index' b q.2)
Tactic:
simp at h
Proof state after:
case pos
ι : Type
inst✝ : LinearOrder ι
α : Type u
β : Type v
a : Stream ι α
b : Stream ι β
q : (zip a b).σ
h✝ : (zip a b).valid q = true
h : a.valid q.1 = true ∧ b.valid q.2 = true
⊢ ↑((zip a b).index { val := q, property := h✝ }) = max (index' a q.1) (index' b q.2)
Theorem: Etch.Verification.Stream.zip_index'
Proof state before:
case pos
ι : Type
inst✝ : LinearOrder ι
α : Type u
β : Type v
a : Stream ι α
b : Stream ι β
q : (zip a b).σ
h✝ : (zip a b).valid q = true
h : a.valid q.1 = true ∧ b.valid q.2 = true
⊢ ↑((zip a b).index { val := q, property := h✝ }) = max (index' a q.1) (index' b q.2)
Tactic:
simp [index'_val' _ h.1, index'_val' _ h.2]
Proof state after:
case pos
ι : Type
inst✝ : LinearOrder ι
α : Type u
β : Type v
a : Stream ι α
b : Stream ι β
q : (zip a b).σ
h✝ : (zip a b).valid q = true
h : a.valid q.1 = true ∧ b.valid q.2 = true
⊢ max ↑(a.index (mul.valid.fst { val := q, property := h✝ })) ↑(b.index (mul.valid.snd { val := q, property := h✝ })) =
    max ↑(a.index { val := q.1, property := ⋯ }) ↑(b.index { val := q.2, property := ⋯ })
Theorem: Etch.Verification.Stream.zip_index'
Proof state before:
case pos
ι : Type
inst✝ : LinearOrder ι
α : Type u
β : Type v
a : Stream ι α
b : Stream ι β
q : (zip a b).σ
h✝ : (zip a b).valid q = true
h : a.valid q.1 = true ∧ b.valid q.2 = true
⊢ max ↑(a.index (mul.valid.fst { val := q, property := h✝ })) ↑(b.index (mul.valid.snd { val := q, property := h✝ })) =
    max ↑(a.index { val := q.1, property := ⋯ }) ↑(b.index { val := q.2, property := ⋯ })
Tactic:
rfl
Proof state after:
no goals
Theorem: Etch.Verification.Stream.zip_index'
Proof state before:
case neg
ι : Type
inst✝ : LinearOrder ι
α : Type u
β : Type v
a : Stream ι α
b : Stream ι β
q : (zip a b).σ
h : ¬(zip a b).valid q = true
⊢ ⊤ = max (index' a q.1) (index' b q.2)
Tactic:
simp [-not_and, not_and_or] at h
Proof state after:
case neg
ι : Type
inst✝ : LinearOrder ι
α : Type u
β : Type v
a : Stream ι α
b : Stream ι β
q : (zip a b).σ
h : a.valid q.1 = false ∨ b.valid q.2 = false
⊢ ⊤ = max (index' a q.1) (index' b q.2)
Theorem: Etch.Verification.Stream.zip_index'
Proof state before:
case neg
ι : Type
inst✝ : LinearOrder ι
α : Type u
β : Type v
a : Stream ι α
b : Stream ι β
q : (zip a b).σ
h : a.valid q.1 = false ∨ b.valid q.2 = false
⊢ ⊤ = max (index' a q.1) (index' b q.2)
Tactic:
rcases h with h | h
<;> simp [index'_invalid h]
Proof state after:
no goals
Theorem: Etch.Verification.Stream.min_toOrder_le
Proof state before:
ι : Type
inst✝ : LinearOrder ι
α : Type u
β : Type v
a : Stream ι α
b : Stream ι β
q : { p // mul.valid a b p = true }
⊢ min (toOrder a (mul.valid.fst q)) (toOrder b (mul.valid.snd q)) ≤ toOrder (zip a b) q
Tactic:
rw [Prod.Lex.le_iff'']
Proof state after:
ι : Type
inst✝ : LinearOrder ι
α : Type u
β : Type v
a : Stream ι α
b : Stream ι β
q : { p // mul.valid a b p = true }
⊢ (min (toOrder a (mul.valid.fst q)) (toOrder b (mul.valid.snd q))).1 ≤ (toOrder (zip a b) q).1 ∧
    ((min (toOrder a (mul.valid.fst q)) (toOrder b (mul.valid.snd q))).1 = (toOrder (zip a b) q).1 →
      (min (toOrder a (mul.valid.fst q)) (toOrder b (mul.valid.snd q))).2 ≤ (toOrder (zip a b) q).2)
Theorem: Etch.Verification.Stream.min_toOrder_le
Proof state before:
ι : Type
inst✝ : LinearOrder ι
α : Type u
β : Type v
a : Stream ι α
b : Stream ι β
q : { p // mul.valid a b p = true }
⊢ (min (toOrder a (mul.valid.fst q)) (toOrder b (mul.valid.snd q))).1 ≤ (toOrder (zip a b) q).1 ∧
    ((min (toOrder a (mul.valid.fst q)) (toOrder b (mul.valid.snd q))).1 = (toOrder (zip a b) q).1 →
      (min (toOrder a (mul.valid.fst q)) (toOrder b (mul.valid.snd q))).2 ≤ (toOrder (zip a b) q).2)
Tactic:
simp only [Monotone.map_min (@Prod.Lex.fst_mono ι Bool _ _)]
Proof state after:
ι : Type
inst✝ : LinearOrder ι
α : Type u
β : Type v
a : Stream ι α
b : Stream ι β
q : { p // mul.valid a b p = true }
⊢ min (toOrder a (mul.valid.fst q)).1 (toOrder b (mul.valid.snd q)).1 ≤ (toOrder (zip a b) q).1 ∧
    (min (toOrder a (mul.valid.fst q)).1 (toOrder b (mul.valid.snd q)).1 = (toOrder (zip a b) q).1 →
      (min (toOrder a (mul.valid.fst q)) (toOrder b (mul.valid.snd q))).2 ≤ (toOrder (zip a b) q).2)