Zulip Chat Archive

Stream: new members

Topic: Recursively prove


view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip AHan (Nov 04 2018 at 03:59):

Oh!! Thanks a lot for the explanation!!


Last updated: May 08 2021 at 05:14 UTC