All Questions
4
questions
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 ...