syntax

Stream: new members

[Alex Zhang]

I found the following in a file

/-- The transpose of a matrix. -/
def transpose (M : matrix m n α) : matrix n m α
| x y := M y x

What does | mean here?

[Eric Wieser]

https://leanprover.github.io/theorem_proving_in_lean/induction_and_recursion.html#pattern-matching

[Eric Wieser]

Remember thatmatrix n m α is just n → m → α

[Kevin Buzzard]

The definition of addition on the natural numbers uses these pipe symbols to write the two cases X+0 and X+(succ n)

[Alex Zhang]

In

lemma map_add [add_monoid α] [add_monoid β] (f : α →+ β)
  (M N : matrix m n α) : (M + N).map f = M.map f + N.map f :=
by { ext, simp, }

What does the plus sign before β mean in (f : α →+ β)?

[Eric Rodriguez]

an additive morphism, i.e. f 0 = 0 and f a + f b = f (a + b)

[Eric Rodriguez]

there's similarly →* and →+*

[Eric Rodriguez]

and many variations, e.g. a ring equiv is ≃+*

[Alex Zhang]

Thanks a lot!

[Kevin Buzzard]

@Alex Zhang this is bundled morphisms/isomorphisms :-) We worked with unbundled ones for a while but bundled ones work better in most situations because "you can use dot notation".

[Eric Rodriguez]

for the record - this stuff is complicated and confusion is very understandable! even mathlib changes its mind often; the most recent that comes to mind was module bases used to be unbundled, and now they are bundled

[Anne Baanen]

