Mechanics of Proof 1.4

Stream: new members

[Adam Millar]

Hello!
I am rather new/rusty when it comes to LEAN and Zulip, so if there are better ways or threads to share my questions/code/work, please let me know.

I am working through the first chapter of Heather MacBeth's book Mechanics of Proof, and I am beginning to doubt my understanding of the LEAN infoview and the tactic state.

For this exercise:
image.png

I produced the following LEAN proof:
image.png

So far, I have been relying on the tactic state to 'check' whether LEAN agrees that the given justification (tactic?) suffices to deduce my conclusion on the RHS.
If I see 'No Goals,' I interpret that as meaning that LEAN can produce a valid deduction, in this case using the rel rule and the stated hypotheses.
If I see any error, it means the hypotheses are insufficient or the rule is inappropriate.

When I constructed the first line manually, to see which hypotheses were necessary, I did;
image.png

Where h6 and h7 are necessary to justify the steps

$y \leq B$
$\Downarrow$
$uy \leq uB$

and

$x \leq B$
$\Downarrow$
$vx \leq vB$

Respectively, are they not? Otherwise we cannot guarantee that the direction of $\leq$ does not flip.

So, in my manual solution, I had the first line in the calc justified := by rel [h4,h5,h6,h7]
But the infoview showed that the goal was closed after only [h4,h5]!

I'm asking for a bit of guidance as to where exactly my misunderstanding lies.
Am I just forgetting facts about inequalities?
Am I mistaken in thinking that all hypotheses should be used?
How should I be using the LEAN infoview to guide my derivations?
Where are the errors in my manual derivation or the LEAN derivation?

I appreciate any time you are willing to devote to address my questions, and I am happy to clarify any point I made.

[Kyle Miller]

I think the deal is that the rel tactic tries to automatically prove side conditions using positivity, which can make use of hypotheses like h6 and h7 by itself. You could try by clear h6 h7; rel [h4, h5] to check whether h6 and h7 are necessary for the rel tactic to succeed.

[Kyle Miller]

That's just one experiment I thought of, but there are other techniques to see whether a particular hypotheses was used inside a particular tactic proof too.

[Kyle Miller]

Generally speaking, assuming your source is syntactically correct, and you don't see any errors (indicated by red squiggles in the source text), if your cursor is right after a particular tactic then if you see "No Goals" in the Infoview you know that the tactic has solved the goals.

[Adam Millar]

Kyle Miller said:

clear h6 h7; rel [h4, h5]

Thank you for your response!
I tried the by clear h6 h7; rel [h4, h5] as you suggested and it did cause the error you indicated, so yes the hypotheses are necessary.
I'm interested in the pedagogical uses of LEAN and the goals of this book, so it's fascinating to see places where, on the one hand, we want the 'rigor' of knowing that all of our hypotheses are necessary, at the same time as the brevity of LEAN performing some 'trivial' or 'obvious' derivations 'under the hood' and out of sight.

[Patrick Massot]

This is a very well-known challenge of using a proof assistant for teaching. We want the proof assistant to do automatically what we wouldn’t want students to explain on paper. But this is extremely poorly specified (and also non-trivial to implement).

[Adam Millar]

Patrick Massot said:

This is a very well-known challenge of using a proof assistant for teaching. We want the proof assistant to do automatically what we wouldn’t want students to explain on paper. But this is extremely poorly specified (and also non-trivial to implement).

Poorly specified AND prone to change.
Early in a topic I may want to emphasize that small details are technically necessary to draw valid deductions.
Later I will say that, in many cases, we don't need exhaustive derivations; the level of rigor will change.
Once we've seen that it is technically necessary, we can acknowledge that full rigor would waste time or miss the point.
I'm curious then, how choices are made about which things LEAN does 'automatically,' and what this would look like from a student's perspective.

[Adam Millar]

For instance, in this book, we use ring for Z, Q, and R, and while I am curious about, for each exercise, why in this case the variables need only be integers, while in another they must be rationals, depending on which ring properties are necessary, I feel to a student who as never encountered the notion of a ring will see things like n : ℤ as essentially arbitrary

[Kyle Miller]

Heather's made her own dialect of Lean for this book, taking into account pedagogical aspects of learning to prove things. You can look around in the project directory for some explanations. For example, the constructor tactic is restricted to only work with certain types.

For "production grade" Lean, instead tactics are designed to get things done. If there's a pedagogical aspect, it's centered around learning what tactics do, not around learning how to prove things. Lots of tactics will incorporate some extra reasoning if it's not algorithmically expensive to do so (for example, positivity finding all the relevant hypotheses automatically, rather than requiring that they be specified by the user).

[Patrick Massot]

Adam, you may also be interested in https://github.com/PatrickMassot/verbose-lean4/blob/master/README.md. Among other things, this library allows some automation tuning.

[Heather Macbeth]

@Adam Millar My personal approach to teaching this point (the necessity of positivity side conditions in inequality calculations) is:

