Zulip Chat Archive

Stream: new members

Topic: how to read non-tactic-mode and use of digits with $


Filippo A. E. Nuccio (Jun 18 2020 at 11:22):

I am trying to digest the proof that in an integral domain, every non-zero element is not a zero-divisor. This is in localization.lean, line 676, lemma mem_non_zero_divisors_iff_ne_zero. But the proof is not written in tactic mode (I believe this is what a begin...end proof is called, right)? Hence, when I try to read it line-by-line to understand what every small piece of code does, I don't see anything in the Lean Goals.

I also realise that the symbol $ is used, and I believe this is not really OK for begin...end proofs, as I have read here
https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/What.20does.20.24.20mean.3F/near/201220084
(but this is too difficult for me)

Filippo A. E. Nuccio (Jun 18 2020 at 11:28):

What puzzles me in particular is the code
zero_ne_one (hm 1 $ by rw [hz, one_mul]).symm,
where hm is the hypothesis that a certain element xx is not a zero-divisor, and hz is the hypothesis that x=0x=0 (I suppose that the point is to derive a contradiction).

Kevin Buzzard (Jun 18 2020 at 11:32):

The proof is written in term mode, yes.

lemma mem_non_zero_divisors_iff_ne_zero {A : Type*} [integral_domain A] {x : A} :
  x  non_zero_divisors A  x  0 :=
⟨λ hm hz, zero_ne_one (hm 1 $ by rw [hz, one_mul]).symm,
 λ hnx z, eq_zero_of_ne_zero_of_mul_eq_zero hnx

The proof is an if and only if proof, and the term mode constructor for and iff proof is ⟨left_implies_right, right_implies_left⟩. The lambdas are term mode for intro, the $ can be replaced by brackets, and by means "drop into tactic mode for one tactic only", enabling the use of the rw tactic.

Filippo A. E. Nuccio (Jun 18 2020 at 11:34):

So how would you rewrite the part (hm 1 $ by rw [hz, one_mul]) in tactic mode?

Kevin Buzzard (Jun 18 2020 at 11:34):

Here is what the proof looks like if you partially take it apart into tactic mode:

lemma mem_non_zero_divisors_iff_ne_zero {A : Type*} [integral_domain A] {x : A} :
  x  non_zero_divisors A  x  0 :=
begin
  split,
  { intros hm hz,
    exact zero_ne_one (hm 1 $ by rw [hz, one_mul]).symm,
  },
  { intros hnx z,
    exact eq_zero_of_ne_zero_of_mul_eq_zero hnx
  }
end

Filippo A. E. Nuccio (Jun 18 2020 at 11:34):

(deleted)

Kevin Buzzard (Jun 18 2020 at 11:34):

But I didn't answer your question

Filippo A. E. Nuccio (Jun 18 2020 at 11:35):

Kevin Buzzard said:

But I didn't answer your question

Yes, I hoped that that part would disappear in tactic mode... so I'm still keen to get the answer

Kevin Buzzard (Jun 18 2020 at 11:35):

lemma mem_non_zero_divisors_iff_ne_zero {A : Type*} [integral_domain A] {x : A} :
  x  non_zero_divisors A  x  0 :=
begin
  split,
  { intros hm hz,
    apply @zero_ne_one A,
    symmetry,
    apply hm,
    rw [hz, one_mul],
  },
  { intros hnx z,
    apply eq_zero_of_ne_zero_of_mul_eq_zero,
    exact hnx
  }
end

Kevin Buzzard (Jun 18 2020 at 11:36):

You can click through it now and see what's going on.

Filippo A. E. Nuccio (Jun 18 2020 at 11:37):

Does the @ before zero_ne_one mean something like "we get a contradiction from..."?

Anne Baanen (Jun 18 2020 at 11:37):

It makes implicit arguments explicit

Kevin Buzzard (Jun 18 2020 at 11:37):

If you look at the goal at that point, you can see it's false. @zero_ne_one A is the statement that 0 ≠ 1 (these being regarded as elements of A).

Kevin Buzzard (Jun 18 2020 at 11:38):

Internally, X ≠ Y is represented as (X = Y) -> false, so we are applying this function, which changes the goal from false to 0 = 1.

