# 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
94 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 ...
147 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: ...
• 121
235 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 ...
1 vote
115 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 ...
42 views

### Induction error on mutually defined types in Coq

I want to define two types that depend on each other ...
• 131
1 vote
98 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 ...
196 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
148 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. ...
• 446
109 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
321 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 ...
143 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
184 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: ...
59 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 ...
• 191
1 vote
85 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 ...
• 303
160 views

### Organizing a Coq proof

What would be a more convenient better way to solve this proof in a less clustered/confusing way? ...
123 views

### Help with strong induction

I have the following definition of divisibility by 3. ...
220 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 ...
200 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? ...
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 ...
• 387
1 vote
48 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
148 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 ...
69 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
38 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 ...
1 vote
200 views

### Weird use of equality in Coq

I have a situation that is kind of like this: ...
• 193
159 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
864 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
64 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 ...
1 vote
84 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: ...
175 views

...
1 vote
326 views

### Dependent sum and equality with Coq

I have types B and A n where n:nat. I want to prove that ...
176 views

### Rewriting with heterogeneous equality (JMeq)

Consider the below (reproducible) snippet: ...
• 63
1 vote
99 views

### How to prove this correctness principle of transposition of lists of lists in Coq?

I have defined the function transpose as follows: ...
1 vote
48 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 ...
237 views

### Is there a formalism of "coinductive" data types with negative occurrences?

Consider the following program in Haskell: ...
1 vote
166 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: ...
116 views

### How to prove a statement about sublists?

I create sublist from list in this way: ...
• 121
255 views

...
1 vote
120 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
393 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 ...
462 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
198 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
89 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
245 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
95 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
59 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
194 views

### Program Fixpoint decreasing on measure produces unsolvable goal

I have trouble understanding how to produce more sensible goal in the obligation ...
• 138
1 vote
82 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 ...
190 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 ...
• 138
1 vote