All Questions
Tagged with coq proof-review
8
questions
2
votes
2
answers
84
views
Code Review: $\mathbb{Z}[\sqrt{-2}]$ is an integral domain
I proved that $\mathbb{Z}[\sqrt{-2}]$ is an integral domain; I would like a review of this proof.
My by hand argument is in Appendix A. It is not the original argument I used. I made a stupid mistake ...
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:
...
1
vote
1
answer
648
views
Strong induction for nat in Coq
I'm doing some exercises on Coq and trying to prove the strong induction principle for nat:
...
2
votes
1
answer
247
views
Axiomization of Peano arithmetic in constructive first-order logic
I've been playing with axiomising systems of first-order logic in Coq. I've started to develop the beginning of a framework. As an example I give a minimal phrasing of Peano arithmetic in Coq in the ...
6
votes
2
answers
274
views
Problem proving a binary add function
I'm fairly new to the Coq language and I want to prove a function that does an binary add from numbers represented as a list (least significant bit upfront).
I have created this badd function that ...
3
votes
1
answer
175
views
Code Review: Proving that a simple propositional logic satisfies Aristotle's Thesis
I'm proving that a simple propositional logic satisfies Aristotle's thesis.
I'm curious how to improve the code in question.
Here are the things I know that are wrong with it:
I'm using ...
5
votes
1
answer
173
views
How to implement first-order relational structures in Coq?
I'm trying to define a first-order relational structure in Coq.
I have a way to define a pre-first-order-relational-structure, which is not a standard notion, but seems simple enough.
I also have a ...
4
votes
2
answers
120
views
Proof Review: Basic theorem about ternary relations in Coq
I'm proving a simple fact about ternary relations in Coq as an exercise.
I'm interested in ternary relations at the moment because they are a simple thing that can represent a finitary consequence ...