# Zulip Chat Archive

## Stream: new members

### Topic: Eq.refl synthesised terms

#### Matthew Pocock (Sep 02 2023 at 15:40):

I'm working through chapter 4 of the Theorem Proving in Lean 4 book. I've reached the part where we use `Eq.refl _`

to mechanically derive some trivial proofs. In the example:

```
example : 2 + 3 = 5 := Eq.refl _
```

My vscode is telling me that the `Eq.refl _`

value is `2 + 3 = 2 + 3`

which presumably means that `_`

was instantiated to `2 + 3`

? I still don't see how that completes the proof, since it's not obviously done anything with `5`

. I have essentially the same question about the other examples.

#### Damiano Testa (Sep 02 2023 at 15:44):

My naive understanding of this is as follows: `Eq.refl _`

tells lean that you are expecting the rhs to be the same as the lhs (note the asymmetry). So, it unifies `_`

with `2 + 3`

and then is left with the goal of showing that `2 + 3`

is the same as `5`

. "Same" here means "they both reduce to the same term", something that now the kernel works on and realizes that it was indeed the case, after all.

#### Ruben Van de Velde (Sep 02 2023 at 15:47):

Basically, naturals are defined in the way of Peano, so on the LHS you get SS0 + SSS0, and the recursive definition of + is unfolded to SSS0 + SS0 and then to SSSS0 + S0 and then SSSSS0 + 0 which is defined in the base case of the recursion to be just SSSSS0 which is exactly the RHS

#### Damiano Testa (Sep 02 2023 at 15:49):

It looks like my answer was the easy part: "get the kernel to check this".

Ruben's answer was: "and the kernel checks it as follows!".

#### Ruben Van de Velde (Sep 02 2023 at 15:51):

And I missed some parentheses: a + Sb is S(a+b), not (Sa)+b

#### Kevin Buzzard (Sep 02 2023 at 15:58):

@Matthew Pocock there are three kinds of equality which you have to understand in order to see why lean does what it does: I write about them here. The natural numbers 2+3 and 5 are definitionally equal (but not syntactically equal). The real numbers 2+3 and 5 are not definitionally equal, but they're propositionally equal. These refined concepts of equality are not mathematical notions, they are all to do with how things are implemented under the hood.

#### Kyle Miller (Sep 02 2023 at 15:58):

(A technicality: the checking is done as-if it's how Ruben described, but the kernel knows about some basic natural number operations, and when it wants to check that `2 + 3`

and `5`

are definitionally equal it'll use fast operations to reduce both sides to `5`

, rather than using the recursive definition of `Nat.add`

. This is new in Lean 4, and Ruben's explanation is how Lean 3 works. I'm not sure how much it's worth knowing this, but it does mean `rfl`

works for natural number arithmetic with bigger numbers than you might expect.)

#### Matthew Pocock (Sep 02 2023 at 16:09):

Thanks everybody. So what I'm getting from this is that if we have the prop+proof `a=b := Eq.refl _`

, this makes `a=b := a=a`

which then causes the kernel to equalify prop.right with proof.right, which could involve some actual work, like arithmetic or running functions.

#### Matthew Ballard (Sep 02 2023 at 16:18):

`set_option trace.Meta.isDefEq in`

is also useful to see the steps taken in unificación

#### Kyle Miller (Sep 02 2023 at 16:25):

Yeah, the fact that typechecking involves doing actual computational work is important to understand.

Here's an outline of the steps that are taken when processing `example : 2 + 3 = 5 := Eq.refl _`

(and skipping some like parsing).

- The elaborator looks at
`2 + 3 = 5`

and figures out eventually that`2`

,`3`

, and`5`

are`Nat`

s and that`+`

is natural number addition. The full expression is close to`@Eq Nat (Nat.add 2 3) 5`

, but if you actually inspect it you'll see`HAdd.hAdd Nat Nat Nat instNatAdd (OfNat.ofNat Nat 2 ...) (OfNat.ofNat Nat 3 ...)`

or something similar. - The elaborator looks at
`Eq.refl _`

with`2 + 3 = 5`

as its expected type. The placeholder (`_`

) becomes a metavariable, call it`?m.1`

