Timeline for Strong induction on ℕ with function α → ℕ
Current License: CC BY-SA 4.0
16 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| May 16, 2022 at 17:34 | history | edited | Eric♦ |
edited tags
|
|
| Mar 17, 2022 at 12:40 | answer | added | Eric♦ | timeline score: 11 | |
| Mar 15, 2022 at 10:34 | vote | accept | burek | ||
| Mar 15, 2022 at 1:34 | comment | added | KANG Rongji | Ohhh... I see... | |
| Mar 14, 2022 at 23:03 | answer | added | Andrej Bauer | timeline score: 9 | |
| Mar 14, 2022 at 22:33 | history | edited | Andrej Bauer | CC BY-SA 4.0 |
added 9 characters in body
|
| Mar 14, 2022 at 19:59 | history | edited | taylor.2317 | CC BY-SA 4.0 |
deleted 17 characters in body
|
| Mar 14, 2022 at 18:55 | comment | added | burek |
@KANG Rongji I do have that, since f a : ℕ, so we can use cases on nat, the problem is then I don't get the inductive hypothesis I want.
|
|
| Mar 14, 2022 at 18:52 | comment | added | burek |
I also have that, I can get P a given P b i.e. ind gives me a b s.t. f b < f a and a function P b -> P a , but my assumption doesn't give me P b. That's why I want to use induction on ℕ somehow.
|
|
| Mar 14, 2022 at 17:46 | comment | added | KANG Rongji |
P.S. By + I mean the sum type. I am not sure what symbol Lean uses.
|
|
| Mar 14, 2022 at 17:44 | comment | added | KANG Rongji |
Add (∀ a : α, f a = 0 + f a > 0) in your definition of foo. Then pattern match on case. You should provide some term of type ∀ n : ℕ, n = 0 + n > 0.
|
|
| Mar 14, 2022 at 17:00 | comment | added | Rupert Swarbrick |
Well, that hypothesis doesn't give you an inductive step: you still need something that says how to get P a out of P b when f b < f a.
|
|
| Mar 14, 2022 at 16:41 | history | edited | burek | CC BY-SA 4.0 |
Fixed `ind` term bases on comment
|
| Mar 14, 2022 at 16:39 | comment | added | burek |
Aha sorry, I actually wrote it incorrectly, the ind term should actually be something like (ind : ∀ a : α, f a > 0 → ∃ b : α, f b < f a). But I don't apriori know that P b. I fixed it in the question. Perhaps ind is not the best name for this term.
|
|
| Mar 14, 2022 at 16:30 | comment | added | Rupert Swarbrick |
Your ind term looks a bit odd to me. I would have expected the "exists" term to be something like (∀ b, f b < f a -> P b). Your term says that there exists some b such that P b.
|
|
| Mar 14, 2022 at 16:23 | history | asked | burek | CC BY-SA 4.0 |