Also, because there are many ways to write the same map f: f \comp id, id \comp f, λ x, f x, ... and it's hard to automatically recognize when is_ring_hom f can apply to a given f' (even if f and f' are "obviously" the same).

[Kevin Buzzard]

(back at a keyboard) @Alex Zhang Here is the advantage of bundled f : α →+ β morphisms. This →+ notation means add_monoid_hom, so really it says f : add_monoid_hom α β (and it's just displayed using the notation to make it easier to read for humans). Any theorem about additive monoid or group homomorphisms, such that f 0 = 0, can be given then name add_monoid_hom.map_zero, and then it can be accessed with f.map_zero easily -- this is how dot notation works. If f were unbundled it would be a function type and you wouldn't be able to pull off this trick. This works because add_monoid_hom is a structure but not a class (you can't have it being a class because given two groups it's completely reasonable to want to consider more than one group hom between them). In contrast, in your other thread, fintype p is a class (because you only need one proof that a type is finite) which means that the term of type fintype p doesn't have a name which users will ever need to worry about (it will be called something like _inst_37) and so you can't pull off the dot notation trick, so unbundled is best.

[Alex Zhang]

universes v w
variables {l m n o : Type*} [fintype l] [fintype m] [fintype n] [fintype o]
variables {α : Type v} {β : Type w}

What are the differences between Type* and Type u and why should we declare l m n o to be in Type* (I am actually not sure whether we should always do this)

[Ruben Van de Velde]

variables {X : Type*}

is (nearly?) equivalent to

universe u
variables {X : Type u}

but less typing

[Kevin Buzzard]

The only difference I can think of is that universe u lets you easily make several variables in the same universe.

[Alex Zhang]

What are the differences between Type and Type u then?
Thanks a lot for all your above answers!

[Huỳnh Trần Khanh]

I just use Type u. I used Type* several times when I was very new to Lean but I found it kind of... not necessary for the kind of things that I usually formalize.

[Eric Wieser]

Type is just short for Type 0

[Eric Wieser]

Note that variables {X Y : Type u} means "put X and Y in the same universe" but {X Y : Type*} means "create a new universe for each". Separate universes are preferred whenever it doesn't make the proofs harder.

[Kevin Buzzard]

When I was teaching Lean to mathematicians earlier this year I just completely ignored universes, and used X : Type for every set/type/whatever your mental model of these things is. Mathlib style is to be "as universe polymorphic as possible", so e.g. if R is a ring and M is an R-module then R is supposed to live in universe u and M in universe v, but in practice if you're just writing maths in code which isn't going into mathlib there's no harm in using Type everywhere. If you know about how to set up maths in set theory, then Type = Type 0 is sets, and Type 1 includes proper classes, and then there are even higher universes containing absurdly mega-infinite things which one hardly ever sees in practice in most normal mathematics, except if one is specifically messing with large objects (e.g. studying large cardinals or whatever)

[Alex Zhang]

Many thanks!

[Alex Zhang]

What is the difference between Type and Sort?

[Eric Wieser]

Roughly speaking Type u = Sort (u+1) but Gabriel will probably remind me there's a max that belongs there somewhere.

[Damiano Testa]

As far as I can tell, Type* is Sort (1 or higher). Type is actually Type 0, while Sort is, I think, Prop. There is a hierarchy

Sort 0 = Prop
Sort 1 = Type 0 = Type
...
Sort (u+1) = Type u -- thanks Eric!

[Eric Wieser]

Use Sort* if you want to include Prop, use Type* if you don't

[Huỳnh Trần Khanh]

Eric Wieser said:

Roughly speaking Type u = Sort (u+1) but Gabriel will probably remind me there's a max that belongs there somewhere.

What? There is a max somewhere?

[Huỳnh Trần Khanh]

Type u abbreviates Sort (u + 1) when u is a universe variable

[Huỳnh Trần Khanh]

The Lean reference says otherwise.

[Eric Wieser]

I remember being told that at some point during lean's development the link between type and sort was changed

[Eric Wieser]

So either I'm misremembering the direction of the flip, or that document predates it

[Eric Wieser]

@Gabriel Ebner, am I imagining you telling me that?

[Gabriel Ebner]

A long long time ago, in a repository far away, it used to be the case that Prop = Type 0. And option had the type Type (max 1 u), which caused all kinds of issues with universe level unification. https://github.com/leanprover/lean/issues/1341
Floris then suggested to use Type u = Sort (u+1) and thereby separate Type from Prop. And the universe level unification issues were again gone from our kingdom.

[Alex Zhang]

This is a piece of code from Theorem Proving in Lean

inductive weekday : Type
| sunday : weekday
| monday : weekday
| tuesday : weekday
| wednesday : weekday
| thursday : weekday
| friday : weekday
| saturday : weekday

namespace weekday

@[reducible]
private def cases_on := @weekday.cases_on

def number_of_day (d : weekday) : nat :=
weekday.cases_on d 1 2 3 4 5 6 7
end weekday

In @[reducible] private def cases_on := @weekday.cases_on, why do we need @ before weekday.cases_on and why does it report an error invalid definition, a declaration named 'weekday.cases_on' has already been declared when private is removed?

[Eric Wieser]

What does #print weekday.cases_on show before and after that line?

[Kevin Buzzard]

Usually def x := @y is used when no @ means that lean has to solve a type class problem with no clues

[Kevin Buzzard]

Obviously the error about having something already defined is because you're trying to define something when it's already been defined. I don't know what private does though.

[Mario Carneiro]

private gives the declaration a weird namespace, so it doesn't clash with the existing one

[Alex Zhang]

Eric Wieser said:

What does #print weekday.cases_on show before and after that line?

Both give

@[reducible]
protected def weekday.cases_on : Π {C : weekday → Sort l} (n : weekday),
  C sunday → C monday → C tuesday → C wednesday → C thursday → C friday → C saturday → C n :=
λ {C : weekday → Sort l} (n : weekday) (e_1 : C sunday) (e_2 : C monday) (e_3 : C tuesday) (e_4 : C wednesday)
(e_5 : C thursday) (e_6 : C friday) (e_7 : C saturday), weekday.rec e_1 e_2 e_3 e_4 e_5 e_6 e_7 n

[Mario Carneiro]

That's the built in weekday.cases_on function

[Mario Carneiro]

not your private alias

[Mario Carneiro]

to refer to the private alias you can use #print cases_on inside the section, and outside the section you can't refer to it

[Eric Wieser]

So in the example above then the private def isn't being used anyway?

[Alex Zhang]

I think cases_on can be used as a shortcut then. I just didn't quite understand the syntax there at the beginning.

[Alex Zhang]

Is there a better (i.e. shorter) way to equivalently write
begin (some tactic), exact ***, end

[Kevin Buzzard]

If the tactic is rw and the *** is a hypothesis then the rwa tactic can be used to do both at once.

[Kevin Buzzard]

If the tactic is simp then you might just be able to add *** to the list which simp optionally accepts

[Kevin Buzzard]

In general your question is probably too broad. If you want something then it would be a cool exercise to write a new tactic which does what you want :-) There are some useful resources on basic tactic writing nowadays (something on the website, Rob Lewis' LFTCM videos)

[Alex Zhang]

Is

@[class]
inductive decidable (p : Prop)
| is_false (h : ¬p) : decidable
| is_true  (h : p) : decidable

equivalent to

class inductive decidable (p : Prop) : Type
| is_false : ¬p → decidable
| is_true  :  p → decidable

?

[Mario Carneiro]

yes

[Alex Zhang]

universe u

structure Semigroup : Type (u+1) :=
(carrier : Type u)
(mul : carrier → carrier → carrier)
(mul_assoc : ∀ a b c : carrier, mul (mul a b) c = mul a (mul b c))


instance Semigroup_to_sort : has_coe_to_sort Semigroup :=
{S := Type u, coe := λ S, S.carrier}

[Alex Zhang]

Will there be any difference if I change the last two lines to

instance Semigroup_to_sort' : has_coe_to_sort Semigroup :=
⟨_, λ S, S.carrier⟩

?

[Johan Commelin]

Nope, it's equivalent.

[Alex Zhang]

variables {M N : matrix m n α}
theorem ext_iff : (∀ i j, M i j = N i j) ↔ M = N :=
⟨λ h, funext $ λ i, funext $ h i, λ h, by simp [h]⟩

What does the dollar sign mean here?

[Huỳnh Trần Khanh]

alright i accept defeat i don't understand $ either

[Damiano Testa]

The $ means "open a parenthesis from here until the end". It is sometimes useful to avoid ending a line with )))).

