Sunday, June 30, 2024

03 - Symbols, No Numbers

Task

This task is similar to the previous one, but this time there are no numbers involved. The idea is to see Lean prove purely symbolic statements. Because these don't mention specific numbers, they can be more general statements.

Imagine we're given the following facts about the variables x, y, z and c, all of which are real numbers.

$$\begin{align}z&=y^{2}\\&\\y&=x+c\end{align}$$

Our task is to prove

$$z=(x+c)^{2}$$

If true, this statement holds for any values of $x$ and $c$.


Maths

The task is not difficult. Even so, let's try to write out a structured proof.

$$\begin{align}z&=y^{2}&&\text{given fact}\tag{1}\label{3.1}\\y&=x+c&&\text{given fact}\tag{2}\label{3.2}\\&&&\\z&=y^{2}&&\text{using fact }(\ref{3.1})\\&=(x+c)^{2}&&\text{substitution using fact }(\ref{3.2})\tag*{\(\Box\)}\end{align}$$

Let's talk through this proof.

  • We start by listing the two given facts, $z=y^{2}$ and $y=x+c$. 
  • We want to prove something about z, so starting with the first fact about $z$ is a good strategy. This gives us $z=y^{2}$. We'd like express that $y$ in terms of $x$ and $c$, if possible. 
  • The second fact tells us $y=x+c$. We can use it to substitute for the $y$ in $y^{2}$. This gives us $z=(x+c)^{2}$, our objective.

This proof has no numbers, it is entirely symbolic.


Code

Let's look at a Lean program that proves $z=(x+c)^{2}$, given $z=y^{2}$ and $y=x+c$. 


-- 03 - Symbols, No Numbers

import Mathlib.Tactic

example {x y z c: ℝ} (h1 : z = y^2) (h2: y = x + c) : z = (x + c)^2 := by
  calc
    z = y^2 := by rw [h1]
    _ = (x + c)^2 := by rw [h2]

Notice how similar this code is to the code from the previous chapter. We can see in the proof header how we define the variables x, y, z and c as real numbers, list the two hypotheses, and specify the overall proof objective z = (x + c)^2. 

The main body of the proof is also similar. We first establish that z = y^2, justifying it by the first hypothesis h1. Then we say this is the same as (x + c)^2, justifying it with second hypothesis h2. 

That completes the proof, which is one line shorter than the previous one because we don't need to do a numerical calculation.


Exercise

Write a Lean program to prove that $z=x$ given $z=y$ and $y=x$, where $x$ and $y$ are real numbers.


at