Questions tagged [coq]
Coq is a formal proof management system. It is often referred to as a proof assistant.
223
questions
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
3
answers
123
views
LEM, the halting problem, the curry-howard correspondence -> deep connection?
I posted the following on the math stackexchange, but it occurs to me that this might be a more (or at least equally?) appropriate forum:
It was recently said to me by a prominent mathematician, who I ...
- 101
0
votes
1
answer
50
views
What is the difference between these inductive definitions in Coq?
I came up with the following inductive definitions in Coq for an even number:
...
- 101
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
4
votes
1
answer
106
views
What is the best way to learn Iris completely independently
I am looking forward to learning Iris by myself, I have essential basic knowledge of Coq and logic but I don't know where to start. Logically, I looked into materials on the project website; the video ...
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
1
vote
1
answer
84
views
problem with unification
I've faced a problem. I'm not sure how to explain it, so, that is why I'm asking.
...
- 215
1
vote
1
answer
63
views
How to express that two equivalence relations can setoid rewrite across each other (Coq)
I am looking for a way to express that two equivalence relations are compatible and can (setoid) rewrite across each other. As an example here's an ordinary proof I wrote that a left inverse implies ...
- 113
3
votes
2
answers
198
views
Universe inconsistency errors when using ZF model in Coq
I am trying to use a formal logic system I recently implemented in Coq to study ZF set theory. In order to do this, I need to define a type representing the domain in question, and then prove that ...
- 195
0
votes
1
answer
134
views
Why inductive types (or variants) are so rigid in terms of the set of constructors
An inductive type definition normally carries a set of constructors C, but I am not so sure why the set of constructors C is always once-for-all statically defined.
For instance:
...
- 125
2
votes
2
answers
93
views
Continue a section (with context) in coq
So I have a file in coq, which is a bit like the following:
...
- 245
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
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 ...
5
votes
1
answer
169
views
Universe polymorphism and Coq standard library
When developing in Coq with the Universe Polymorphism flag on, the standard library introduces unwelcome universe constraints because it is universe monomorphic.
Is there an alternative standard ...
- 75
1
vote
1
answer
68
views
Use proof irrelevance in cast
I'm working using cast in Coq.Vectors. When trying to rewrite with proofs, I'd like to use the fact of proof irrelevance (Coq.Logic.Eqdep_dec), preferably automatically. I.e., when I have a lemma ...
- 23
2
votes
2
answers
115
views
Proving that a minimum example exists if any example exists in nat
I'm trying to prove that if a function from nat -> bool is true for any natural number, then there exists a minimum natural number which the function is true for.
I've been trying to find a good ...
- 125
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
2
votes
1
answer
92
views
Eta-equality for records: the case of semigroups
Consider the following definition of a semigroup:
...
- 75
3
votes
1
answer
92
views
gappa seems to generate bad Coq
I'm using the -Bcoq backend of gappa.
The coq file contains dollar signs.
So far as I can tell, a coq file should not contain dollar signs.
Here is a snippet from -Bcoq :
...
2
votes
1
answer
193
views
6
votes
1
answer
248
views
(Dis)Advantages of basing a proof assistant on CH correspondence?
Major proof assistants like Lean and Coq are fundamentally based on the Curry-Howard correspondence: propositions are encoded as types, quantified propositions are encoded as dependent types, proofs ...
- 273
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
1
vote
1
answer
88
views
confused about stlc from Programming Language Foundations
I have two related quetions. I made my way to STLC and Typechecking from Programming Lang Foundations, yet I am more or less mentally stuck at the STLC chapter, hence many things related to it are ...
- 51
2
votes
1
answer
58
views
Eliminating dependent destruction in Coq
I'm working on developing a theory of arithmetic within a framework for first-order logic I constructed in Coq. The following is a simplified version of the scenario I'm working with.
...
- 195
0
votes
1
answer
68
views
Specializing forall quantifiers in Coq
I have an inductively defined type of expressions:
...
1
vote
2
answers
73
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,241
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
2
votes
2
answers
118
views
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
1
answer
59
views
İnduction/inversion and others in coq
I'm trying to learn Coq using the software foundations. I somehow made it to the 2nd volume but I'm struggling writing proofs on my own. Especially whether I should be using inversion or induction.
I ...
- 51
1
vote
1
answer
75
views
Proving function existence in Coq
Coq beginner here! My question is how to formalize reasoning of the kind "...consider the following function, it has some property, therefore..." in Coq.
The challenge is to prove the ...
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
2
votes
2
answers
111
views
How to download (e.g. from Github) Coq, if its main site is down?
There are quite a moments, when Coq main site https://coq.inria.fr/download is down. Has Coq any downloads available from its main github repository https://github.com/coq/coq or some other mirrors? ...
- 133
2
votes
1
answer
250
views
How to install dependencies correctly? [Cannot find a physical path bound to logical path]
There's this library I'd like to use. The idea is to be able to use this library with Require Import easily in any other *.v ...
- 143
1
vote
2
answers
239
views
Formalization of a model of ∞-category in a proof assistant
I am aware of similar question in MO whose comment nicely lists zoo of possible models and only such models can be formalized. But I have not found any implementation so far which I could use or ...
- 133
2
votes
1
answer
145
views
Coq: Would adding "inline inductive definition expressions" introduce inconsistency?
Scenario: new ind syntax
As far as I know, in Coq, you cannot create new inductive types by only using expressions. You must use commands--namely, the ...
- 143
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 ...
2
votes
2
answers
201
views
How to reason about and extract code for inductive types with negative occurrences in Coq?
I'm interested in proving correctness of the interpreter of Appel's compiler (appendix B), and compare it to the machine semantics given by Kennedy on his paper. The interpreter acts as a denotational ...
- 133
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
1
vote
1
answer
84
views
Rewriting inside quantified propositions in Coq?
Is there a simple way to use rewrites inside quantified Props? As an example, consider the following:
...
- 1,241
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
3
votes
1
answer
69
views
"Expected a single focused goal but 2 goals are focused." error in coq regarding string equality(I think)
I'm working through Software Foundations, I'm at "Maps" right now. There's an exercise:
...
- 51
1
vote
1
answer
49
views
What is the correct way to define a DecidableType module?
I have this type in Coq:
Inductive s_symb : Type :=
| s_symb_expr : nat -> s_symb
| s_symb_fld : nat -> list string -> s_symb.
I want to create a ...
- 212
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 ...
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
0
votes
3
answers
130
views
How do I extract efficient string code in Coq to OCaml?
I have a Gallina (Coq) program that I am extracting to OCaml. The program is a (symbolic) interpreter for a small programming language, and I defined functions to stringify the states so I can print ...
- 212
1
vote
2
answers
100
views
Partitioning a list with 2 elements in the middle in coq
I am trying to prove some theorems using sequent calculus, for some parts (e.g. cases with Exchange rule) I need a theorem like below
...
0
votes
1
answer
20
views
Induction error on mutually defined types in Coq
I want to define two types that depend on each other
...
- 131