Skip to main content

Questions tagged [coq]

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

Filter by
Sorted by
Tagged with
1 vote
2 answers
30 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 ...
Bruno's user avatar
  • 227
0 votes
2 answers
34 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. ...
Greg Nisbet's user avatar
  • 2,829
0 votes
1 answer
38 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 ...
Greg Nisbet's user avatar
  • 2,829
2 votes
0 answers
91 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 ...
Ember Edison's user avatar
2 votes
1 answer
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 ...
Greg Nisbet's user avatar
  • 2,829
0 votes
1 answer
36 views

Proof General tell Coq where a physical path is

Here is the first few lines of Auto.v in Software Foundations Volume 1. ...
Greg Nisbet's user avatar
  • 2,829
0 votes
0 answers
37 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 ...
Greg Nisbet's user avatar
  • 2,829
1 vote
1 answer
108 views

Problems with dependent sums

Very simple trees (I trew away everything unnecessary) ...
Pavel Shuhray's user avatar
1 vote
1 answer
49 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): ...
return true's user avatar
3 votes
2 answers
105 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 ...
alphie k's user avatar
0 votes
1 answer
27 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 ...
user2628206's user avatar
4 votes
3 answers
446 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 ...
Peter LeFanu Lumsdaine's user avatar
10 votes
5 answers
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 ...
2 votes
2 answers
122 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 ...
Bruno's user avatar
  • 227
1 vote
2 answers
80 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 ...
Greg Nisbet's user avatar
  • 2,829
0 votes
0 answers
26 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 ...
TomR's user avatar
  • 133
2 votes
0 answers
92 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 ...
Veky's user avatar
  • 121
2 votes
0 answers
43 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. ...
Glyn Webster's user avatar
0 votes
1 answer
31 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: ...
return true's user avatar
2 votes
2 answers
97 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 ...
Jennifer Paykin's user avatar
2 votes
1 answer
71 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: ...
Bruno Rafael's user avatar
2 votes
1 answer
59 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.: ...
Ke Du's user avatar
  • 23
3 votes
1 answer
145 views

Error `Abstracting over the term leads to a term which is ill-typed` when doing a destruct

I'm trying to make a version of nth that cannot fail because it knows that the index is inbounds. So far, so good: ...
return true's user avatar
0 votes
1 answer
52 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 ...
user2628206's user avatar
2 votes
4 answers
136 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 ...
Glyn Webster's user avatar
2 votes
1 answer
38 views

Rewriting/Applying unidirectional morphisms in Coq

Link to Code Gist I have the following definition ...
Agnishom Chattopadhyay's user avatar
2 votes
1 answer
91 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: ...
Jay Lee's user avatar
  • 123
3 votes
3 answers
224 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 ...
Glyn Webster's user avatar
1 vote
1 answer
74 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 ...
Djoser's user avatar
  • 1
3 votes
1 answer
118 views

Inductive from CoInductive?

It is possible to represent CoInductive using parts that are Inductive. As a simple example, ...
scubed's user avatar
  • 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: ...
camsterwheel's user avatar
1 vote
1 answer
72 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 ...
Agnishom Chattopadhyay's user avatar
4 votes
1 answer
254 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. ...
ignorant student's user avatar
0 votes
1 answer
70 views

Coq, Merging two forall definitions ranging over the same types

...
The Circle's user avatar
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 ...
Pietro Braione's user avatar
2 votes
1 answer
89 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 ...
The Circle's user avatar
6 votes
0 answers
166 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 ...
Patrick Nicodemus's user avatar
2 votes
1 answer
70 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 ...
user2628206's user avatar
3 votes
2 answers
66 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 ...
Hiroki Chen's user avatar
4 votes
2 answers
99 views

what symbols can I use in coq?

Is it possible to use symbols like $\mathbb{N},\forall,\implies$ in Coq?
RataMágica's user avatar
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 ...
Julius Hamilton's user avatar
0 votes
1 answer
36 views

Tactic to Propify a bool expression

Let's say I have bool expressions <bexp> consisting of true, false, variables, ...
Agnishom Chattopadhyay's user avatar
0 votes
0 answers
42 views

Coq: Language server crashes when trying to introduce an equality-hypothesis

I'm working in Coq in VSCode (using VSCoq). Repeatedly the Coq language server crashes. I try to prove the following: ...
name1les's user avatar
3 votes
2 answers
64 views

Creating a tactic for 'destructing' a list by last element?

Sometimes, I have a context in which I have some l : list X, and I want to prove the goal by proving that (1) If l = [], the ...
Agnishom Chattopadhyay's user avatar
2 votes
0 answers
80 views

Why does the following Coq code fail to meet Coq's positivity requirement for inductive types?

I'm currently studying a proof of Gödel's incompleteness theorem written in Coq, by Russell O'Connor. I would like to understand the following section: 2.2 Definition of Term For any given language, ...
Julius Hamilton's user avatar
1 vote
1 answer
92 views

Assistance using destruct on an equality proof for functors

Context I am currently learning how to use the Coq proof assistant and am at the level where I know the fundamentals of dependent-type theory and have done most of the "Software Foundations" ...
user2628206's user avatar
5 votes
2 answers
587 views

In Coq, what tactic can I use to remove a True precondition from a hypothesis

One of my hypothesis is an implication with an always-true condition (x=x->P). What tactic can I use to rewrite this hypothesis into its conclusion ...
hugomg's user avatar
  • 153
4 votes
3 answers
188 views

For formal proofs of graph structures and algorithms, which proof assistant should I learn?

My goal is to be able to make formal proofs for graph structures and algorithms, proving i.e. for every vertex in a directed-acyclic-graph there exists a path from a source vertex to that vertex, or i....
Snowybluesky's user avatar
0 votes
1 answer
54 views

Proving non-existence of "least" subtype generator in Coq

I'm working through Programming Language Foundations in my free time. In the subtyping chapter, I am greeted by the following exercise, where TF P := P \/ ~ P: <...
Charles Averill's user avatar
5 votes
4 answers
1k views

How to prove non-existence of terms that contain themselves in Coq

Why can't inversion figure out that it isn't structurally possible for a term to contain itself? Here's a basic example: ...
Charles Averill's user avatar

1
2 3 4 5
7