Questions tagged [coq]

Coq is a formal proof management system. It is often referred to as a proof assistant.

19 questions with no upvoted or accepted answers
Filter by
Sorted by
Tagged with
7 votes
0 answers
137 views

What was the first proof assistant with eta equality for records?

The Agda language supports eta equality for (non-(co)inductive) record types: ...
  • 421
6 votes
0 answers
82 views

In VSCoq, how to issue an arbitrary Gallina query via the prompt?

I’m currently trying out Visual Studio + VSCoq, having previously used Emacs + Proof General for Coq, and there’s one part of my usual workflow that I haven’t managed to replicate yet. Is there a way ...
6 votes
0 answers
115 views

How to write heavily indexed proofs?

I've been playing with hereditary substitution. However, things get very awkward because substitution isn't total unless you index by the environment somehow. In my old approach terms were not indexed ...
5 votes
0 answers
56 views

What are Generic Arguments in Coq and how are they structured in their OCaml code?

I was trying to figure out why it seems that in a Coq generic argument there seems to be 3 arguments to the constructor GenArg when according to me there should ...
5 votes
0 answers
136 views

How does one systematically traverse OCaml representations of Coq ASTs terms?

I want to be able to (tree) traverse Coq terms (e.g. in OCaml or using their s-expression representation in any language). My main challenge is to figure out how to do this systematically because I ...
5 votes
0 answers
122 views

Unfolding expressions in Coq by one layer

Are there any ways to unfold an expression in Coq by a single layer? I have only come up with this obvious solution: ...
5 votes
0 answers
85 views

Display style proofs using Coq

How to display proofs using in Gentzen tree style and (or) Fitch-style, using CoqIDE or JsCoq? PS: I'm rookie used coq.
5 votes
0 answers
111 views

Prove equality in a record type

I am trying to prove something about monoids an categories. This results in the following (partial) proof: ...
3 votes
0 answers
73 views

Coq Typeclass on Functions Gets Confused by Equality

I was trying to use typeclasses to generalize the different notions of homomorphisms, but I’ve run into an annoying issue. Consider this code which demonstrates the issue: ...
  • 171
3 votes
0 answers
26 views

.CoqMakefile.d required by CoqMakefile but not generated

I am trying to use CoqMakefile to automatically build my Coq project in Coq 8.15.2. When I did this the compilation failed because a file ".CoqMakefile.d" was expected by make but did not ...
3 votes
0 answers
68 views

Where is the discriminate tactic defined in Coq?

One can read the Coq documentation about discriminate tactic here. Were is this tactic actually defined?
3 votes
0 answers
103 views

Recursive notations with forall quantifier

How can I implement a notation of the form: ∀ x ≤ y ≤ .. ≤ z ≤ t, φ in Coq? A similar notation (but without quantifiers) appears here ...
3 votes
0 answers
60 views

SSReflect tuple constructor: why not use phantom?

I was reading the mathcomp book learning about canonical structures and following along with the mathcomp source to compare how things were done in practice. Specifically I was looking at sections 6....
2 votes
0 answers
113 views

Cannot open pixbuf loader module file in Windows

I installed Coq from the 8.15 64-bit installation file in Windows. I ran coqide and got the error message: ...
  • 21
1 vote
0 answers
62 views

How to reason about equality between different datatypes?

I am working on a verification project where the specification uses the following inductive datatype to represent bitvectors (MIT's bbv) ...
  • 11
1 vote
0 answers
22 views

Why does TacArg accepts a value of CAst.t type when it should only accept values of types?

See the argument for TacArg: | TacArg of ('t, 'dtrm, 'p, 'c, 'r, 'n, 'tacexpr, 'l) gen_tactic_arg but the reply has a type CAst.t as an argument for TacArg: <...
0 votes
1 answer
71 views

an argument why stack blocks are never unexpectedly freed in the RTL intermediate language in CompCert

I apologize if this is not the right site to ask this, as the question is not about a proof assistant per se, but about a particular formalization. In the semantics of the RTL intermediate language in ...
0 votes
0 answers
54 views

If I make some new structure like Q, then can I use 'rewrite' tactic for my new structure in Coq?

From $\mathbb{Q}$, the set of all rational numbers, I make some new structure $I$, and also make strict order and (equivalence) equality on $I$. I want to use rewrite tactic for my defined relations (...
-2 votes
1 answer
131 views

How to write a summation in Coq

I have just started getting acquainted with Coq and I would like to write this sum on it: $\sum_{p=1}^{n} \frac{\mathrm{d}^p}{\mathrm{d}x^p} f(x)$ This is what I have tried: ...