# Questions tagged [coq]

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

333 questions
Filter by
Sorted by
Tagged with
100 views

### How to use Modus Ponens in L axiomatic system

I have copied a system of axioms for L system described in book Mendelson "Introduction into Logics": ...
• 125
80 views

### Is it possible to simplify/normalize nat arithmetic expressions in Coq?

I'm writing a tactic to apply some normalizing rewriting rules on a substitution algebra, similar to the autosubst project. I've made a sigma tactic that applies ...
• 153
85 views

### Extensional sets in Coq and induction

I would like to define the following data type in Coq: Inductive X : Type := | constr : FinSet X -> X. Here constr should take a single argument, which is a finite set of elements of X. I need this ...
384 views

### How does Coq guess i is decreasing?

As far as I know, fix must be called with a decreasing argument. In the following code, i is the decreasing argument of ...
• 223
1 vote
59 views

### Accessing nested typeclasses elegantly

I have a situation where one typeclass is "nested" in another one like this: ...
• 179
57 views

### Strict implicit arguments in Coq

In the following code ...
• 271
1 vote
61 views

### How do I apply a lemma to both sides of an equality hypothesis?

I have the following Coq code: ...
• 13
43 views

### How to apply the same tactic to multiple match patterns in Ltac

I'd like to apply the same ltac_expr to multiple match_patterns in the Ltac language. For instance, I would like to do something like ...
• 153
56 views

### STLC substitution behaviour with lambda body normalisation

UPDATE 31/07/'24 12.57: It is false: Assume v, w, x, y, z all type variables. Take t = (\y. y) (x w) --> x w = t', then ...
1 vote
65 views

### What is a simple example of transforming some Objects / Arrows in visual, categorical definition into actual Coq code. An MWE recipe that is

Injective object - Wikipedia In modern category theory literature, the whole definition of injective object can be written as: Definition. An object $Q$ in a category $C$ is injective $\iff$: ...
• 303
1 vote
145 views

### Can some existing proof assistant, in its current state of the art, encode this small theory about a twin prime counting function?

Remark 1. The following counting formula can be derived using arithmetic properties of inequalities, properties of floor / ceiling, inclusion-exclusion, sieve-of-Eratosthenes, and the inclusion-...
• 303
84 views

### The uniform inheritance condition of coercions to dependent types in Coq

I'm encoding a HOAS in Coq, but my coercions are not working well. Here is a MWE: ...
• 153
68 views

...
• 154
132 views

### Code Review: $\mathbb{Z}[\sqrt{-2}]$ is an integral domain

I proved that $\mathbb{Z}[\sqrt{-2}]$ is an integral domain; I would like a review of this proof. My by hand argument is in Appendix A. It is not the original argument I used. I made a stupid mistake ...
• 3,105
1 vote
82 views

### Prove that a function's result cannot dependent on Prop-valued parameters in Coq

Consider the following function elem and the lemma that the result of elem does not depend on the proof of ...
• 179
266 views

### Uniqueness of proofs for inductively defined predicates

In Init/Peano.v the less-than-or-equal predicate is defined as follows: ...
54 views

### Found no matching subterm in goal while it does seem to be there when doing rewrite

I have two places in my code which are very similar. I want to apply rewrite there. In the first place it works fine. In the other not. Why not? First place (works fine): ...
132 views

### Type inference with type classes in Coq

I don't understand type classes in Coq. I tried to use them as follows. I have a type cat that is supposed to represent the type of categories and I define the type ...
• 271
33 views

### What to import to use le_not_gt_iff?

According to the documentation, there should be a Lemma le_not_gt_iff in Coq.Structures.OrdersFacts, but I haven't succeeded in referencing it. I am trying to prove ...
• 159
1 vote
51 views

### Arguing with sumbools

I have the following definitions: Variables Sd_pre : nat -> Prop. Definition Sd_dec : forall t, { Sd_pre t } + { ~Sd_pre t }. Admitted. And the following are ...
• 159
128 views

### A $\mu$-recursive function converges at an input, how to find the output?

Summary: I want to implement an interpreter for $\mu$-recursive functions which, for any $\mu$-recursive function $f$ and input $\mathbf{x}$, returns $f \left( \mathbf{x} \right)$ if it is defined. ...
• 223
89 views

### Using if in Fixpoint

I have this recursive function I am trying to define by way of Fixpoint, but the if condition is giving me trouble. ...
• 159
629 views

### What is a positive coinductive type and why are they so bad?

What is a positive coinductive type and why are they so bad? This question is specifically within the context of Coq and is inspired by this question, the opening lines of which are: Since positive ...
• 3,105
1 vote
82 views

### Best practices: Should I prefer definitions or iff when defining predicates?

I am a beginner in Coq, and I have a proposition I defined in this way: ...
• 159
3k views

### Less ridiculous way to prove that an Ascii character compares equal with itself in Coq

How do you prove that an Ascii character compares equal with itself in Coq idiomatically? In the course of trying to prove a random exercise in Logical Foundations, I wanted to prove the following ...
• 3,105
221 views

