avoid typing the same thing 7 times without using let

Stream: general

[Kenny Lau]

I've just figured a way to avoid typing the same thing 7 times without using let:

def test : ℕ :=
(λ n, n * n + 2 * n + 1) 123456789

[Reid Barton]

I think have is actually syntax for this

[Kenny Lau]

but have doesn't remember definition

[Kenny Lau]

this is a way to have abbreviations without breaking anything (if you use let, you'll have a hard time working in tactic mode)

[Simon Hudon]

What can you do with this that you can't do with a let?

[Kenny Lau]

you can substitute this easily using beta reduction, which is automatically performed by many tactics

[Kenny Lau]

my personal experience tells me that let is hard to work with

[Kevin Buzzard]

If you use let and then go into tactic mode then sometimes your goals come out really kooky.

[Ryan Lahfa]

Kenny Lau said:

but have doesn't remember definition

set can work too AFAIK

[Kenny Lau]

I'm not abbreviating in the middle of a proof. It's in the definition of some data.

[Kenny Lau]

Simon Hudon said:

What can you do with this that you can't do with a let?

to be more specific:

def test : ℕ :=
(λ n, n * n + 2 * n + 1) 123456789

def test' : ℕ :=
let n := 123456789 in n * n + 2 * n + 1

example : test = 0 := by unfold test    -- ⊢ 123456789 * 123456789 + 2 * 123456789 + 1 = 0
example : test' = 0 := by unfold test'  -- ⊢ (let n : ℕ := 123456789 in n * n + 2 * n + 1) = 0

[Kevin Buzzard]

kooky goal alert

[Kenny Lau]

is "kooky" pronounced the same as "cookie"?

[Kevin Buzzard]

It's pronounced the way cookie monster says cookie.

[Kenny Lau]

but it's almost spelt the same; English is weird

[Reid Barton]

def test'' : ℕ :=
have n : ℕ := 123456789, n * n + 2 * n + 1

example : test'' = 0 := by unfold test''  -- ⊢ 123456789 * 123456789 + 2 * 123456789 + 1 = 0

[Reid Barton]

def test₂ :=
(λ n, (rfl : n = 0)) 0          -- invalid type ascription

def test₂' :=
let n := 0 in (rfl : n = 0)

The lambda "forgets" the definition in the same way that have does.

[Kenny Lau]

wow. when I use the underscore I don't see 123456789:

def test'' : ℕ :=
have n : ℕ := 123456789, _
/-
don't know how to synthesize placeholder
context:
n : ℕ
⊢ ℕ
-/

[Reid Barton]

Inside the body you "don't know" what the value of n is. Outside you do.

[Mario Carneiro]

I can confirm Reid's first comment: have is sugar for this expression. let requires additional magic, but morally it is syntax for the result of substituting the variable, which is why you get the defeq inside the body

[Mario Carneiro]

Fun fact, have inside tactic mode is neither of these, it is actually performing the substitution. So the result contains no redexes at the end:

def test : ℕ :=
by have n := 123456789; exact n * n + 2 * n + 1

#print test -- 123456789 * 123456789 + 2 * 123456789 + 1

[Kevin Buzzard]

What's a redex? This funny (let x = y in z) thing which I sometimes see in goals?

[Mario Carneiro]

redex is a shortening for "reducible expression", and it refers to when there is a piece of the term that can be directly simplified by one of the "greek rules". For example 1 + 2 = (\lam x, x) 3 contains a beta redex, and f = g \circ (\lam x, h x) contains an eta redex

[Mario Carneiro]

a let expression is always a redex (a zeta redex, if you care) because there is a rule that simplifies it to z[y/x]