is there a way to rename a type such as N := Nat

Stream: lean4

[Xiaoning Bian]

is there a way to rename a type such as N := Nat

[Alok Singh]

abbrev? abbrev N := Nat

[Alex J. Best]

Or you can use notation like ℕ as defined in libraries

[Xiaoning Bian]

thanks. 'abbrev' works! I used 'def' before, Lean4 cannot recognize elements of N. Strangely, I roughly went though some doc, but I didn't see any about 'abbrev'. Everyone is using Nat instead of N.

[Xiaoning Bian]

Alex J. Best said:

Or you can use notation like ℕ as defined in libraries

Yes, I mean ℕ. Just don't know how to type it in chat. Thanks.

[Alex J. Best]

My point is that in Mathlib we have a line

notation "ℕ" => Nat

which is probably closer to what you want than abbrev then

[Xiaoning Bian]

Alex J. Best said:

My point is that in Mathlib we have a line

notation "ℕ" => Nat

which is probably closer to what you want than abbrev then

I see. Thanks. I just tried 'notation'. It works.

[Xiaoning Bian]

BTW, in Agda, 'N = Nat' works. '=' in Lean4 is used for equality. '=' in Agda is for any kinds of renaming: N = Nat, f = g, a = 1. the following code works in Agda.

a = 1

M = ℕ
f : M -> M
f zero = a
f (suc x) = x

g = f

So, syntax in Lean4 is a little bit convoluted.

[Mario Carneiro]

The equivalent of N = Nat in lean is def N := Nat

[Mario Carneiro]

it's just not necessarily what you want to do in this instance

[Xiaoning Bian]

Mario Carneiro said:

The equivalent of N = Nat in lean is def N := Nat

For some reason, 'def N := Nat' won't work. I tried that. E.g.

-- These two worked.
-- notation "ℕ" => Nat
--abbrev ℕ := Nat

-- But not this one:
def ℕ := Nat

inductive Ket : ℕ -> Type where
| Ket1 : Bool -> (Ket 1)
| KetS : {n : Nat} -> Ket 1 -> Ket n -> Ket (n + 1)

[Mario Carneiro]

that's because in lean definitions are opaque to typeclass inference (which is a feature, it means you can put different typeclasses on a newtype)

[Mario Carneiro]

I think there is no such distinction in agda

[Xiaoning Bian]

Mario Carneiro said:

that's because in lean definitions are opaque to typeclass inference (which is a feature, it means you can put different typeclasses on a newtype)

1) Agda does not support typeclass (but you can code your own in Agda). It seems that once you use '=' in Agda, then lhs is rhs without any difference(I like it).
2) We can alway wrap a type in a new type if we want this feature in Agda:

data NN : Set where
Wrap : ℕ -> NN

This seems also the only way to make new typeclass instances in Haskell when a type already has such an instance. E.g. I might want a different Show instance for Nat, then I have to wrap Nat in a new type. We can do the same in Lean4.

3)
instance OfNat ℕ n where
ofNat := n

worked, but it's very confusing, since the OfNat definition

class OfNat (α : Type) (_ : Nat) where
ofNat : α

indicates n : Nat, but ofNat := n is of type ℕ . Why sometimes Lean4 reacognizes ℕ is Nat, and sometimes doesn't. Also,

instance OfNat ℕ 0 where
ofNat := 0

won't typecheck. It worked for all n, but why not for an instance 0?

4) I just checked, using 'def N := Nat' won't let you do pattern matching on N. So why are we using and allowing 'def N := Nat'? what's the purpose of 'def N := Nat'? what's the constructor of N?

[Trebor Huang]

Agda supports typeclasses, but during typeclass resolution, the same level of judgemental equality is used as implicit variable resolution.

[Mario Carneiro]

1) Agda does not support typeclass (but you can code your own in Agda). It seems that once you use '=' in Agda, then lhs is rhs without any difference(I like it).

What do you mean by "without any difference"? There are clearly some differences, like the spelling. In lean there are quite a few notions of equality at different levels of strictness and notation, abbrev, def and irreducible_def produce things that are "the same" as their bodies at these different levels of strictness

[Mario Carneiro]

notation produces the strictest level of equality, the LHS is literally expanded to the RHS at parse time. But you certainly don't want to write a whole library development that way, terms would get exponentially large

[Kyle Miller]

@Xiaoning Bian Re 4, yes you can do pattern matching.

def N := Nat
def add : N → N → N
  | m, .zero => m
  | m, .succ n => .succ (add m n)

[Kyle Miller]

