Calculate simple equation

Stream: general

[Oliver Smith]

I am just starting to learn Lean4. I have a simple equation a = b - c + d and I try to calculate the missing variable by giving any other three of the variables.

My code looks like this:

import Mathlib.Data.Real.Basic

structure equation :=
(a b c d : ℤ)
(rule : a = b - c + d)

def example1 : equation :=
{
a := 2
--b := 4
c := 3
d := 1
rule := rfl
}

#eval example1.b
And it does not work. It can calculate only the a variable when commenting it out. And also it can "check" the equation when all the variables are given.

I assume that my code can be totally wrong and the solution requires another approach. Maybe the "rfl" is a wrong choice.

[Martin Dvořák]

My two cents:
(1) #backticks
(2) Lean is not Prolog. Lean is not a computer algebra package either. You can use rfl for some inference when it is like this:

import Mathlib.Data.Real.Basic

structure equation :=
(a b c d : ℤ)
(rule : a = b - c + d)

def example1 : equation :=
{
b := 4
c := 3
d := 1
rule := rfl
}

#eval example1.a

[Winston Yin (尹維晨)]

If you’d like Lean to solve for b, c, or d given the other three variables, you need to define a function to compute each of them. Even in Mathematica, you have to write Solve[…, b], which is now the function that you have to implement in Lean. Then you can #eval that function. Try and see if you can do that.

[Winston Yin (尹維晨)]

And for that, I would just write fun (a : ℤ) (b : ℤ) (c : ℤ) : ℤ := … instead of using the structure you defined.

[Winston Yin (尹維晨)]

(deleted)

[Oliver Smith]

Do you mean to define 4 different functions for every variable a b c d? If yes, then I am actually trying to avoid it.
I want Lean to work by rearranging the function by itself.
After some trial and error, I found that by changing the type to natural numbers and rearranging the formula, Lean can calculate the a and b variables, but not the c and d.

import Mathlib.Data.Real.Basic

structure equation :=
  (a b c d : ℕ)
  (rule : a + c = b + d)

def example1 : equation :=
{
  a := 2
  b := 4
  c := 3
  d := 1
  rule := rfl
}

#eval example1.a

[Oliver Smith]

Winston Yin (尹維晨)

[Martin Dvořák]

Oliver Smith said:

I want Lean to work by rearranging the function by itself.

Lean is not a computer algebra system.

[Martin Dvořák]

Maybe you have some misconception about what Lean is for.
Typical workflow in Lean is this:
(1) You define a function.
(2) You specify what properties you believe the function has.
(3) You write a proof of those properties.
(4) Lean checks that your proof is correct, assuring you that your function indeed has those properties.

[Jason Rute]

@Oliver Smith what is the #xy here? Why do you want this? What are you trying to do?

[Oliver Smith]

Martin Dvořák
Yes, I understand it. But still, even in https://lean-lang.org/theorem_proving_in_lean4/induction_and_recursion.html everyone can find as an example a structural recursion the Fibonacci function:

def fib : Nat → Nat
  | 0   => 1
  | 1   => 1
  | n+2 => fib (n+1) + fib n

example : fib 0 = 1 := rfl
example : fib 1 = 1 := rfl
example : fib (n + 2) = fib (n + 1) + fib n := rfl

example : fib 7 = 21 := rfl

So, let's say, I am trying to get Lean to check that my proof (equation) is correct by finding (calculating) the value.

[Oliver Smith]

Jason Rute said:

Oliver Smith what is the #xy here? Why do you want this? What are you trying to do?

I have different simple geometry formulas (theorems), like a = b + c. And I want Lean to prove them, by giving Lean some of the variables. And the goal is not to write the rearranged formula by myself.

[Alex Meiburg]

So, let's say, I am trying to get Lean to check that my proof (equation) is correct by finding (calculating) the value.

If you had a different equation for Fibonacci numbers, say,

def fasterFib : Nat -> Nat := (GoldenRatio^n – (1-GoldenRatio)^n)/(2*GoldenRatio – 1)

then you would prove this is correct with a statement like

theorem fasterFib_eq_fib (n : Nat) : ∀n, fasterFib n = fib n := by
  sorry -- proof goes here

This doesn't necessarily mean that it's "correct" in the sense of "does what you want", it just means that one implementation fasterFib is equal to another reference implementation, fib, that is just the manifest _definition_ of the Fibonacci numbers. Alternately you could prove things like

theorem fasterFib_has_fibonacci_properties (n : Nat) :
   fasterFib 0 = 1 ∧
   fasterFib 1 = 1 ∧
   ∀n, fasterFib n + fasterFib (n+1) = fasterFib (n+2) := by
 sorry -- proof goes here

[Chris Wong]

Oliver Smith said:

After some trial and error, I found that by changing the type to natural numbers and rearranging the formula, Lean can calculate the a and b variables, but not the c and d.

This is because addition on natural numbers is defined by recursion on the second argument, and Lean cannot see through recursion unless the argument is already fixed. See: docs#Nat.add

I think what @Martin Dvořák said is your best answer here. Lean is for checking your answers, not finding them. If solving equations on numbers is all you need, then perhaps a computer algebra system or SMT solver is what you're looking for.