Type mismatch while using the `have` syntax.

Stream: new members

[LizBonn]

As far as I know, the syntax have h : p := s; t is equivalent to the expression (fun (h : p) => t) s. So it is reasonable to have the following proof in Lean.

example : (have x : Nat := 1; @rfl Nat x) = (fun x : Nat => @rfl Nat x) 1 :=
  rfl

And the latter one can be used as a proof of 1 = 1.

example : 1 = 1 :=
  (fun x : Nat => @rfl Nat x) 1

However, when I want to use the have syntax to give a proof of 1 = 1, Lean complains.

/-
Error message:
  Type mismatch
    rfl
  has type
    x = x
  but is expected to have type
  1 = 1
-/
example : 1 = 1 :=
  (have x : Nat := 1; @rfl Nat x)

Also, a similar error occurs when using the letFun syntax.

/-
Error message:
  Type mismatch
    rfl
  has type
    x = x
  but is expected to have type
    1 = x
-/
example : 1 = 1 :=
  letFun 1 (fun x : Nat => @rfl Nat x)

Is this a bug? Or is the way that have syntax works different from what I think?

THX in advance.

[suhr]

This works:

example : 1 = 1 :=
  (let x : Nat := 1; @rfl Nat x)

have is opaque, but you are using it in an expression that requires the content of the definition.

[Yan Yablonovskiy 🇺🇦]

As was already stated above , but i was preparing this already:

The have tactic is for adding opaque definitions and hypotheses to the local context of the main goal. The definitions forget their associated value and cannot be unfolded, unlike definitions added by the let

source

In particular

• The have h : t := e is like doing let h : t := e; clear_value h.

[LizBonn]

I understand that when have is used as a tactic. But I'm still a little confused by the this documentation. It says, have x := v; b/letFun v (fun x => b) is equal to (fun x => b) v and the value of x is not accessible to b.

Does this mean one cannot use x to construct the term b? But if so, how is f a dependent function of type (x : α) → β x?

[Damiano Testa]

I think that it means that you cannot use v to construct b.

[Aaron Liu]

this works:

example : 1 = 1 :=
  have +generalize x := 1
  @rfl Nat x

[LizBonn]

That looks good. It seems that the elaboration order matters a lot. Is there any documentation explaining the mechanism for let, have and the elaboration process?