Questions tagged [natural-numbers]
For question about natural numbers $\Bbb N$, their properties and applications
12
questions
2
votes
1
answer
97
views
How to Prove Theorem le_zero in Lean4: If x ≤ 0, then x = 0?
I am playing the Natural Number Game found here and am trying to prove a theorem in Lean4. The theorem states that if a natural number x is less than or equal to 0, ...
- 141
2
votes
2
answers
113
views
Proving that a minimum example exists if any example exists in nat
I'm trying to prove that if a function from nat -> bool is true for any natural number, then there exists a minimum natural number which the function is true for.
I've been trying to find a good ...
- 125
0
votes
1
answer
44
views
proof-based Pos type class
I'm working my way through the chapter on type classes in Functional Programming in Lean. The text demonstrates type-classes by representing positive numbers this way:
...
- 197
1
vote
0
answers
58
views
Injectivity, Surjectivity and Smallness on lists of natural numbers imply each other
Require Import Coq.Lists.List.
I have the following properties defined on a list of natural numbers:
...
- 1,241
-2
votes
2
answers
78
views
Help with strong induction
I have the following definition of divisibility by 3.
...
1
vote
1
answer
77
views
Is every type-theoretic function ℕ → A extensionally equal to one written in terms of the ℕ-eliminator
In Category Theory the Natural Numbers object ℕ has the universal mapping-out property that tells us how to build arrows out of ℕ into an arbitrary object A. But it doesn't say that every arrow ...
- 345
3
votes
1
answer
409
views
Using the contrapositive in lean 4
I'm trying to learn lean (version 4) by proving some basic facts about the natural numbers. Please feel free to critique my code if you see have general comments, but I also have a specific question ...
- 133
4
votes
2
answers
91
views
How do I approach the final step in proving the cancellation law in Coq?
I'm trying to prove the cancellation law for natural numbers. This is my proof so far:
...
- 155
7
votes
1
answer
288
views
Can you build W-types out of natural numbers predicatively?
I understand that we can use W-types to encode natural numbers and a wide variety of other inductive types in intensional MLTT. Can we encode W-types using only natural numbers within type theory, ...
- 517
3
votes
1
answer
143
views
Proof by Exhaustive Computation for small initial segment of natural numbers (in Coq)
I have two functions f, g : nat -> nat. Let's pretend that f and g are cheap to compute.
...
- 1,241
1
vote
1
answer
411
views
Strong induction for nat in Coq
I'm doing some exercises on Coq and trying to prove the strong induction principle for nat:
...
- 195
13
votes
1
answer
275
views
Does the canonicity of natural number imply that of all types?
I've heard about a folklore claim that
If all terms of ℕ are literals, all closed terms admit canonical form.
In MLTT-style type theories.
I am assured that it's true for Bool if one also assumes ...
- 660