Re 2, Haskell's newtype is like Lean's def (though not completely, since Lean's can still unfold), and Haskell's type is like Lean's abbrev. You can also use data in Haskell, or data in Agda, or structure/inductive in Lean to create a completely new type by wrapping.

[Mario Carneiro]

Here's a demonstration of 5 different kinds of equality in lean and the things that differentiate them:

import Mathlib.Tactic.IrreducibleDef
import Mathlib.Logic.Equiv.Basic

notation "T1" => Nat
abbrev T2 := Nat
def T3 := Nat
irreducible_def T4 := Nat
structure T5 := val : Nat

-- syntactic equality means that there is no difference between x0 and x1
def x0 := Nat  #print x0 -- def x0 : Type := T1
def x1 := T1   #print x1 -- def x1 : Type := T1
def x2 := T2   #print x2 -- def x2 : Type := T2
def x3 := T3   #print x3 -- def x3 : Type := T3
def x4 := T4   #print x4 -- def x4 : Type := T4
def x5 := T5   #print x5 -- def x5 : Type := T5

-- reducible equality means that tactics like simp will not differentiate them
example {α} (h : Nat = α) : T1 = α := by simp only [h] -- ok
example {α} (h : Nat = α) : T2 = α := by simp only [h] -- ok
example {α} (h : Nat = α) : T3 = α := by simp only [h] -- failed
example {α} (h : Nat = α) : T4 = α := by simp only [h] -- failed
example {α} (h : Nat = α) : T5 = α := by simp only [h] -- failed

-- definitional equality means that rfl proves the equality
example : T1 = Nat := rfl -- ok
example : T2 = Nat := rfl -- ok
example : T3 = Nat := rfl -- ok
example : T4 = Nat := rfl -- failed
example : T5 = Nat := rfl -- failed

-- propositional equality means that the equality is provable
example : T1 = Nat := rfl -- ok
example : T2 = Nat := rfl -- ok
example : T3 = Nat := rfl -- ok
example : T4 = Nat := T4_def -- ok
example : T5 = Nat := sorry -- not provable

-- equivalence means that the types have the same elements
example : T1 ≃ Nat := .refl _
example : T2 ≃ Nat := .refl _
example : T3 ≃ Nat := .refl _
example : T4 ≃ Nat := T4_def ▸ .refl _
example : T5 ≃ Nat := ⟨T5.val, T5.mk, fun _ => rfl, fun _ => rfl⟩

[Xiaoning Bian]

Trebor Huang said:

Agda supports typeclasses, but during typeclass resolution, the same level of judgemental equality is used as implicit variable resolution.

Thanks for pointing it out. Yeah, you can use "instance argument" to mimic typeclass. I mentioned you can code your own meaning using instance argument. Agda just doesn't have a 'typeclass' keyword as in Haskell, or 'class' as in Lean4. But you have to use the special syntax to open a record in Agda.

[Mario Carneiro]

Xiaoning Bian said:

3)
instance OfNat ℕ n where
ofNat := n

worked, but it's very confusing, since the OfNat definition

class OfNat (α : Type) (_ : Nat) where
ofNat : α

indicates n : Nat, but ofNat := n is of type ℕ .

This works because the types ℕ and Nat are definitionally equal (the rfl test just above). Another place where definitional equality comes up is that if x : A and A and B are definitionally equal then lean accepts x : B.

Why sometimes Lean4 reacognizes ℕ is Nat, and sometimes doesn't. Also,

instance OfNat ℕ 0 where
ofNat := 0

won't typecheck. It worked for all n, but why not for an instance 0?

This is because 0 is type-generic, it uses the OfNat instance to find it and since you are in the middle of defining that instance it of course can't find one yet. You could write show Nat from 0 though to force lean to look for 0 as a Nat, and then assert that it has type ℕ, instead of looking for 0 : ℕ directly which will require the OfNat ℕ 0 instance.

[Mario Carneiro]

4) I just checked, using 'def N := Nat' won't let you do pattern matching on N. So why are we using and allowing 'def N := Nat'? what's the purpose of 'def N := Nat'? what's the constructor of N?

You can do pattern matching on N, you just can't use 0 and +1 because these are generic operators and will cause instance search for OfNat and HAdd respectively, which will fail on the new type (unless you define these, of course). If you use Nat.zero and Nat.succ it will work

[Xiaoning Bian]

Kyle Miller said:

