indent after have

Stream: lean4

[Chris Lovett]

What does the indent after the have mean in this lean3 proof? If I try this in lean4 I get syntax error expected '|' ? If I remove the indent then I get the error (it seems the indent is not required in lean3)...

type mismatch
  add_lt_add_right (succ e * a) (succ e * b) he ?m.3947
has type
  succ e * a + ?m.3947 < succ e * b + ?m.3947 : Prop
but is expected to have type
  succ e * a + a < succ e * b + b : Prop

The lean3 proof I'm porting:

theorem mul_lt_mul_of_pos_left (a b c : mynat) : a < b → 0 < c → c * a < c * b :=
begin [nat_num_game]
  intro hab,
  intro hc,
  cases c with d,
    exfalso,
    exact lt_irrefl 0 hc,
  clear hc,
  induction d with e he,
    rw [succ_mul,zero_mul, zero_add, succ_mul, zero_mul, zero_add],
    exact hab,
  rw succ_mul,
  rw succ_mul (succ e),
  have h : succ e * a + a < succ e * b + a,
    exact add_lt_add_right _ _ he _,
  apply lt_trans _ _ _ h,
  rw add_comm,
  rw add_comm _ b,
  apply add_lt_add_right,
  assumption
end

For repro see Level 18

[Chris Lovett]

Never mind I just found the have tactic documentation in https://leanprover.github.io/theorem_proving_in_lean4/tactics.html.

So the answer is:

      let h : succ e * a + a < succ e * b + a := by
        exact add_lt_add_right _ _ he _

[Mario Carneiro]

