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
0 votes
0 answers
20 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 ...
1 vote
0 answers
79 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 ...
2 votes
1 answer
137 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 ...
2 votes
2 answers
74 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 ...
2 votes
0 answers
39 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. ...
1 vote
1 answer
63 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: ...
0 votes
1 answer
27 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: ...
26 votes
4 answers
1k views

What are the differences between MLTT and CIC?

In the theory and design of proof assistants based upon dependent types, I feel like there’s a somewhat cultural divide between the "MLTT" world (with Agda as the main representative proof ...
2 votes
1 answer
55 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.: ...
3 votes
1 answer
136 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: ...
2 votes
4 answers
132 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 ...
0 votes
1 answer
44 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 ...
2 votes
5 answers
447 views

LEM, the halting problem, the curry-howard correspondence -> deep connection?

I posted the following on the math stackexchange, but it occurs to me that this might be a more (or at least equally?) appropriate forum: It was recently said to me by a prominent mathematician, who I ...
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 ...
2 votes
1 answer
38 views

Rewriting/Applying unidirectional morphisms in Coq

Link to Code Gist I have the following definition ...
2 votes
1 answer
85 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: ...
3 votes
3 answers
217 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 ...
3 votes
1 answer
114 views

Inductive from CoInductive?

It is possible to represent CoInductive using parts that are Inductive. As a simple example, ...
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: ...
1 vote
1 answer
71 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 ...
4 votes
1 answer
245 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. ...
0 votes
1 answer
68 views

Coq, Merging two forall definitions ranging over the same types

...
2 votes
1 answer
88 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 ...
0 votes
1 answer
93 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 ...
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 ...
6 votes
0 answers
164 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 ...
2 votes
1 answer
66 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 ...
3 votes
2 answers
63 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 ...
4 votes
2 answers
95 views

what symbols can I use in coq?

Is it possible to use symbols like $\mathbb{N},\forall,\implies$ in Coq?
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 ...
0 votes
1 answer
35 views

Tactic to Propify a bool expression

Let's say I have bool expressions <bexp> consisting of true, false, variables, ...
0 votes
1 answer
74 views

Coq - Overloading over multiple parameters with canonical structures

The following is a minimal example of overloading a function on one parameter with canonical structures: ...
0 votes
0 answers
38 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: ...
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 ...
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, ...
1 vote
1 answer
91 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" ...
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: ...
4 votes
3 answers
182 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....
5 votes
2 answers
581 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 ...
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: <...
2 votes
1 answer
88 views

Proving that equality is decidable on an ``Inductive Set``

I've managed to prove that equality within a type is indeed decidable. ...
0 votes
1 answer
163 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? ...
2 votes
1 answer
139 views

Is there a way to rename parameters when including/reusing a module type in Coq?

Say I have a (more general) module type Collection that specifies some operations like read and write and now I want to create (more specialized) module types like <...
0 votes
1 answer
136 views

Can proof assistants reflect the informal notion of a “theory” as the formally logical notion of a “theory”?

Let us say that I wish to study and understand gauge symmetry using a formally verified mathematical programming language like Lean or Coq. Lean has many libraries you can import to express ...
6 votes
1 answer
342 views

What are the principal differences between Agda's core type theory and Coq's?

Agda is said to be based on Luo's unifying theory of dependent types while Coq is based on the Calculus of Inductive Constructions. Both of these as I understand it extend the impredicative ...
1 vote
1 answer
54 views

Using coIH as an argument to the transitivity of Bisimilarity (cofix and pcofix)

It might be a very silly question for the logic gurus but less so for me. First I generally describe the issue, than I provide a proper example with code. Assume three streams of nats: xs, ys, zs. ...
2 votes
3 answers
113 views

Induction on indexed type family without JMeq

I'm trying to do induction on an instance of an indexed type family in Coq. Here's a simplified example: ...
3 votes
1 answer
99 views

Stuck in a proof about sum types and nonempty lists

I have a hard time proving an apparently simple property or finding a counterexample. It is about sum types and nonempty lists. I first define two basic functions about sum types: ...
3 votes
1 answer
141 views

Recursive notations with forall quantifier

How can I implement a notation of the form: ∀ x ≤ y ≤ .. ≤ z ≤ t, φ in Coq? A similar notation (but without quantifiers) appears here ...
3 votes
2 answers
95 views

Defining and using bisimilarity for negatively-defined conatural numbers

Since positive coinductive types in Coq are evil and break subject reduction, I am trying to develop the theory of the conatural numbers using the following negative formulation (within a module ...

1
2 3 4 5 6