7
votes
Accepted
5
votes
Accepted
How to show in type theory (like in a proof assistant) that finite sets of different cardinalities are not isomorphic?
This is called the Pigeonhole Principle. In a weak form it says that there is no injection from Fin (n+1) to Fin n. In a ...
5
votes
Counting in two ways
I see the work on Combinatorial Species as being a vast generalization of that. The various series associated to a species give you different kinds of ways of counting.
The example worked out in full ...
- 429
4
votes
Accepted
Proving a disjunction without left nor right in Coq
The statement you are trying to prove is true classically but not intuitionistically, so proving it needs some classical law, either as an explicit assumption to the theorem or as an axiom.
Here is ...
- 596
4
votes
Examples of theories where tactic language is required for simple proofs
so far I do not see any reasons why the same reasoning would not work for the rest of SF
Wait for (or jump straight to) at least https://softwarefoundations.cis.upenn.edu/slf-current/Rules.html ;)
3. ...
- 704
4
votes
How do I prove a record related lemma?
Remember that a records is syntactic sugar for an inductive with one constructor. Your record is mostly equivalent to:
...
- 381
4
votes
Counting in two ways
Here's a connection with some existing work in type theory. Consider this inductive type, whose values are meant to correspond to finite subtypes of an $n$-valued type:
...
- 1,002
4
votes
Accepted
Counting in two ways
One lesson may be that not all proofs are meant to be formalized. The gap between an informal proof and a formal proof is often substantial, and you could reasonably treat this as an extreme instance ...
- 2,242
3
votes
How to show in type theory (like in a proof assistant) that finite sets of different cardinalities are not isomorphic?
This is essentially the pigeonhole principle. If $m < n$, then $f : \mathsf{Fin}\ n → \mathsf{Fin}\ m$ takes two distinct values to the same value, meaning it cannot be an equivalence. This can ...
- 1,002
3
votes
Proving strict positivity in Agda
Are there any techniques that could allow formalizing this argument?
Beluga has a notion of 'stratified types' that corresponds to this type of construction. From the user manual:
We distinguish ...
- 1,264
3
votes
Accepted
Can some existing proof assistant, in its current state of the art, encode this small theory about a twin prime counting function?
First, any modern proof assistant should be able to encode these lemmas, but it will be easier if the relevant definitions and background theory are already in the proof assistant.
I'm not an expert ...
- 10.3k
2
votes
How to write this non-constructive proof in Lean?
I eventually managed to write a proof (execute here).
What I was looking for was essentially the tactic by_cases for cases disjunction.
It is also longer than I ...
- 313
1
vote
İnduction/inversion and others in coq
Intuitively induction is for reasoning about all possible values of an inductive type. Inversion is reasoning about a particular « shape » of a term of an inductive type.
For instance if you have a ...
- 381
1
vote
Proving strict positivity in Agda
Here's a solution, that I have been making progress with, that fits normal Agda.
The aim of defining a type via induction, yet allowing non-obviously decreasing argument in a negative position can be ...
- 547
Only top scored, non community-wiki answers of a minimum length are eligible