Mechanics of Proof 2.1

Stream: new members

[Adam Millar]

Thank you again all, for your responses.
I've been able to generate verified deductions (in this course's configuration) for all of the exercises for chapter 1 and have moved on to chapter 2 but am quickly reaching a point where, while I feel I can grasp the structure of the proof, I am not sure enough of the syntax to reflect the proof structure in the code environment.

Previously, the proofs have followed a structure similar to classic two column proofs where the := by serves to separate a claim from its justification.
Now that I can introduce intermediate steps, and multiple goals, the status of my open goals, and where in the code a relevant tactic must be invoked, is becoming increasingly unclear to me.

More concretely, there are just some of the exercises where I feel like I hit a wall when it comes to producing the proof in lean, and I am not sure if it is a result of a gap in my understanding of the relevant mathematics, proof technique, or simply how to implement it in code. :sweat_smile:

Maybe I just need a hint to get back on track.

Here is one that has been vexing me for a while :sweat: ;
image.png

All of my manual proofs keep getting stuck at deriving y = 1 /x

[Ruben Van de Velde]

I'm curious what h1 is supposed to be I can't read

[Ruben Van de Velde]

To prove this statement, I might start by noting we can multiply both sides of the goal by x

[Heather Macbeth]

Maybe a meta-principle to keep in mind is that these chapters are training the user to avoid division wherever possible (replacing it by tricks such as the one suggested by Ruben): division is really painful in Lean (and, I claim, also in careful paper mathematics) because it requires keeping track verbally of the nonzeroness of the denominator.

[Adam Millar]

Ruben Van de Velde said:

I'm curious what h1 is supposed to be I can't read

Thank you for your help.
Multiplying the goal by $x$ gives

$\vdash x * y \leq x * 1$

I am still unsure how to derive this from the hypotheses.
Is this something that can be done in the calc environment? So far the calc environment has felt like the LHS is fixed. That is, I would have to begin from

$$y = _$$ or $$y \leq _$$.

That is, invoking lemmas feels like the only way to modify the LHS as you suggest.
Or is there a lemma I can invoke to update the goal to this?

$$$$

[Kevin Buzzard]

Just to be clear -- you can prove the goal mathematically, right?

The calc environment can be used to prove this goal, I don't know why you want to start with y =, clearly it should start with x * y = because that's the LHS.

[Adam Millar]

I apologize, the final goal of this exercise is that $y \leq 1$

[Adam Millar]

I am going to prove it by hand again

[Heather Macbeth]

Adam Millar said:

Multiplying the goal by $x$ gives

$\vdash x * y \leq x * 1$

I am still unsure how to derive this from the hypotheses.

You can use a structure like:

have H : x * y ≤ x * 1 := by
  sorry -- main proof here
cancel x at H

[Notification Bot]

9 messages were moved here from #new members > Mechanics of Proof 1.4 by Heather Macbeth.