## The integers.

Lean has integers inbuilt as part of the core library. You can call them `int`

if you want to be old skool, but if you type `\Z`

(and then hit the space bar) in VS Code or emacs or the lean web editor you should get a nice looking `ℤ`

.

A word of warning before we start — if you just type some number like 3, then Lean will by default assume that it is a natural number, and the natural number 3 is a different 3 to the integer 3 — that’s how type theory works. You can demand the integer 3 by writing `(3:ℤ)`

(the brackets are essential).

Many basic operations on the integers are defined by recursion (which just means induction for definitions — we prove by induction and define by recursion). This means that secretly there is a computer program in the background which is running the show, complete with proofs of its beliefs. One consequence of this is that often to check explicit calculations using the magic words “dec_trivial” (which I think means “this is trivial, by decidability of equality on the integers”). For example

```
theorem easy : (4:ℤ) - (5:ℤ) = (-1:ℤ) := dec_trivial
```

[Just a brief reminder of how these things are thought about in type theory — the idea is that the statement `4-5=-1`

is a type (it also has a type, which is `Prop`

), “easy” is a new Lean term whose type is `4-5=-1`

, and `dec_trivial`

is a computer program which has produced this term. If this still makes your head hurt, forget it.]

In short, “explicit” calculations with integers can

be done using `dec_trivial`

. But what about simple lemmas? How do we prove that addition is commutative on the integers? Well, if you worked through the explicit proof that addition on the natural numbers was commutative, then you could imagine that it’s going to be some sort of delicate proof by induction. But fortunately this has all been done for you by the lean developers, and we can just invoke the theorem in the core lean library to check addition is commutative:

```
example : ∀ a b : ℤ, a + b = b + a := add_comm
```

Indeed there are lots of basic facts about the integers which are inbuilt into Lean — you can see a few more here or (same words, different presentation) here. I wrote that document. Let me know which version you prefer and I will write further such documents using the style you like best. Learning to navigate your way around the library is a very important skill, and one which I say a little more about below when I leave you to work on this stuff on your own.

## Congruences.

Let’s now define what it means for two integers `a`

and `b`

to be congruent mod `m`

. We know exactly what it means though — it just means that `b-a`

is a multiple of `m`

. And what does it mean for `b-a`

to be a multiple of `m`

? It means that there’s some integer `n`

such that `b-a=m*n`

. We know what subtraction and multiplication mean — they are inbuilt into Lean. So we have our definition. Let’s also add some notation for it. You can get the standard `≡`

symbol by typing `\==`

in Lean.

```
namespace xena
definition cong (a b m : ℤ) : Prop := ∃ n : ℤ, b - a = m * n
notation a ` ≡ ` b ` mod ` m := cong a b m
#check (7 ≡ 22 mod 5)
end xena
```

What does that `#check`

mean? Unfortunately it doesn’t mean “check this is true” — it means “check this makes sense, and if it does, return its type”. If you click on the `#check`

(and if you have the messages buffer open — click one of those symbols that looks like some white rectangular blocks in a pile on top of each other if you don’t) you will see `7 ≡ 22 mod 5 : Prop`

. So Lean is telling us that `7 ≡ 22 mod 5`

is a `Prop`

, in other words a true-false statement. It is not telling us whether it’s true or false though! Indeed, if you change the numbers to `#check (7 ≡ 8 mod 5)`

or anything else, Lean will still happily report that it is a true-false statement.

## Proving that congruences are true.

So how do we prove `7 ≡ 22 mod 5`

? Well it looks like some concrete statement involving only known integers, so maybe we can use `dec_trivial`

to prove it.

`example : 7 ≡ 22 mod 5 := dec_trivial -- fails!`

Why does fail when things like subtraction of concrete integers succeeds? It’s because Lean is trying to check that there exists an integer `n`

such that `5 * n`

is `15`

, and this is beyond `dec_trivial`

‘s pay grade. The proof that `7 ≡ 22 mod 5`

