internlm/Lean-Github huggingface dataset:
Theorem: Etch.Verification.Stream.zip_ready_eq'
Proof state before:
ι : Type
inst✝² : LinearOrder ι
α : Type u
β : Type v
a : Stream ι α
b : Stream ι β
inst✝¹ : IsStrictLawful a
inst✝ : IsStrictLawful b
q : { x // (zip a b).valid x = true }
h : (zip a b).ready q = true
Ha : (zip a b).index q = a.index (mul.valid.fst q)
Hb : (zip a b).index q = b.index (mul.valid.snd q)
⊢ evalOption a (↑(mul.valid.fst q)) ((zip a b).index q) = some (a.value (mul.ready.fst { val := q, property := h })) ∧
    evalOption b (↑(mul.valid.snd q)) ((zip a b).index q) = some (b.value (mul.ready.snd { val := q, property := h }))
Tactic:
constructor
Proof state after:
case left
ι : Type
inst✝² : LinearOrder ι
α : Type u
β : Type v
a : Stream ι α
b : Stream ι β
inst✝¹ : IsStrictLawful a
inst✝ : IsStrictLawful b
q : { x // (zip a b).valid x = true }
h : (zip a b).ready q = true
Ha : (zip a b).index q = a.index (mul.valid.fst q)
Hb : (zip a b).index q = b.index (mul.valid.snd q)
⊢ evalOption a (↑(mul.valid.fst q)) ((zip a b).index q) = some (a.value (mul.ready.fst { val := q, property := h }))

case right
ι : Type
inst✝² : LinearOrder ι
α : Type u
β : Type v
a : Stream ι α
b : Stream ι β
inst✝¹ : IsStrictLawful a
inst✝ : IsStrictLawful b
q : { x // (zip a b).valid x = true }
h : (zip a b).ready q = true
Ha : (zip a b).index q = a.index (mul.valid.fst q)
Hb : (zip a b).index q = b.index (mul.valid.snd q)
⊢ evalOption b (↑(mul.valid.snd q)) ((zip a b).index q) = some (b.value (mul.ready.snd { val := q, property := h }))
Theorem: Etch.Verification.Stream.zip_ready_eq'
Proof state before:
ι : Type
inst✝² : LinearOrder ι
α : Type u
β : Type v
a : Stream ι α
b : Stream ι β
inst✝¹ : IsStrictLawful a
inst✝ : IsStrictLawful b
q : { x // (zip a b).valid x = true }
h : (zip a b).ready q = true
⊢ (zip a b).index q = a.index (mul.valid.fst q)
Tactic:
aesop
Proof state after:
no goals
Theorem: Etch.Verification.Stream.zip_ready_eq'
Proof state before:
ι : Type
inst✝² : LinearOrder ι
α : Type u
β : Type v
a : Stream ι α
b : Stream ι β
inst✝¹ : IsStrictLawful a
inst✝ : IsStrictLawful b
q : { x // (zip a b).valid x = true }
h : (zip a b).ready q = true
Ha : (zip a b).index q = a.index (mul.valid.fst q)
⊢ (zip a b).index q = b.index (mul.valid.snd q)
Tactic:
aesop
Proof state after:
no goals
Theorem: Etch.Verification.Stream.zip_ready_eq'
Proof state before:
case left
ι : Type
inst✝² : LinearOrder ι
α : Type u
β : Type v
a : Stream ι α
b : Stream ι β
inst✝¹ : IsStrictLawful a
inst✝ : IsStrictLawful b
q : { x // (zip a b).valid x = true }
h : (zip a b).ready q = true
Ha : (zip a b).index q = a.index (mul.valid.fst q)
Hb : (zip a b).index q = b.index (mul.valid.snd q)
⊢ evalOption a (↑(mul.valid.fst q)) ((zip a b).index q) = some (a.value (mul.ready.fst { val := q, property := h }))
Tactic:
rw [Ha, a.strictMono.evalOption_ready]
Proof state after:
case left
ι : Type
inst✝² : LinearOrder ι
α : Type u
β : Type v
a : Stream ι α
b : Stream ι β
inst✝¹ : IsStrictLawful a
inst✝ : IsStrictLawful b
q : { x // (zip a b).valid x = true }
h : (zip a b).ready q = true
Ha : (zip a b).index q = a.index (mul.valid.fst q)
Hb : (zip a b).index q = b.index (mul.valid.snd q)
⊢ some (a.value { val := mul.valid.fst q, property := ?left }) =
    some (a.value (mul.ready.fst { val := q, property := h }))

case left
ι : Type
inst✝² : LinearOrder ι
α : Type u
β : Type v
a : Stream ι α
b : Stream ι β
inst✝¹ : IsStrictLawful a
inst✝ : IsStrictLawful b
q : { x // (zip a b).valid x = true }
h : (zip a b).ready q = true
Ha : (zip a b).index q = a.index (mul.valid.fst q)
Hb : (zip a b).index q = b.index (mul.valid.snd q)
⊢ a.ready (mul.valid.fst q) = true
Theorem: Etch.Verification.Stream.zip_ready_eq'
Proof state before:
case left
ι : Type
inst✝² : LinearOrder ι
α : Type u
β : Type v
a : Stream ι α
b : Stream ι β
inst✝¹ : IsStrictLawful a
inst✝ : IsStrictLawful b
q : { x // (zip a b).valid x = true }
h : (zip a b).ready q = true
Ha : (zip a b).index q = a.index (mul.valid.fst q)
Hb : (zip a b).index q = b.index (mul.valid.snd q)
⊢ some (a.value { val := mul.valid.fst q, property := ?left }) =
    some (a.value (mul.ready.fst { val := q, property := h }))

case left
ι : Type
inst✝² : LinearOrder ι
α : Type u
β : Type v
a : Stream ι α
b : Stream ι β
inst✝¹ : IsStrictLawful a
inst✝ : IsStrictLawful b
q : { x // (zip a b).valid x = true }
h : (zip a b).ready q = true
Ha : (zip a b).index q = a.index (mul.valid.fst q)
Hb : (zip a b).index q = b.index (mul.valid.snd q)
⊢ a.ready (mul.valid.fst q) = true
Tactic:
rfl
Proof state after:
no goals
Theorem: Etch.Verification.Stream.zip_ready_eq'
Proof state before:
case right
ι : Type
inst✝² : LinearOrder ι
α : Type u
β : Type v
a : Stream ι α
b : Stream ι β
inst✝¹ : IsStrictLawful a
inst✝ : IsStrictLawful b
q : { x // (zip a b).valid x = true }
h : (zip a b).ready q = true
Ha : (zip a b).index q = a.index (mul.valid.fst q)
Hb : (zip a b).index q = b.index (mul.valid.snd q)
⊢ evalOption b (↑(mul.valid.snd q)) ((zip a b).index q) = some (b.value (mul.ready.snd { val := q, property := h }))
Tactic:
rw [Hb, b.strictMono.evalOption_ready]
Proof state after:
case right
ι : Type
inst✝² : LinearOrder ι
α : Type u
β : Type v
a : Stream ι α
b : Stream ι β
inst✝¹ : IsStrictLawful a
inst✝ : IsStrictLawful b
q : { x // (zip a b).valid x = true }
h : (zip a b).ready q = true
Ha : (zip a b).index q = a.index (mul.valid.fst q)
Hb : (zip a b).index q = b.index (mul.valid.snd q)
⊢ some (b.value { val := mul.valid.snd q, property := ?right }) =
    some (b.value (mul.ready.snd { val := q, property := h }))

case right
ι : Type
inst✝² : LinearOrder ι
α : Type u
β : Type v
a : Stream ι α
b : Stream ι β
inst✝¹ : IsStrictLawful a
inst✝ : IsStrictLawful b
q : { x // (zip a b).valid x = true }
h : (zip a b).ready q = true
Ha : (zip a b).index q = a.index (mul.valid.fst q)
Hb : (zip a b).index q = b.index (mul.valid.snd q)
⊢ b.ready (mul.valid.snd q) = true
Theorem: Etch.Verification.Stream.zip_ready_eq'
Proof state before:
case right
ι : Type
inst✝² : LinearOrder ι
α : Type u
β : Type v
a : Stream ι α
b : Stream ι β
inst✝¹ : IsStrictLawful a
inst✝ : IsStrictLawful b
q : { x // (zip a b).valid x = true }
h : (zip a b).ready q = true
Ha : (zip a b).index q = a.index (mul.valid.fst q)
Hb : (zip a b).index q = b.index (mul.valid.snd q)
⊢ some (b.value { val := mul.valid.snd q, property := ?right }) =
    some (b.value (mul.ready.snd { val := q, property := h }))

case right
ι : Type
inst✝² : LinearOrder ι
α : Type u
β : Type v
a : Stream ι α
b : Stream ι β
inst✝¹ : IsStrictLawful a
inst✝ : IsStrictLawful b
q : { x // (zip a b).valid x = true }
h : (zip a b).ready q = true
Ha : (zip a b).index q = a.index (mul.valid.fst q)
Hb : (zip a b).index q = b.index (mul.valid.snd q)
⊢ b.ready (mul.valid.snd q) = true
Tactic:
rfl
Proof state after:
no goals
Theorem: Etch.Verification.Stream.left_right_eval_eq_of_toOrder_le
Proof state before:
case right
ι : Type
inst✝² : LinearOrder ι
α : Type u
β : Type v
a : Stream ι α
b : Stream ι β
inst✝¹ : IsStrictLawful a
inst✝ : IsStrictLawful b
i : ι
q : { q // (zip a b).valid q = true }
hi : toOrder (zip a b) q ≤ (i, false)
⊢ evalOption b (advance (zip a b) ↑q).2 i = evalOption b (↑(mul.valid.snd q)) i
Tactic:
simp only [zip_σ, zip_valid, advance_val, zip_seek, evalOption, coe_mul_valid_fst, coe_mul_valid_snd, mul.valid]
Proof state after:
case right
ι : Type
inst✝² : LinearOrder ι
α : Type u
β : Type v
a : Stream ι α
b : Stream ι β
inst✝¹ : IsStrictLawful a
inst✝ : IsStrictLawful b
i : ι
q : { q // (zip a b).valid q = true }
hi : toOrder (zip a b) q ≤ (i, false)
⊢ Multiset.get ((evalMultiset b (b.seek (mul.valid.snd q) (toOrder (zip a b) q))) i) =
    Multiset.get ((evalMultiset b (↑q).2) i)
Theorem: Etch.Verification.Stream.left_right_eval_eq_of_toOrder_le
Proof state before:
case right
ι : Type
inst✝² : LinearOrder ι
α : Type u
β : Type v
a : Stream ι α
b : Stream ι β
inst✝¹ : IsStrictLawful a
inst✝ : IsStrictLawful b
i : ι
q : { q // (zip a b).valid q = true }
hi : toOrder (zip a b) q ≤ (i, false)
⊢ Multiset.get ((evalMultiset b (b.seek (mul.valid.snd q) (toOrder (zip a b) q))) i) =
    Multiset.get ((evalMultiset b (↑q).2) i)
Tactic:
rw [IsLawful.seek_spec _ _ _ hi]
Proof state after:
case right
ι : Type
inst✝² : LinearOrder ι
α : Type u
β : Type v
a : Stream ι α
b : Stream ι β
inst✝¹ : IsStrictLawful a
inst✝ : IsStrictLawful b
i : ι
q : { q // (zip a b).valid q = true }
hi : toOrder (zip a b) q ≤ (i, false)
⊢ Multiset.get ((evalMultiset b ↑(mul.valid.snd q)) i) = Multiset.get ((evalMultiset b (↑q).2) i)
Theorem: Etch.Verification.Stream.left_right_eval_eq_of_toOrder_le
Proof state before:
case right
ι : Type
inst✝² : LinearOrder ι
α : Type u
β : Type v
a : Stream ι α
b : Stream ι β
inst✝¹ : IsStrictLawful a
inst✝ : IsStrictLawful b
i : ι
q : { q // (zip a b).valid q = true }
hi : toOrder (zip a b) q ≤ (i, false)
⊢ Multiset.get ((evalMultiset b ↑(mul.valid.snd q)) i) = Multiset.get ((evalMultiset b (↑q).2) i)
Tactic:
rfl
Proof state after:
no goals
Theorem: Etch.Verification.Stream.zip_spec
Proof state before:
ι : Type
inst✝² : LinearOrder ι
α : Type u
β : Type v
a : Stream ι α
b : Stream ι β
inst✝¹ : IsStrictLawful a
inst✝ : IsStrictLawful b
q : (zip a b).σ
i : ι
⊢ evalOption (zip a b) q i = Option.map₂ Prod.mk (evalOption a q.1 i) (evalOption b q.2 i)
Tactic:
apply (a.zip b).wf.induction q
Proof state after:
ι : Type
inst✝² : LinearOrder ι
α : Type u
β : Type v
a : Stream ι α
b : Stream ι β
inst✝¹ : IsStrictLawful a
inst✝ : IsStrictLawful b
q : (zip a b).σ
i : ι
⊢ ∀ (x : (zip a b).σ),
    (∀ (y : (zip a b).σ),
        WfRel (zip a b) y x →
          evalOption (zip a b) y i = Option.map₂ Prod.mk (evalOption a y.1 i) (evalOption b y.2 i)) →
      evalOption (zip a b) x i = Option.map₂ Prod.mk (evalOption a x.1 i) (evalOption b x.2 i)
Theorem: Etch.Verification.Stream.zip_spec
Proof state before:
ι : Type
inst✝² : LinearOrder ι
α : Type u
β : Type v
a : Stream ι α
b : Stream ι β
inst✝¹ : IsStrictLawful a
inst✝ : IsStrictLawful b
q : (zip a b).σ
i : ι
⊢ ∀ (x : (zip a b).σ),
    (∀ (y : (zip a b).σ),
        WfRel (zip a b) y x →
          evalOption (zip a b) y i = Option.map₂ Prod.mk (evalOption a y.1 i) (evalOption b y.2 i)) →
      evalOption (zip a b) x i = Option.map₂ Prod.mk (evalOption a x.1 i) (evalOption b x.2 i)
Tactic:
clear q
Proof state after:
ι : Type
inst✝² : LinearOrder ι
α : Type u
β : Type v
a : Stream ι α
b : Stream ι β
inst✝¹ : IsStrictLawful a
inst✝ : IsStrictLawful b
i : ι
⊢ ∀ (x : (zip a b).σ),
    (∀ (y : (zip a b).σ),
        WfRel (zip a b) y x →
          evalOption (zip a b) y i = Option.map₂ Prod.mk (evalOption a y.1 i) (evalOption b y.2 i)) →
      evalOption (zip a b) x i = Option.map₂ Prod.mk (evalOption a x.1 i) (evalOption b x.2 i)
Theorem: Etch.Verification.Stream.zip_spec
Proof state before:
ι : Type
inst✝² : LinearOrder ι
α : Type u
β : Type v
a : Stream ι α
b : Stream ι β
inst✝¹ : IsStrictLawful a
inst✝ : IsStrictLawful b
i : ι
⊢ ∀ (x : (zip a b).σ),
    (∀ (y : (zip a b).σ),
        WfRel (zip a b) y x →
          evalOption (zip a b) y i = Option.map₂ Prod.mk (evalOption a y.1 i) (evalOption b y.2 i)) →
      evalOption (zip a b) x i = Option.map₂ Prod.mk (evalOption a x.1 i) (evalOption b x.2 i)
Tactic:
intro q ih
Proof state after:
ι : Type
inst✝² : LinearOrder ι
α : Type u
β : Type v
a : Stream ι α
b : Stream ι β
inst✝¹ : IsStrictLawful a
inst✝ : IsStrictLawful b
i : ι
q : (zip a b).σ
ih :
  ∀ (y : (zip a b).σ),
    WfRel (zip a b) y q → evalOption (zip a b) y i = Option.map₂ Prod.mk (evalOption a y.1 i) (evalOption b y.2 i)
⊢ evalOption (zip a b) q i = Option.map₂ Prod.mk (evalOption a q.1 i) (evalOption b q.2 i)
Theorem: Etch.Verification.Stream.zip_spec
Proof state before:
ι : Type
inst✝² : LinearOrder ι
α : Type u
β : Type v
a : Stream ι α
b : Stream ι β
inst✝¹ : IsStrictLawful a
inst✝ : IsStrictLawful b
i : ι
q : (zip a b).σ
ih :
  ∀ (y : (zip a b).σ),
    WfRel (zip a b) y q → evalOption (zip a b) y i = Option.map₂ Prod.mk (evalOption a y.1 i) (evalOption b y.2 i)
⊢ evalOption (zip a b) q i = Option.map₂ Prod.mk (evalOption a q.1 i) (evalOption b q.2 i)
Tactic:
by_cases hv : (a.zip b).valid q
Proof state after:
case pos
ι : Type
inst✝² : LinearOrder ι
α : Type u
β : Type v
a : Stream ι α
b : Stream ι β
inst✝¹ : IsStrictLawful a
inst✝ : IsStrictLawful b
i : ι
q : (zip a b).σ
ih :
  ∀ (y : (zip a b).σ),
    WfRel (zip a b) y q → evalOption (zip a b) y i = Option.map₂ Prod.mk (evalOption a y.1 i) (evalOption b y.2 i)
hv : (zip a b).valid q = true
⊢ evalOption (zip a b) q i = Option.map₂ Prod.mk (evalOption a q.1 i) (evalOption b q.2 i)

case neg
ι : Type
inst✝² : LinearOrder ι
α : Type u
β : Type v
a : Stream ι α
b : Stream ι β
inst✝¹ : IsStrictLawful a
inst✝ : IsStrictLawful b
i : ι
q : (zip a b).σ
ih :
  ∀ (y : (zip a b).σ),
    WfRel (zip a b) y q → evalOption (zip a b) y i = Option.map₂ Prod.mk (evalOption a y.1 i) (evalOption b y.2 i)
hv : ¬(zip a b).valid q = true
⊢ evalOption (zip a b) q i = Option.map₂ Prod.mk (evalOption a q.1 i) (evalOption b q.2 i)
Theorem: Etch.Verification.Stream.zip_spec
Proof state before:
case pos
ι : Type
inst✝² : LinearOrder ι
α : Type u
β : Type v
a : Stream ι α
b : Stream ι β
inst✝¹ : IsStrictLawful a
inst✝ : IsStrictLawful b
i : ι
q : (zip a b).σ
ih :
  ∀ (y : (zip a b).σ),
    WfRel (zip a b) y q → evalOption (zip a b) y i = Option.map₂ Prod.mk (evalOption a y.1 i) (evalOption b y.2 i)
hv : (zip a b).valid q = true
⊢ evalOption (zip a b) q i = Option.map₂ Prod.mk (evalOption a q.1 i) (evalOption b q.2 i)

case neg
ι : Type
inst✝² : LinearOrder ι
α : Type u
β : Type v
a : Stream ι α
b : Stream ι β
inst✝¹ : IsStrictLawful a
inst✝ : IsStrictLawful b
i : ι
q : (zip a b).σ
ih :
  ∀ (y : (zip a b).σ),
    WfRel (zip a b) y q → evalOption (zip a b) y i = Option.map₂ Prod.mk (evalOption a y.1 i) (evalOption b y.2 i)
hv : ¬(zip a b).valid q = true
⊢ evalOption (zip a b) q i = Option.map₂ Prod.mk (evalOption a q.1 i) (evalOption b q.2 i)
Tactic:
swap
Proof state after:
case neg
ι : Type
inst✝² : LinearOrder ι
α : Type u
β : Type v
a : Stream ι α
b : Stream ι β
inst✝¹ : IsStrictLawful a
inst✝ : IsStrictLawful b
i : ι
q : (zip a b).σ
ih :
  ∀ (y : (zip a b).σ),
    WfRel (zip a b) y q → evalOption (zip a b) y i = Option.map₂ Prod.mk (evalOption a y.1 i) (evalOption b y.2 i)
hv : ¬(zip a b).valid q = true
⊢ evalOption (zip a b) q i = Option.map₂ Prod.mk (evalOption a q.1 i) (evalOption b q.2 i)

case pos
ι : Type
inst✝² : LinearOrder ι
α : Type u
β : Type v
a : Stream ι α
b : Stream ι β
inst✝¹ : IsStrictLawful a
inst✝ : IsStrictLawful b
i : ι
q : (zip a b).σ
ih :
  ∀ (y : (zip a b).σ),
    WfRel (zip a b) y q → evalOption (zip a b) y i = Option.map₂ Prod.mk (evalOption a y.1 i) (evalOption b y.2 i)
hv : (zip a b).valid q = true
⊢ evalOption (zip a b) q i = Option.map₂ Prod.mk (evalOption a q.1 i) (evalOption b q.2 i)
Theorem: Etch.Verification.Stream.zip_spec
Proof state before:
case neg
ι : Type
inst✝² : LinearOrder ι
α : Type u
β : Type v
a : Stream ι α
b : Stream ι β
inst✝¹ : IsStrictLawful a
inst✝ : IsStrictLawful b
i : ι
q : (zip a b).σ
ih :
  ∀ (y : (zip a b).σ),
    WfRel (zip a b) y q → evalOption (zip a b) y i = Option.map₂ Prod.mk (evalOption a y.1 i) (evalOption b y.2 i)
hv : ¬(zip a b).valid q = true
⊢ evalOption (zip a b) q i = Option.map₂ Prod.mk (evalOption a q.1 i) (evalOption b q.2 i)
Tactic:
have := hv
Proof state after:
case neg
ι : Type
inst✝² : LinearOrder ι
α : Type u
β : Type v
a : Stream ι α
b : Stream ι β
inst✝¹ : IsStrictLawful a
inst✝ : IsStrictLawful b
i : ι
q : (zip a b).σ
ih :
  ∀ (y : (zip a b).σ),
    WfRel (zip a b) y q → evalOption (zip a b) y i = Option.map₂ Prod.mk (evalOption a y.1 i) (evalOption b y.2 i)
hv this : ¬(zip a b).valid q = true
⊢ evalOption (zip a b) q i = Option.map₂ Prod.mk (evalOption a q.1 i) (evalOption b q.2 i)
Theorem: Etch.Verification.Stream.zip_spec
Proof state before:
case neg
ι : Type
inst✝² : LinearOrder ι
α : Type u
β : Type v
a : Stream ι α
b : Stream ι β
inst✝¹ : IsStrictLawful a
inst✝ : IsStrictLawful b
i : ι
q : (zip a b).σ
ih :
  ∀ (y : (zip a b).σ),
    WfRel (zip a b) y q → evalOption (zip a b) y i = Option.map₂ Prod.mk (evalOption a y.1 i) (evalOption b y.2 i)
hv this : ¬(zip a b).valid q = true
⊢ evalOption (zip a b) q i = Option.map₂ Prod.mk (evalOption a q.1 i) (evalOption b q.2 i)
Tactic:
simp only [zip_valid, Bool.and_eq_true, not_and_or, Bool.not_eq_true] at hv
Proof state after:
case neg
ι : Type
inst✝² : LinearOrder ι
α : Type u
β : Type v
a : Stream ι α
b : Stream ι β
inst✝¹ : IsStrictLawful a
inst✝ : IsStrictLawful b
i : ι
q : (zip a b).σ
ih :
  ∀ (y : (zip a b).σ),
    WfRel (zip a b) y q → evalOption (zip a b) y i = Option.map₂ Prod.mk (evalOption a y.1 i) (evalOption b y.2 i)
this : ¬(zip a b).valid q = true
hv : a.valid q.1 = false ∨ b.valid q.2 = false
⊢ evalOption (zip a b) q i = Option.map₂ Prod.mk (evalOption a q.1 i) (evalOption b q.2 i)
Theorem: Etch.Verification.Stream.zip_spec
Proof state before:
case neg
ι : Type
inst✝² : LinearOrder ι
α : Type u
β : Type v
a : Stream ι α
b : Stream ι β
inst✝¹ : IsStrictLawful a
inst✝ : IsStrictLawful b
i : ι
q : (zip a b).σ
ih :
  ∀ (y : (zip a b).σ),
    WfRel (zip a b) y q → evalOption (zip a b) y i = Option.map₂ Prod.mk (evalOption a y.1 i) (evalOption b y.2 i)
this : ¬(zip a b).valid q = true
hv : a.valid q.1 = false ∨ b.valid q.2 = false
⊢ evalOption (zip a b) q i = Option.map₂ Prod.mk (evalOption a q.1 i) (evalOption b q.2 i)
Tactic:
rcases hv with hv' | hv' <;> simp [this, hv']
Proof state after:
no goals
Theorem: Etch.Verification.Stream.zip_spec
Proof state before:
case pos
ι : Type
inst✝² : LinearOrder ι
α : Type u
β : Type v
a : Stream ι α
b : Stream ι β
inst✝¹ : IsStrictLawful a
inst✝ : IsStrictLawful b
i : ι
q : (zip a b).σ
ih :
  ∀ (y : (zip a b).σ),
    WfRel (zip a b) y q → evalOption (zip a b) y i = Option.map₂ Prod.mk (evalOption a y.1 i) (evalOption b y.2 i)
hv : (zip a b).valid q = true
⊢ evalOption (zip a b) q i = Option.map₂ Prod.mk (evalOption a q.1 i) (evalOption b q.2 i)
Tactic:
rcases lt_trichotomy (α := StreamOrder ι) (i, true) ((a.zip b).toOrder ⟨q, hv⟩) with h|h|h
Proof state after:
case pos.inl
ι : Type
inst✝² : LinearOrder ι
α : Type u
β : Type v
a : Stream ι α
b : Stream ι β
inst✝¹ : IsStrictLawful a
inst✝ : IsStrictLawful b
i : ι
q : (zip a b).σ
ih :
  ∀ (y : (zip a b).σ),
    WfRel (zip a b) y q → evalOption (zip a b) y i = Option.map₂ Prod.mk (evalOption a y.1 i) (evalOption b y.2 i)
hv : (zip a b).valid q = true
h : (i, true) < toOrder (zip a b) { val := q, property := hv }
⊢ evalOption (zip a b) q i = Option.map₂ Prod.mk (evalOption a q.1 i) (evalOption b q.2 i)

case pos.inr.inl
ι : Type
inst✝² : LinearOrder ι
α : Type u
β : Type v
a : Stream ι α
b : Stream ι β
inst✝¹ : IsStrictLawful a
inst✝ : IsStrictLawful b
i : ι
q : (zip a b).σ
ih :
  ∀ (y : (zip a b).σ),
    WfRel (zip a b) y q → evalOption (zip a b) y i = Option.map₂ Prod.mk (evalOption a y.1 i) (evalOption b y.2 i)
hv : (zip a b).valid q = true
h : (i, true) = toOrder (zip a b) { val := q, property := hv }
⊢ evalOption (zip a b) q i = Option.map₂ Prod.mk (evalOption a q.1 i) (evalOption b q.2 i)

case pos.inr.inr
ι : Type
inst✝² : LinearOrder ι
α : Type u
β : Type v
a : Stream ι α
b : Stream ι β
inst✝¹ : IsStrictLawful a
inst✝ : IsStrictLawful b
i : ι
q : (zip a b).σ
ih :
  ∀ (y : (zip a b).σ),
    WfRel (zip a b) y q → evalOption (zip a b) y i = Option.map₂ Prod.mk (evalOption a y.1 i) (evalOption b y.2 i)
hv : (zip a b).valid q = true
h : toOrder (zip a b) { val := q, property := hv } < (i, true)
⊢ evalOption (zip a b) q i = Option.map₂ Prod.mk (evalOption a q.1 i) (evalOption b q.2 i)
Theorem: Etch.Verification.Stream.zip_spec
Proof state before:
case pos.inl
ι : Type
inst✝² : LinearOrder ι
α : Type u
β : Type v
a : Stream ι α
b : Stream ι β
inst✝¹ : IsStrictLawful a
inst✝ : IsStrictLawful b
i : ι
q : (zip a b).σ
ih :
  ∀ (y : (zip a b).σ),
    WfRel (zip a b) y q → evalOption (zip a b) y i = Option.map₂ Prod.mk (evalOption a y.1 i) (evalOption b y.2 i)
hv : (zip a b).valid q = true
h : (i, true) < toOrder (zip a b) { val := q, property := hv }
⊢ evalOption (zip a b) q i = Option.map₂ Prod.mk (evalOption a q.1 i) (evalOption b q.2 i)
Tactic:
rw [Prod.Lex.mk_true_lt_iff_lt, toOrder_fst] at h
Proof state after:
case pos.inl
ι : Type
inst✝² : LinearOrder ι
α : Type u
β : Type v
a : Stream ι α
b : Stream ι β
inst✝¹ : IsStrictLawful a
inst✝ : IsStrictLawful b
i : ι
q : (zip a b).σ
ih :
  ∀ (y : (zip a b).σ),
    WfRel (zip a b) y q → evalOption (zip a b) y i = Option.map₂ Prod.mk (evalOption a y.1 i) (evalOption b y.2 i)
hv : (zip a b).valid q = true
h : i < (zip a b).index { val := q, property := hv }
⊢ evalOption (zip a b) q i = Option.map₂ Prod.mk (evalOption a q.1 i) (evalOption b q.2 i)
Theorem: Etch.Verification.Stream.zip_spec
Proof state before:
case pos.inl
ι : Type
inst✝² : LinearOrder ι
α : Type u
β : Type v
a : Stream ι α
b : Stream ι β
inst✝¹ : IsStrictLawful a
inst✝ : IsStrictLawful b
i : ι
q : (zip a b).σ
ih :
  ∀ (y : (zip a b).σ),
    WfRel (zip a b) y q → evalOption (zip a b) y i = Option.map₂ Prod.mk (evalOption a y.1 i) (evalOption b y.2 i)
hv : (zip a b).valid q = true
h : i < (zip a b).index { val := q, property := hv }
⊢ evalOption (zip a b) q i = Option.map₂ Prod.mk (evalOption a q.1 i) (evalOption b q.2 i)
Tactic:
rw [zip_eq_zero_of_lt_toOrder h]
Proof state after:
case pos.inl
ι : Type
inst✝² : LinearOrder ι
α : Type u
β : Type v
a : Stream ι α
b : Stream ι β
inst✝¹ : IsStrictLawful a
inst✝ : IsStrictLawful b
i : ι
q : (zip a b).σ
ih :
  ∀ (y : (zip a b).σ),
    WfRel (zip a b) y q → evalOption (zip a b) y i = Option.map₂ Prod.mk (evalOption a y.1 i) (evalOption b y.2 i)
hv : (zip a b).valid q = true
h : i < (zip a b).index { val := q, property := hv }
⊢ none = Option.map₂ Prod.mk (evalOption a q.1 i) (evalOption b q.2 i)
Theorem: Etch.Verification.Stream.zip_spec
Proof state before:
case pos.inl.inr
ι : Type
inst✝² : LinearOrder ι
α : Type u
β : Type v
a : Stream ι α
b : Stream ι β
inst✝¹ : IsStrictLawful a
inst✝ : IsStrictLawful b
i : ι
q : (zip a b).σ
ih :
  ∀ (y : (zip a b).σ),
    WfRel (zip a b) y q → evalOption (zip a b) y i = Option.map₂ Prod.mk (evalOption a y.1 i) (evalOption b y.2 i)
hv : (zip a b).valid q = true
h : i < (zip a b).index { val := q, property := hv }
h₂ : evalOption b (↑(mul.valid.snd { val := q, property := hv })) i = none
⊢ none = Option.map₂ Prod.mk (evalOption a q.1 i) (evalOption b q.2 i)
Tactic:
simp only [zip_σ, zip_valid, coe_mul_valid_fst, coe_mul_valid_snd] at h₂
Proof state after:
case pos.inl.inr
ι : Type
inst✝² : LinearOrder ι
α : Type u
β : Type v
a : Stream ι α
b : Stream ι β
inst✝¹ : IsStrictLawful a
inst✝ : IsStrictLawful b
i : ι
q : (zip a b).σ
ih :
  ∀ (y : (zip a b).σ),
    WfRel (zip a b) y q → evalOption (zip a b) y i = Option.map₂ Prod.mk (evalOption a y.1 i) (evalOption b y.2 i)
hv : (zip a b).valid q = true
h : i < (zip a b).index { val := q, property := hv }
h₂ : evalOption b q.2 i = none
⊢ none = Option.map₂ Prod.mk (evalOption a q.1 i) (evalOption b q.2 i)
Theorem: Etch.Verification.Stream.zip_spec
Proof state before:
case pos.inl.inr
ι : Type
inst✝² : LinearOrder ι
α : Type u
β : Type v
a : Stream ι α
b : Stream ι β
inst✝¹ : IsStrictLawful a
inst✝ : IsStrictLawful b
i : ι
q : (zip a b).σ
ih :
  ∀ (y : (zip a b).σ),
    WfRel (zip a b) y q → evalOption (zip a b) y i = Option.map₂ Prod.mk (evalOption a y.1 i) (evalOption b y.2 i)
hv : (zip a b).valid q = true
h : i < (zip a b).index { val := q, property := hv }
h₂ : evalOption b q.2 i = none
⊢ none = Option.map₂ Prod.mk (evalOption a q.1 i) (evalOption b q.2 i)
Tactic:
simp [h₂]
Proof state after:
no goals