Questions tagged [natural-numbers]
For question about natural numbers $\Bbb N$, their properties and applications
15
questions
1
vote
1
answer
65
views
Lean4: Prove that ∑ ii : Fin nn, k (Fin.castLE _ ↑↑ii) = ∑ x : Fin nn, k (Fin.castLE _ ↑↑x) (sums over Fin n)
Im working with sums over Fin n for some n : Nat, and I am stuck with two sums, that should be equal (and look exactly equal in ...
- 13
3
votes
1
answer
186
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,306
3
votes
1
answer
146
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
2
votes
1
answer
274
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
2
votes
2
answers
133
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
65
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:
...
- 237
1
vote
0
answers
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:
...
- 1,502
-2
votes
2
answers
118
views
Help with strong induction
I have the following definition of divisibility by 3.
...
1
vote
1
answer
85
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
915
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
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:
...
- 209
10
votes
1
answer
408
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
3
votes
1
answer
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,502
1
vote
1
answer
643
views
Strong induction for nat in Coq
I'm doing some exercises on Coq and trying to prove the strong induction principle for nat:
...
- 205
13
votes
1
answer
307
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 ...
- 680