syntactic equality

Stream: general

[Kevin Buzzard]

Notation 0=has_zero.zero -- those are syntactically equal, right? The notation is just something for the parser and pretty printer.

[Chris Hughes]

I think 0 is notation for Nat.zero as well.

[Floris van Doorn]

There are multiple terms (which are syntactically different) that can represent the same numeral. You can see your representation if you use the option set_option pp.numerals false:

set_option pp.numerals false
example : nat.zero = 0 := _ /- not syntactically equal -/

[Floris van Doorn]

I should remark that without changing the option pp.numeralsthe goal is displayed as 0 = 0

[Kevin Buzzard]

gaargh, #print notation 0 is an error because 0 is some sort of numeral. Maybe my question is: is (has_le.le 3 4) = (3 ≤ 4) a syntactic equality?

[Mario Carneiro]

yes, assuming you haven't locally overridden <=

[Mario Carneiro]

and assuming 3 and 4 aren't being represented differently on the two sides, which can happen "in the wild"

[Kevin Buzzard]

example (n : ℕ) : n + nat.zero = n :=
begin
  rw add_zero,
end

example (n : ℕ) : n + has_zero.zero ℕ = n :=
begin
  rw add_zero,
end

I am surprised both of these work.

[Kevin Buzzard]

example (n : ℕ) : n + nat.zero < n :=
begin
  rw add_zero,
  sorry
end

example (n : ℕ) : n + has_zero.zero ℕ < n :=
begin
  rw add_zero,
  sorry
end

Maybe that's a better example of what I mean. I thought rw was picky about syntactic equality. Neither rewrite fails.

[Mario Carneiro]

#check bit1 (nat.succ nat.zero) -- 3
#check bit1 (has_one.one ℕ) -- 3

[Kevin Buzzard]

I understand the numerals point. I'm trying to work out when rewrites work, that's the heart of it.

[Mario Carneiro]

has_zero.zero is reducible

[Kevin Buzzard]

But is has_zero.zero nat syntactically equal to nat.zero?

[Mario Carneiro]

no

[Mario Carneiro]

but it is up to unfolding reducible definitions

[Kevin Buzzard]

So does Lean unfold all reducible definitions before trying to rewrite?

[Mario Carneiro]

I think so

[Kevin Buzzard]

Or does it just internally store them as unfolded?

[Mario Carneiro]

or at least it does something equivalent to that

[Mario Carneiro]

I think it unfolds when necessary in the matching algorithm

[Mario Carneiro]

it's the same as the unification you get from exact except it only unfolds reducible instead of reducible + semireducible

[Kevin Buzzard]

I see. A rewrite attempts to find a subterm of the goal which is "equal" to the lhs of what I'm wanting to rewrite with, and "equal" is somewhere between syntactic and definitional equality.

[Mario Carneiro]

yes

[Mario Carneiro]

yet another equality, I know

[Kevin Buzzard]

class has_scalar (α : Type u) (γ : Type v) := (smul : α → γ → γ)
(from mathlib somewhere). Why is that marked as [reducible]?

[Kevin Buzzard]

I mean

[Kevin Buzzard]

how come has_scalar.smul is reducible?

[Kevin Buzzard]

I don't see anyone adding the tag explicitly

[Kevin Buzzard]

but apparently the system is that notation is reducible

[Kevin Buzzard]

and I can indeed check it's reducible using #print

[Kevin Buzzard]

Are all fields of a class automatically reducible?

[Mario Carneiro]

Hm, I didn't know that. I would guess all fields are reducible by default

[Kevin Buzzard]

If z : complex then is z.re syntactically equal to complex.re z?

[Keeley Hoek]

I'm pretty sure z.re is elaborated into complex.re z before the expression you typed is even "real"

[Keeley Hoek]

something something "projection macro"

[Chris Hughes]

I think it's actually parsed as complex.re z, rather than elaborated.

[Keeley Hoek]

I thought the parser created a projection macro application which said "remember to turn this into a something.re later, you can figure out what something means then too" and that's why if you write nonsense.foo you get a special error in the elaborator "invalid field notation... blah"

[Keeley Hoek]

Indeed, https://github.com/leanprover/lean/blob/ceacfa7445953cbc8860ddabc55407430a9ca5c3/src/frontends/lean/elaborator.cpp#L1921

[Chris Hughes]

You're probably right. I don't know that much about this.

[Chris Hughes]

Incidentally

#eval expr.alpha_eqv `(λ z : ℂ, complex.re z) `(λ z : ℂ, z.re) -- tt

[Chris Hughes]

I'm not sure if alpha_eqv is the same as syntactically equal.

[Kevin Buzzard]

Aah -- if I can test for syntactic equality then I don't need to bug you guys with questions :D

[Keeley Hoek]

Here is that macro in action

[Keeley Hoek]

run_cmd (do tactic.trace ``(nat.a_proj).to_raw_fmt)

[Kevin Buzzard]