Kevin Buzzard (Jun 18 2020 at 11:39):

After the term mode proof in mathlib, just edit your mathlib and add

lemma mem_non_zero_divisors_iff_ne_zero' {A : Type*} [integral_domain A] {x : A} :
  x  non_zero_divisors A  x  0 :=
begin
  split,
  { intros hm hz,
    apply @zero_ne_one A,
    symmetry,
    apply hm,
    rw [hz, one_mul],
  },
  { intros hnx z,
    apply eq_zero_of_ne_zero_of_mul_eq_zero,
    exact hnx
  }
end

(I added a prime in the lemma name) and you'll be able to click around and inspect the proof.

Alex J. Best (Jun 18 2020 at 11:40):

I see your questions have been answered by now, but here is how I would deconstruct this term from outside to in in my head to understand what its doing.
zero_ne_one is the statement that 0 \ne 1 i.e. 0 = 1 \to false, so zero_ne_one (hm 1 $ by rw [hz, one_mul]).symm will result in a term of type false if (hm 1 $ by rw [hz, one_mul]).symm is of type 0 = 1, the .symm swaps the sides of an equality so hm 1 $ by rw [hz, one_mul] should have type 1=0, then hm has type ∀ z, z * x = 0 → z = 0, so hm 1 is of type 1 * x = 0 → 1 = 0, so the part after the dollar (which is just the same as bracketing the rest of the line) should have type 1 * x = 0 this can be shown by rewriting with hz : x = 0 and then one_mul to reduce it to 0 = 0 .

Filippo A. E. Nuccio (Jun 18 2020 at 11:40):

Ok, thanks. This I undestand. Then one more question: why does apply hm transform the goal from 1=0 to 1*x=0? I understand that this is useful for the rest of the proof, but why "applying the hypothesis that xx is not a zero-divisor" multiplies by it?

Kevin Buzzard (Jun 18 2020 at 11:40):

But do remember to unedit mathlib after. Another possibility is to make a new file and do this:

import ring_theory.localization

lemma mem_non_zero_divisors_iff_ne_zero' {A : Type*} [integral_domain A] {x : A} :
  x  non_zero_divisors A  x  0 :=
begin
  split,
  { intros hm hz,
    apply @zero_ne_one A,
    symmetry,
    apply hm,
    rw [hz, one_mul],
  },
  { intros hnx z,
    apply eq_zero_of_ne_zero_of_mul_eq_zero,
    exact hnx
  }
end

Filippo A. E. Nuccio (Jun 18 2020 at 11:41):

Kevin Buzzard said:

But do remember to unedit mathlib after. Another possibility is to make a new file and do this:

import ring_theory.localization

lemma mem_non_zero_divisors_iff_ne_zero' {A : Type*} [integral_domain A] {x : A} :
  x  non_zero_divisors A  x  0 :=
begin
  split,
  { intros hm hz,
    apply @zero_ne_one A,
    symmetry,
    apply hm,
    rw [hz, one_mul],
  },
  { intros hnx z,
    apply eq_zero_of_ne_zero_of_mul_eq_zero,
    exact hnx
  }
end

Thanks-I will probably just delete it after I've understood

Anne Baanen (Jun 18 2020 at 11:42):

x ∈ non_zero_divisors A is defined to be ∀ z, z * x = 0 → z = 0, so apply hm matches z = 0 with the goal 1 = 0, making the new goal 1 * x = 0

Filippo A. E. Nuccio (Jun 18 2020 at 11:42):

Anne Baanen said:

x ∈ non_zero_divisors A is defined to be ∀ z, z * x = 0 → z = 0, so apply hm matches z = 0 with the goal 1 = 0, making the new goal 1 * x = 0

