How to evaluate a function at a given point

Stream: new members

[RedPig]

How to evaluate a function like this ?

theorem evaluate_f_at_1 (f : ℝ → ℝ) (h₀ : ∀ x, f x = x^2 - 2 * Real.sqrt x + 1) : f 1 = 0 := by sorry

Maybe I am wrong but it seems super weird to me that we can not simplify it with one tactic, I can create arbitrary function like say

theorem evaluate_f_at_1 (f : ℝ → ℝ) (h₀ : ∀ x, f x = x^2 - 2 * Real.sqrt (Real.sqrt (Real.sqrt (Real.sqrt x)) )) + 1 : f 1 = 0 := by sorry

then how to evaluate it at 1?

Same apply to complex function

theorem evaluate_f_at_I (f : ℂ → ℂ) (h₀ : ∀ x, f x = x^2024) : f Complex.I = 1 := by sorry

[Kevin Buzzard]

I'm on mobile and hence face a font issue but rw [h0], or whatever the name of that hypothesis is, will replace f with the equation used to define it, and if you think you're now one tactic away from happiness then I think you're confusing a theorem prover with a computer algebra system. I would love it if lean were more like a computer algebra system but the majority of the work in mathlib is pure mathematicians proving new theorems rather than doing eg symbolic manipulation. Note that these are reals, not floats. Sqrt 1 = 1 is a theorem about a currently noncomputable function applied to an infinite precision object. This is different to running a computable Float.sqrt on a computationally well-behaved but theoretically horrible Float type.

Making lean into some kind of symbolic calculator is definitely possible and maybe people will point out tricks which will enable a quick completion here (norm_num might do it, and if not then norm_num plus the hint that sqrt 1 = 1 will surely do it) but in general you shouldn't imagine that lean is able to do what a generic computer algebra system is able to do. Yet.

[Daniel Weber]

The second theorem is false, but you can do:

import Mathlib

theorem evaluate_f_at_1 (f : ℝ → ℝ) (h₀ : ∀ x, f x = x^2 - 2 * Real.sqrt x + 1) : f 1 = 0 := by
  simp [h₀]
  norm_num

theorem evaluate_f_at_1' (f : ℝ → ℝ) (h₀ : ∀ x, f x = x^2 - 2 * Real.sqrt (Real.sqrt (Real.sqrt (Real.sqrt x)) + 1)) : f 1 = 0 := by
  simp [h₀]
  -- ⊢ 1 - 2 * √(1 + 1) = 0, the theorem is false.
  sorry

@[simp] lemma Complex.I_ne_one : (I : ℂ) ≠ 1 := mt (congr_arg im) zero_ne_one.symm

@[simp] lemma Complex.neg_I_ne_one : (-I : ℂ) ≠ 1 := mt (congr_arg im) (by simp)

@[simp]
theorem Complex.orderOf_I_eq_four : orderOf I = 4 := by
  rw [orderOf_eq_iff (by norm_num)]
  simp only [Complex.I_pow_four, ne_eq, true_and]
  intro m hm1 hm2
  interval_cases m <;> norm_num [pow_succ]

theorem evaluate_f_at_I (f : ℂ → ℂ) (h₀ : ∀ x, f x = x^2024) : f Complex.I = 1 := by
  simp [h₀, ← orderOf_dvd_iff_pow_eq_one]
  norm_num

[RedPig]

Daniel Weber said:

@[simp] lemma Complex.I_ne_one : (I : ℂ) ≠ 1 := mt (congr_arg im) zero_ne_one.symm

@[simp] lemma Complex.neg_I_ne_one : (-I : ℂ) ≠ 1 := mt (congr_arg im) (by simp)

I see, this is really helpful, basically simp can do the algebra $\sqrt{1} = 1$ because there is tactics available for it. Like in the case of Complex.I, one need to first prove the order lemma and apply it via simp. However, I am not able to generalize the proof with a slight change
theorem evaluate_f_at_I_2 (f : ℂ → ℂ) (h₀ : ∀ x, f x = x^2025) : f Complex.I = Complex.I := by
This is just because my very limited knowledge of LEAN, which is the struggle for beginners like me

P.S. good catch on thm, there was a mismatch parenthesis, same as above, It is great that simp works for 1 but the question is really how to generalize the proof to a case simp does not work.

theorem evaluate_f_at_1' (f : ℝ → ℝ) (h₀ : ∀ x, f x = x^2 - 2 * Real.sqrt (Real.sqrt (Real.sqrt (Real.sqrt x))) + 1 ) : f (2^16) = 4294967293 := by
  simp [h₀]