I usually avoid talking about different kinds of equality when teaching maths undergrads, but because I'm lecturing a term-long course devoted to Lean I am going to try and tackle it. I realise I don't fully know the definition of syntactic equality. My working definition which I usually tell UGs is "literally the same keypresses in the same order". But I know there are exceptions to this. For example changing the names of bound variables doesn't destroy syntactic equality, and replacing notation by what it's notation doesn't either, I believe (because I think the parser does this before we even get to what the rest of Lean thinks; the parser might also be the reason for the bound variables thing, I have no idea about de Bruijn indices). But I think I just discovered another possibility -- perhaps changing bracket types also doesn't break syntactic equality? I'm not entirely sure how to check this. Here's an attempt, based on the maxim "rw works up to syntactic equality":

def foo : (∀ {x : ℕ}, x = 1) ↔ (∀ (x : ℕ), x = 1) := iff.rfl

example : ∀ {x : ℕ}, x = 1 :=
begin
  rw foo, -- ⊢ ∀ (x : ℕ), x = 1
  rw foo, -- ⊢ ∀ (x : ℕ), x = 1
  rw ← foo, -- ⊢ ∀ {x : ℕ}, x = 1
  rw ← foo, -- ⊢ ∀ {x : ℕ}, x = 1
  sorry,
end

Is there actually a well-defined notion of being syntactically equal or is it a slightly informal notion? If the former, does changing binder types (is that what they're called?) preserve syntactic equality?

I am living in mild fear that when I send this message I'll find a message just above it explaining everything; I couldn't figure out how to efficiently read a thread called syntactic equality other than by posting to it.

[Kevin Buzzard]

Aah great Chris Hughes gave me clues in 2019!

[Kevin Buzzard]

#eval expr.alpha_eqv `(∀ {x : ℕ}, x = 1) `(∀ (x : ℕ), x = 1) -- tt

But the above thread also teaches me that "rw works up to syntactic equality" is not actually true?

[Kevin Buzzard]

#eval expr.alpha_eqv `(@has_zero.zero nat) `(nat.zero) -- ff

gaargh. Is one of "syntactically equal" and "alpha equivalent" strictly stronger than the other? I suspect I was asking about 0 because I was trying to write NNG by the way.

[Rob Lewis]

"literally the same keypresses in the same order" is probably not a good way to phrase this, since these concepts apply to elaborated expressions, not input (pre-) expressions. I would interpret "syntactically equal" as a judgment about the abstract syntax trees of the expressions. Think of an expr as a term of type docs#expr , so a tree of applications of those constructors. Two exprs are equal if they have identical trees. Two exprs are alpha-equivalent if their trees are the same, ignoring name and binder type arguments.

[Rob Lewis]

ignoring name and binder type arguments.

(I think. I actually just tried this out and it seems like binder types are identified by alpha equiv, but that's news to me.)

[Kevin Buzzard]

re the same keypresses -- I need a way to explain it to mathematicians and I'm absolutely not talking about exprs, so this was a good first approximation.

[Kevin Buzzard]

Right -- one of the #evals above seemed to indicate that binder types were identified by alpha equiv assuming that's what alpha_eqv stands for

[Rob Lewis]

Kevin Buzzard said:

#eval expr.alpha_eqv `(@has_zero.zero nat) `(nat.zero) -- ff

gaargh. Is one of "syntactically equal" and "alpha equivalent" strictly stronger than the other? I suspect I was asking about 0 because I was trying to write NNG by the way.

These aren't even definitionally equal -- the first is waiting for an argument of type has_zero nat -- but even with that extra argument they're not alpha equivalent. Different syntax trees, one is an application of has_zero.zero and the other is a constant nat.zero.

[Mario Carneiro]

Kevin Buzzard said:

#eval expr.alpha_eqv `(∀ {x : ℕ}, x = 1) `(∀ (x : ℕ), x = 1) -- tt

But the above thread also teaches me that "rw works up to syntactic equality" is not actually true?

It's not actually true. rw works up to defeq modulo reducible definitions, which, assuming there are no reducible definitions involved, is roughly alpha equivalence

[Mario Carneiro]

Kevin Buzzard said:

#eval expr.alpha_eqv `(@has_zero.zero nat) `(nat.zero) -- ff

gaargh. Is one of "syntactically equal" and "alpha equivalent" strictly stronger than the other? I suspect I was asking about 0 because I was trying to write NNG by the way.

"syntactically equal" is the most equal equal. It is equality at the meta-level, so it implies any other notion of equivalence

[Mario Carneiro]

In meta-lean, it means if you have a : expr and b : expr we're talking about a = b

[Mario Carneiro]

"the same keypresses in the same order" is closer to equality of pre-expressions, a = b where a, b : pexpr. There can be different pre-expressions that produce the same expr after elaboration, which is why "syntactically equal" ignores certain aspects like use of notations. (Amusingly, you can also have the same pre-expression produce two exprs in two different contexts, so there is no implication in either direction here.)

[Mario Carneiro]

def foo (_ : ℕ → ℕ) (_ : ℤ → ℤ) : Prop := false
notation `parse_me_twice` x := foo x x

#check parse_me_twice (λ x, x)
-- foo (λ (x : ℕ), x) (λ (x : ℤ), x) : Prop

[Yaël Dillies]

There is potential for such weird notation!