Lean 4 på svenska

I Mathlib definieras sinus, cosinus och tangens för komplexa tal med hjälp av exponentialfunktioner vilka sedan användas för att definiera motsvarande reella funktioner:

import Mathlib
set_option autoImplicit false
noncomputable section

def complex_sin (z : ℂ) : ℂ := (Complex.exp (-z * Complex.I) - Complex.exp (z * Complex.I)) * Complex.I / 2
def complex_cos (z : ℂ) : ℂ := (Complex.exp (z * Complex.I) + Complex.exp (-z * Complex.I)) / 2
def complex_tan (z : ℂ) : ℂ := complex_sin z / complex_cos z

def real_sin (x : ℝ) : ℝ := (complex_sin x).re
def real_cos (x : ℝ) : ℝ := (complex_cos x).re
def real_tan (x : ℝ) : ℝ := (complex_tan x).re

open Real
example (x : ℝ) : real_sin x = sin x := by rfl
example (x : ℝ) : real_cos x = cos x := by rfl
example (x : ℝ) : real_tan x = tan x := by rfl

Kommandot rfl används för att bevisa att två uttryck är definitionellt lika, det vill säga att de är exakt samma uttryck efter eventuell expansion av definitioner.

Ovan används rfl för att verifiera att de nydefinierade funktionerna real_sin, real_cos och real_tan exakt motsvarar de redan befintliga funktionerna sin, cos och tan i Mathlib för reella tal.

Mathlib hanterar värdena på sinus, cosinus och tangens för standardvinklarna 0, π / 6, π / 4, π / 3 och π / 2:

import Mathlib
set_option autoImplicit false
open Real

-- standardvinklarna för sinus
example : sin (0) = 0 := by simp
example : sin (π / 6) = 1/2 := by simp
example : sin (π / 4) = √2/2 := by simp
example : sin (π / 3) = √3/2 := by simp
example : sin (π / 2) = 1 := by simp

-- standardvinklarna för cosinus
example : cos (0) = 1 := by simp
example : cos (π / 6) = √3/2 := by simp
example : cos (π / 4) = √2/2 := by simp
example : cos (π / 3) = 1/2 := by simp
example : cos (π / 2) = 0 := by simp

-- standardvinklarna för tangens
example : tan (0) = 0 := by simp
example : tan (π / 6) = 1/√3 := by simp
example : tan (π / 4) = 1 := by simp
example : tan (π / 3) = √3 := by simp
-- tan (π / 2) är odefinierat

I ovanstående formaliserade framställning använde vi uttrycket √2/2 istället för det ekvivalenta uttrycket 1/√2. Vi vill istället använda 1/√2 i vårt exempel krävs att vi använder beviset för att √x / x = (√x)⁻¹ vilket i Mathlib benämns Real.sqrt_div_self:

import Mathlib
set_option autoImplicit false
open Real

example : √2/2 = 1/√2 := by
  simp
  exact sqrt_div_self
example : sin (π / 4) = √2/2 := by simp
example : sin (π / 4) = 1/√2 := by
  simp
  exact sqrt_div_self

simp används för att systematiskt förenkla uttryck genom att tillämpa en uppsättning definierade omskrivningsregler som leder till enklare eller mer standardiserade former uttryck.

Notera att omskrivningen √x / x = (√x)⁻¹ inte utförs automatiskt av simp då högerledet inte nödvändigtvis utgör en förenkling av vänsterledet.

Vi kan även observera att Real.sqrt_div_self inte är annoterad med @[simp] i källkoden till Mathlib, och används därmed inte av simp-kommandot.

Mathlib innehåller till ett stort antal trigonometriska samband, varav några av de mest grundläggande återges här:

import Mathlib
set_option autoImplicit false
noncomputable section
open Real

-- Trigonometriska ettan
example (x : ℝ) : (cos x)^2 + (sin x)^2 = 1 := by simp

-- Cosinus är en jämn funktion. Sinus och tangens är udda funktioner.
example (x : ℝ) : sin (-x) = -sin (x) := by simp
example (x : ℝ) : cos (-x) = cos (x) := by simp
example (x : ℝ) : tan (-x) = -tan (x) := by simp

-- Symmetriegenskaper
example (x : ℝ) : sin (x) = sin (π - x) := by simp
example (x : ℝ) : cos (x) = -cos (π - x) := by simp

-- Period
example (x : ℝ) : sin (x + 2 * π) = sin (x) := by simp
example (x : ℝ) : cos (x + 2 * π) = cos (x) := by simp
example (x : ℝ) : tan (x + π) = tan (x) := by exact tan_add_pi x

example : Function.Periodic sin (2 * π) := by simp
example : Function.Periodic cos (2 * π) := by simp
example : Function.Periodic tan (π) := by exact tan_periodic

-- Övrigt
example (x : ℝ) : sin (x + π) = -sin (x) := by simp
example (x : ℝ) : cos (x + π) = -cos (x) := by simp
example (x : ℝ) : sin x = cos (x - π/2) := by exact Eq.symm (cos_sub_pi_div_two x)
example (x : ℝ) : cos x = sin (x + π/2) := by exact Eq.symm (sin_add_pi_div_two x)