[Johan Commelin]

In the examply be @Huỳnh Trần Khanh you don't really see the power of $ shine. Here's when $ is helpful:

You have a function f that you can apply to some arguments, and as last argument you want to apply a function application g x y z.
Then you would usually write f 1 2 3 (g x y z). But maybe you don't want to pass z, but instead some function application h a b c, so then you write f 1 2 3 (g x y (h a b c)). But maybe you don't want to pass c, but rather s k l m, so you write

f 1 2 3 (g x y (h a b (s k l m)))

Using $, you can tell Lean "hey, every thing that follows $ should be interpreted as the final argument to the function application left of the $!"

So you can write

f 1 2 3 $ g x y $ h a b $ s k l m

[Alex Zhang]

I don't quite understand the syntax of the defn of simple graphs: what does . obviously mean and what is its function?

structure simple_graph (V : Type u) :=
(adj : V → V → Prop)
(sym : symmetric adj . obviously)
(loopless : irreflexive adj . obviously)

[Patrick Massot]

Did you try the search field on top of https://leanprover-community.github.io/mathlib_docs/?

[Horatiu Cheval]

The syntax x : A . t means "try to synthesize the argument x of type A using tactic t"

[Horatiu Cheval]

So in your case Lean will try to prove symmetric adj by the tactic obviously when you define a simple_graph

[Julian Berman]

It's briefly mentioned here if you want a reference: https://leanprover.github.io/reference/expressions.html#implicit-arguments

[Kevin Buzzard]

Horatiu Cheval said:

So in your case Lean will try to prove symmetric adj by the tactic obviously when you define a simple_graph

(iff you don't provide a proof yourself)

[Kyle Miller]

I think the only use of this so far in the simple graph library is

def complete_graph (V : Type u) : simple_graph V :=
{ adj := ne }

[Alex Zhang]

How can I input other letters like f as a subscript like ₖ?

[Alex Zhang]

\_f gives me ₐf

[Kevin Buzzard]

You can't input all of them, only the ones which unicode allows. To get subscript k you do \_k and if that doesn't work for other letters then it might be literally impossible in the sense that the subscripts are not in the unicode "alphabet" or whatever it's called.

[Kyle Miller]

Here are all of them:

₀₁₂₃₄₅₆₇₈₉₊₋₌₍₎ₐₑₒₓₔₕₖₗₘₙₚₛₜ

You don't see subscript-schwa (xₔ) nearly often enough in math :smile: (Weird, between backticks ₔ shows up as a superscript even though it's a subscript character...)

[Eric Wieser]

That's very strange: "ₔᵊ" appears asₔᵊ, which is a double superscript in my font.

[Taylor Belcher]

