Questions tagged [coq]
Coq is a formal proof management system. It is often referred to as a proof assistant.
41
questions with no upvoted or accepted answers
7
votes
0
answers
68
views
How do I write a minimal working example (MWE) in Coq to demonstrate some problem?
To get help with some incomplete proof script or definition in Coq, or demonstrate some failing (e.g., Ltac) tactic or command, I am often asked to write a minimal working example (MWE) of Coq ...
- 395
7
votes
0
answers
173
views
What was the first proof assistant with eta equality for records?
The Agda language supports eta equality for (non-(co)inductive) record types:
...
- 486
6
votes
0
answers
102
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
73
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 ...
- 199
6
votes
0
answers
170
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 ...
- 199
6
votes
0
answers
127
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 ...
- 2,768
5
votes
0
answers
104
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.
- 51
5
votes
0
answers
127
views
Prove equality in a record type
I am trying to prove something about monoids an categories. This results in the following (partial) proof:
...
- 245
4
votes
0
answers
46
views
Using CoqHammer from Ltac2
As it seems most likely to me, due to the special way arguments are evaluated in CoqHammer tactics (I tried to read the source code in OCaml but unfortunately I didn't understand much of it), it is ...
3
votes
0
answers
75
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:
...
- 193
3
votes
0
answers
31
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 ...
- 96
3
votes
0
answers
77
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
116
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
64
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....
- 31
2
votes
0
answers
27
views
Problem working with FMapWeakList and Parametrized Records
Consider the following definition of a record R, parametrized over an arbitrary eqType:
...
- 63
2
votes
0
answers
46
views
Factoring custom grammar rules for integers and lists in Coq custom entries
Is there a nice way to use custom entries to parse the following grammar? ("nice" meaning ~ "without massive duplication" and ~ "without needing to resort to separate ...
- 1,447
2
votes
0
answers
61
views
Have Hyperdoctrines been formalized?
I was thinking of formalizing them myself for a project if they haven't been already, and I looked in libraries and couldn't find anything.
I was thinking of coq in particular because it's the only ...
- 143
2
votes
1
answer
77
views
Debug autorewrite in Coq
I often meet proofs using autorewrite which Coq takes a while to process for some reason. (Setoid rewriting)
I then manually figure out which rewrite rules were ...
- 224
2
votes
0
answers
138
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:
...
- 23
1
vote
0
answers
68
views
Unfolding constants while rewriting using rewrite_strat and a hint database
I'm working with a substitution algebra as described by the Autosubst team, and I'm trying to automate some rewritings. As I'm using more than one calculus in my code, I'm trying to use the rewrite ...
- 133
1
vote
0
answers
58
views
Injectivity, Surjectivity and Smallness on lists of natural numbers imply each other
Require Import Coq.Lists.List.
I have the following properties defined on a list of natural numbers:
...
- 1,241
1
vote
0
answers
46
views
Why does Coq not allow constructor argument types to be strictly positive mutual inductive types?
Note: Apologies for the wicked mouthful of a title. I'm still getting acquainted with Coq terminology, so I might not have chosen the best words. If you have a better title suggestion, edits are more ...
- 143
1
vote
0
answers
45
views
Can you always replace mutually recursive references with parameters?
This is a follow up to a question someone else previously posted: Expressivity of mutual/nested inductives vs. regular inductives.
pigworker answered that
Adopting Agda-ish notation, the basic ...
- 143
1
vote
1
answer
92
views
Defining Kripke models and the canonical model for $S4$ modal logic
I have defined the syntax of modal logic in Coq and now I'm having trouble with the semantics. This is how I defined the Kripke model:
...
- 111
1
vote
1
answer
140
views
Equivalence Relations COQ
I am also unfamiliar and trying to solve proofs relative to the topic Relations and Divisibility but I would like to solve such COQ proof theorems. I am not quite sure how to solve proofs like this ...
1
vote
0
answers
44
views
Help with proofs in analysis
I would like to prove this in real analysis, but I’m finding it difficult to do it in Coq. Can someone help me, please.
If $f(x_j)$ is non-linear
$x_j \geq 0$, and
$f(x_j) \geq 0$, and
$f(0) = 0$, and
...
1
vote
2
answers
192
views
Dependent sum and equality with Coq
I have types B and A n where n:nat. I want to prove that ...
1
vote
0
answers
44
views
How do I prove this property about a factorial specification in Coq?
Notes: This post got pretty long... my apologies but hopefully somebody can take the time to look through it. Also, some of the code below uses terms that are defined elsewhere in my file and not ...
1
vote
0
answers
82
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)
...
- 63
1
vote
0
answers
25
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:
<...
- 199
0
votes
0
answers
3
views
Coq makefile complains about extension points on Windows 10
I installed Coq 8.16.1 on Windows 10 recently. I have a full development previously written in Coq 8.9.0 on Linux and want to upgrade to this.
When I run make, I get this error:
process_begin: ...
0
votes
0
answers
16
views
reference ospecialize and variable prim_base_irreducible not found in the current environment
Error encountered when trying to make after coq_makefile -f _CoqProject -o Makefile for lambda-rust
...
- 123
0
votes
0
answers
56
views
How to check a Zenon-generated proof with Coq?
I installed zenon (opam package, github) and tried to use it to generate a Coq proof.
I couldn't find any documentation for the Zenon's main syntax, so I looked at its test suite.
I grabbed this test ...
- 2,711
0
votes
0
answers
63
views
Help with fixing a Coq installation using docker and vscoq
I'm following the logic foundation preface and just began learning. I tried to use the docker with vscoq like the suggested in the book but it didn't work for me and kept asking me to install coq ...
0
votes
0
answers
31
views
Why does Program Fixpoint leave behind a temporary_proof2_subproof axiom in this example?
I have reduced my development into the following minimal reproducer:
...
- 151
0
votes
0
answers
97
views
Formalization of partial functions for combinatorial counting
I need assistance in defining axioms for partial functions in total function theory that is available in Coq.
Specifically, I'm looking for a constructive definition of a partial function that ...
- 11
0
votes
1
answer
45
views
How to prove commutation of a recursive function over a finite set encoded with binary nat in coq
I needed to define some things in finite set, the original library seemed too complex so I took my friend's advice and I used a library he was developing for this purpose. The library uses BinNat ...
0
votes
1
answer
131
views
Induction COQ Question
Just practicing some induction proofs and was wondering what would be the fastest and most effective way to solve this proof and proofs similar to this?
...
0
votes
0
answers
58
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 (...
- 357
-2
votes
2
answers
79
views
Help with strong induction
I have the following definition of divisibility by 3.
...
-2
votes
1
answer
192
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:
...
- 21