Float に対するアルゴリズムの性質を証明する方法

Float を含むような広い型クラスを定義しておいて、証明は R に対して行う。

see: https://leanprover.zulipchat.com/#narrow/channel/113489-new-members/topic/Need.20help.20understanding.20ring_nf/near/497758564

import Mathlib

open Filter Set

-- specification over reals
def lagrangeInterpolSpec (n : ℕ) (f : ℝ → ℝ) (x : ℝ) : ℝ := sorry

-- executable program
def lagrangeInterpol {R} [Add R] [Mul R] [Zero R] [One R] (n : ℕ) (f : R → R) (x : R) : R := sorry

-- exacutable program satisfies the spec
theorem lagrangeInterpol_spec (n : ℕ) (f : ℝ → ℝ) (x : ℝ) :
  lagrangeInterpol n f x = lagrangeInterpolSpec n f x := sorry

-- Lagrange interpolating polynom is actually converging to the function under some assumptions
theorem lagrangeInterpolSpec_limit (f : ℝ → ℝ) (hf : ContDiff ℝ ⊤ f) (x : ℝ) :
  ∀ x ∈ Icc 0 1, f x = lim ((⊤ : Filter ℕ).map (lagrangeInterpolSpec · f x)) := sorry

Start with the proposed lagrangeInterpol, lagrangeInterpolSpec, lagrangeInterpol_spec, and lagrangeInterpolSpec_limit declarations in the issue, then read the linked Zulip discussion about ring_nf. Done means documenting a decided, workable approach for relating the broad executable type to the real-number specification and proving the stated properties.