Advanced Addition World - Level 10 and 11

[miguel-negrao]

The text in level 11 says "We just proved add_left_eq_zero (a b : mynat) : a + b = 0 → b = 0. " but actually the theorem in level 10 is "add_left_eq_zero {{a b : mynat}} (H : a + b = 0) : b = 0".

Also, the fact that add_left_eq_zero is not an implication but has the premise as an "argument?" left me confused, I don't think I had seen this before ? I think a theorem which has an hypothesis as argument needs to be explained ? I don't think I can use "apply" on add_left_eq_zero, right ?

[kbuzzard]

variables (P Q : Prop)

def example1 (hP : P) : Q := sorry
def example2 : P → Q := sorry

example : example1 = example2 := rfl -- they're the same

[miguel-negrao]

Ah, ok, that wasn't clear, thanks ! In any case it's worth checking if this is explained before somewhere on the text.

But then I get stuck I believe on the implicit parameters:

intro h,
rw add_comm a b at h,
apply add_left_eq_zero,

gives

2 goals
a b : mynat,
h : b + a = 0
⊢ ?m_1 + a = 0

a b : mynat,
h : b + a = 0
⊢ mynat

I was able to solve it reading about implicit parameters in lean's manual:

intro h,
rw add_comm a b at h,
apply @add_left_eq_zero b a,
exact h,

edit: Ah, actually it also works if I ignore the problem and continue anyway since that term is not needed after:

intro h,
rw add_comm a b at h,
apply add_left_eq_zero,
exact h,