1. teach the naive calculus of "substitution" of inequalities, like in Examples 1.4.1-4, then
2. give some trickier examples, like Example 1.4.5, which tempt students to make "wrong" substitutions, and let the fact that rel fails here alert students to the subtlety.

Have you been looking at the HTML text of the book as well as the Lean files? There are several discussions of this point about positivity side conditions (in Example 1.4.1, 1.4.2, 1.4.4, 1.4.5).

[Adam Millar]

[Quoting…]

@Patrick Massot thank you for your reply.
I like this resource, and how it streamlines investigating exactly what tactics do.
I also like the name, as I know I lean toward the exhaustive, verbose side of constructing proofs.
I confess to being unsure exactly how to implement it though.
I have been working just in the gitpod environment where I've loaded Heather's book and LEAN itself.
How exactly would I add the Verbose LEAN Library?

[Patrick Massot]

You can create your own Lean project that uses the library. Currently there is no full course using the Lean 4 version of this library.

[Adam Millar]

Heather Macbeth said:

Adam Millar My personal approach to teaching this point (the necessity of positivity side conditions in inequality calculations) is:

1. teach the naive calculus of "substitution" of inequalities, like in Examples 1.4.1-4, then
2. give some trickier examples, like Example 1.4.5, which tempt students to make "wrong" substitutions, and let the fact that rel fails here alert students to the subtlety.

Have you been looking at the HTML text of the book as well as the Lean files? There are several discussions of this point about positivity side conditions (in Example 1.4.1, 1.4.2, 1.4.4, 1.4.5).

@Heather Macbeth
Thank you for your reply!
Yes, I have been reading along with the HTML file.
I'm trying my best to mimic the student experience you outline in the Preface, with one window for the textbook, one for gitpod running the repository with LEAN, and my own handwritten versions of the proofs.

I realize that my goals for learning more about LEAN have a slight tension with your stated goal that "most of your intellectual effort in solving the problems will be devoted to the mathematics, not to Lean’s implementation details or quirks of syntax."
But the book, and discussions like this about your choices, are certainly excellent resources for seeing how a theorem prover can part of a course.

One obstacle I think I have to seeing how the course meets that goal is that I don't have the the 25mins of blackboard instruction you mention being part of the typical lesson for the course.

My guess is that you follow the same kind of narrative about transitioning from equational reasoning to inequalities, all manually.
You solve a few (1.4.1, 1.4.2) that can be solved naively.
Is the idea that you demonstrate, before using LEAN at all, that the naive approach can lead to mistakes, and then show how LEAN can help us catch these mistakes?
As you say for 1.4.6 "Also try writing out the incorrect solution in Lean, and check that Lean complains."

Regarding my difficulty with 1.4.4, re-reading your discussing under the solution, is the idea here that while h6 and h7 (the non-negativity of u and v) must be part of the context for the calculation, LEAN aligns with the typical mathematical practice of omitting reference to these 'obvious' facts by making use of them 'silently.'
That is, we need not reference them explicitly as a hypothesis for rel?

[Patrick Massot]

If you want to play in GitPod, I added the necessary setup. So you can go to https://gitpod.io/new/#https://github.com/patrickmassot/verbose-lean4 and use the file explorer to open Verbose/English/Examples.lean if you want to play a bit.

[Heather Macbeth]

Adam Millar said:

My guess is that you follow the same kind of narrative about transitioning from equational reasoning to inequalities, all manually.
You solve a few (1.4.1, 1.4.2) that can be solved naively.
Is the idea that you demonstrate, before using LEAN at all, that the naive approach can lead to mistakes, and then show how LEAN can help us catch these mistakes?
As you say for 1.4.6 "Also try writing out the incorrect solution in Lean, and check that Lean complains."

Yes, that's right!

[Heather Macbeth]

Adam Millar said:

Regarding my difficulty with 1.4.4

is the idea here that while h6 and h7 (the non-negativity of u and v) must be part of the context for the calculation, LEAN aligns with the typical mathematical practice of omitting reference to these 'obvious' facts by making use of them 'silently.'
That is, we need not reference them explicitly as a hypothesis for rel?

Yes, that's right. Although as Kyle noted above, it's wrong to say that "Lean" does this. Rather, the particular Lean libraries and Lean configuration options in my course repository do this, because I set them up to follow my own pedagogical preferences on this point.

Off-the-shelf Lean with no libraries requres more input from the user in this situation. And mainstream Mathlib-style Lean requires less input from the user! (See the description of the tactic gcongr in the appendix to my book.)

[Heather Macbeth]

You might like to try the following experiment: change rel [h4, h5] to show_term rel [h4, h5], then look at the output in the infoview (the panel on the right). You'll see the "term" that rel [h4, h5] is constructing (which indeed involves h6 and h7):

add_le_add_right
  (add_le_add
    (mul_le_mul_of_nonneg_left h5
      (le_trans (Mathlib.Meta.Positivity.nonneg_of_isNat (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_zero)) h6))
    (mul_le_mul_of_nonneg_left h4
      (le_trans (Mathlib.Meta.Positivity.nonneg_of_isNat (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_zero)) h7)))
  (u * v)