the quest to fully understand lean

Stream: new members

[Levi]

Hey everyone. I am a math student with a bit of computer science (generally imperative programming languages, just a little bit of functional programming) background trying to learn lean. So far I have tried reading mathematics in lean, as well as theorem proving in lean. However in both of those books at some point I have encountered examples that I simply could not understand or get ahold of. And I just wanted to ask what is the best way of dealing with this type of problem?
Should I just put more time into reading and understanding / trying or perhaps are there more "beginner" friendly ressources, or should I just ask in communities like here?
(I hope this is the correct channel to ask :) )

[Riccardo Brasca]

Mathematics in Lean should be understandable, with very little prerequisites (but you have to read it carefully step by step). Can you point out the example you don't understand?

[Riccardo Brasca]

Otherwise you can try the natural number game, that is perfect for people not knowing anything about Lean

[Levi]

I was currently reading Theorem Proving in Lean, but I will switch back to mathematics in Lean and get back here when I encounter what I mentioned earlier. I myself can't remember what it was that set me so off.

[Levi]

Btw is there a PDF version of the up to date Theorem Proving in Lean? I seem to be only finding an old pdf version. Because I am kind of interested in the logic behind how Lean works. Right now I got a basic grasp of Lean, in a sense of like I can use tactics and all to achieve basic goals, but in some examples I feel like I don't understand Lean itself enough to fully comprehend why a certain proof works.

[Aaron Liu]

of course, you can ask questions on Zulip

[Levi]

Aaron Liu said:

of course, you can ask questions on Zulip

