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
31 views

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

I have the following Coq code: ...
31 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
47 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
61 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
104 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
77 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
62 views

...
• 154
121 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,095
1 vote
69 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 ...
• 167
255 views

Uniqueness of proofs for inductively defined predicates

In Init/Peano.v the less-than-or-equal predicate is defined as follows: ...
44 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): ...
119 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 ...
• 249
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
49 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
126 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. ...
86 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
591 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,095
1 vote
80 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,095
209 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
37 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,095
1 vote
223 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
255 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,095
119 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,095
1 vote
59 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
100 views

Trying to use 'Equations'

Examples from Chlipala's book https://mattam82.github.io/Coq-Equations/examples/Examples.MoreDep.html ...
71 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,095
1 vote
72 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 ...
• 249
81 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,095
62 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,095
115 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
43 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,095
65 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,095
41 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,095
1 vote
121 views

Problems with dependent sums

Very simple trees (I trew away everything unnecessary) ...
1 vote
58 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): ...
• 167
124 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
34 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
981 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 ...
129 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 ...
• 249
1 vote
89 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,095
29 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
104 views

An unexpectedly hard question about type equality (of sigma types)

Suppose you have A: Type and P Q: A -> Prop such that {x : A | P x} = {x : A | Q x}. Can ...
• 121
45 views

A module signature is silently changed when it is imported. Its eq_dec lemma has its = operator changed to eq and no longer works

This following works as I'd expect it to. But if I place the TypeDef_S signature in another file then the apply typeDef.eq_dec. ...
33 views

Ltac with explicit constructor not working

I'm trying to do very simple reasoning about paths (e.g. in graphs) that are defined like follows: ...
• 167
99 views

How do I properly interact with CertiCoq's garbage collector when calling library functions from C++?

I am trying to build a C++ library backed by Coq sets, but I am continuously running into segfaults which I believe are related to garbage collection or memory leaks. I am using Coq 8.17.1 with a ...
81 views

About the use of command Canonical in Coq for mantaining Record Type information

Inside the MathComp book https://zenodo.org/records/7118596 there is the following example of use for the Canonical command: ...
68 views

What's the idiomatic way to instantiate a tuple of evars in Ltac2?

Suppose that I have a local definition of a type ty in the context, and ty can be any nested tuple, e.g.: ...
• 33