needs to read like this: “`n=3`

works, and the proof of this is trivial”. So how do we feed this information into Lean? Well, it turns out we do it like this:

`example : 7 ≡ 22 mod 5 := ⟨3,dec_trivial⟩ -- works!`

The pointy brackets on the right can be typeset with `\<`

and `\>`

. To prove something of the form `∃ n, H`

(“there exists n such that H is true”) we use `⟨n0,proof⟩`

, where `n0`

is our choice for `n`

and `proof`

is our proof that it works. In the case above, `H`

is `22-7=5*3`

and this is exactly the sort of thing that `dec_trivial`

can produce a proof of.

## Proving facts about congruences.

[NB we are going to be writing simple proofs, here, and I would recommend that you have taken a look at at least some of this older post about building the natural numbers before you go much further into this post here.]

We can only use `dec_trivial`

when all the numbers are known. If we have variables then we need to use theorems. Let’s see this in action. Let’s try and prove that for a fixed m, congruence mod m is an equivalence relation. Let’s start with reflexivity. Even here we will find we need a theorem.

## Reflexivity.

Let’s state the theorem.

```
namespace xena
definition cong (a b m : ℤ) : Prop := ∃ n : ℤ, b - a = m * n
notation a ` ≡ ` b ` mod ` m := cong a b m
theorem cong_refl (m : ℤ) : ∀ a : ℤ, a ≡ a mod m :=
begin
end
end xena
```

[or click here to try in the Lean Web Editor]. The begin/end block put us into “tactic mode”, which is by far my favourite lean mode. Our job is to fill in the blank between the begin and the end. Our code currently has an error, saying that we wrote “end” but we hadn’t finished yet (indeed we haven’t started).

We are trying to prove something of the form `for all a, ...`

so we can start with `intro a`

(don’t forget the comma afterwards) and now our goal becomes `a ≡ a mod m`

. Now this is _actually_ notation, and whilst it is what Lean prints, our goal is *actually* the meaning of the notation, which is `cong a a m`

. We can’t unfold notation, but we can

unfold that cong. We don’t have to (indeed when we’re finished try deleting that unfold and notice that the proof still works fine), but let’s do it anyway:

```
theorem cong_refl (m : ℤ) : ∀ a : ℤ, a ≡ a mod m :=
begin
intro a,
unfold cong,
end
```

and if we put the cursor in that gap, we see that our goal is now

`∃ (n : ℤ), a - a = m * n`

, and clearly our next step is going to be to prove this by suggesting that the reason it is true is because `n=0`

works. We saw in “term mode” (i.e. outside a begin/end block) that we could use some pointy brackets, and we could do something fancy-schmancy like `refine ⟨0,_⟩`

in tactic mode, but there’s an explicit tactic which will also work for us — the `existsi`

tactic, which we can use to suggest the value to use in an exists statement. So let’s try

`existsi (0:ℤ),`

for the next line, and our goal now becomes

`a - a = m * 0`

That definitely looks true! But we can’t prove it with `dec_trivial`

because there are variables in it. We need theorems, or automation (i.e. tactics which do heavy lifting). Here’s how to do it using theorems. First we observe that there’s a theorem called `mul_zero`

which says that `x*0=0`

for any `x`

. We can rewrite our goal using that theorem:

`rw [mul_zero]`

[NB what do you think the theorem that says that for all `x`

, `0*x=0`

is called? Can you see why this is a different theorem?]

Now we have to show that any integer, subtract itself, is zero. This theorem is called `sub_self`

, and rewriting again is going to finish the job:

`rw [sub_self]`

If you followed along carefully and remembered all the commas, you now have

```
theorem cong_refl (m : ℤ) : ∀ a : ℤ, a ≡ a mod m :=
begin
intro a,
unfold cong,
existsi (0:ℤ),
rw [mul_zero],
rw [sub_self],
end
```

and no red lines any more, so we’re done.

There is however a nicer way to finish the job after our brilliant idea to set `n=0`