Re 2, Haskell's newtype is like Lean's def (though not completely, since Lean's can still unfold), and Haskell's type is like Lean's abbrev. You can also use data in Haskell, or data in Agda, or structure/inductive in Lean to create a completely new type by wrapping.

Thanks. I didn't know I need put a dot before a constuctor. I come from Agda, there, a dot pattern means a different thing. I am very happy to know "type ~ abbrev". "data = newtype ~ ~ def" is also good to know. Thanks.

[Kyle Miller]

This use of dot means "use the expected type to figure out the namespace for the function". It's able to unfold defs while figuring this out.

Here's an alternative:

def N := Nat

open Nat

def add : N → N → N
  | m, zero => m
  | m, succ n => succ (add m n)

Or you can write Nat.zero and Nat.succ instead of using open Nat.

[Xiaoning Bian]

Mario Carneiro said:

Here's a demonstration of 5 different kinds of equality in lean and the things that differentiate them:

import Mathlib.Tactic.IrreducibleDef
import Mathlib.Logic.Equiv.Basic

notation "T1" => Nat
abbrev T2 := Nat
def T3 := Nat
irreducible_def T4 := Nat
structure T5 := val : Nat

-- syntactic equality means that there is no difference between x0 and x1
def x0 := Nat  #print x0 -- def x0 : Type := T1
def x1 := T1   #print x1 -- def x1 : Type := T1
def x2 := T2   #print x2 -- def x2 : Type := T2
def x3 := T3   #print x3 -- def x3 : Type := T3
def x4 := T4   #print x4 -- def x4 : Type := T4
def x5 := T5   #print x5 -- def x5 : Type := T5

-- reducible equality means that tactics like simp will not differentiate them
example {α} (h : Nat = α) : T1 = α := by simp only [h] -- ok
example {α} (h : Nat = α) : T2 = α := by simp only [h] -- ok
example {α} (h : Nat = α) : T3 = α := by simp only [h] -- failed
example {α} (h : Nat = α) : T4 = α := by simp only [h] -- failed
example {α} (h : Nat = α) : T5 = α := by simp only [h] -- failed

-- definitional equality means that rfl proves the equality
example : T1 = Nat := rfl -- ok
example : T2 = Nat := rfl -- ok
example : T3 = Nat := rfl -- ok
example : T4 = Nat := rfl -- failed
example : T5 = Nat := rfl -- failed

-- propositional equality means that the equality is provable
example : T1 = Nat := rfl -- ok
example : T2 = Nat := rfl -- ok
example : T3 = Nat := rfl -- ok
example : T4 = Nat := T4_def -- ok
example : T5 = Nat := sorry -- not provable

-- equivalence means that the types have the same elements
example : T1 ≃ Nat := .refl _
example : T2 ≃ Nat := .refl _
example : T3 ≃ Nat := .refl _
example : T4 ≃ Nat := T4_def ▸ .refl _
example : T5 ≃ Nat := ⟨T5.val, T5.mk, fun _ => rfl, fun _ => rfl⟩

wow, thanks for the clarification. I didn't know there are so many layers of "equality". Still one thing is strange:

example {α} (h : Nat = α) : T3 = α := by simp only [h] -- failed
example {α} (h : Nat = α) : T3 = α := h -- worked

If seems definitional equality implies reducible equality?

Before, I only vaguely have two kinds of equality: the '=' in Agda is like the syntactic equality here, and '≡' in Agda the definitional equality here. And also the equivalence in both Agda and here.

[Xiaoning Bian]

Mario Carneiro said:

4) I just checked, using 'def N := Nat' won't let you do pattern matching on N. So why are we using and allowing 'def N := Nat'? what's the purpose of 'def N := Nat'? what's the constructor of N?

You can do pattern matching on N, you just can't use 0 and +1 because these are generic operators and will cause instance search for OfNat and HAdd respectively, which will fail on the new type (unless you define these, of course). If you use Nat.zero and Nat.succ it will work

Yeah, it worked. Thanks.

[Xiaoning Bian]

Kyle Miller said:

This use of dot means "use the expected type to figure out the namespace for the function". It's able to unfold defs while figuring this out.

Here's an alternative:

def N := Nat

open Nat

def add : N → N → N
  | m, zero => m
  | m, succ n => succ (add m n)

Or you can write Nat.zero and Nat.succ instead of using open Nat.

"use the expected type to figure out the namespace for the function" <--- Nice!! Thanks.

[Mario Carneiro]

If seems definitional equality implies reducible equality?

Yes, it's also known as reducible defeq for this reason

Before, I only vaguely have two kinds of equality: the '=' in Agda is like the syntactic equality here, and '≡' in Agda the definitional equality here. And also the equivalence in both Agda and here.

