Questions tagged [coq]
Coq is a formal proof management system. It is often referred to as a proof assistant.
224
questions
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
1
vote
1
answer
48
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
114
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
96
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
80
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
299
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 ...
- 773
0
votes
1
answer
88
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
2
votes
1
answer
130
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:
...
- 195
2
votes
1
answer
53
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
71
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 ...
- 269
2
votes
1
answer
155
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
79
views
Help with strong induction
I have the following definition of divisibility by 3.
...
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 ...
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?
...
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
125
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,241
0
votes
1
answer
60
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 ...
- 63
0
votes
1
answer
36
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 ...
- 125
1
vote
2
answers
126
views
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
6
votes
4
answers
626
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
3
votes
1
answer
46
views
Coq: Unify with a pattern and get the result
I want to do change t with (f _), where t is a term and f is a function, but ...
- 71
1
vote
1
answer
59
views
Can I show Coq equality of types without using a mapping between the types?
Say that I have a list structure and a lemma:
...
0
votes
2
answers
124
views
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 ...
2
votes
1
answer
127
views
1
vote
1
answer
92
views
How to prove this correctness principle of transposition of lists of lists in Coq?
I have defined the function transpose as follows:
...
- 1,241
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 ...
6
votes
2
answers
208
views
Is there a formalism of "coinductive" data types with negative occurrences?
Consider the following program in Haskell:
...
1
vote
1
answer
66
views
How do I prove an expression in Coq that involves pattern matching?
I'm working on a proof in Coq and my proof state is as follows:
...
2
votes
1
answer
88
views
-4
votes
1
answer
187
views
1
vote
3
answers
97
views
Model and Prove Unsigned Integer Operation Wrapping Behavior in Coq
I'm learning Coq and trying to do something useful with it. For daily programming tasks, especially binary parsing, one of the things I must deal with is to check and handle integer arithmetic ...
- 113
5
votes
1
answer
310
views
Why can't I use let bindings to pattern match a 3-tuple in Coq?
Consider the following
Axiom foo : nat -> nat * nat.
Definition fooX (x : nat) :=
let (y, z) := foo x in
y + z.
which is fine.
Now, consider
...
- 1,241
4
votes
3
answers
261
views
Rewrite with definitional equality and dependent types
In Coq, there are some terms that are equal by definition, but there's not an easy way to replace one value with the other inside a proof. The two ways that I know that work in general are to use the ...
- 193
0
votes
1
answer
115
views
I don't know how to fire up coqtail
I installed coq and coqtail in my computer. According to this page:
https://github.com/whonore/Coqtail
Im now supposed to use the command
CoqStart
to launch the plugin. However, when I type ":...
- 103
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
3
votes
2
answers
211
views
How to abstract over function arity in Lean and Coq?
Given types $A, B$ I would like to express the type of all functions $f$ for which there exists an $n \in ℕ$ such that $f$ has type $A^n \to B$. And possibly in such a way, that for $a_1, \dots, a_n : ...
- 224
1
vote
1
answer
69
views
Coq Induction on Hypothesis destroys the Hypothesis
I'm trying to prove something in coq
I have and Inductive prop type named in_order_merge which is a relation between three lists that shows third one is in_order merge of first two, here is the ...
1
vote
2
answers
50
views
Destructing transitivity hypothesis on simple predicate logic
I'm new to Coq and am working on some exercises with predicate logic. In one of the exercises, a transitivity hypothesis is defined as follows:
...
- 11
2
votes
1
answer
85
views
Program Fixpoint decreasing on measure produces unsolvable goal
I have trouble understanding how to produce more sensible goal in the obligation
...
- 63
1
vote
1
answer
81
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 ...
- 121
2
votes
2
answers
123
views
How to get rid of opaque proof-terms in computation
My goal is to construct list of vectors from filtered by length list of lists
Something like
Compute foo [[1;2]; [3]; [4;5]]. (* [[1;2]%vector; [4;5]%vector] *)
My ...
- 63
1
vote
1
answer
78
views
Coq abilities and usage
What abilities does coq have apart from simple proofs? Can it complete induction? Can I use it to solve polynomial equations? Can I use it to prove bijections?
- 11
1
vote
3
answers
90
views
Two-step induction of inductive predicate on Streams
If I want to have an induction principle for nats from n to n+2, I can define and prove this ...
- 131
0
votes
2
answers
126
views
Why can't I write a function that doesn't take a type argument besides Set, Prop, or Type?
I'm trying to make a "formal" model of a C++ domain specific language. One thing the language has is a notion of a "reducer" where you take an array and add up all the elements. I ...
- 123
0
votes
2
answers
60
views
Stream of all finite prefixes of a stream
If I want to construct of list of all (obviously finite) prefixes of a list, I can define this function:
...
- 131
1
vote
3
answers
138
views
How do I express a fixpoint of a decreasing argument that is not a subterm of the function's argument?
I have a recursively defined function in Coq whose arguments in the recursive invocations are surely decreasing, but Coq cannot understand this fact since they are not subterms of the function's ...
- 212
0
votes
1
answer
104
views
What is the idiomatic way in Coq to write recursive functions over product types?
I need to write a recursive function in Coq that takes an argument with type T and produces a result with type option T. The problem is, the recursive invocation is not properly on a subterm of its ...
- 212