Questions tagged [coq]
Coq is a formal proof management system. It is often referred to as a proof assistant.
202
questions
2
votes
1
answer
139
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 ...
- 153
0
votes
0
answers
29
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
47
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
1
vote
1
answer
42
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.
...
0
votes
1
answer
53
views
Specializing forall quantifiers in Coq
I have an inductively defined type of expressions:
...
1
vote
2
answers
63
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,231
0
votes
0
answers
96
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
96
views
1
vote
0
answers
55
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,231
1
vote
1
answer
38
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
61
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
33
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
43
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
97
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
173
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
1
answer
158
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
137
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
41
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
194
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 ...
- 123
2
votes
0
answers
40
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,437
1
vote
1
answer
81
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,231
2
votes
0
answers
60
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
56
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
41
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
42
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
69
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
100
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
94
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
17
views
Induction error on mutually defined types in Coq
I want to define two types that depend on each other
...
- 131
1
vote
1
answer
33
views
How do I debug Gallina (Coq) code?
I have some complex functional code in Gallina that I run under Coq. From time to time bugs emerge and I need to debug the code. Is there a way to debug the code from Coq, or am I stuck with doing ...
- 212
4
votes
2
answers
92
views
Ltac - run tactic for each hypothesis of given pattern
Especially in the context of lia, which can sometimes fail to prove a theorem in the form of
forall x, x <> 0 -> P x
...
- 171
3
votes
1
answer
89
views
Coq's elimination restriction corner cases -- when can you eliminate Prop's into Type?
In order to ensure soundness, and to keep axioms like proof irrelevance admissible, Coq has an "elimination restriction" on inductive types in Prop.
...
- 98
3
votes
1
answer
70
views
Tricks for proving equalities under type cast
I sometimes stumble across proofs that prove equalities in the form of
forall a b (p: a = b), C a = match p with | eq_refl => C b end
without resorting to ...
- 171
4
votes
2
answers
287
views
Reasoning about CwFs in a proof assistant
I've been chatting with folks on Mastodon about this but the perspective there is markedly Agda-focused, so I thought I'd ask here for some broader opinions.
What tools/libraries are there for ...
- 768
0
votes
1
answer
67
views
Natural deduction in Coq
I am trying to verify the proofs by natural deduction from Ryan and Huth based on the information in Natural deduction with coq proof assistant. Here is Example 1.13 and its proof.
Step 4 is ...
- 23
1
vote
1
answer
97
views
Induction scheme on two arguments for custom type in Coq
I've been working on formalizing a Hilbert deductive system within Coq. I have the following definition for a term in first-order logic:
...
2
votes
1
answer
51
views
Proving a logic riddle in Coq : testing equivalence in an Inductive set
I'm trying to formalize in Coq the following riddle and its solution
Alice, Bob and Charlie are one of each role:
a truth teller (always tells the truth)
a liar (always lies)
and a spy (can lie or ...
- 131
1
vote
1
answer
61
views
Can Coq grab some data over HTTP and then write the data as declartions in Coq itself?
The data I'm referring to is just an easy to understand JSON format of objects / arrows and the styling information about the arrows.
For example, if an arrow is two-headed I need in Coq locally to ...
2
votes
1
answer
151
views
Organizing a Coq proof
What would be a more convenient better way to solve this proof in a less clustered/confusing way?
...
-2
votes
2
answers
68
views
Help with strong induction
I have the following definition of divisibility by 3.
...
1
vote
1
answer
79
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 ...
0
votes
1
answer
102
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?
...
7
votes
2
answers
1k
views
Is it possible to make a proof assistant program based on ZFC?
I heard that many proof assistant programs are made based on the type theory.
For me, as a mathematician, when I met Coq at first, it is difficult to accustomed with it.
So I have a question.
Is it ...
- 357
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
1
answer
113
views
How to deduce this equality based on the fact that these two terms must be the same?
Brief (but possibly inaccurate) Summary:
I have a proposition H : Prop1 p q. When I use inversion on the proposition, I get ...
- 1,231
0
votes
1
answer
56
views
Reasoning about non reflexive equalities & type conversions
Following-up from the answers to this question, reasoning about conversions between types that have decidable equalities is somewhat trivial (here I'm taking nat as ...
- 43
0
votes
1
answer
32
views
Coq: Proving snd divmod doesn't depend on parameter q?
I have another proof I'm trying to complete in Coq involving the Divmod function, but the inductive case has a different value of q for the divmod function.
The q parameter is only involved in the ...
- 103
1
vote
2
answers
106
views
2
votes
1
answer
53
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
6
votes
4
answers
546
views
Inductive vs. recursive definitions
In Coq there are two ways to define a new type on an inductive type: Using Inductive and using Fixpoint. What are pros and cons ...
- 224