Eq.refl synthesised terms

Stream: new members

[Matthew Pocock]

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]

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]

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]

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]

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

[Kevin Buzzard]

@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]

(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]

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]

set_option trace.Meta.isDefEq in is also useful to see the steps taken in unificación

[Kyle Miller]

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).

1. The elaborator looks at 2 + 3 = 5 and figures out eventually that 2, 3, and 5 are Nats 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.
2. 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.
3. 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).
4. 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.
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.
6. Hence, Eq.refl _ elaborates to @Eq.refl Nat (2 + 3).
7. Elaboration is finished.
8. 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]

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]

This is the Expr right?

[Eric Wieser]

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]

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]

Kevin, yes, that is the Expr. Branching in the visualization happens at each subexpression, with the exception that Expr.apps collect all the nested apps and print them as all branching out of their initial parent.

For instance, you see Nat, HAdd.hAdd and OfNat.ofNatall branching out of the first Eq, whereas really these would be nested arguments to consecutive apps. I find it clearer to interpret like this.

[Kyle Miller]

@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]

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]

In Lean 3 there was extra protection via eta expansion, that effectively prevented add being unfolded anywhere except on numerals

[Kevin Buzzard]

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]

In NNG4 we explicitly break rfl working as a proof of 2+2=4.

[Matthew Pocock]

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]

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

[Kevin Buzzard]

I would do cases on r at any rate

[Yaël Dillies]

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

[Matthew Pocock]

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]

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]

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]

Kevin Buzzard said:

In NNG4 we explicitly break rfl working as a proof of 2+2=4.

how is this done?

[Eric Rodriguez]

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]

@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]

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]

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