I am not sure what the double and single up arrows mean in this code: https://leanprover-community.github.io/mathlib_docs/data/polynomial/field_division.html#polynomial.normalization_monoid Can someone explain?

[Eric Wieser]

You can click on them on the web docs and it will take you to the names that correspond to the notation.

[Alex J. Best]

They are different types of coercions, you can read a bit about this at https://leanprover.github.io/theorem_proving_in_lean/type_classes.html#coercions-using-type-classes.

[Taylor Belcher]

Thank you!

[Alex Zhang]

instance test [semiring α] [decidable_eq I] : semiring (matrix I I α) :=
{ ..matrix.non_unital_semiring, ..matrix.non_assoc_semiring }

Could anyone please explain the syntax in { ..matrix.non_unital_semiring, ..matrix.non_assoc_semiring }?

[Kevin Buzzard]

You are trying to make an instance of a structure here. A structure is an inductive type with only one constructor, namely a list of inputs. There is a lot of syntax sugar available for making structures and you're looking at some of it right now. A semiring structure has a lot of fields, e.g. it has a data field containing a multiplication, and a proof field containing the proof that the multiplication is associative etc etc.

What's happening in your example is that Lean already knows about two structures, namely matrix.non_unital_semiring : non_unital_semiring (matrix I I alpha) and matrix.non_assoc_semiring: non_assoc_semiring (matrix I I alpha). These are also structures which have lots of fields. The .. notation means "take the definition of the fields used in these other structures, and use them as the definition of the fields in this structure". In this case we're lucky and every field which we need is already defined in one of the other structures, so we don't need to do anything else.

[david]

Hi, I wonder if there is some learning resource/tutorial that focuses more on the "lexical/syntax" aspect of lean. A purpose is to grasp the boundaries of the language supported by lean. For example, is there a page that explains the usage of these keyword [#check, def, class, instance, example, meta def, variables, lemma, theorem, #print, ...]. Maybe a similar resource I'm thinking of in the case of python is https://docs.python.org/3/reference/lexical_analysis.html#keywords

[david]

It would also be great if something similar to https://docs.python.org/3/library/functions.html#built-in-funcs exists, if a similar concept applies to lean!

[Horatiu Cheval]

The reference manual is probably what you need

[Horatiu Cheval]

https://leanprover.github.io/reference/

[david]

Thank you! That is exactly what I am looking for!

[Maria]

Hello ! I am a beginner and I would need a little help, unfortunately I can't find it on the net. I want to formalize this problem in lean, but I don't know where I should start and what I should do. Can you give me a little help? For example: what are the stages? image_2021-09-22_103831.png

[Yaël Dillies]

Ahah! You're right on time. We're formalizing many AMC questions at the moment. The way to translate this statement is to ask for the existence of a docs#finset of cardinality the answer whose elements are exactly the solutions to the equation.

[Yaël Dillies]

import data.real.pi.bounds

example :
  ∃ s : finset ℝ, s.card = the_answer ∧
    ∀ x, x ∈ s ↔ 0 ≤ x ∧ x ≤ π ∧ sin (π/2 * cos x) = cos (π/2 * sin x) :=
sorry

[Marcus Rossel]

Here's two more ways you could state it:

import data.finset.basic
import data.real.basic
import analysis.special_functions.trigonometric

open real
notation `π` := real.pi

example : ∀ (s : finset ℝ), (∀ (x : ℝ), x ∈ s ↔ 0 ≤ x ∧ x ≤ π ∧ sin (π/2 * cos x) = cos (π/2 * sin x)) → s.card = the_answer := sorry

example : ∀ (s : finset ℝ), s = {x ∈ s | 0 ≤ x ∧ x ≤ π ∧ sin (π/2 * cos x) = cos (π/2 * sin x)} → s.card = the_answer := sorry

[Eric Wieser]

Isn't that second one false when s = ∅?

[Eric Wieser]

I think you meant {x : ℝ | ...} not {x ∈ s | ...}

[Elias Fåkvam]

Im trying to prove that given a category X and x : X , there exists f: x \hom x. But i cant figure out how to express "there exists f: x \hom x".

Excuse me i was certain i posted this in the syntax thread.

[Kevin Buzzard]

You probably want to ask this question in a more appropriate thread.

[Eric Wieser]

You can edit the thread of your message above