search

girving / interval

Conservative floating point interval arithmetic in Lean
Apache License 2.0
7 stars 1 forks source link

Missing lemmas for new casts #9

Closed adomasbaliuka closed 3 weeks ago

adomasbaliuka commented 3 weeks ago

Since adding instances for NatCast, IntCast and Coe Rat Interval in #8, the approx tactic has trouble seeing through these conversions. We need lemmas like 

@[approx] lemma mem_approx_natCast (n : ℕ) : (n : ℝ) ∈ approx (n : Interval) := by
  have : approx (n : Interval) = approx (Interval.ofNat n) := by simp [Nat.cast, NatCast.natCast]
  rw [this]
  approx

Probably the proof could be made nicer. Do you want to add such lemmas? If yes, shall they be right below the instances?

girving commented 3 weeks ago

Yes, we should definitely have those @[approx] lemmas.