, and the implicit argument to`Eq.refl`

becomes a metavariable too, call it`?m.2`

. So far`Eq.refl _`

is`@Eq.refl ?m.2 ?m.1`

. - It computes the inferred type of this, and we have
`@Eq.refl ?m.2 ?m.1 : ?m.1 = ?m.1`

(where that equality is short for`@Eq ?m.2 ?m.1 ?m.1`

). - Since the expected type is
`@Eq Nat (2 + 3) 5`

, it attempts to unify the inferred type with the expected type. This creates the equations`?m.2 ≟ Nat`

,`?m.1 ≟ 2 + 3`

, and`?m.1 ≟ 5`

. Solving them in order, we get`?m.2`

is assigned to be`Nat`

,`?m.1`

is assigned to be`2 + 3`

, and then the last equation is`2 + 3 ≟ 5`

. - Since this isn't just an equation between a metavariable and an expression, we need a defeq (definitional equality) check. The elaborator sees these are natural numbers and then reduces both sides, yielding
`5 ≟ 5`

, which is true by reflexivity, so the check passes. - Hence,
`Eq.refl _`

elaborates to`@Eq.refl Nat (2 + 3)`

. - Elaboration is finished.
- The elaborator now passes
`def _example : @Eq Nat (2 + 3) 5 := @Eq.refl Nat (2 + 3)`

to the kernel for a final check. The kernel follows a similar process when checking that every term has the type it is expected to have, but now there are no metavariables, just definitional equality checks. The kernel also knows about natural number reduction when computing defeq checks.

#### Damiano Testa (Sep 02 2023 at 16:30):

Since I have the tool available, here is what the expression `2 + 3 = 5`

looks like:

```
inspect: '2 + 3 = 5'
'Eq' -- app
|-'Nat' '[]' -- const
|-'HAdd.hAdd' -- app
| |-'Nat' '[]' -- const
| |-'Nat' '[]' -- const
| |-'Nat' '[]' -- const
| |-'instHAdd' -- app
| | |-'Nat' '[]' -- const
| | |-'instAddNat' '[]' -- const
| |-'OfNat.ofNat' -- app
| | |-'Nat' '[]' -- const
| | |-'2' -- lit
| | |-'instOfNatNat' -- app
| | | |-'2' -- lit
| |-'OfNat.ofNat' -- app
| | |-'Nat' '[]' -- const
| | |-'3' -- lit
| | |-'instOfNatNat' -- app
| | | |-'3' -- lit
|-'OfNat.ofNat' -- app
| |-'Nat' '[]' -- const
| |-'5' -- lit
| |-'instOfNatNat' -- app
| | |-'5' -- lit
```

#### Kevin Buzzard (Sep 02 2023 at 16:58):

This is the `Expr`

right?

#### Eric Wieser (Sep 02 2023 at 17:00):

Kevin Buzzard said:

The real numbers 2+3 and 5 are not definitionally equal, but they're propositionally equal.

Interestingly the only reason for this is "we decided to not let the kernel see how `+`

(src) is implemented on real numbers". If it could see that, it would conclude they were definitionally equal after all.

#### Matthew Pocock (Sep 02 2023 at 17:03):

Brill. That's all much clearer now. I was a bit thrown by the Calculational Proofs section of chapter 4, as it uses an existential but appears as the section directly before existentials. I don't know if it would make sense to swap the order of these two?

#### Damiano Testa (Sep 02 2023 at 17:05):

Kevin, yes, that is the `Expr`

. Branching in the visualization happens at each subexpression, with the exception that `Expr.app`

s collect all the nested `app`

s and print them as all branching out of their initial parent.

For instance, you see `Nat`

, `HAdd.hAdd`

and `OfNat.ofNat`

all branching out of the first `Eq`

, whereas really these would be nested arguments to consecutive `app`

s. I find it clearer to interpret like this.

#### Kyle Miller (Sep 02 2023 at 17:13):

@Eric Wieser This is to keep defeq checking from doing unnecessary expensive defeq computations, right? I wonder what it would be like if you could give unification hints that are allowed to break through this abstraction barrier conditionally, for adding `OfNat Real`

