Questions tagged [coq]
Coq is a formal proof management system. It is often referred to as a proof assistant.
322
questions
2
votes
0
answers
59
views
2
votes
2
answers
112
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 ...
- 3,095
1
vote
1
answer
64
views
Prove that a function's result cannot dependent on Prop-valued parameters in Coq
Consider the following function elem and the lemma that the result of elem does not depend on the proof of ...
- 167
2
votes
3
answers
247
views
Uniqueness of proofs for inductively defined predicates
In Init/Peano.v the less-than-or-equal predicate is defined as follows:
...
- 127
0
votes
0
answers
41
views
Found no matching subterm in goal while it does seem to be there when doing rewrite
I have two places in my code which are very similar. I want to apply rewrite there. In the first place it works fine. In the other not. Why not?
First place (works fine):
...
2
votes
2
answers
119
views
Type inference with type classes in Coq
I don't understand type classes in Coq. I tried to use them as follows. I have a type cat that is supposed to represent the type of categories and I define the type ...
- 249
0
votes
1
answer
31
views
What to import to use le_not_gt_iff?
According to the documentation, there should be a Lemma le_not_gt_iff in Coq.Structures.OrdersFacts, but I haven't succeeded in referencing it.
I am trying to prove ...
- 159
1
vote
1
answer
46
views
Arguing with sumbools
I have the following definitions:
Variables Sd_pre : nat -> Prop.
Definition Sd_dec : forall t, { Sd_pre t } + { ~Sd_pre t }.
Admitted.
And the following are ...
- 159
3
votes
2
answers
118
views
A $\mu$-recursive function converges at an input, how to find the output?
Summary: I want to implement an interpreter for $\mu$-recursive functions which, for any $\mu$-recursive function $f$ and input $\mathbf{x}$, returns $f \left( \mathbf{x} \right)$ if it is defined.
...
- 83
3
votes
2
answers
86
views
Using if in Fixpoint
I have this recursive function I am trying to define by way of Fixpoint, but the if condition is giving me trouble.
...
- 159
2
votes
3
answers
578
views
What is a positive coinductive type and why are they so bad?
What is a positive coinductive type and why are they so bad?
This question is specifically within the context of Coq and is inspired by this question, the opening lines of which are:
Since positive ...
- 3,095
1
vote
1
answer
76
views
Best practices: Should I prefer definitions or iff when defining predicates?
I am a beginner in Coq, and I have a proposition I defined in this way:
...
- 159
5
votes
4
answers
3k
views
Less ridiculous way to prove that an Ascii character compares equal with itself in Coq
How do you prove that an Ascii character compares equal with itself in Coq idiomatically?
In the course of trying to prove a random exercise in Logical Foundations, I wanted to prove the following ...
- 3,095
3
votes
1
answer
207
views
Finding reflexive, transitive closure
I got a relation like: R: A -> A -> bool.
Using this, I need to find an Rclose: A -> A -> bool such that ...
- 131
1
vote
1
answer
32
views
Feeding rewrites and other hints into an omnibus tactic
How do I feed rewrites that I've marked as safe into a custom tactic?
I'm trying to write shorter Coq proofs with more of the easy stuff hidden. To that end, in the script below I proved that ...
- 3,095