Agda = is definitely not syntactic equality, but programming languages which are sufficiently restricted in metaprogramming and similar capabilities can sometimes present a notion of equality that is not observably different from syntactic equality

[Mario Carneiro]

My guess is that agda = is most similar to reducible defeq, in that it is internally actually a different type and it is not eagerly expanded by the compiler, but all parts of the system unfold it on demand so as to treat them as equivalent for all user-visible purposes

[Xiaoning Bian]

Mario Carneiro said:

My guess is that agda = is most similar to reducible defeq, in that it is internally actually a different type and it is not eagerly expanded by the compiler, but all parts of the system unfold it on demand so as to treat them as equivalent for all user-visible purposes

Got it. Thanks. I am more of a user. I come here from Agda for efficency issues. There, a 2^12 case distinction, with each case being an easy computation, takes hours. I am translating my code to Lean4, hoping it works.

[Mario Carneiro]

I don't think lean is that great at gigantic inductive types or case distinctions, but it should not be hours

[Xiaoning Bian]

Thanks a lot for the help, @everyone. I like here! Unlike the SSprove, I filed an issue 3 months ago on github, still wating for an answer.

[Kevin Buzzard]

Re q4: one purpose of allowing def N := Nat is that now I can define my own <= on N, for example I can define a <= b on N to mean a divides b in Nat.

[Xiaoning Bian]

Mario Carneiro said:

If seems definitional equality implies reducible equality?

Yes, it's also known as reducible defeq for this reason

Before, I only vaguely have two kinds of equality: the '=' in Agda is like the syntactic equality here, and '≡' in Agda the definitional equality here. And also the equivalence in both Agda and here.

Agda = is definitely not syntactic equality, but programming languages which are sufficiently restricted in metaprogramming and similar capabilities can sometimes present a notion of equality that is not observably different from syntactic equality

Yeah, '=' is not the syntactic equality. 'pattern a = b' is, for which, you can use 'a' for 'b' if 'b' is a constructor when pattern-matching. We cannot if using '='.

[Mario Carneiro]

in lean that's the @[match_pattern] attribute

[Markus Schmaus]

Mario Carneiro said:

Here's a demonstration of 5 different kinds of equality in lean and the things that differentiate them:

import Mathlib.Tactic.IrreducibleDef
import Mathlib.Logic.Equiv.Basic

notation "T1" => Nat
abbrev T2 := Nat
def T3 := Nat
irreducible_def T4 := Nat
structure T5 := val : Nat

-- syntactic equality means that there is no difference between x0 and x1
def x0 := Nat  #print x0 -- def x0 : Type := T1
def x1 := T1   #print x1 -- def x1 : Type := T1
def x2 := T2   #print x2 -- def x2 : Type := T2
def x3 := T3   #print x3 -- def x3 : Type := T3
def x4 := T4   #print x4 -- def x4 : Type := T4
def x5 := T5   #print x5 -- def x5 : Type := T5

-- reducible equality means that tactics like simp will not differentiate them
example {α} (h : Nat = α) : T1 = α := by simp only [h] -- ok
example {α} (h : Nat = α) : T2 = α := by simp only [h] -- ok
example {α} (h : Nat = α) : T3 = α := by simp only [h] -- failed
example {α} (h : Nat = α) : T4 = α := by simp only [h] -- failed
example {α} (h : Nat = α) : T5 = α := by simp only [h] -- failed

-- definitional equality means that rfl proves the equality
example : T1 = Nat := rfl -- ok
example : T2 = Nat := rfl -- ok
example : T3 = Nat := rfl -- ok
example : T4 = Nat := rfl -- failed
example : T5 = Nat := rfl -- failed

-- propositional equality means that the equality is provable
example : T1 = Nat := rfl -- ok
example : T2 = Nat := rfl -- ok
example : T3 = Nat := rfl -- ok
example : T4 = Nat := T4_def -- ok
example : T5 = Nat := sorry -- not provable

-- equivalence means that the types have the same elements
example : T1 ≃ Nat := .refl _
example : T2 ≃ Nat := .refl _
example : T3 ≃ Nat := .refl _
example : T4 ≃ Nat := T4_def ▸ .refl _
example : T5 ≃ Nat := ⟨T5.val, T5.mk, fun _ => rfl, fun _ => rfl⟩

This deserves to be somewhere (the Lean manual?) where newbies to Lean can easily find it. I'm learning Lean and reading this was super useful, and I only stumbled upon it by browsing some Zulip threads.

[Julian Berman]

Adding them to the glossary as terms seems like a decent idea (as well, not as a replacement)