expressions. I feel like I saw someone mention a paper about extending a proof assistant that allowed unfolding certain definitions only within certain scopes, but that's all I'm remembering.

#### Eric Wieser (Sep 02 2023 at 17:28):

I think it's partly a performance thing, and partly just a moral thing of "you're not allowed to care about the magic behind the real numbers unless you really ask nicely"

#### Eric Wieser (Sep 02 2023 at 17:29):

In Lean 3 there was extra protection via eta expansion, that effectively prevented `add`

being unfolded anywhere except on numerals

#### Kevin Buzzard (Sep 02 2023 at 17:47):

I think that we should be discouraging `rfl`

proofs for numerals, not considering making them more likely to work. This obsession with `rfl`

proofs is what slowed the area down for decades.

#### Kevin Buzzard (Sep 02 2023 at 17:47):

In NNG4 we explicitly break `rfl`

working as a proof of `2+2=4`

.

#### Matthew Pocock (Sep 02 2023 at 20:03):

I've got stuck on one of the exercises. The case I can't seem to make progress on is:

```
example : (∀ x, p x ∨ r) → (∀ x, p x) ∨ r :=
λ h ↦ sorry
```

My mental block is that to extract `p x ∨ r`

, I need to first introduce `λ a: α`

to apply to h. But having that lambda on the "outside" prevents me exposing `r`

outside of that lambda. The actual exercise uses ↔ in place of → but I've done the proof for the reverse direction.

#### Kevin Buzzard (Sep 02 2023 at 20:25):

Are you allowed to use tactics? I start all my proofs with `by`

.

#### Kevin Buzzard (Sep 02 2023 at 20:27):

I would do cases on r at any rate

#### Yaël Dillies (Sep 02 2023 at 20:40):

Yes, this statement is lot true intuitionistically, so you need some case-split somewhere.

#### Matthew Pocock (Sep 02 2023 at 20:40):

Kevin Buzzard said:

Are you allowed to use tactics? I start all my proofs with

`by`

.

This is in the tutorial before we reach the tactics chapter, so I am expecting that it can be achieved structurally. I've just spotted in the blurb it states "one direction of the second of these requires classical logic", so perhaps I need to try to prove this by contradiction.

#### Ruben Van de Velde (Sep 02 2023 at 20:46):

I think you want a case split on `r`

rather than by contradiction, as Kevin said.

(Also, you should have created a new thread for this)

#### Matthew Pocock (Sep 02 2023 at 20:55):

Ruben Van de Velde said:

I think you want a case split on

`r`

rather than by contradiction, as Kevin said.(Also, you should have created a new thread for this)

Thanks. The byCase function has got me a little further. Sorry - still getting used to how zulip works.

#### Eric Rodriguez (Sep 02 2023 at 23:34):

Kevin Buzzard said:

In NNG4 we explicitly break

`rfl`

working as a proof of`2+2=4`

.

how is this done?

#### Eric Rodriguez (Sep 02 2023 at 23:34):

on the other hand, for the specific case of `Nat`

(/maybe `Int`

), I thought we were using GMP so we _should_ use `rfl`

, no?

#### Kyle Miller (Sep 02 2023 at 23:42):

@Eric Rodriguez I think GMP only means that we *can* not that we *should*. I think you should feel free to rely on defeq for natural number expressions being fast if you want (i.e., if it helps you write maintainable proofs), but I think we should save reliance on GMP for meta code. You can use `by norm_num`

for something less low-level -- it works for more than just `Nat`

/`Int`

, and it knows how to take advantage of Nat rfls.

#### Kyle Miller (Sep 02 2023 at 23:45):

Eric Rodriguez said:

how is this done?

Looks like it's doing `rfl`

at reducible transparency: https://github.com/hhu-adam/NNG4/blob/main/Game/Tactic/Rfl.lean#L22

while also defining a custom `MyNat`

: https://github.com/hhu-adam/NNG4/blob/main/Game/MyNat/Definition.lean#L2

#### Kevin Buzzard (Sep 03 2023 at 08:31):

(I said "we" but the person who did all the dirty work in NNG4 is Jom Eugster, I'm just writing the levels)

Last updated: Dec 20 2023 at 11:08 UTC