### Finding reflexive, transitive closure

I got a relation like: R: A -> A -> bool. Using this, I need to find an Rclose: A -> A -> bool such that ...
• 131
1 vote
40 views

### Feeding rewrites and other hints into an omnibus tactic

How do I feed rewrites that I've marked as safe into a custom tactic? I'm trying to write shorter Coq proofs with more of the easy stuff hidden. To that end, in the script below I proved that ...
• 3,105
1 vote
232 views

### Formalizing "finite or infinite" in Coq

In Coq, I am trying to formalize the notion of a finite or infinite sequence, e.g. of natural numbers: call it a run, and call ...
1 vote
266 views

### Why did this proof succeed without function extensionality?

I'm very confused as to why a proof of a lemma succeeded without function extensionality. I'm messing around with some trivial Coq proofs for manipulating pseudosequences of the form ...
• 3,105
130 views

### How to use SSReflect to prove commutativity and associativity of addition idiomatically?

How do you prove commutativity and associativity of addition idiomatically using SSReflect? I am trying to learn SSReflect so I have another tool in my belt for ...
• 3,105
1 vote
60 views

### Applying an axiom from a class in a proof

I'm trying to represent Boole-Schroder Algebra in Coq, and am trying to use apply to start a proof using one of my defined axioms, but I'm getting an "unable ...
1 vote
105 views

### Trying to use 'Equations'

Examples from Chlipala's book https://mattam82.github.io/Coq-Equations/examples/Examples.MoreDep.html ...
72 views

### Checking if a goal is *definitely wrong* by testing it against random examples in Coq

I'm currently poking around in a medium-sized Coq codebase that I didn't write and am not very familiar with ... and I'm trying off and on to make progress on some lemmas where the proof attempt was <...
• 3,105
1 vote
74 views

### Dependent equality in Coq

Let’s say that cat is the type of categories (I don’t think its precise formalization really matters here). I define the type of « initial structures » of a ...
• 271
82 views

### Coq can you enter a tactic context inside of a Fixpoint definition?

I can use an opaque term created by a tactic in a Fixpoint definition. ...
• 3,105
69 views

### Coq equivalent of Lean's nth_rewrite

Does Coq have an equivalent of Lean's nth_rewrite? rewrite ... at ... appears to specialize at its first unification site ...
• 3,105
125 views

### Lower bounds in type theory proof assistant with ordinals and universes without axioms

I saw a PowerPoint that claimed to achieve $\psi_0(\Gamma_{\Omega+1})$ in Agda without any axioms. I was wondering if a better lower bound exists in 2024? My ...
• 279
46 views

### Coq cannot simple apply reflexivity in custom tactic

The fast reflexivity tactic shown below is very interesting. It exposes some of the unification machinery by disabling it. I'm planning on going back and using it in the first part of Software ...
• 3,105
88 views

### Proof General tell Coq where a physical path is

Here is the first few lines of Auto.v in Software Foundations Volume 1. ...
• 3,105
49 views

### Intuitive understanding of limits of intuition tactic in Coq

On an intuitive level, why does intuition get stuck in cases where the proof can be unblocked with a destruct? What options are ...
• 3,105
1 vote
122 views

### Problems with dependent sums

Very simple trees (I trew away everything unnecessary) ...
1 vote
59 views

### Using if-then-else in Program Definition's obligation

Consider the following program (which is a simpler version of what I'm trying to do): ...
• 179
128 views

### Is the validity of induction in Coq axiomatic?

When one defines an inductive type in Coq, for example, natural numbers, Inductive nat : Set := | O : nat | S : nat -> nat. Coq automatically creates an ...
• 33
36 views

### Changing workflow from coq_makefile to Dune, unable to view built project in a toplevel

After learning to write libraries for Coq using the Makefile approach I have decided to take the plunge and try to switch over to using the Dune system. My question consists of help with getting to ...
• 133
1k views

### Tools like leanblueprint for other proof assistants, especially Coq?

In my (relatively little) experience with Lean, one of the things I’ve appreciated most is the leanblueprint tool. For those not familiar with it, it’s a tool for planning a Lean development and ...
2k views

### How do real-world proof assistants bind variables and check equality?

There are many possible ways to represent syntax with variable binding, such as named variables, De Bruijn indices, De Bruijn levels, locally nameless terms, nominal type theories, etc. There are also ...
134 views

### Bijections on Coq

In the ssr.ssrfun library we have the following definition: Variant bijective : Prop := Bijective g of cancel f g & cancel g f. At first glance it was what I ...
• 271
1 vote
94 views

### Mimicking classic set extensionality in Coq

I am interested in strategies for encoding classical mathematics in Coq as a way of learning more about Coq and getting my hands dirty, so to speak. To that end, I have found this paper. I have read ...
• 3,105
31 views

### Coq 8.18 is not starting on Windows 10 - How to troubleshoot?

I have installed Coq on Windows 10 and I have managed to run and use it one time. But I was in need to restart my laptop and I hard-terminated Coq. Now I have restarted my computer and I am trying to ...
• 133