In lean 3, the have tactic has an optional := argument, and if you omit it it produces two goals. In mathlib the first goal is usually surrounded by { }, but some people also just indent the subproof without using the braces (since as we've established they are not strictly necessary).

[Chris Lovett]

Ok, now I have done all of NNG except one last proof. I'm stuck on defining mul_le_mul for lemma le_mul which is defined in lean3 using a calc proof. When I port that to Lean4

lemma mul_le_mul {a b c d : MyNat} (hac : a ≤ c) (hbd : b ≤ d) (nn_b : 0 ≤ b) (nn_c : 0 ≤ c) : a * b ≤ c * d := by
  calc
    a * b ≤ c * b := by apply mul_le_mul_of_nonneg_right hac nn_b
    _ ≤ c * d := by apply mul_le_mul_of_nonneg_left hbd nn_c

I'm getting an error:

invalid 'calc' step, failed to synthesize `Trans` instance
  Trans LE.le LE.le ?m.4473

So what type instance do I need to create for calc to be happy? I see these instances in the prelude:

instance (r : α → γ → Sort u) : Trans Eq r r where
  trans heq h' := heq ▸ h'

instance (r : α → β → Sort u) : Trans r Eq r where
  trans h' heq := heq ▸ h'

but it seems to be looking for a Trans on LE.le (rather than on Eq) , and I don't know how to make that work with my custom MyNat type? I already have this but it didn't help:

instance : LE MyNat where
  le := MyNat.le

[Mario Carneiro]

It says - you need an instance of the form Trans LE.le LE.le ?m.4473

[Mario Carneiro]

also relevant is that those LE.le applications are over MyNat (if you hover over the error message you should be able to see this)

[Chris Lovett]

Ah, thanks for the hint, I just found these in mathlibe Order.lean:

instance : @Trans α α α LE.le LE.le LE.le := ⟨le_trans⟩
instance : @Trans α α α LT.lt LE.le LT.lt := ⟨lt_of_lt_of_le⟩
instance : @Trans α α α LE.le LT.lt LT.lt := ⟨lt_of_le_of_lt⟩

yikes, sorting through all this now...

[Mario Carneiro]

Basically, calc sees that you have given it two proofs, of R x y and S y z for some relations R and S, and we're asking it to prove T x z for some relation T not provided. So it uses those instances to say "how can I combine a proof of R and a proof of S, what relation does the transitive thing have?" And that's exactly what the instance says. You just have to give it your proof of MyNat.le_trans and then calc can use it

[Mario Carneiro]

that way you can write things like

calc
  x < y := sorry
  y <= z := sorry
  z = w := sorry

and it somehow is able to figure out that this is supposed to be a proof of x < w

[Chris Lovett]

Ok, I think I made some progress, the NNG was dependent on level 5 doing this instance which I had commented out:

instance : preorder mynat := by structure_helper

so I've replaced this with

instance : Preorder MyNat :=
  ⟨le_refl_mynat, le_trans, lt⟩

and now I'm getting a different error from the calc proof, it doesn't like my hac and hbd terms:

image.png

but they were ported directly from the lean3 versions and work:

theorem mul_le_mul_of_nonneg_left (a b c : MyNat) : a ≤ b → 0 ≤ c → c * a ≤ c * b := by
  intro hab
  intro h0
  cases hab with
  | _ d hd =>
    rw [hd]
    rw [mul_add]
    use c * d

theorem mul_le_mul_of_nonneg_right (a b c : MyNat) : a ≤ b → 0 ≤ c → a * c ≤ b * c := by
  intro hab
  intro h0
  rw [mul_comm]
  rw [mul_comm b]
  apply mul_le_mul_of_nonneg_left
  assumption
  assumption

I get this error:

application type mismatch
  mul_le_mul_of_nonneg_right hac
argument
  hac
has type
  a ≤ c : Prop
but is expected to have type
  MyNat : Type

I found the Nat.mul_le_mul theorem which is completely different, so I'm trying that route, but it appears I need to boot up a huge chunk of theorems on MyNat for that to work...

[Mario Carneiro]

You have explicit arguments in mul_le_mul_of_nonneg_left; NNG probably uses implicit arguments {a b c : MyNat}

[Chris Lovett]

Nope, I ported it as directly as possible, and NNG lean3 has

theorem mul_le_mul_of_nonneg_left (a b c : mynat) : a ≤ b → 0 ≤ c → c * a ≤ c * b :=
begin [nat_num_game]
  intro hab,
  intro h0,
  cases hab with d hd,
  rw hd,
  rw mul_add,
  use c * d,
  refl
end

[Mario Carneiro]

Is it actually using that theorem?

[Mario Carneiro]

there is another theorem with that name in core lean

[Mario Carneiro]

what does the theorem you are currently porting look like in lean 3?

[Chris Lovett]

It's in the same file, but there is this intermediate thing, does this change the game?

instance : ordered_semiring mynat :=
{ mul_le_mul_of_nonneg_left := mul_le_mul_of_nonneg_left,
  mul_le_mul_of_nonneg_right := mul_le_mul_of_nonneg_right,
  mul_lt_mul_of_pos_left := mul_lt_mul_of_pos_left,
  mul_lt_mul_of_pos_right := mul_lt_mul_of_pos_right,
  ..mynat.semiring,
  ..mynat.ordered_cancel_comm_monoid
}

and the lean3 proof I'm porting is this one from level18a

lemma le_mul (a b c d : mynat) : a ≤ b → c ≤ d → a * c ≤ b * d :=
begin [nat_num_game]
intros hab hcd,
cases a with t Ht,
  rw [zero_mul],
  apply zero_le,
have cz : 0 ≤ c,
  apply zero_le,
have bz : 0 ≤ b,
  apply zero_le,
apply mul_le_mul hab hcd cz bz,
end

[Mario Carneiro]

yes, instances are something to pay attention to

[Mario Carneiro]

and indeed it explains the behavior - ordered_semiring is the typeclass that would make the mul_le_mul_of_nonneg_left lemma from core work on mynat

[Mario Carneiro]

That's not going to work in lean 4 until sufficiently much of mathlib4 is ported

[Chris Lovett]

Oh, and the mathlib3 implementation of mu_le_mul is more general it operates on any alpha, whereas I fixed mine to MyNat...

lemma mul_le_mul {a b c d : α} (hac : a ≤ c) (hbd : b ≤ d) (nn_b : 0 ≤ b) (nn_c : 0 ≤ c) : a * b ≤ c * d :=
calc
  a * b ≤ c * b : mul_le_mul_of_nonneg_right hac nn_b
    ... ≤ c * d : mul_le_mul_of_nonneg_left hbd nn_c

[Mario Carneiro]

but the easy solution in your case is just to make the arguments implicit or use _ _ _ in the theorem application

[Mario Carneiro]

right, that instance is saying that since you proved some basic facts about <= and *, a whole bunch of other facts follow from that like mul_le_mul

[Mario Carneiro]

You won't be able to use the typeclass or suite of theorems since they don't exist yet in lean 4, but hopefully NNG isn't making too much use of them? It's basically cheating from the NNG perspective

[Chris Lovett]

yeah, I thought so, when F12 jumped to Ordered_ring.lean which is the same name as that instance ordered_semiring. But I figured I could cheat and jump straight to mul_le_mul, and so long as I could provide that then lemma le_mul should be happy without the full ordered_semiring...

[Mario Carneiro]

it could actually be a mistake in the lean 3 code

[Chris Lovett]

The lean3 level18a.lean compiles with no errors though.

[Chris Lovett]

so perhaps I'd be better off giving up on mul_le_mul and find another way to complete lemma le_mul...

[Chris Lovett]

I have this to complete:
image.png

[Mario Carneiro]

You should be able to prove mul_le_mul exactly the way it was done in ordered_ring.lean

[Mario Carneiro]

it's just transitivity on mul_le_mul_of_nonneg_right and mul_le_mul_of_nonneg_left

[Mario Carneiro]

which you must have proved previously since they are inputs to the ordered_ring instance

[Chris Lovett]

That's what I was trying to do with this:

lemma mul_le_mul {a b c d : MyNat} (hac : a ≤ c) (hbd : b ≤ d) (nn_b : 0 ≤ b) (nn_c : 0 ≤ c) : a * b ≤ c * d := by
  calc
    a * b ≤ c * b := by apply mul_le_mul_of_nonneg_right hac nn_c
    _ ≤ c * d := by apply mul_le_mul_of_nonneg_left hbd nn_b

But perhaps I can prove it without using calc and then skip the needs for the Trans instance...

[Mario Carneiro]

Is there a reason you don't want the Trans instance?

[Mario Carneiro]

Note that the Trans LE LE LE instance holds in general for any Preorder so you can hide it in whatever library is defining Preorder

[Mario Carneiro]

the proof without calc just combines those two theorems using le_trans

[Chris Lovett]

Oh, I finally got what you were talking about with _ _ _ and so I'm trying this:

lemma mul_le_mul {a b c d : MyNat} (hac : a ≤ c) (hbd : b ≤ d) (nn_b : 0 ≤ b) (nn_c : 0 ≤ c) : a * b ≤ c * d := by
  calc
    a * b ≤ c * b := mul_le_mul_of_nonneg_right _ _ _ hac nn_c
    _ ≤ c * d := mul_le_mul_of_nonneg_left _ _ _ hbd nn_b

But now it complains about the nn_c term and the nn_b term saying

image.png

[Chris Lovett]

PS: I remember now something about lean3 allowing terms to go unspecified inside a proof making those arguments implicit, but lean4 doesn't allow that.

[Chris Lovett]

Oh hey, I just got it trying random things, turns out I just had to switch the terms for some reason and this works in lean4:

lemma mul_le_mul {a b c d : MyNat} (hac : a ≤ c) (hbd : b ≤ d) (nn_b : 0 ≤ b) (nn_c : 0 ≤ c) : a * b ≤ c * d := by
  calc
    a * b ≤ c * b := mul_le_mul_of_nonneg_right _ _ _ hac nn_b
    _ ≤ c * d := mul_le_mul_of_nonneg_left _ _ _ hbd nn_c

So with that all proofs are ported from NNG :-) (but there's still some todo work items to do with these "instances" which NNG calls collectibles.

[Chris Lovett]

See https://lovettsoftware.com/NaturalNumbers/InequalityWorld/Level18.lean.html, they all work now.

[Mario Carneiro]

turns out I just had to switch the terms for some reason

did you or NNG perhaps interchange the meanings of mul_le_mul_of_nonneg_left and mul_le_mul_of_nonneg_right? It's not really obvious which way around is supposed to be "left"

[Mario Carneiro]

Chris Lovett said:

PS: I remember now something about lean3 allowing terms to go unspecified inside a proof making those arguments implicit, but lean4 doesn't allow that.

not sure what this is a reference to. Perhaps the fact that refine foo _ doesn't work where refine' foo _ does?

[Chris Lovett]

No the reason I needed to add the _ _ _ in mul_le_mul_of_nonneg_right _ _ _ hac nn_b but it was not needed in lean3 version.

[Chris Lovett]

Never mind, somehow in my messing around I must have switched them or mistyped them or something, the lean3 semiring has them in the same order with

lemma mul_le_mul {a b c d : α} (hac : a ≤ c) (hbd : b ≤ d) (nn_b : 0 ≤ b) (nn_c : 0 ≤ c) : a * b ≤ c * d :=
calc
  a * b ≤ c * b : mul_le_mul_of_nonneg_right hac nn_b
    ... ≤ c * d : mul_le_mul_of_nonneg_left hbd nn_c

we we're all good now.

[Mario Carneiro]

Chris Lovett said:

No the reason I needed to add the _ _ _ in mul_le_mul_of_nonneg_right _ _ _ hac nn_b but it was not needed in lean3 version.

The reason you needed to add that is because in your version of the theorem the a b c arguments are in () binders. In the lean 3 version (in the ordered_ring.lean file, not in NNG since the NNG is referencing the version from ordered_ring.lean) they are in {} binders

[Chris Lovett]

Right but in NNG they redefined mul_le_mul_of_nonneg_right the same way I did (because I just ported it from there).

[Kevin Buzzard]

It might be the case that I made up my own binders and it might be the case that the choice of binders changed in lean 3 since I made the game (about three years ago). Binders are something I don't teach.