but is this the right "channel"? (I've never used Zulip before) :sweat_smile:

[Kenny Lau]

yes

[Levi]

ok great. I already got my first question.
So I'm starting at the very beginning the type theory. Why is it that Nat.succ has type Nat.succ(n : Nat) : Nat as I kind of expected it to be a function with type Nat -> Nat

[Aaron Liu]

if you #check Nat.succ then #check has special support for checking constants so it can show you the signature in a pretty way

[Aaron Liu]

if you #check (Nat.succ) then (Nat.succ) isn't syntactically a constant anymore (it's a parenthesized term) so it bypasses this special support and you get Nat.succ : Nat → Nat

[Levi]

ohhh, yeah I see it now. Thanks!

[Levi]

That's kind of what I mean, when I was talking about those two books, I feel like they presume a certain extend of knowledge about Lean before they can be worked really through from beginning to end. (Not to complain though, so far they have been great generally)

[Kenny Lau]

@Levi the best way to complement a book is to ask question here with fully working code (see #mwe)

[Kenny Lau]

e.g. if you review the question you just asked, you didn't include the code where you checked the type of Nat.succ, so it was impossible to guess that you accidentally included brackets

[Levi]

Kenny Lau said:

e.g. if you review the question you just asked, you didn't include the code where you checked the type of Nat.succ, so it was impossible to guess that you accidentally included brackets

ah i understand. Yeah, my bad. Will keep in mind :thumbs_up:

[Riccardo Brasca]

Anyway the type of Nat.succ is ℕ → ℕ as you expect. It's like saying the function $\sin$ or the function $\sin(x)$.

[Levi]

I am now tackling the core of the dependent type theory and the primary example in the book is the type list. However I am asking myself whether this compose function would also be an example of an dependant type, as it's type depends on it's arguments

def compose (α β γ : Type) (g : β → γ) (f : α → β) (x : α) : γ :=
  g (f x)

although (I hope I understood that correctly) in this case the return type of this function is one of it's argument, whereas the type of the List would be of the same type as it's argument's type.

[Kenny Lau]

@Levi compose is a term, not a type

[Kenny Lau]

but i think the type of compose is a dependent type

[Kenny Lau]

the type of g, f, x, and the return type γ depend on the first three arguments

[Kevin Buzzard]

compose is a lambda-term (a function); its type is a Pi-type (a big collection of functions).

[Kevin Buzzard]

import Mathlib.Init

def compose (α β γ : Type) (g : β → γ) (f : α → β) (x : α) : γ :=
  g (f x)

#print compose
/-
def compose : (α β γ : Type) → (β → γ) → (α → β) → α → γ :=
fun α β γ g f x ↦ g (f x)

compose : Type-of-compose :=
definition-of-compose

-/

[Kevin Buzzard]

fun is what Lean 4 calls what most functional languages call lambda, and (X : Type) -> Y is what some people call \Pi X, Y.

[Levi]

Oh, I see. It makes more sense that compose is a term. Thanks

[Levi]

Just a question out of curiosity, in the book (Theorem Proving in Lean Chapter 3) it says that if p : Prop and t1 t2: p (fixed typo) then t1 and t2 are definitially equal (makes sense :thumbs_up: ), but then it says "... much the same way as it treat (fun x => t) s and t[s/x] as definitionally equal."

What does t[s/x] mean, is it some sort of sugarcoat for replace all occurrences of x with s in term t? I have never seen an expression of this type before (in this book and in general).

[Aaron Liu]

that means "t with s for x", so you substitute all the occurrences of x in t to s

[Kevin Buzzard]

Typo : t1 t2 : p

[Kenny Lau]

Levi said:

I have never seen an expression of this type before (in this book and in general).

it's used in the field of mathematical logic

[suhr]

If you want to dive more deeply into typed lambda calculus, you can consult https://home.ttic.edu/~dreyer/course/papers/barendregt.pdf.

It uses a different notation for substitution though (t[x := s]).

[suhr]

Look at λPω.

[Levi]

Probably a stupid question, but I haven't been able to find any good explanation from a quick search. What is the difference between Nat and \N. The current project that I am in does not use Mathlib. I understand that \N is just sugar-coating for Nat, but without Mathlib it seems that \N is not recognized. Why is that?

[Riccardo Brasca]

ℕ is defined in Mathlib/Data/Nat/Notation.lean, so if you don't import that file you don't have the symbol available.

[Levi]

I see. But it is technically no different to Nat right?

[Riccardo Brasca]

Exactly, the full code is

@[inherit_doc] notation "ℕ" => Nat

so ℕ and Nat are the same thing.

[Levi]

Ah perfect. Thank you :thumbs_up:

[Riccardo Brasca]

If you use VS Code you can right click on the symbol and then "go to declaration" to see the definition

[Levi]

Hey I am back. For some reason I struggle to understand hwo to use the suffice construct as an alternative to have. I fully understand how the have construct works. But from the example given in the book:

variable (p q : Prop)

example (h : p ∧ q) : q ∧ p :=
  have hp : p := h.left
  suffices hq : q from And.intro hq hp
  And.right h

I do not fully understand how suffices works. Is it always couples with from? I played a bit around and whenever I leave the from part out it shows me some error, and I have not been able to get it running with another expression. The book does not really goes into detail on that

[Aaron Liu]

What have you tried?

[Levi]

Well, from how I understood the text, suffices assumes that hq : q is true and continues to go on to prove the initial statement. Then after that is done, it goes back to proving that hq : q is true.
So I sort of assumed that it should have worked without from and it did not. After that I tried using := but then I realized that that wouldn't make any sense, as it would be the same as using have.

So, I am just generally curious what the syntax for suffices is and what advantages it has compared to have. Because as I see it, it just leaves less space for the "main" proof, isn't it?

[Aaron Liu]

I guess you can look at src#Lean.Parser.Term.suffices

[Kevin Buzzard]

I'm not sure that that is a helpful comment for a beginner (in the sense that I'm not a beginner and I definitely can't look at that and make any sense of it). I believe that suffices ... by <tactic sequence> also works.

[Levi]

Kevin Buzzard said:

I'm not sure that this is a helpful comment for a beginner. I believe that suffices ... by <tactic sequence> also works.

ah i see. Yeah that seems to work. But this puts it into tactic mode, correct?

Yeah, @Aaron Liu I tried to follow that link, however it leads to a source file of lean on github. I do have a bit of programming background, but honestly to me that looked all like gibberish :sweat_smile: , couldn't really understand what was going on there. Nonetheless thanks for your help and the faith you've put into me :D

[Kevin Buzzard]

Levi said:

But this puts it into tactic mode, correct?

Yeah. from drops you into term mode, and by into tactic mode, and in both cases you have what you claim suffices as a hypothesis and the old goal as a goal. And then when you've closed that you have a new goal where you have to prove what you claimed sufficed.

[Levi]

Kevin Buzzard said:

Levi said:

But this puts it into tactic mode, correct?

Yeah. from drops you into term mode, and by into tactic mode, and in both cases you have what you claim suffices as a hypothesis and the old goal as a goal. And then when you've closed that you have a new goal where you have to prove what you claimed sufficed.

Wonderful! I don't know why, but somehow this explanation just clicks in my head. Thanks a lot!

[Aaron Liu]

I tried to find something in the Lean Language Reference but either it's not there or my searching skills aren't good enough

[Levi]

Aaron Liu said:

I tried to find something in the Lean Language Reference but either it's not there or my searching skills aren't good enough

I didn't want to come over as stupid ;-), so I also tried to search before I asked, but I just couldn't find anything that explains it in a decent way.

[Kevin Buzzard]

The way to understand what suffices does is to use it correctly once and then hover over it and read the docstring. This should hopefully tell you everything you need to know; you don't need to read the parser or guess.

[Michael Rothgang]

The mathlib manual has a section all tactics, and suffices is documented there: https://leanprover-community.github.io/mathlib-manual/html-multi/Tactics/All-tactics/#suffices-next

[Michael Rothgang]

Given a main goal ctx ⊢ t, suffices h : t' from e replaces the main goal with ctx ⊢ t', e must have type t in the context ctx, h : t'.

The variant suffices h : t' by tac is a shorthand for suffices h : t' from by tac. If h : is omitted, the name this is used.

[Aaron Liu]

technically that's a different piece of syntax

[Michael Rothgang]

Does that answer your question?

[Kenny Lau]

Levi said:

So, I am just generally curious what the syntax for suffices is

this information is usually included in the docstring of suffices i.e. when you hover over it

[Ruben Van de Velde]

But before hover works, you need to have some (sufficiently?) valid syntax first, no?

[Damiano Testa]

It turns out that you only need a very crude valid syntax in this case:

import Mathlib

#find_syntax "suffices"  -- hover in the infoview!

[Levi]

I just read about the "bullet" notation for structuring tactic proofs. However I have to honestly say, that I do not understand what this notation is trying to achieve. Is it merely to the indentation?

[Kenny Lau]

yes, and indentation is real (as in it is part of the syntax, and lean will complain if you don't correctly indent)

[Kenny Lau]

the main point is that sometimes you get 3 goals, the bullet notation is to use one bullet to close one goal

[Levi]

ah i see. I should have tested it. I just kinda assumed you could just indent it however you want

[Levi]

What is the most intuitive way of explaining the apply tactic? It takes (what does it even take? functions?) something, let's call it a and checks whether this a's type matches the current goal, then puts all the hypothesis / arguments of a as subgoals?

[Aaron Liu]

it takes a term

[Aaron Liu]

it figures out how many arguments to add to a to make its type match the goal

[Aaron Liu]

and it closes the goal with that and makes one new goal for each argument added

[Levi]

:thumbs_up: alright got it. Isn't everything a term?

[Aaron Liu]

everything you can feed to exact is a term

[Aaron Liu]

everything you can #check is a term

[Levi]

btw does the intro command do anything interesting. Or given

example (\a  \b : Type) : \a \to \b := by
    intro a
    /- ... -/

this type of situation, intro just gives you a variable of type \a

oh god, lemme fix this. What is going on :(
I give it up, D: but i hope its clear what i mean :D

[Kenny Lau]

@Levi the most basic function of apply is this:

example {P Q : Prop} (h : P → Q) (hp : P) : Q := by
  -- the goal is `⊢ Q`, i.e. we need to prove `Q`
  -- we know that `P` implies `Q` (that's what `h` says)
  -- so if we apply `h`, then it will suffice to prove `P`
  apply h
  -- goal is now `⊢ P`
  exact hp

[Kenny Lau]

Levi said:

btw does the intro command do anything interesting

it introduces a variable based on either -> or forall, it's mathematically equivalent to "let n be arbitrary" or "suppose p is true" in the two cases anti-respectively

[Kenny Lau]

the easiest way to learn how they work is just to observe how the goal changes and try to understand that logically

[Kenny Lau]

example : ∀ n : Nat, n = n := by
  -- let `n` be an arbitrary `Nat`
  intro n
  -- goal is now `⊢ n = n`

example {P Q : Prop} : P → Q := by
  -- suppose `P` is true
  intro hp
  -- goal is now `⊢ Q`

[Levi]

hmmm, does this ⊢ symbol have any special meaning? Or is it equivalent to suppose ...

[Kenny Lau]

no, it means "you need to prove ..."

[Levi]

And on another thought, I thought that forall was just another way of writing ->?

[Levi]

Kenny Lau said:

no, it means "you need to prove ..."

oh of course, yeah i see it now. stupid me...

[Kenny Lau]

Levi said:

And on another thought, I thought that forall was just another way of writing ->?

correct, which is why intro works for both

[Levi]

Kenny Lau said:

Levi said:

And on another thought, I thought that forall was just another way of writing ->?

correct, which is why intro works for both

ok nice! finally something i got right. Thank you so much for your patience :D

[Levi]

If I use intros then it will create anonymous hypothesis which I can not access via any names right? I am kinda questioning in what scenario this would be helpful

[Eric Paul]

Here is an example:

example (a b : Nat) : a = b → ¬a = b → 1 = 2 := by
  intros
  contradiction

The contradiction tactic looks for any contradictions between your local hypotheses, regardless of whether or not they have accessible names. If you comment out the intros line then it fails because there are no local hypotheses. It's convenient in this situation to not have to give things names if we're never going to use them

[Levi]

Perhaps a weird question, but is there any way in vscode to "autocomplete" types. Like in this example

example : ¬ (p ∧ ¬p) :=
  fun (hpnp: p ∧ ¬p) =>
    have hp: p := hpnp.left
    have hnp: ¬p := hpnp.right
    hnp hp

I would like to leave the type of hpnp out and have the editor auto fill it itself. I know that this question is not really lean related, as it is a vscode thing, but perhaps someone has encountered something that works?
(PS: I know that you can hover over it to see the type that lean expects the variable to have, however it would be great for the workflow if there was some way of automating this, as it is always nicer to directly see the type written out on the screen rather than guessing, or having to hover over it every time)

when I mean auto complete, I mean something like this
image.png
where the implicit arguemnt {p} is displayed

[Riccardo Brasca]

You can just write fun hpnp => ...

[Riccardo Brasca]

Or do you really want to see it?

[Levi]

yeah, i know that you could leave out the type. And in this example it is kind of obvious what the type would be, but in general i was thinking that having the type displayed would be good. Especially if the type is some complex term

[Riccardo Brasca]

You write fun hpnp => and you hoover with the cursor over hpnp you will see it's type, not sure if this helps.

[Levi]

Riccardo Brasca said:

You write fun hpnp => and you hoover with the cursor over hpnp you will see it's type, not sure if this helps.

ah yes, this would work, but is there no way of having it displayed in line?

[Riccardo Brasca]

And in tactic mode of course you see it in the infoview.

[Levi]

ah right, yeah nevermind then, i forgot about tactic mode.

[Kenny Lau]

what if we write a macro type? and then you would type fun hpnp : type? => and then it will generate an action message containing the elaborated type

[Kenny Lau]

or even better, call it _?

[Aaron Liu]

it'd have to delay the showing somehow

[Kenny Lau]

i mean _ already exists and it does show the inferred type in its hover

[Aaron Liu]

but if you put it inline then

[Aaron Liu]

I guess it could be a code action

[Aaron Liu]

yeah that makes sense

[Levi]

Kenny Lau said:

what if we write a macro type? and then you would type fun hpnp : type? => and then it will generate an action message containing the elaborated type

hmm, yeah nice idea. But I don't know if I am skilled enough :D

[Levi]

But I will look into it once I have time (and the skill).

[Levi]

Another question though. Is there any difference between repeat intro and intros

[Kenny Lau]

@Levi if you write code you can hover over stuff to get info

image.png

[Kenny Lau]

@Levi and if you want more stuff behind the scenes, intros calls MVarId.intros, and it calculates the number of intros via getIntrosSize, which operates purely on the level of expressions without doing any definitional unfolding, as you can see from the definition:

image.png

it just does the very simple stuff of "I see forall, I increase the count by 1"

[Aaron Liu]

this took so long

import Lean

open Lean CodeAction Server RequestM

@[hole_code_action]
def fillHoleCodeAction : HoleCodeAction := fun _ _ contextInfo termInfo => do
  let doc ← readDoc
  let eager : Lsp.CodeAction := {
    title := "Replace hole with inferred value"
  }
  pure #[{
    eager
    lazy? := some do
      let some start := termInfo.stx.getPos? true | return eager
      let some tail := termInfo.stx.getTailPos? true | return eager
      let map := doc.meta.text
      let (indent, column) := Meta.Tactic.TryThis.getIndentAndColumn map ⟨start, tail⟩
      let newText ← termInfo.runMetaM contextInfo do
        let expr ← instantiateMVars termInfo.expr
        let term ← PrettyPrinter.delab expr
        let format ← PrettyPrinter.ppTerm term
        return format.pretty (indent := indent) (column := column)
      pure { eager with
        edit? := some <| .ofTextEdit doc.versionedIdentifier {
          range := map.utf8RangeToLspRange ⟨start, tail⟩
          newText
        }
      }
  }]

example : ¬ (p ∧ ¬p) :=
  fun hpnp : _ =>
    have hp: p := hpnp.left
    have hnp: ¬p := hpnp.right
    hnp hp

[Aaron Liu]

now to figure out how to get it to not fire when the value can't be inferred

[Levi]

Kenny Lau said:

Levi and if you want more stuff behind the scenes, intros calls MVarId.intros, and it calculates the number of intros via getIntrosSize, which operates purely on the level of expressions without doing any definitional unfolding, as you can see from the definition:

image.png

it just does the very simple stuff of "I see forall, I increase the count by 1"

oh i see! very interesting. And sorry if I am asking stupid questions.

[Levi]

Aaron Liu said:

this took so long

import Lean

open Lean CodeAction Server RequestM

@[hole_code_action]
def fillHoleCodeAction : HoleCodeAction := fun _ _ contextInfo termInfo => do
  let doc ← readDoc
  let eager : Lsp.CodeAction := {
    title := "Replace hole with inferred value"
  }
  pure #[{
    eager
    lazy? := some do
      let some start := termInfo.stx.getPos? true | return eager
      let some tail := termInfo.stx.getTailPos? true | return eager
      let map := doc.meta.text
      let (indent, column) := Meta.Tactic.TryThis.getIndentAndColumn map ⟨start, tail⟩
      let newText ← termInfo.runMetaM contextInfo do
        let expr ← instantiateMVars termInfo.expr
        let term ← PrettyPrinter.delab expr
        let format ← PrettyPrinter.ppTerm term
        return format.pretty (indent := indent) (column := column)
      pure { eager with
        edit? := some <| .ofTextEdit doc.versionedIdentifier {
          range := map.utf8RangeToLspRange ⟨start, tail⟩
          newText
        }
      }
  }]

example : ¬ (p ∧ ¬p) :=
  fun hpnp : _ =>
    have hp: p := hpnp.left
    have hnp: ¬p := hpnp.right
    hnp hp

I stupidly straightfoward copied the code, but it does not seem to autofill it for me. But I guess I copied it to the wrong place?

[Aaron Liu]

Put your cursor in the underscore

[Aaron Liu]

it's a code action should pop up

[Levi]

hmm, i did. but it just shows me Prop and the the other definition thingy

[Aaron Liu]

no put your text cursor in there

[Aaron Liu]

like the little vertical flashing line

[Levi]

image.png

[Aaron Liu]

click the lightbulb

[Levi]

ahh, now i understand. Thanks! Wow this is pretty awesome work! And so quick :starry_eyed:

[Kenny Lau]

@Aaron Liu nice!

[Aaron Liu]

I copied the code from all the other code actions

[Aaron Liu]

so it's inspired by the guard_msgs action and the try this action

[Kenny Lau]

do you think it's easy to convert it to the simp?-style action where you get a blue underscore and a button in the infoview

[Aaron Liu]

not very hard

[Aaron Liu]

but it'll show up on every hole

[Aaron Liu]

actually you need to modify the infotree

[Aaron Liu]

this might be easy and it might be impossible

[Kenny Lau]

Aaron Liu said:

but it'll show up on every hole

well my suggested syntax was _?

[Aaron Liu]

oh yeah

[Levi]

is there anyway to have this autotrigger or certain input? Like I know I am nitpicking right now, but that surely would be awesome I think (if it is possible)

[Aaron Liu]

since I'm using @[hole_code_action] it only works on _ right now

[Aaron Liu]

I don't know how to make it do _? instead

[Kenny Lau]

do you know how simp? works? (i don't)

[Aaron Liu]

it calls docs#Lean.Meta.Tactic.TryThis.addSuggestion I think

[Aaron Liu]

the problem is that you have to pretty print the value in the hole after everything else has finished otherwise you'll just get an unassigned metavariable

[Kenny Lau]

import Mathlib

example {P : Prop} (h : ¬P) : ¬P :=
  show_term fun h ↦ sorry

maybe we can modify show_term instead?

[Kenny Lau]

since we can't tweak the elaboration order from within the hole

[Levi]

Sorry if this is a topic break. But I am thinking about assumption right now. The straight forward application is quite intuitive, it just searches for an assumption that matches the current goal. But the book also talks about "unifying metavariables if necessary", I don't really understand what that means. I think I understand the example they gave:

example (h1 : x = y) (h2 : y = z) (h3 : z = w) : x = w := by
  apply Eq.trans
  assumption
  apply Eq.trans
  repeat assumption

But I don't think I fully understand what unifying meta variables means.

[Kenny Lau]

@Levi when you apply Eq.trans, you're reducing the goal x = w to now two goals, x = something and something = w. Lean does not yet know what the something should be, so it's called a metavariable, and when you look at it in the infoview, it shows up with a ? before it, i.e. it shows up as x = ?b and ?b = w, where ?b is the metavariable

[Kenny Lau]

when you now do assumption on the first goal x = ?b, it tries to match this against each assumption you have, and only h1 : x = y matches this, so now Lean infers that ?b should have been y, this process is called unifying the metavariable

[Kenny Lau]

so basically every time you supply not enough information, that blank is called a metavariable, and the process of filling in the blank is called unifying the metavariable

[Levi]

I see, so if I had a hypothesis for x = y and y = w it would have immediately solved the goal by infering that the metavariables should be y. Thanks for the help again!

[Levi]

Another quick question. Is there any useful application of revert in any proof? Because all those examples I have seen only used revert to rename the hypothesis, which is kind of "pointless" in my eyes.

[Aaron Liu]

sometimes I have to revert something for rw to generate a type correct motive

[Levi]

hmmm... That might be asking for a bit too much, but is there any simple example for this? I can't really think of anything straight out of my head that would make any sense. (Not that I have many examples that I can think of :D )

[Aaron Liu]

simple example

example {ι : Type u} (f : ι → Type v) (i j : ι)
    (h : Subsingleton (f i)) (x : f i) (y : f j) (hij : i = j) :
    HEq x y := by
  -- rw [← hij]
  revert y
  rw [← hij]
  intro y
  rw [h.elim x y]

[Kenny Lau]

there is also decide +revert, and then I mostly use induction .. generalizing .. which encompasses revert in a way

[Kenny Lau]

example (x : Fin 3) : x = 0 ∨ x = 1 ∨ x = 2 := by decide
example (x : Fin 3) : x = 0 ∨ x = 1 ∨ x = 2 := by decide +revert

example (m n : Nat) : m + n = n + m := by
  induction n
  -- a✝ : m + n✝ = n✝ + m

example (m n : Nat) : m + n = n + m := by
  induction n generalizing m
  -- a✝ : ∀ (m : Nat), m + n✝ = n✝ + m

[Levi]

Aaron Liu said:

simple example

example {ι : Type u} (f : ι → Type v) (i j : ι)
    (h : Subsingleton (f i)) (x : f i) (y : f j) (hij : i = j) :
    HEq x y := by
  -- rw [← hij]
  revert y
  rw [← hij]
  intro y
  rw [h.elim x y]

Thanks. I'm still too bad to understand it immediately, but I will try to understand what it does.

[Kenny Lau]

@Levi read the docstring on each tactic, look at the goal (and context) before and after each line, and try to connect the logic

[Levi]

Kenny Lau said:

Levi read the docstring on each tactic, look at the goal (and context) before and after each line, and try to connect the logic

Thanks for the tip! But I already got some difficulties understanding the statement iself. But I think that is mainly because I have never seen HEq before.

[Levi]

Another unrelated question. If constructor just applies the first possible constructor for any given type, what is the advantage of using it instead of the actual constructor? Because if I am trying to prove a disjunction but i dont want to use the first constructor (whatever that is) then constructor wouldn't really help me either way.
But I guess constructor can be used in some automations?

[Kenny Lau]

yeah that is a bit involved, maybe you can ignore HEq for now

[Kenny Lau]

Levi said:

what is the advantage of using it instead of the actual constructor?

a lot of the time there is only one constructor

Levi said:

trying to prove a disjunction

there are the tactics left and right

[Aaron Liu]

Levi said:

Another unrelated question. If constructor just applies the first possible constructor for any given type, what is the advantage of using it instead of the actual constructor? Because if I am trying to prove a disjunction but i dont want to use the first constructor (whatever that is) then constructor wouldn't really help me either way.
But I guess constructor can be used in some automations?

You don't have to know the name of the constructor or how many arguments it takes or which constructor to use (if there are multiple constructors but only one of them with based on the type of the goal)

[Levi]

i see, yeah that's what I guessed. Yeah not having to know the name makes sense. But does a conjunction count as inductive type? Maybe this is a horrendously stupid question, but I thought it was just a "normal" type.

Ah, so if there are multiple constructors, but only one's "output" matches the goal then it will apply that constructor (or the first kind of those constructors), right?

And I didn't knew about left and right before, how enlightening.

[Aaron Liu]

what do you mean "normal" type?

[Aaron Liu]

there aren't that many ways to construct types in Lean

[Levi]

i thought it was just a structure with some fields. I don't really know the formal definition for inductive types in lean (yet :D )

[Aaron Liu]

A structure is a kind of inductive type

[Kevin Buzzard]

There are three kinds of types in lean: inductive types, function types and quotient types. If you're trying to "fully understand lean" then this is one of the absolute basics. Have you read the first couple of chapters of #tpil yet?

[Levi]

Kevin Buzzard said:

There are three kinds of types in lean: inductive types, function types and quotient types. If you're trying to "fully understand lean" then this is one of the absolute basics. Have you read the first couple of chapters of #tpil yet?

yes, i am on chapter 5, that's why im asking all those questions about tactics :sweat_smile:
And yes fully understanding lean is perhaps a bit optimistic, but at least partially :D so that I can use it to prove something interesting.

[Kenny Lau]

Levi said:

the formal definition for inductive types in lean

forget formal, inductive type allows you to build elements "from scratch", and guarantees that those are all the elements that exist. for example, you can build a natural number using Nat.zero or Nat.succ, and every natural number is built that way.

In contrast, there's no way for you to build a function Nat -> Nat from scratch, because you can do all sorts of things, so Nat -> Nat is not an inductive type

and for quotient, it's a bit more subtle, it doesn't satisfy the "injectivity" criterion; for example, there's an axiom saying that if you build a natural number using a different pathway, then you are guaranteed to obtain a different natural number. this is why Nat.zero cannot be equal to Nat.succ Nat.zero. However, quotient types don't have this property, because you can use different pathways to build the same object.

[Kenny Lau]

I shouldn't have to explain all this, I would assume that tpil has covered this

[Levi]

Kenny Lau said:

I shouldn't have to explain all this, I would assume that tpil has covered this

I suppose. :sweat_smile: I hope they do in chapter 7, at least that's the one labelled inductive types. But I haven't dared to take a peek into that yet. Still thanks for the explanation, it really does make a lot more sense now.

[Axel Boldt]

Is there a table somewhere that shows the Lean operators, their precedences, and whether they're left or right associative? All the colons, arrows, equal signs are a bit much...

[Kenny Lau]

Axel Boldt said:

Is there a table somewhere that shows the Lean operators, their precedences, and whether they're left or right associative? All the colons, arrows, equal signs are a bit much...

it's basically all here, L280-L458

[Axel Boldt]

Kenny Lau said:

it's basically all here, L280-L458

That's pretty good, thanks! But the scariest ones I cannot find there, like:
:
->
:=
,
<;>
↑
▸

[Kenny Lau]

@Axel Boldt some of these are really fundamental (like :=) and some of them isn't one syntax (like (foo, bar)) but you can generally do:

import Mathlib

#find_syntax "↑"

and then see

In `Init.Coe`:
  coeNotation: '↑'

and then go to coeNotation

[Axel Boldt]

Kenny Lau said:

some of these are really fundamental (like :=)

They sure are, and confusing! For example, the very first piece of Lean code in the TPIL book has the line

have hp : p := And.left hpq

Here, most laymen would assume that hp is some sort of name for the following assignment, where p is given the value of And.left hpq. The experts will know that : binds stronger than :=, and both bind stronger than have.

[Kenny Lau]

I guess I don't really think about it in terms of binding, I just know the pattern <decl-name> : <type> := <definition>

[Kenny Lau]

to me this is one syntax

[Aaron Liu]

:= is actually a lot of syntaxes that are all done roughly the same way so you only have to learn it once

[Aaron Liu]

Axel Boldt said:

The experts will know that : binds stronger than :=, and both bind stronger than have.

If you look at the AST it's

(Term.have
  "have"
  (Term.letConfig [])
  (Term.letDecl
   (Term.letIdDecl
    (Term.letId `hp)
    []
    [(Term.typeSpec ":" `p)]
    ":="
    (Term.app `And.left [`hpq])))
  []
  (the rest of the expression))

