## Stream: new members

### Topic: Recursively prove

#### AHan (Nov 03 2018 at 08:19):

Sorry, this might seems to be stupid, but I just can't figure out how to prove the problem inductively....

lemma add_nat_ge_self {a : ℕ} (b : ℕ) : a + b ≥ b := match b with | 0 := begin simp, apply nat.zero_le end | succ n := sorry

#### Mario Carneiro (Nov 03 2018 at 09:40):

In lean we write inductive definitions by pattern matching in the definition itself, not using match blocks like coq

#### Mario Carneiro (Nov 03 2018 at 09:41):

lemma add_nat_ge_self {a :  ℕ} : ∀(b : ℕ), a + b ≥ b
| 0 := begin simp, apply nat.zero_le end
| (succ n) := sorry


#### Mario Carneiro (Nov 03 2018 at 09:42):

at the sorry you should now have access to add_nat_ge_self which you can apply recursively

#### Bryan Gin-ge Chen (Nov 03 2018 at 13:37):

What Mario wrote is cleaner but I want to point out that the following is probably what you were going for:

lemma add_nat_ge_self {a :  ℕ} (b : ℕ) : a + b ≥ b :=
match a, b with
| a, 0 := begin simp, apply nat.zero_le end
| a, (nat.succ n) := sorry
end


#### Mario Carneiro (Nov 03 2018 at 13:39):

well if you write it like that you won't be able to fill in the sorry because you don't have access to the recursive function

#### Bryan Gin-ge Chen (Nov 03 2018 at 13:54):

It's there, but it gets a funny name:

lemma add_nat_ge_self {a :  ℕ} (b : ℕ) : a + b ≥ b :=
match a, b with
| a, 0 := begin simp, apply nat.zero_le end
| a, (nat.succ n) := begin
refine nat.succ_le_succ _,
exact _match a n
end
end


#### Bryan Gin-ge Chen (Nov 03 2018 at 14:02):

And I guess you only get access to it if you go into tactic mode; i.e. I can't remove the by exact below:

lemma add_nat_ge_self {a :  ℕ} (b : ℕ) : a + b ≥ b :=
match a, b with
| a, 0 := begin simp, apply nat.zero_le end
| a, (nat.succ n) := nat.succ_le_succ (by exact _match a n)
end


#### AHan (Nov 04 2018 at 03:59):

Oh!! Thanks a lot for the explanation!!

Last updated: May 08 2021 at 05:14 UTC