internlm/Lean-Github huggingface dataset:
Theorem: Etch.Verification.Stream.LawfulOfStream.get_fold
Proof state before:
case pos
ι : Type
inst✝⁹ : LinearOrder ι
α : Type u_1
β : Type u_2
m : Type u_3
γ : Type u_4
inst✝⁸ : Zero α
inst✝⁷ : Zero β
inst✝⁶ : Zero m
inst✝⁵ : AddCommMonoid γ
inst✝⁴ : EvalToFinsupp α γ
inst✝³ : EvalToFinsupp β γ
inst✝² : LawfulOfStream α β γ
inst✝¹ : LawfulModifiable ι β m
s : Stream ι α
inst✝ : IsBounded s
i : ι
b : m
q : { t // s.valid t = true }
ih :
  ∀ (y : s.σ),
    WfRel s y ↑q →
      ∀ (b : m),
        evalFinsupp (Readable.get (fold_wf Modifiable.update (map OfStream.eval s) y b) i) =
          evalFinsupp (Readable.get b i) + (eval (map (⇑evalFinsupp) s) y) i
hr : s.ready q = true
heq : s.index q = i
⊢ evalFinsupp (OfStream.eval (s.value { val := q, property := hr }) (Readable.get b i)) +
      (eval (map (⇑evalFinsupp) s) (s.seek q (toOrder s q))) i =
    evalFinsupp (Readable.get b i) +
      (evalFinsupp (s.value { val := q, property := hr }) + (eval (map (⇑evalFinsupp) s) (s.seek q (toOrder s q))) i)
Tactic:
rw [← add_assoc]
Proof state after:
case pos
ι : Type
inst✝⁹ : LinearOrder ι
α : Type u_1
β : Type u_2
m : Type u_3
γ : Type u_4
inst✝⁸ : Zero α
inst✝⁷ : Zero β
inst✝⁶ : Zero m
inst✝⁵ : AddCommMonoid γ
inst✝⁴ : EvalToFinsupp α γ
inst✝³ : EvalToFinsupp β γ
inst✝² : LawfulOfStream α β γ
inst✝¹ : LawfulModifiable ι β m
s : Stream ι α
inst✝ : IsBounded s
i : ι
b : m
q : { t // s.valid t = true }
ih :
  ∀ (y : s.σ),
    WfRel s y ↑q →
      ∀ (b : m),
        evalFinsupp (Readable.get (fold_wf Modifiable.update (map OfStream.eval s) y b) i) =
          evalFinsupp (Readable.get b i) + (eval (map (⇑evalFinsupp) s) y) i
hr : s.ready q = true
heq : s.index q = i
⊢ evalFinsupp (OfStream.eval (s.value { val := q, property := hr }) (Readable.get b i)) +
      (eval (map (⇑evalFinsupp) s) (s.seek q (toOrder s q))) i =
    evalFinsupp (Readable.get b i) + evalFinsupp (s.value { val := q, property := hr }) +
      (eval (map (⇑evalFinsupp) s) (s.seek q (toOrder s q))) i
Theorem: Etch.Verification.Stream.LawfulOfStream.get_fold
Proof state before:
case pos
ι : Type
inst✝⁹ : LinearOrder ι
α : Type u_1
β : Type u_2
m : Type u_3
γ : Type u_4
inst✝⁸ : Zero α
inst✝⁷ : Zero β
inst✝⁶ : Zero m
inst✝⁵ : AddCommMonoid γ
inst✝⁴ : EvalToFinsupp α γ
inst✝³ : EvalToFinsupp β γ
inst✝² : LawfulOfStream α β γ
inst✝¹ : LawfulModifiable ι β m
s : Stream ι α
inst✝ : IsBounded s
i : ι
b : m
q : { t // s.valid t = true }
ih :
  ∀ (y : s.σ),
    WfRel s y ↑q →
      ∀ (b : m),
        evalFinsupp (Readable.get (fold_wf Modifiable.update (map OfStream.eval s) y b) i) =
          evalFinsupp (Readable.get b i) + (eval (map (⇑evalFinsupp) s) y) i
hr : s.ready q = true
heq : s.index q = i
⊢ evalFinsupp (OfStream.eval (s.value { val := q, property := hr }) (Readable.get b i)) +
      (eval (map (⇑evalFinsupp) s) (s.seek q (toOrder s q))) i =
    evalFinsupp (Readable.get b i) + evalFinsupp (s.value { val := q, property := hr }) +
      (eval (map (⇑evalFinsupp) s) (s.seek q (toOrder s q))) i
Tactic:
rw [LawfulOfStream.eval_of_stream]
Proof state after:
no goals
Theorem: Etch.Verification.Stream.LawfulOfStream.get_fold
Proof state before:
case neg
ι : Type
inst✝⁹ : LinearOrder ι
α : Type u_1
β : Type u_2
m : Type u_3
γ : Type u_4
inst✝⁸ : Zero α
inst✝⁷ : Zero β
inst✝⁶ : Zero m
inst✝⁵ : AddCommMonoid γ
inst✝⁴ : EvalToFinsupp α γ
inst✝³ : EvalToFinsupp β γ
inst✝² : LawfulOfStream α β γ
inst✝¹ : LawfulModifiable ι β m
s : Stream ι α
inst✝ : IsBounded s
i : ι
b : m
q : { t // s.valid t = true }
ih :
  ∀ (y : s.σ),
    WfRel s y ↑q →
      ∀ (b : m),
        evalFinsupp (Readable.get (fold_wf Modifiable.update (map OfStream.eval s) y b) i) =
          evalFinsupp (Readable.get b i) + (eval (map (⇑evalFinsupp) s) y) i
hr : s.ready q = true
heq : ¬s.index q = i
⊢ evalFinsupp (Readable.get b i) + (eval (map (⇑evalFinsupp) s) (s.seek q (toOrder s q))) i =
    evalFinsupp (Readable.get b i) + (0 + (eval (map (⇑evalFinsupp) s) (s.seek q (toOrder s q))) i)
Tactic:
simp
Proof state after:
no goals
Theorem: Etch.Verification.Stream.LawfulOfStream.get_fold
Proof state before:
case neg
ι : Type
inst✝⁹ : LinearOrder ι
α : Type u_1
β : Type u_2
m : Type u_3
γ : Type u_4
inst✝⁸ : Zero α
inst✝⁷ : Zero β
inst✝⁶ : Zero m
inst✝⁵ : AddCommMonoid γ
inst✝⁴ : EvalToFinsupp α γ
inst✝³ : EvalToFinsupp β γ
inst✝² : LawfulOfStream α β γ
inst✝¹ : LawfulModifiable ι β m
s : Stream ι α
inst✝ : IsBounded s
i : ι
b : m
q : { t // s.valid t = true }
ih :
  ∀ (y : s.σ),
    WfRel s y ↑q →
      ∀ (b : m),
        evalFinsupp (Readable.get (fold_wf Modifiable.update (map OfStream.eval s) y b) i) =
          evalFinsupp (Readable.get b i) + (eval (map (⇑evalFinsupp) s) y) i
hr : ¬s.ready q = true
⊢ evalFinsupp (Readable.get b i) + (eval (map (⇑evalFinsupp) s) (s.seek q (toOrder s q))) i =
    evalFinsupp (Readable.get b i) + (0 i + (eval (map (⇑evalFinsupp) s) (s.seek q (toOrder s q))) i)
Tactic:
simp
Proof state after:
no goals
Theorem: Etch.Verification.Stream.LawfulOfStream.get_fold
Proof state before:
case pos.a
ι : Type
inst✝⁹ : LinearOrder ι
α : Type u_1
β : Type u_2
m : Type u_3
γ : Type u_4
inst✝⁸ : Zero α
inst✝⁷ : Zero β
inst✝⁶ : Zero m
inst✝⁵ : AddCommMonoid γ
inst✝⁴ : EvalToFinsupp α γ
inst✝³ : EvalToFinsupp β γ
inst✝² : LawfulOfStream α β γ
inst✝¹ : LawfulModifiable ι β m
s : Stream ι α
inst✝ : IsBounded s
i : ι
b : m
q : { t // s.valid t = true }
ih :
  ∀ (y : s.σ),
    WfRel s y ↑q →
      ∀ (b : m),
        evalFinsupp (Readable.get (fold_wf Modifiable.update (map OfStream.eval s) y b) i) =
          evalFinsupp (Readable.get b i) + (eval (map (⇑evalFinsupp) s) y) i
⊢ WfRel s (s.seek q (toOrder s q)) ↑q
Tactic:
exact s.progress rfl.le
Proof state after:
no goals
Theorem: Etch.Verification.Stream.LawfulOfStream.get_fold
Proof state before:
case neg
ι : Type
inst✝⁹ : LinearOrder ι
α : Type u_1
β : Type u_2
m : Type u_3
γ : Type u_4
inst✝⁸ : Zero α
inst✝⁷ : Zero β
inst✝⁶ : Zero m
inst✝⁵ : AddCommMonoid γ
inst✝⁴ : EvalToFinsupp α γ
inst✝³ : EvalToFinsupp β γ
inst✝² : LawfulOfStream α β γ
inst✝¹ : LawfulModifiable ι β m
s : Stream ι α
inst✝ : IsBounded s
i : ι
q : s.σ
ih :
  ∀ (y : s.σ),
    WfRel s y q →
      ∀ (b : m),
        evalFinsupp (Readable.get (fold_wf Modifiable.update (map OfStream.eval s) y b) i) =
          evalFinsupp (Readable.get b i) + (eval (map (⇑evalFinsupp) s) y) i
b : m
hv : ¬s.valid q = true
⊢ evalFinsupp (Readable.get (fold_wf Modifiable.update (map OfStream.eval s) q b) i) =
    evalFinsupp (Readable.get b i) + (eval (map (⇑evalFinsupp) s) q) i
Tactic:
rw [Stream.fold_wf_invalid, Stream.eval_invalid]
Proof state after:
case neg
ι : Type
inst✝⁹ : LinearOrder ι
α : Type u_1
β : Type u_2
m : Type u_3
γ : Type u_4
inst✝⁸ : Zero α
inst✝⁷ : Zero β
inst✝⁶ : Zero m
inst✝⁵ : AddCommMonoid γ
inst✝⁴ : EvalToFinsupp α γ
inst✝³ : EvalToFinsupp β γ
inst✝² : LawfulOfStream α β γ
inst✝¹ : LawfulModifiable ι β m
s : Stream ι α
inst✝ : IsBounded s
i : ι
q : s.σ
ih :
  ∀ (y : s.σ),
    WfRel s y q →
      ∀ (b : m),
        evalFinsupp (Readable.get (fold_wf Modifiable.update (map OfStream.eval s) y b) i) =
          evalFinsupp (Readable.get b i) + (eval (map (⇑evalFinsupp) s) y) i
b : m
hv : ¬s.valid q = true
⊢ evalFinsupp (Readable.get b i) = evalFinsupp (Readable.get b i) + 0 i

case neg.h
ι : Type
inst✝⁹ : LinearOrder ι
α : Type u_1
β : Type u_2
m : Type u_3
γ : Type u_4
inst✝⁸ : Zero α
inst✝⁷ : Zero β
inst✝⁶ : Zero m
inst✝⁵ : AddCommMonoid γ
inst✝⁴ : EvalToFinsupp α γ
inst✝³ : EvalToFinsupp β γ
inst✝² : LawfulOfStream α β γ
inst✝¹ : LawfulModifiable ι β m
s : Stream ι α
inst✝ : IsBounded s
i : ι
q : s.σ
ih :
  ∀ (y : s.σ),
    WfRel s y q →
      ∀ (b : m),
        evalFinsupp (Readable.get (fold_wf Modifiable.update (map OfStream.eval s) y b) i) =
          evalFinsupp (Readable.get b i) + (eval (map (⇑evalFinsupp) s) y) i
b : m
hv : ¬s.valid q = true
⊢ ¬(map (⇑evalFinsupp) s).valid q = true

case neg.h
ι : Type
inst✝⁹ : LinearOrder ι
α : Type u_1
β : Type u_2
m : Type u_3
γ : Type u_4
inst✝⁸ : Zero α
inst✝⁷ : Zero β
inst✝⁶ : Zero m
inst✝⁵ : AddCommMonoid γ
inst✝⁴ : EvalToFinsupp α γ
inst✝³ : EvalToFinsupp β γ
inst✝² : LawfulOfStream α β γ
inst✝¹ : LawfulModifiable ι β m
s : Stream ι α
inst✝ : IsBounded s
i : ι
q : s.σ
ih :
  ∀ (y : s.σ),
    WfRel s y q →
      ∀ (b : m),
        evalFinsupp (Readable.get (fold_wf Modifiable.update (map OfStream.eval s) y b) i) =
          evalFinsupp (Readable.get b i) + (eval (map (⇑evalFinsupp) s) y) i
b : m
hv : ¬s.valid q = true
⊢ ¬(map OfStream.eval s).valid q = true
Theorem: Etch.Verification.Stream.LawfulOfStream.get_fold
Proof state before:
case neg
ι : Type
inst✝⁹ : LinearOrder ι
α : Type u_1
β : Type u_2
m : Type u_3
γ : Type u_4
inst✝⁸ : Zero α
inst✝⁷ : Zero β
inst✝⁶ : Zero m
inst✝⁵ : AddCommMonoid γ
inst✝⁴ : EvalToFinsupp α γ
inst✝³ : EvalToFinsupp β γ
inst✝² : LawfulOfStream α β γ
inst✝¹ : LawfulModifiable ι β m
s : Stream ι α
inst✝ : IsBounded s
i : ι
q : s.σ
ih :
  ∀ (y : s.σ),
    WfRel s y q →
      ∀ (b : m),
        evalFinsupp (Readable.get (fold_wf Modifiable.update (map OfStream.eval s) y b) i) =
          evalFinsupp (Readable.get b i) + (eval (map (⇑evalFinsupp) s) y) i
b : m
hv : ¬s.valid q = true
⊢ evalFinsupp (Readable.get b i) = evalFinsupp (Readable.get b i) + 0 i

case neg.h
ι : Type
inst✝⁹ : LinearOrder ι
α : Type u_1
β : Type u_2
m : Type u_3
γ : Type u_4
inst✝⁸ : Zero α
inst✝⁷ : Zero β
inst✝⁶ : Zero m
inst✝⁵ : AddCommMonoid γ
inst✝⁴ : EvalToFinsupp α γ
inst✝³ : EvalToFinsupp β γ
inst✝² : LawfulOfStream α β γ
inst✝¹ : LawfulModifiable ι β m
s : Stream ι α
inst✝ : IsBounded s
i : ι
q : s.σ
ih :
  ∀ (y : s.σ),
    WfRel s y q →
      ∀ (b : m),
        evalFinsupp (Readable.get (fold_wf Modifiable.update (map OfStream.eval s) y b) i) =
          evalFinsupp (Readable.get b i) + (eval (map (⇑evalFinsupp) s) y) i
b : m
hv : ¬s.valid q = true
⊢ ¬(map (⇑evalFinsupp) s).valid q = true

case neg.h
ι : Type
inst✝⁹ : LinearOrder ι
α : Type u_1
β : Type u_2
m : Type u_3
γ : Type u_4
inst✝⁸ : Zero α
inst✝⁷ : Zero β
inst✝⁶ : Zero m
inst✝⁵ : AddCommMonoid γ
inst✝⁴ : EvalToFinsupp α γ
inst✝³ : EvalToFinsupp β γ
inst✝² : LawfulOfStream α β γ
inst✝¹ : LawfulModifiable ι β m
s : Stream ι α
inst✝ : IsBounded s
i : ι
q : s.σ
ih :
  ∀ (y : s.σ),
    WfRel s y q →
      ∀ (b : m),
        evalFinsupp (Readable.get (fold_wf Modifiable.update (map OfStream.eval s) y b) i) =
          evalFinsupp (Readable.get b i) + (eval (map (⇑evalFinsupp) s) y) i
b : m
hv : ¬s.valid q = true
⊢ ¬(map OfStream.eval s).valid q = true
Tactic:
all_goals (try exact hv)
Proof state after:
case neg
ι : Type
inst✝⁹ : LinearOrder ι
α : Type u_1
β : Type u_2
m : Type u_3
γ : Type u_4
inst✝⁸ : Zero α
inst✝⁷ : Zero β
inst✝⁶ : Zero m
inst✝⁵ : AddCommMonoid γ
inst✝⁴ : EvalToFinsupp α γ
inst✝³ : EvalToFinsupp β γ
inst✝² : LawfulOfStream α β γ
inst✝¹ : LawfulModifiable ι β m
s : Stream ι α
inst✝ : IsBounded s
i : ι
q : s.σ
ih :
  ∀ (y : s.σ),
    WfRel s y q →
      ∀ (b : m),
        evalFinsupp (Readable.get (fold_wf Modifiable.update (map OfStream.eval s) y b) i) =
          evalFinsupp (Readable.get b i) + (eval (map (⇑evalFinsupp) s) y) i
b : m
hv : ¬s.valid q = true
⊢ evalFinsupp (Readable.get b i) = evalFinsupp (Readable.get b i) + 0 i
Theorem: Etch.Verification.Stream.LawfulOfStream.get_fold
Proof state before:
case neg
ι : Type
inst✝⁹ : LinearOrder ι
α : Type u_1
β : Type u_2
m : Type u_3
γ : Type u_4
inst✝⁸ : Zero α
inst✝⁷ : Zero β
inst✝⁶ : Zero m
inst✝⁵ : AddCommMonoid γ
inst✝⁴ : EvalToFinsupp α γ
inst✝³ : EvalToFinsupp β γ
inst✝² : LawfulOfStream α β γ
inst✝¹ : LawfulModifiable ι β m
s : Stream ι α
inst✝ : IsBounded s
i : ι
q : s.σ
ih :
  ∀ (y : s.σ),
    WfRel s y q →
      ∀ (b : m),
        evalFinsupp (Readable.get (fold_wf Modifiable.update (map OfStream.eval s) y b) i) =
          evalFinsupp (Readable.get b i) + (eval (map (⇑evalFinsupp) s) y) i
b : m
hv : ¬s.valid q = true
⊢ evalFinsupp (Readable.get b i) = evalFinsupp (Readable.get b i) + 0 i
Tactic:
simp
Proof state after:
no goals
Theorem: Etch.Verification.Stream.LawfulOfStream.get_fold
Proof state before:
case neg.h
ι : Type
inst✝⁹ : LinearOrder ι
α : Type u_1
β : Type u_2
m : Type u_3
γ : Type u_4
inst✝⁸ : Zero α
inst✝⁷ : Zero β
inst✝⁶ : Zero m
inst✝⁵ : AddCommMonoid γ
inst✝⁴ : EvalToFinsupp α γ
inst✝³ : EvalToFinsupp β γ
inst✝² : LawfulOfStream α β γ
inst✝¹ : LawfulModifiable ι β m
s : Stream ι α
inst✝ : IsBounded s
i : ι
q : s.σ
ih :
  ∀ (y : s.σ),
    WfRel s y q →
      ∀ (b : m),
        evalFinsupp (Readable.get (fold_wf Modifiable.update (map OfStream.eval s) y b) i) =
          evalFinsupp (Readable.get b i) + (eval (map (⇑evalFinsupp) s) y) i
b : m
hv : ¬s.valid q = true
⊢ ¬(map OfStream.eval s).valid q = true
Tactic:
(try exact hv)
Proof state after:
no goals
Theorem: Etch.Verification.Stream.LawfulOfStream.get_fold
Proof state before:
case neg.h
ι : Type
inst✝⁹ : LinearOrder ι
α : Type u_1
β : Type u_2
m : Type u_3
γ : Type u_4
inst✝⁸ : Zero α
inst✝⁷ : Zero β
inst✝⁶ : Zero m
inst✝⁵ : AddCommMonoid γ
inst✝⁴ : EvalToFinsupp α γ
inst✝³ : EvalToFinsupp β γ
inst✝² : LawfulOfStream α β γ
inst✝¹ : LawfulModifiable ι β m
s : Stream ι α
inst✝ : IsBounded s
i : ι
q : s.σ
ih :
  ∀ (y : s.σ),
    WfRel s y q →
      ∀ (b : m),
        evalFinsupp (Readable.get (fold_wf Modifiable.update (map OfStream.eval s) y b) i) =
          evalFinsupp (Readable.get b i) + (eval (map (⇑evalFinsupp) s) y) i
b : m
hv : ¬s.valid q = true
⊢ ¬(map OfStream.eval s).valid q = true
Tactic:
try exact hv
Proof state after:
no goals
Theorem: Etch.Verification.Stream.LawfulOfStream.get_fold
Proof state before:
case neg.h
ι : Type
inst✝⁹ : LinearOrder ι
α : Type u_1
β : Type u_2
m : Type u_3
γ : Type u_4
inst✝⁸ : Zero α
inst✝⁷ : Zero β
inst✝⁶ : Zero m
inst✝⁵ : AddCommMonoid γ
inst✝⁴ : EvalToFinsupp α γ
inst✝³ : EvalToFinsupp β γ
inst✝² : LawfulOfStream α β γ
inst✝¹ : LawfulModifiable ι β m
s : Stream ι α
inst✝ : IsBounded s
i : ι
q : s.σ
ih :
  ∀ (y : s.σ),
    WfRel s y q →
      ∀ (b : m),
        evalFinsupp (Readable.get (fold_wf Modifiable.update (map OfStream.eval s) y b) i) =
          evalFinsupp (Readable.get b i) + (eval (map (⇑evalFinsupp) s) y) i
b : m
hv : ¬s.valid q = true
⊢ ¬(map OfStream.eval s).valid q = true
Tactic:
exact hv
Proof state after:
no goals
Theorem: Finsupp.sumRange_eq_sum
Proof state before:
α : Type u_2
β : Type u_1
γ : Type ?u.8099
inst✝ : AddCommMonoid β
f g : α →₀ β
⊢ sumRange f = sum f fun x v => v
Tactic:
simp [sumRange, mapDomain]
Proof state after:
no goals
Theorem: Finsupp.sumRange_single
Proof state before:
α : Type u_2
β : Type u_1
γ : Type ?u.14307
inst✝ : AddCommMonoid β
f g : α →₀ β
x : α
y : β
⊢ (sumRange fun₀ | x => y) = y
Tactic:
simp [sumRange]
Proof state after:
no goals
Theorem: Finsupp.mapDomain_sumRange
Proof state before:
α : Type u_3
β : Type u_1
γ : Type u_2
inst✝ : AddCommMonoid β
f g : α →₀ β
h : α → γ
⊢ sumRange (mapDomain h f) = sumRange f
Tactic:
simp [sumRange, ← mapDomain_comp]
Proof state after:
no goals
Theorem: Etch.Verification.Stream.lt_iff_of_eq_compare
Proof state before:
ι ι' : Type
inst✝¹ : LinearOrder ι
inst✝ : LinearOrder ι'
a b : ι
c d : ι'
h : compareOfLessAndEq a b = compareOfLessAndEq c d
⊢ a < b ↔ c < d
Tactic:
simp only [compareOfLessAndEq] at h
Proof state after:
ι ι' : Type
inst✝¹ : LinearOrder ι
inst✝ : LinearOrder ι'
a b : ι
c d : ι'
h :
  (if a < b then Ordering.lt else if a = b then Ordering.eq else Ordering.gt) =
    if c < d then Ordering.lt else if c = d then Ordering.eq else Ordering.gt
⊢ a < b ↔ c < d
Theorem: Etch.Verification.Stream.lt_iff_of_eq_compare
Proof state before:
ι ι' : Type
inst✝¹ : LinearOrder ι
inst✝ : LinearOrder ι'
a b : ι
c d : ι'
h :
  (if a < b then Ordering.lt else if a = b then Ordering.eq else Ordering.gt) =
    if c < d then Ordering.lt else if c = d then Ordering.eq else Ordering.gt
⊢ a < b ↔ c < d
Tactic:
split_ifs at h <;> simp [*]
Proof state after:
no goals
Theorem: Etch.Verification.Stream.eq_iff_of_eq_compare
Proof state before:
ι ι' : Type
inst✝¹ : LinearOrder ι
inst✝ : LinearOrder ι'
a b : ι
c d : ι'
h : compareOfLessAndEq a b = compareOfLessAndEq c d
⊢ a = b ↔ c = d
Tactic:
simp only [compareOfLessAndEq] at h
Proof state after:
ι ι' : Type
inst✝¹ : LinearOrder ι
inst✝ : LinearOrder ι'
a b : ι
c d : ι'
h :
  (if a < b then Ordering.lt else if a = b then Ordering.eq else Ordering.gt) =
    if c < d then Ordering.lt else if c = d then Ordering.eq else Ordering.gt
⊢ a = b ↔ c = d
Theorem: Etch.Verification.Stream.eq_iff_of_eq_compare
Proof state before:
ι ι' : Type
inst✝¹ : LinearOrder ι
inst✝ : LinearOrder ι'
a b : ι
c d : ι'
h :
  (if a < b then Ordering.lt else if a = b then Ordering.eq else Ordering.gt) =
    if c < d then Ordering.lt else if c = d then Ordering.eq else Ordering.gt
⊢ a = b ↔ c = d
Tactic:
split_ifs at h with h₁ h₂ <;> aesop
Proof state after:
no goals
Theorem: Etch.Verification.Stream.le_iff_of_eq_compare
Proof state before:
ι ι' : Type
inst✝¹ : LinearOrder ι
inst✝ : LinearOrder ι'
a b : ι
c d : ι'
h : compareOfLessAndEq a b = compareOfLessAndEq c d
⊢ a ≤ b ↔ c ≤ d
Tactic:
simp [le_iff_lt_or_eq, lt_iff_of_eq_compare h, eq_iff_of_eq_compare h]
Proof state after:
no goals
Theorem: Etch.Verification.Stream.gt_iff_of_eq_compare
Proof state before:
ι ι' : Type
inst✝¹ : LinearOrder ι
inst✝ : LinearOrder ι'
a b : ι
c d : ι'
h : compareOfLessAndEq a b = compareOfLessAndEq c d
⊢ b < a ↔ d < c
Tactic:
simpa using (le_iff_of_eq_compare h).not
Proof state after:
no goals
Theorem: Etch.Verification.Stream.IsBounded.imap
Proof 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, ?_⟩
Proof 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
Theorem: Etch.Verification.Stream.IsBounded.imap
Proof 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⟩
Proof 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
Theorem: Etch.Verification.Stream.IsBounded.imap
Proof 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 ?_)
Proof 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
Theorem: Etch.Verification.Stream.IsBounded.imap
Proof 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]
Proof 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)
Theorem: Etch.Verification.Stream.IsBounded.imap
Proof 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
Proof 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)
Theorem: Etch.Verification.Stream.IsBounded.imap
Proof 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)]
Proof state after:
no goals
Theorem: Etch.Verification.Stream.IsMonotonic.imap
Proof state before:
ι ι' : Type
inst✝¹ : LinearOrder ι
inst✝ : LinearOrder ι'
α : Type u_1
s : Stream ι α
hs : IsMonotonic s
f : ι → ι'
g : ι → ι' → ι
hf : Monotone f
⊢ IsMonotonic (imap_general f g s)
Tactic:
rw [Stream.isMonotonic_iff]
Proof state after:
ι ι' : 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 : Lex (ι' × Bool))
    (hq : (imap_general f g s).valid ((imap_general f g s).seek q i) = true),
    (imap_general f g s).index q ≤ (imap_general f g s).index { val := (imap_general f g s).seek q i, property := hq }
Theorem: Etch.Verification.Stream.IsMonotonic.imap
Proof state before:
ι ι' : 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 : Lex (ι' × Bool))
    (hq : (imap_general f g s).valid ((imap_general f g s).seek q i) = true),
    (imap_general f g s).index q ≤ (imap_general f g s).index { val := (imap_general f g s).seek q i, property := hq }
Tactic:
rintro q ⟨i, b⟩ 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 // (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 }