All Questions
Tagged with coq definition
5
questions
2
votes
1
answer
78
views
Packaging Mathematical Structures in Coq: Help Understanding a Definition
Context
I am a relatively new user to Coq with a decent understanding of the basics of dependent type theory and am midway through chapter 2 of the Software Foundations Series of books. I want to ...
- 133
2
votes
1
answer
150
views
Is there a way to rename parameters when including/reusing a module type in Coq?
Say I have a (more general) module type Collection that specifies some operations like read and write and now I want to create (more specialized) module types like <...
- 121
1
vote
2
answers
100
views
Defining a Recursive Function decreasing on one argument with < and another structurally
I want to define a function which decreases in one argument using < and on another structurally. What is the least painful way to do this? Among the many options (Function, Program Fixpoint, ...
- 1,502
0
votes
1
answer
83
views
Define a function using another function
I want to define a translation function g from another function f.
Definition trans (f g : Q -> Q) (t : Q) :=
forall q : Q, f (q + t) == g q.
In the above code,...
- 387
4
votes
2
answers
209
views
Coq defining a hierarchy of collections of integers with infinitely many "levels"
I'm trying to formalize a small part of higher-order arithmetic in Coq as an exercise (Wikipedia article for second-order arithmetic).
It's straightforward to formalize something resembling second-...
- 3,073