Questions tagged [coq]
Coq is a formal proof management system. It is often referred to as a proof assistant.
320
questions
2
votes
1
answer
93
views
What does `induction ... in ...` do in Coq?
I'm self-studying the Semantics course, and met the following proof script in the warmup directory:
...
- 123
3
votes
3
answers
230
views
My Inductive function over a pair of lists gives "Cannot guess decreasing argument of fix."
This is the smallest example that causes the problem. It should decrease, but I don't know how to reassure Coq that it will. I'm going to have to compare lots of lists of pairs for what I'm doing so ...
- 75
1
vote
1
answer
78
views
Book on Coq that helps me write proofs regarding integral equations
I want to read a book about Coq that would help me construct proofs of theorems in signal processing, particularly Fourier and Wavelet Transforms.
Have seen https://coq.inria.fr/documentation but ...
- 1
3
votes
1
answer
121
views
Inductive from CoInductive?
It is possible to represent CoInductive using parts that are Inductive. As a simple example,
...
- 133
1
vote
0
answers
125
views
Trouble proving a theorem using induction in Coq
Theorem five_and_three: forall i, exists a b, i + 8 = 3 * a + 5 * b.
I'm currently using these tactics:
...
- 11
1
vote
1
answer
73
views
How do I enable this kind of rewriting?
Link to Code Gist
Given two extensionally equal sets, s1 ≡ s2, I want to be able to obtain a ∈ s2 from ...
- 1,502
4
votes
1
answer
262
views
Dealing an equality with coq. - beginner's question
I am studying the sf book - ProofObjects.v file.
I'm confused with "equality__leibniz_equality_term" exercise.
...
0
votes
1
answer
73
views
5
votes
2
answers
1k
views
How do I express a negative premise in Coq?
I would like to express a transition system in the style of the small-step operational semantics as found in volume 2 of "Software foundations". Unfortunately my transition system has rules ...
- 282
2
votes
1
answer
91
views
How to use a lemma that is defined in a Coq module?
How can I use the Lemma div_0_l from the standard library?
Somehow I cannot instantiate the module that is defined as
...
- 25
6
votes
0
answers
170
views
Coq - Are there functions which are provably equal but not definitionally equal?
In Coq, are there types A,B and functions f, g : A -> B such that f = g propositionally ...
2
votes
1
answer
78
views
Packaging Mathematical Structures in Coq: Help Understanding a Definition
Context
I am a relatively new user to Coq with a decent understanding of the basics of dependent type theory and am midway through chapter 2 of the Software Foundations Series of books. I want to ...
- 133
3
votes
2
answers
69
views
What is the most ergonomic way to eliminate multiple similar goals in Coq?
I recently bumped into some theorems that can be proved easily but not very elegantly. It is not elegant because when I was doing case analysis, Coq discharged many goals, but most of them can be ...
- 420
4
votes
2
answers
109
views
what symbols can I use in coq?
Is it possible to use symbols like $\mathbb{N},\forall,\implies$ in Coq?
- 143
0
votes
0
answers
51
views
Analysis of proof that for a category which is also a poset, every diagram commutes
A poset may be defined as a set (axioms of ZFC go here to define "set") and a binary relation (which is taken as a primitive notion in first-order logic), which meets these conditions:
$a R ...