, namely letting automation finish the job. For example

```
theorem cong_refl (m : ℤ) : ∀ a : ℤ, a ≡ a mod m :=
begin
intro a,
unfold cong,
existsi (0:ℤ),
simp
end
```

The simp tactic does all the easy calculations for us. It does use `mul_zero`

to simplify the right hand side, but it doesn’t use `sub_self`

for the left — those that are interested in seeing the lemmas it does use can type `set_option trace.simplify true`

just before the line stating the theorem and then click on the simp line (which should now be underlined in green as it is producing output in the messages terminal now) and take a look at what it actually does.

Here’s everything in the Lean Web Editor.

## Symmetry.

Here’s what we’re after. I would add this after reflexivity if I were you (but before `end xena`

).

```
theorem cong_symm (m : ℤ) : ∀ a b : ℤ, (a ≡ b mod m) → (b ≡ a mod m) :=
begin
end
```

Notation is fickle; I had hoped we could get away without the brackets but we don’t seem to be able to. I guess they do clarify what’s going on.

After `intro`

ing `a`

and `b`

, we can also `intro`

our hypothesis `H : a ≡ b mod m`

. Our hypotheses and goal should now look like this:

```
m a b : ℤ,
H : a ≡ b mod m
⊢ b ≡ a mod m
```

We now have a new problem with `∃`

— instead of wanting to get rid of it in a goal, we want to use the fact that we have one in a hypothesis: we now have an _assumption_ that something exists (remember that `H`

really says `∃ (n : ℤ), b - a = m * n`

as you will be able to see if you type

`unfold cong at H,`

). So how can we use this? Well we need to use a new command — `cases`

.

`cases H with t Ht,`

destroys `H`

and replaces it with an integer `t`

(the integer that exists) and a new hypothesis `Ht`

, the proof that `t`

does what it is supposed to do. At this point our hypotheses and goal looks like this:

```
m a b t : ℤ,
Ht : b - a = m * t
⊢ b ≡ a mod m
```

In particular we now have four integers available to us, namely `m, a, b, t`

, plus the hypothesis that `b-a`

is `m*t`

. Our goal is notation and, unfolding it in our heads (or even using `unfold cong`

we see that it is `∃ (n : ℤ), a - b = m * n`

.

I think I might leave the rest to you.

**Q1** Now comes the maths! We need to write `existsi [something]`

. And once we’ve done that, we need to invoke some theorems. Here’s a useful one — `mul_neg_eq_neg_mul_symm`

. Use `#check mul_neg_eq_neg_mul_symm`

to find out what it does. You are going to be using rewrites and simps. Did you know that you can write `rw ←Ht`

? If you didn’t know that, you might want to do the exercise about the natural numbers before attempting this one.

### Transitivity.

**Q2** Formulate and prove transitivity. Did you ever get stuck? Please let me know where. If you need to find lemmas in the lean libraries I would recommend typing `#check`

and then some useful-looking keywords into Lean, and then hitting ctrl-space (and then escape and then ctrl-space again — I don’t know why but it works better the second time). This link might help you with keywords — make sure you know the difference between `sub`

(a binary operator) and `neg`

(a unary one). Remember also that `A_of_B`

means “B implies A”.

### More.

**Q3** Can you now prove

`theorem cong_is_equiv_reln (m : ℤ) : equivalence (λ a b, cong a b m) := sorry`

?

Can you prove that if `a ≡ b mod m`

and `c ≡ d mod m`

then `a + c ≡ b + d mod m`

? And what about `a * c ≡ b * d mod m`

? Can you prove `a ^ n ≡ b ^ n mod m`

? You might have trouble getting `^`

to work — that is because core lean has been designed with an operator overloading issue which has not yet been fixed yet and might not be fixed for quite some time. Work your way around it with `local infix ` ^ ` := monoid.pow`

at the top of your code [edit: curses! You need to have mathlib for this to work You need to get `import algebra.group_power`

to work as well :-/]. If you can do all of these things, well done!