Question on `let`

Stream: general

[Peter Pfaffelhuber]

I know that bracketing can be tricky. For let, my working hypotehsis was that let h : α := ... and let (h : α) := ... are the same, but apparently this is not the case. Here is a MWE:

Here, rfl gives an error, saying that q is not definitionally equal to 1...

example : True := by
  let (q : ℕ) := 1
  have hq : q = 1 := by
    rfl
  sorry

...while everything works fine without the brackets...

example : True := by
  let q : ℕ := 1
  have hq : q = 1 := by
    rfl
  sorry

Can someone explain to my why that is?

[Mario Carneiro]

no, the syntax of let/have is like have (name)? (binders)? (: type)? := value, and the name cannot be in parentheses, so when you put parentheses it gets interpreted as a binder. have (x : A) := x is a definition of the identity function named this

[Mario Carneiro]

for let it's slightly more complicated because let doesn't allow the name to be optional (not exactly sure why, it may be on some stage of being changed to be more like have). So it is probably just a syntax error to do let (q : ℕ) := 1?

[Mario Carneiro]

ah, looks like the syntax unification has already happened, let acts the same as have. So let (q : ℕ) := 1 is equivalent to let this (q : ℕ) := 1 or let this := fun (q : ℕ) => 1, it declares a constant function

[Edward van de Meent]

that doesn't seem to be the case, looking at the tactic state after the let?

[Peter Pfaffelhuber]

Ok, I understand this, thanks. However, when I use let (q : ℕ) := 1, the infoveiw in the next line tells me that q : ℕ, so it is not a function. (When I use let q : ℕ := 1, the proof state tells me q : ℕ := 1.)

[Edward van de Meent]

in particular, the effect seems more like refine (fun q => ?a) (1:Nat)

[Peter Pfaffelhuber]

Edward van de Meent schrieb:

in particular, the effect seems more like refine (fun q => ?a) (1:Nat)

That`s right, the proof state looks exactly the same...

[Mario Carneiro]

that seems like a bug then?

[Mario Carneiro]

for have it produces a function, and I think we definitely don't want divergence between them

[Mario Carneiro]

I was wrong, the let this PR has not merged yet. This isn't a parse error, it's interpreted as a pattern matching let

[Mario Carneiro]

but the pattern expression is just a type ascription

[Mario Carneiro]

so it ends up equivalent to have ((q : Nat)) := 1

[Mario Carneiro]

I lied earlier, the syntax of have is not just have (name)? (binders)* (: type)? := value, there is a second form which is have (pattern) (: type)? := value, with no binders and no name allowed

[Mario Carneiro]

and (pattern) here is just term, it accepts any term and rejects anything that doesn't resolve to some constructor expression (more or less)

[Mario Carneiro]

but type ascriptions are allowed in patterns

[Mario Carneiro]

and let (pattern) := value is identical to have (pattern) := value, i.e. it doesn't actually produce a let binding

[Edward van de Meent]

ah right, like how in do-notation you can write let .some a := [0,2].get? 2

[Edward van de Meent]

that makes more sense

[Mario Carneiro]

yes, or let (x, y) := (1, 2)

[Mario Carneiro]

which does not produce let bindings even though people might hope for it