# Questions tagged [coq]

Coq is a formal proof management system. It is often referred to as a proof assistant.

328 questions
Filter by
Sorted by
Tagged with
66 views

### Ltac, How to intro a fresh variable which may already have a good estiblished name given by a universal quantifier?

Context I am currently self studying Coq following the Software Foundations book series which I am finding very approachable. I have finally gotten round to ...
• 133
146 views

### How do I define an induction principle for a type with a nested list of tuples?

I want to define an inductive type that describes records. The records are lists of elements, each element has a name and type. This requires nested recursion, so I've had to define an induction ...
42 views

### Rewriting/Applying unidirectional morphisms in Coq

Link to Code Gist I have the following definition ...
105 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: ...
• 153
236 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 ...
1 vote
83 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 ...
123 views

### Inductive from CoInductive?

It is possible to represent CoInductive using parts that are Inductive. As a simple example, ...
• 133
1 vote
127 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: ...
1 vote
79 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 ...
276 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. ...
76 views

...
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 ...
98 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 ...
176 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 ...
80 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
83 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
123 views

### what symbols can I use in coq?

Is it possible to use symbols like $\mathbb{N},\forall,\implies$ in Coq?
• 143
52 views

1 vote
107 views

We have ...
• 249
1 vote
104 views

### How to apply constructor injectivity in the goal

Suppose I have a goal Goal forall m n, S m = S n -> m = n. intros m n H. 1 goal m, n : nat H : S m = S n ============================ m = n I know ...
• 13
1 vote
211 views

### How to correctly feed type argument in this toy theorem?

I have a recursive function combine defined as following: ...
• 113
222 views

### Coq / Lean endpoint for GPT actions

I'm trying to produce Coq and Lean code using a custom GPT but I want GPT to try running its proof scripts (and revising them if they fail) before suggesting them to me (via gpt actions). Right now, ...
• 233
1 vote