lean4 newbie

Stream: new members

[Chris B]

There's a theorem absurd : ∀ {a b : Prop}, a → ¬a → b. For decidable equality (like Nat), you can use by decide as in example : ¬1 = 2 := by decide. There are also noConfusion declarations for inductive types, which you might need elsewhere. <type>.noConfusion is the primitive for showing that an inductive type's constructors are injective and disjoint:

example : ¬0 = 1 := fun h => Nat.noConfusion h
-- or just this, but it might be less clear.
example : ¬0 = 1 := Nat.noConfusion

[Chris B]

In the future, you're probably better off posting in the new members stream and not the rss stream.

[Notification Bot]

This topic was moved here from #rss > lean4 newbie by Kyle Miller.

[Shreyas Srinivas]

A question about lean 4 syntax. I'd like to illustrate this with a basic example of a vector.
For starters the following type checks correctly as it should:

inductive Vector (α : Type) : Nat → Type where
  | Empty : Vector α zero
  | Cons : {x : Nat} → α → Vector α x → Vector α (succ x)

When replacing the Nat in the first line with \N, it still typechecks, which makes sense because \N is synonymous with Nat(https://leanprover.github.io/logic_and_proof/the_natural_numbers_and_induction_in_lean.html) (I am aware this isn't specific to lean 4 but I couldn't find anything equivalent)

inductive Vector (α : Type) : ℕ → Type where
  | Empty : Vector α zero
  | Cons : {x : Nat} → α → Vector α x → Vector α (succ x)

However replacing the Nat inside Cons with \N yields a type error

inductive Vector (α : Type) : ℕ → Type where
  | Empty : Vector α zero
  | Cons : {x : ℕ} → α → Vector α x → Vector α (succ x)

The error is

application type mismatch
  succ x
argument
  x
has type
  ℕ : Type
but is expected to have type
  Nat : Type

which must mean \N and Natare not seen as synonymous here. Why is this happening, has something changed in lean 4 and \N and Nat are no longer synonymous? If so, why did the second example type check correctly?

[Chris B]

The ℕ is no longer associated with Nat by default (it still is in Mathlib). The second example doesn't type check for me on milestone 3 so I assume we're using different versions, but I think the rest of what you're seeing is a consequence of the autoImplicit feature and some of the relaxed error reporting around that.

[Chiyoku]

Hi, i'm trying to make a simple mutual recursion but i'm getting an strange error with the assumption tatic. image.png

[Arthur Paulino]

@Chiyoku That doesn't look like a newbie issue. You might want to post it in the #lean4 stream.
Also, please post text using #backticks instead of a screenshot

[chensc]

Hey guys, just some silly question from a completely newbie. Naively, I expect the code

def W : Type := Nat
def n : W := 4

to behave just like

def n : Nat := 4

But it returns error, so I suppose something is wrong regarding my understanding of the Type object.
Can someone explain it?

[Yaël Dillies]

If you do

@[reducible] def W : Type := Nat
def n : W := 4

then yes it will behave almost exactly the same.

[Arthur Paulino]

#backticks
This also works:

abbrev W : Type := Nat
def n : W := 4

[Henrik Böving]

Note that the reason it doesnt work per default is that lean will not per default eagerly unfold the definition of W to see that its actually a Nat, that is what the abbrev/reducible do

[chensc]

Thanks! However,

@[reducible] def W : Type := Nat
#check W.add

still returns an error.

[Henrik Böving]

That's for a different reason. you see Lean is not an object oriented language so the function add is not defined on the type Nat but rather in a namespace named Nat which can (in theory) exist without a type Nat so this wont just magically carry over to W

[Henrik Böving]

You can however:

namespace W

def add : W → W → W := Nat.add

end W

or:

def W.add : W → W → W := Nat.add

[chensc]

I see. So there is an automatic self-identification between the apriori non-connected "Nat" as a type and the namespace "Nat"?

[Henrik Böving]

Yes Lean 4 does have some mechanisms to figure out that a certain function is hidden behind a namespace when called on a type, example:

abbrev W : Type := Nat

def W.add : W → W → W := Nat.add

def foo : W := 2

example : foo.add 12 = W.add foo 12 := by rfl

[chensc]

Another question: if natural numbers are defined inductively in an unary basis, is it the case that expressions like " 5 + 5" are computed like the mathematical definition of natural numbers\ordinal arithmetic? As it would be highly inefficient, I guess there is some distinction between computational arithmetic of LEAN as programing language and mathematical numbers? But is so, then what is the correlation between "5 + 5" and "Nat.add 5 5"?

[Henrik Böving]

5 + 5 is indeed turned into Nat.add 5 5 by means of notation and type class inference, however while the lean implementation would indeed be highly inefficient the compiled version of Lean 4 does rely on a more efficient internal representation of natural numbers which allows them to be computed basically as efficient as integers in languages like python.

[Henrik Böving]

This is indicated by the extern attribute on the implementation here: docs4#Nat.add which points to the C implementation using the efficient internal representation

[chensc]

I see, thank you!

[chensc]

One more question from the TPIL4, regarding the following code:

universe u v

def f (α : Type u) (β : α → Type v) (a : α) (b : β a) : (a : α) × β a :=
⟨a, b⟩

def h1 (x : Nat) : Nat :=
(f Type (fun α => α) Nat x).2

Is the expression "(f Type (fun α => α) Nat x).2" supposed to be the second coordinate of a generalized ordered pair? And if so, why does the equivalent "(f Type (fun α => α) Nat x).1" return error?

[Arthur Paulino]

#backticks will help you format your texts better here on Zulip.
What's the error message?

[chensc]

type mismatch
  (f Type (fun α => α) Nat x).fst
has type
  Type : Type 1
but is expected to have type
  Nat : Type

[Arthur Paulino]

There you go. The code says that h1 should output a term of type Nat. Look: def H1 ... : Nat. But the first coordinate of what f returns is of type Type.

[Arthur Paulino]

You can remove that part that explicitly states the output type of h1 and let Lean infer it. Then you can use #check h1 and you should see the difference between those two alternatives

[chensc]

Cool, thanks a lot!