Recursively prove

Stream: new members

[AHan]

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]

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

[Mario Carneiro]

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

[Mario Carneiro]

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

[Bryan Gin-ge Chen]

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]

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]

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]

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]

Oh!! Thanks a lot for the explanation!!