# Questions tagged [natural-numbers]

For question about natural numbers $\Bbb N$, their properties and applications

14 questions
Filter by
Sorted by
Tagged with
184 views

### What is the well-established η law for naturals?

Notation. means a general equality. Well, $η$ laws are usually judgmental, but sometimes we provide $η$ laws as theorems. To me $η$ rules are like vibes, because ...
• 6,186
130 views

### Implementing and verifying algorithms for solving equations in Lean

In computer algebra systems, one can enter an equation and ask for integer solutions. Sometimes it is solved. But the output is not guaranteed to be correct. In Lean, one can formalize the solutions ...
• 33
242 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, ...
• 161
129 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 ...
63 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: ...
• 227
1 vote
64 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: ...
114 views

### Help with strong induction

I have the following definition of divisibility by 3. ...
1 vote
84 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
832 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
102 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: ...
400 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, ...
• 547
145 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 vote
620 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