GREAT! Thanks. (Or: how to show I haven't understood yet what "to match" means in concrete terms... slowly getting there).

Kevin Buzzard (Jun 18 2020 at 11:43):

Again we're relying on the definitions of things -- in term mode Lean can see through all definitions. hm is a proof that x is a non-zero-divisor. By definition, this means that hm is a proof of ∀ z, z * x = 0 → z = 0, so hm is a function which takes as input a number z, and a proof that z*x=0, and returns a proof that z=0. Now apply that function to the goal 1 = 0, Lean guesses that z must be 1 (in term mode the 1 was supplied explicitly, in tactic mode I let Lean guess it; I could have written apply hm 1) and the goal is hence reduced to 1*x=0.

Filippo A. E. Nuccio (Jun 18 2020 at 11:44):

Kevin Buzzard said:

Again we're relying on the definitions of things -- in term mode Lean can see through all definitions. hm is a proof that x is a non-zero-divisor. By definition, this means that hm is a proof of ∀ z, z * x = 0 → z = 0, so hm is a function which takes as input a number z, and a proof that z*x=0, and returns a proof that z=0. Now apply that function to the goal 1 = 0, Lean guesses that z must be 1 (in term mode the 1 was supplied explicitly, in tactic mode I let Lean guess it; I could have written apply hm 1) and the goal is hence reduced to 1*x=0.

... crystal clear.

Anne Baanen (Jun 18 2020 at 11:44):

(More details: non_zero_divisors R is a submonoid of R, and (x : R) ∈ (s : submonoid R) is defined to be x ∈ s.carrier. In the definition of non_zero_divisors we have carrier := {x | ∀ z, z * x = 0 → z = 0}, and x ∈ {x | ∀ z, z * x = 0 → z = 0} is defined as ∀ z, z * x = 0 → z = 0.)

Kevin Buzzard (Jun 18 2020 at 11:45):

It's important to remember that there is no magic going on here. Term mode looks like heiroglyphics but it is 100% logical and can be worked out, the problem is that it's much harder to work out than tactic mode because you have to learn to "be the compiler", like Alex was doing above.

Kevin Buzzard (Jun 18 2020 at 11:46):

In tactic mode you can click around and see what's going on. I believe that this functionality is coming to term mode soon!

Kevin Buzzard (Jun 18 2020 at 11:46):

yeah, in fact I have it already :D

Filippo A. E. Nuccio (Jun 18 2020 at 11:46):

Indeed, I confess that coming from the math world, being able to check line-by-line is great to "learn how a proof goes".

Kevin Buzzard (Jun 18 2020 at 11:47):

The sooner we get the widget extension of the Lean addon to VS Code in master, the better :-)

Anne Baanen (Jun 18 2020 at 11:47):

In Emacs, the term mode goal state Just Works :P

Filippo A. E. Nuccio (Jun 18 2020 at 11:50):

At any rate, is there a way to understand the hm 1 $ by part of the term mode code?

Kevin Buzzard (Jun 18 2020 at 11:50):

I totally agree that there is a lot going on here; I found mathlib completely incomprehensible for a long time. I learnt how to use Lean by spending a long time writing tactic mode proofs, and then slowly migrating to term mode. On the other hand there are people here with more of a CS background who did courses in type theory and for whom term mode works much better: these people are typically not looking at theorems about integral domains though, they are just writing 5 different proofs of P and Q -> Q and P because that's what floats their boat. As a mathematician it's much more natural to start thinking about integral domains, because these things are trivialities to us because we're so used to them; but by this stage the term mode proofs have become quite impenetrable if you're a beginner.

Kevin Buzzard (Jun 18 2020 at 11:51):

The CS people go on to start writing little domain specific languages and stuff -- they naturally gravitate towards a completely different kind of question, one for which term mode is often more appropriate (e.g. maybe they are defining algorithms).

Kevin Buzzard (Jun 18 2020 at 11:52):

#tpil is a good introduction to term mode.

Filippo A. E. Nuccio (Jun 18 2020 at 11:53):

Kevin Buzzard said:

I totally agree that there is a lot going on here; I found mathlib completely incomprehensible for a long time. I learnt how to use Lean by spending a long time writing tactic mode proofs, and then slowly migrating to term mode. On the other hand there are people here with more of a CS background who did courses in type theory and for whom term mode works much better: these people are typically not looking at theorems about integral domains though, they are just writing 5 different proofs of P and Q -> Q and P because that's what floats their boat. As a mathematician it's much more natural to start thinking about integral domains, because these things are trivialities to us because we're so used to them; but by this stage the term mode proofs have become quite impenetrable if you're a beginner.

