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

Stream: new members

[Filippo A. E. Nuccio]

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]

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 $x$ is not a zero-divisor, and hz is the hypothesis that $x=0$ (I suppose that the point is to derive a contradiction).

[Kevin Buzzard]

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]

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

[Kevin Buzzard]

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]

(deleted)

[Kevin Buzzard]

But I didn't answer your question

[Filippo A. E. Nuccio]

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]

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]

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

[Filippo A. E. Nuccio]

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

[Anne Baanen]

It makes implicit arguments explicit

[Kevin Buzzard]

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]

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]

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]

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]

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 $x$ is not a zero-divisor" multiplies by it?

[Kevin Buzzard]

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]

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]

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]

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]

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]

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]

(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]

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]

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]

yeah, in fact I have it already :D

[Filippo A. E. Nuccio]

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]

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

[Anne Baanen]

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

[Filippo A. E. Nuccio]

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

[Kevin Buzzard]

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]

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]

#tpil is a good introduction to term mode.

[Filippo A. E. Nuccio]

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]

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]

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]

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

[Scott Morrison]

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]

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]

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]

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]

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

[Kevin Buzzard]

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]

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.