[Arthur Paulino]

Axel, your point make sense!

However, I find it hard to learn any language without understanding at least its basic syntax first. In the learn page of the official site, you'll find other sources, including the official language reference.

I find the topic name of this thread quite intriguing. Anyone intending to fully understand Lean will need to understand that Lean is highly extensible. Several forms of syntax are extensions done either in core, in mathlib or somewhere else.

The have syntax is no exception. If you "go to definition" of have in term-mode, it will take you to

@[builtin_term_elab «have»] def elabHaveDecl : TermElab :=
  fun stx expectedType? => elabLetDeclCore stx expectedType? { nondep := true }

In tactic mode, it will take you to

syntax "have" letConfig letDecl : tactic
macro_rules
  -- special case: when given a nested `by` block, move it outside of the `refine` to enable
  -- incrementality
  | `(tactic| have%$haveTk $id:letId $bs* : $type := by%$byTk $tacs*) => do
...

Often you'll be able to inspect the syntax rules of a piece of code you're interested in. Arguably, learning how to inspect various syntaxes is more aligned with the goal of fully understanding Lean than knowing the precise syntax of every extension.

[Kenny Lau]

(Axel is not OP)

[Arthur Paulino]

Kenny Lau said:

(Axel is not OP)

I understand, sorry! I just wanted to show that you can dig deeper and deeper to understand something in Lean. Ultimately, Lean's frontend is built in Lean itself, so everything is in plain sight (if you know where to look!).

[Arthur Paulino]

Axel Boldt said:

For example, the very first piece of Lean code in the TPIL book has the line

Maybe it makes sense for TPIL to be explicit upfront that for anyone unfamiliar with the very basics of Lean, the language reference should be either preceded or accompanied.

[Arthur Paulino]

Arthur Paulino said:

fully understand Lean

TBH it's hard for me to draw the line of what "fully understanding Lean" means. Even the by DSL for entering tactic mode is, from some perspective, just another arbitrary DSL. Not in the sense that it's carelessly designed or unimportant (on the contrary), but in the sense that one can build their very own DSL for constructing terms of types. I've seen one or two attempts, but it's hard to beat the by DSL in terms of popularity, consistency, completeness and extensibility.

[Levi]

Arthur Paulino said:

Arthur Paulino said:

fully understand Lean

TBH it's hard for me to draw the line of what "fully understanding Lean" means. Even the by DSL for entering tactic mode is, from some perspective, just another arbitrary DSL. Not in the sense that it's carelessly designed or unimportant (on the contrary), but in the sense that one can build their very own DSL for constructing terms of types. I've seen one or two attempts, but it's hard to beat the by DSL in terms of popularity, consistency, completeness and extensibility.

Very interesting and illustrative points that you have made! Now in retroperspective, the name I chose for the thread was a bit optimistic. Also it kind of turned into a big collection of random questions that popped up in my head along the journey so far. And yes, I suppose "fully" understanding lean is quite the optimistic formulation, you are already the second person to point that out :D. (Maybe I should change it to reduce confusion), but what I intended to mean is to understand lean in a way that I could write stuff in it, which right now I realized turned out a bit more difficult than I thought (my background in computer science is only helping me so much, suprisingly). But I am not giving up :D

btw I always meant to ask, whether it is good style to write all these random questions in one thread, as i find it tedious to open up a new channel for every small issue I get. But if this is non standard here, I will try to adapt.

[Stepan Nesterov]

Levi said:

Another quick question. Is there any useful application of revert in any proof? Because all those examples I have seen only used revert to rename the hypothesis, which is kind of "pointless" in my eyes.

I have used revert in situations like

example (h : 23 = 24) : False := by
  revert h
  decide

Not sure if this is the idiomatic way though

[Andrew Yang]

This a totally valid use (although you also have decide +revert but when you want to control what to revert you would need to invoke revert directly).

Another case is that the generalizing clause in induction is also just a revert. If you need to apply induction eliminators by hand (as one sometimes do), you’ll also need to revert by hand.