General Newbie Advice/Questions

Stream: new members

[screentime]

Hi all,

Loving the Lean4 language and Theorem proving book so far. Working my way through the Math book too, but I wanted to ask some general questions at this point.

I am a bit confused on the different options we have for tactics. So I know how to craft value based (non tactics based) proofs for most simple things - e.g. for existential, construct a (witness, proof) pair using Exists.intro; e.g. for universals, construct a function that produces the proof when given the desired input terms; e.g. to produce a proof for a Prop, it suffices to write the code that can, under a type-checker, produce a term of that type.

Ok onto some questions:

Where can I find some formal definitions and nuanced examples of the tactics? I went through the theorem proving book and only really got a rough understanding. For example, I know/think that if I have a goal h, then:

• exact XYZ will work if XYZ is exact same type as h
• rewrite [XYZ] will use an XYZ of type LHS [->,=,...] RHS and rewrite the symbols in "h" from LHS to RHS (and <- to go the other way), changing the goal to h'.
• intro XYZ will change a goal h of type (fun x -> ... something with x ...) into a concrete goal of "... something with XYZ..." (x is changed to XYZ, and it's no longer a function form". This is also the form to unpack a universal quantifier.
• use XYZ will change a goal h of type "exists x, ...something with x..." into a specific goal of "...something with XYZ..." (x Is changed to XYZ, and the existential is dropped)
• calc is a way to break a goal of some transitive relation into a sequence of subgoals, and allow the user to organize their proofs with milestones for those.
• have also allow use to introduce an additional sub-lemma into the context to use towards the goal

What I'm not understanding is:

• what is "apply" exactly? I don't quite get the operational rules of this thing - I just roughly pattern match and sometimes a relevant theorem works. For example, how is this different from rewrite/rw?
• How does cases work? How does the \cdot work? Sometimes I see apply with a what looks like a partial expression, followed by new line and either cases or \cdot, but I couldn't quite find or understand the pattern to how it works.
• What happens when we have multiple goals? Do the tactics just operate on the first applicable goal at a time? Is there a way to say - "I want the next few tactics to work for the first goal, then I want the next few tactics to work on the second goal"?
• I don't quite understand the differences and cases for linarith, dsimp (or simp?), and ring (or ring_nf?). In my mind they seem to be "magic ways to do automated expression solving/simplification" but I can't quite make out a more formal description than that.
• There's a bunch more tactics, it seems, than the ones in the lean book. Are they necessary? Or they just sugar? e.g. aesop, refine, push_neg

Further, I'm having some general questions about workflow:

• In most ordinary set theory math, we generally operate at very high level, and always omit basic operational steps (like the equivalent of ring, dsimp, etc.). Does having to account for the basics and name the exact steps get in the way of doing real work in Lean?
• The structure of a proof by contradiction is very simple in traditional maths. You just assume the opposite of your hypothesis, then you arrive at something that's incompatible with a known fact. And it's common to reach for it unless you really value a constructive proof. But in Lean, you assume (hypothesis -> False). It's not really clear how to use this fact to start the proof. Not sure if this is a real question but maybe just asking some advice - how common are these in doing real math in Lean? any advice here?
• Is there a better way to search for theorems than to just know some assumptions about naming scheme? For example in Haskell there's Hoogle, which allows users to search by type. Or is it generally assumed we need to know a basic repertoire and then the specifics of the field we're working in?

Thanks in advance for any help!

[Zhang Qinchuan]

Currently there seems no offical materials to cover the gap between TPIL/MIL and real world formalization.

But there are some non-offical materials may help.

1. Introduction to basic tactics to handle logic structure:Lean 4 spellbook.
2. References for all available tactics in mathlib:Mathlib4 Tactics.

[Zhang Qinchuan]

For search theorems efficiently, there are:

1. LeanSearch
2. Moogle
3. Loogle
4. Mathlib4Docs

[screentime]

Thank you! The Mathlib4 Tactics seems to have a good (or at least somewhat formal) definition of apply. It seems to say apply e matches e's conclusion with the current goal. And then it replaces the current goal with all of e's premises? So for example, if I have e : LHS -> RHS, and I have a goal that looks like RHS, apply e will replace current goal with LHS?

I should also clarify that I liked the simp section in the theorem book. It seems to apply "simplifications" as defined by some canonical order by walking through a DAG of simplification rules. I guess I don't really get what dsimp's relation is to simp. Mathlib4 link seems to suggest dsimp works on a subset of simp's rules? If so why would I ever use dsimp? And I think I 've hit cases in going through examples in the Math book where dsimp was suggested, and it works; but simp fails to type check in the same line.

Also the theorem search links are great! Anyone integrate that into VSCode?

[Zhang Qinchuan]

screentime said:

Thank you! The Mathlib4 Tactics seems to have a good (or at least somewhat formal) definition of apply. It seems to say apply e matches e's conclusion with the current goal. And then it replaces the current goal with all of e's premises? So for example, if I have e : LHS -> RHS, and I have a goal that looks like RHS, apply e will replace current goal with LHS?

I should also clarify that I liked the simp section in the theorem book. It seems to apply "simplifications" as defined by some canonical order by walking through a DAG of simplification rules. I guess I don't really get what dsimp's relation is to simp. Mathlib4 link seems to suggest dsimp works on a subset of simp's rules? If so why would I ever use dsimp? And I think I 've hit cases in going through examples in the Math book where dsimp was suggested, and it works; but simp fails to type check in the same line.

Also the theorem search links are great! Anyone integrate that into VSCode?

Loogle and Moogle are already in VSCode. You can click the "forall" button to see them in the menu.

If you are using the latest mathlib4, you can also use #leansearch in VSCode.

[Ruben Van de Velde]

Correct re apply

[Ruben Van de Velde]

dsimp is indeed a weaker version of simp which only uses equalities that are true in the stronger sense of "definitional equality"

[Zhang Qinchuan]

This webpage is about simp.

Sometimes simp will oversimplify your goal, hence you need dsimp, simp only [thm] or simp [-thm] to prevent from oversimplification.

[Notification Bot]

This topic was moved here from #general > General Newbie Advice/Questions by Patrick Massot.

[Patrick Massot]

@screentime hopefully https://leanprover-community.github.io/mathematics_in_lean/C02_Basics.html#using-theorems-and-lemmas contains answers to some of your questions about apply and the focusing dots.

[Patrick Massot]

screentime said:

• How does cases work? How does the \cdot work? Sometimes I see apply with a what looks like a partial expression, followed by new line and either cases or \cdot, but I couldn't quite find or understand the pattern to how it works.

cases is one of the tricky tactics for beginners because it is much more tied to the foundations than other tactics. If you are not happy with instructions simply telling you when to use it without seeing the global picture then your best option is probably to carefully read https://lean-lang.org/theorem_proving_in_lean4/inductive_types.html

[Patrick Massot]

screentime said:

• What happens when we have multiple goals? Do the tactics just operate on the first applicable goal at a time? Is there a way to say - "I want the next few tactics to work for the first goal, then I want the next few tactics to work on the second goal"?

Yes, almost all tactics work on the first goal. If you sometimes struggle to see what is the first goal and use VSCode you can set the option Lean 4 > Infoview: Emphasize First Goal. If you want to work on another goal (which is very rare) then you can take a look at https://leanprover-community.github.io/mathlib4_docs/Batteries/Tactic/PermuteGoals.html

[Patrick Massot]

screentime said:

• I don't quite understand the differences and cases for linarith, dsimp (or simp?), and ring (or ring_nf?). In my mind they seem to be "magic ways to do automated expression solving/simplification" but I can't quite make out a more formal description than that.

linarith stands for “linear arithmetic”, it will prove equalities or inequalities that follow from linear combination of your assumptions and the fact you provide (if any). See https://leanprover-community.github.io/mathlib4_docs/Mathlib/Tactic/Linarith/Frontend.html. ring will close goal that follow from the axioms of commutative (semi)-rings, see https://leanprover-community.github.io/mathematics_in_lean/C08_Groups_and_Rings.html#rings and https://leanprover-community.github.io/mathlib4_docs/Mathlib/Tactic/Ring/Basic.html

[Patrick Massot]

screentime said:

• There's a bunch more tactics, it seems, than the ones in the lean book. Are they necessary? Or they just sugar? e.g. aesop, refine, push_neg

In a very precise sense, all tactics are sugar. The Lean kernel consumes only proof terms so you technically never need to use any tactic. Of course in practice tactics are unavoidable if you want to be really productive and you are not some kind of alien (yes, we do have one here). So there is always a trade-off when learning Lean between learning tons of tactics or focusing on the most generally useful ones.

[Patrick Massot]

screentime said:

• In most ordinary set theory math, we generally operate at very high level, and always omit basic operational steps (like the equivalent of ring, dsimp, etc.). Does having to account for the basics and name the exact steps get in the way of doing real work in Lean?

There is nothing like ordinary set theory math. Ordinary math is foundation-independent. And I don’t understand your question. The tactics you mention are precisely tactics allowing you to omit operational steps. And of course the answer to “does it get in the way” is: just look at what was achieved already.

[Patrick Massot]

screentime said:

• The structure of a proof by contradiction is very simple in traditional maths. You just assume the opposite of your hypothesis, then you arrive at something that's incompatible with a known fact. And it's common to reach for it unless you really value a constructive proof. But in Lean, you assume (hypothesis -> False). It's not really clear how to use this fact to start the proof. Not sure if this is a real question but maybe just asking some advice - how common are these in doing real math in Lean? any advice here?

I don’t think you can get a useful answer to this question without being more specific. The by_contra tactic seems to be doing exactly what you ask for. What is your question? Do you have a specific example where you struggle with this?

[Bulhwi Cha]

Here's an example of using the apply tactic:

example {p q r : Prop} (min₁ : p) (min₂ : q) (maj : p → q → r) : r := by
  apply maj
  · exact min₁
  · exact min₂

-- compare the above proof with the following one
example {p q r : Prop} (min₁ : p) (min₂ : q) (maj : p → q → r) : r :=
  maj min₁ min₂

[Bulhwi Cha]

Patrick Massot said:

Yes, almost all tactics work on the first goal. If you sometimes struggle to see what is the first goal and use VSCode you can set the option Lean 4 > Infoview: Emphasize First Goal. If you want to work on another goal (which is very rare) then you can take a look at https://leanprover-community.github.io/mathlib4_docs/Batteries/Tactic/PermuteGoals.html

You can also use the notation case <tag> => <tactics> to choose the goal you want Lean to focus on:

example {p q : Prop} (hl : p) (hr : q) : p ∧ q := by
  constructor
  case left  => exact hl
  case right => exact hr

example {p q : Prop} (hl : p) (hr : q) : p ∧ q := by
  constructor
  case right => exact hr
  case left  => exact hl

[Bulhwi Cha]

Patrick Massot said:

I don’t think you can get a useful answer to this question without being more specific. The by_contra tactic seems to be doing exactly what you ask for. What is your question? Do you have a specific example where you struggle with this?

Here's an example of using the by_contra tactic:

import Batteries.Tactic.Init

example {p : Prop} (h : ¬p → False) : p := by
  by_contra hnp
  exact h hnp

example {p : Prop} (h : ¬p → False) : p :=
  Classical.byContradiction h

-- `¬¬p` and `¬p → False` are definitionally equal
example {p : Prop} : (¬¬p) = (¬p → False) :=
  rfl

[screentime]

Thanks all! This is a great community. This clarifies a lot already - more to explore and read now.

[screentime]

RE: multiple goals. I suppose my question was more about organizing the proof. Like in traditional math we put separate subgoals under different paragraphs or headings, so when we read the proof it's organized. But if you've finished a Lean proof, and you're now reading it, isn't it a bit confusing which lines correspond to what goal? Or is the idea that you have to read a Lean proof inside an editor (as opposed to, say printed onto paper)? I think @Bulhwi Cha 's comment addresses what I was looking for - I'll have to try to understand the constructor breakdown better.

RE: linarith/ring/etc. - if we have a "trivial" operation that should be obvious but requires some combination of these special tactics, what's the advice? Should we manually break it up into multiple have : ... steps each using a single one of these tactics? I'm thinking something like this:

example {x y z : ℝ} : x^2 + 2*x*y + y^2 >= -z^2 := by
  have : z^2 ≥ 0 := by exact sq_nonneg z
  have : (x+y)^2 = (x^2 + 2*x*y + y^2) := by ring
  have : (x+y)^2 ≥ 0 := by exact sq_nonneg (x+y)
  linarith

(EDIT: hmm maybe this isn't a great example - I can remove the ring step and it still works)

RE apply @Bulhwi Cha 's example - it makes a lot of sense! Why do you have the \cdots there? In VSCode, I tried removing them and it equally works:

example {p q r : Prop} (min₁ : p) (min₂ : q) (maj : p → q → r) : r := by
  apply maj
  exact min₁
  exact min₂

[Daniel Weber]

screentime said:

RE: multiple goals. I suppose my question was more about organizing the proof. Like in traditional math we put separate subgoals under different paragraphs or headings, so when we read the proof it's organized. But if you've finished a Lean proof, and you're now reading it, isn't it a bit confusing which lines correspond to what goal? Or is the idea that you have to read a Lean proof inside an editor (as opposed to, say printed onto paper)?

This is the point of \cdots — they focus on the first subgoal, so you know all of the tactics there work on this subgoal. Mathlib coding style recommends never having multiple subgoals active, using \cdots to focus on each one whenever they appear

[Zhang Qinchuan]

screentime said:

RE: multiple goals. I suppose my question was more about organizing the proof. Like in traditional math we put separate subgoals under different paragraphs or headings, so when we read the proof it's organized. But if you've finished a Lean proof, and you're now reading it, isn't it a bit confusing which lines correspond to what goal? Or is the idea that you have to read a Lean proof inside an editor (as opposed to, say printed onto paper)? I think Bulhwi Cha 's comment addresses what I was looking for - I'll have to try to understand the constructor breakdown better.

There are many layers of organizing a proof.

For complex and large theorem, there is blueprint. For exmaple, the blueprint of FLT:https://imperialcollegelondon.github.io/FLT/blueprint/. You need to split your proof into many files and put them into different directories.

For proof abount serval hunders lines of code, it is recommended to split it into small lemmas and then combine them to get the big one.

Finally, inside a theorem you can use .(i.e. dot focus), have, show and comments to make your proof more structural.