I am happy to see that I'm not alone in our sinking boat...

Scott Morrison (Jun 18 2020 at 11:54):

There's also a cultural tendency we've picked up, unfortunately or not, to value "short" proofs in mathlib, regardless of how comprehensible they are.

Scott Morrison (Jun 18 2020 at 11:54):

It's definitely a good skill to learn to take a tactic mode proof and turn it into a term mode proof. But this needn't be done for its own sake.

Scott Morrison (Jun 18 2020 at 11:54):

Better use of "golfing" energy might be to add comments to a tactic mode proof. :-)

Scott Morrison (Jun 18 2020 at 11:55):

A formal development does need lots of trivial lemmas. I absolutely agree that whenever the proof is so easy that no human would ever want to read it, golfing it down to the shortest possible term mode proof is helpful and good, just the boost the signal-to-noise ratio on the page.

Filippo A. E. Nuccio (Jun 18 2020 at 11:56):

Of course I am too new to the game to have an opinion. One idea which comes to my mind is that longer proofs (with a grain of salt) might be more flexible to be used in other proofs of similar statements, because you can " extract part of the proof". This is the way I often work as mathematician.

Kevin Buzzard (Jun 18 2020 at 11:56):

Term mode is literally just applying a bunch of functions. In some sense the main thing you have to learn is how to think of everything as a function. For example the idea that x is a non-zero-divisor is surely not stored by many mathematicians as a function, but when you take it apart in type theory you find that it is -- it is a function which eats a number and a proof and spits out a proof. Normally in mathematics we consider proofs as objects of a completely different nature to numbers. Type theory lets you treat both of these things as terms, and as a consequence a whole lot of new things can be thought of as functions. For example the proof of Fermat's Last Theorem is a function, taking n,x,y,z and some proofs (a proof that n>2 and that x^n+y^n=z^n) and returning another proof (the proof that x*y=0).

Filippo A. E. Nuccio (Jun 18 2020 at 11:58):

Kevin Buzzard said:

Term mode is literally just applying a bunch of functions. In some sense the main thing you have to learn is how to think of everything as a function. For example the idea that x is a non-zero-divisor is surely not stored by many mathematicians as a function, but when you take it apart in type theory you find that it is -- it is a function which eats a number and a proof and spits out a proof. Normally in mathematics we consider proofs as objects of a completely different nature to numbers. Type theory lets you treat both of these things as terms, and as a consequence a whole lot of new things can be thought of as functions. For example the proof of Fermat's Last Theorem is a function, taking n,x,y,z and some proofs (a proof that n>2 and that x^n+y^n=z^n) and returning another proof (the proof that x*y=0).

This makes perfect sense and it is also quite clear (and cute), now that you explain it. The only drawback is that I'd rather go and grab a second PhD in math to format my mind from scracth... :slight_smile:

Patrick Massot (Jun 18 2020 at 11:59):

If you have a recent Lean, putting the cursor at the beginning of a term will you its type.

Kevin Buzzard (Jun 18 2020 at 12:00):

Part of the art of writing a robust API is to figure out exactly all the "little steps" which we mathematicians are taking all the time, and adding these facts as lemmas, and then building up bigger proofs from smaller proofs to ensure that all proofs are short. For example mem_non_zero_divisors_iff_ne_zero uses eq_zero_of_ne_zero_of_mul_eq_zero, which is proved just above and the term mode proof is 1 line long but uses eq_zero_or_eq_zero_of_mul_eq_zero, a theorem whose proof is 1 line long but which uses...

Jalex Stark (Jun 18 2020 at 13:30):

Filippo A. E. Nuccio said:

This makes perfect sense and it is also quite clear (and cute), now that you explain it. The only drawback is that I'd rather go and grab a second PhD in math to format my mind from scracth... :slight_smile:

nah, you don't want to format your mind from scratch. building a bridge to a new way of thinking is slow, but you can get a lot of mileage out of transferring stuff across. some people make their careers almost exclusively out of building such bridges.


Last updated: Dec 20 2023 at 11:08 UTC