Skip to main content

Questions tagged [natural-numbers]

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

Filter by
Sorted by
Tagged with
3 votes
1 answer

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 ...
ice1000's user avatar
  • 6,186
3 votes
1 answer

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 ...
Bogdan's user avatar
  • 33
2 votes
1 answer

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
  • 161
2 votes
2 answers

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

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

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

Help with strong induction

I have the following definition of divisibility by 3. ...
deleted_user0972's user avatar
1 vote
1 answer

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

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

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
10 votes
1 answer

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
  • 547
3 votes
1 answer

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

Strong induction for nat in Coq

I'm doing some exercises on Coq and trying to prove the strong induction principle for nat: ...
Pavel Snopov's user avatar
13 votes
1 answer

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