Questions tagged [natural-numbers]

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

Filter by
Sorted by
Tagged with
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, ...
Rainb's user avatar
  • 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 ...
Tony Peterson's user avatar
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: ...
Nate Glenn's user avatar
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: ...
Agnishom Chattopadhyay's user avatar
-2 votes
2 answers
78 views

Help with strong induction

I have the following definition of divisibility by 3. ...
deleted_user0972's user avatar
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 ...
Russoul's user avatar
  • 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 ...
Jack Maloney's user avatar
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: ...
Charles Averill's user avatar
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, ...
Ilk's user avatar
  • 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. ...
Agnishom Chattopadhyay's user avatar
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: ...
Paul Snopov's user avatar
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 ...
KANG Rongji's user avatar