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
2 votes
3 answers
47 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: ...
LightQuantum's user avatar
0 votes
1 answer
41 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: ...
Soundwave's user avatar
  • 101
3 votes
1 answer
88 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: ...
Dave's user avatar
  • 165
3 votes
2 answers
71 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 ...
Ian Maxwell's user avatar
1 vote
1 answer
61 views

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

I've managed to prove that equality within a type is indeed decidable. ...
Johan Buret's user avatar
5 votes
1 answer
151 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 ...
Patrick Nicodemus's user avatar
2 votes
1 answer
69 views

Define “vector space” from scratch in Coq

I just want to learn how to use Coq better. Supposing I wanted to prove a statement like “a vector space is naturally isomorphic to its dual”. I would like to see how to define the concepts used in ...
Julius H.'s user avatar
1 vote
3 answers
103 views

Is there a way to incorporate K's axiom while keeping the system consistent with univalence?

It has been known that if a type $A$ has decidable equality, i.e., $\forall a b: A, a = b \vee a \neq b$, then we can happily say that any two proofs for $a = b$ must be identical. Sometimes, we will ...
Hiroki Chen's user avatar
3 votes
1 answer
184 views

Selecting both a hypothesis and Goal while applying a tactic

I have a hypothesis H and some function foo. I want to simplify foo in both H and the ...
Agnishom Chattopadhyay's user avatar
2 votes
1 answer
127 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 <...
C.E.Sally's user avatar
  • 121
0 votes
0 answers
58 views

How to get term describing case of pattern match in Coq

In Coq, While trying to write a definition of a function with well-founded recursion, I found myself wanting/having to reference that a term I was trying to match ...
C.E.Sally's user avatar
  • 121
2 votes
1 answer
128 views

Does equality in $\Sigma_{(x : X)} x = x$ implies UIP?

The short version: Is this statement correct? If it is, is it provable in Coq? ...
Liu Xiaoyi's user avatar
1 vote
0 answers
40 views

how to inductively define paths from paths using unimath

I'd like to define a type of graph where given a set of edges, we can define another graph that has everything from graph 1 but extends the set of edges by adding higher level edges to parallel edges(...
noCrayCray's user avatar
0 votes
0 answers
31 views

How to import unimath for coq

I want to be able to import the category theory module from unimath. I already have the coqide and vscode with the coq extensions, I also have wsl. I tried downloading the library from git and used &...
noCrayCray's user avatar
4 votes
0 answers
116 views

Proving "proof methods" as theorems in type-theory based proof systems

For example, suppose we have proved associativity of some binary operator $+ : T \to T$ as add_assoc : forall (x y : T), x + y + z = x + (y + z). We can thus prove ...
user23220385's user avatar
1 vote
1 answer
76 views

In Coq, are there drawbacks in making implicit some arguments?

We have ...
Bruno's user avatar
  • 195
1 vote
1 answer
84 views

How to apply constructor injectivity in the goal

Suppose I have a goal Goal forall m n, S m = S n -> m = n. intros m n H. 1 goal m, n : nat H : S m = S n ============================ m = n I know ...
smithers's user avatar
1 vote
2 answers
201 views

How to correctly feed type argument in this toy theorem?

I have a recursive function combine defined as following: ...
Sajuuk's user avatar
  • 113
1 vote
2 answers
162 views

Coq / Lean endpoint for GPT actions

I'm trying to produce Coq and Lean code using a custom GPT but I want GPT to try running its proof scripts (and revising them if they fail) before suggesting them to me (via gpt actions). Right now, ...
Rand00's user avatar
  • 223
0 votes
2 answers
254 views

How can I generate equalities from an application in Coq?

When I try to apply a lemma or constructor in Coq, I often run into the situation where lemma doesn't unify exactly with goal I'm working on, even though I know it could be rewritten to match. For ...
Matt's user avatar
  • 9
0 votes
1 answer
132 views

How to reason with notations directly?

Intuitive notations are always a big boost when stating and proving things. Modern interactive theorem provers usually have some way of building syntactic sugars aside from their ordinary abstraction ...
yiyuan-cao's user avatar
0 votes
0 answers
60 views

Forward simulation with partial simulation relation

I am trying to prove the following forward simulation statement. ...
user1953221's user avatar
2 votes
4 answers
301 views

How to to use the fact that combining these hypothesis is false in Coq

Suppose that I have a hypothesis H1 : a > y and another hypothesis H2 : a <= y in Coq. I want to use the fact that ...
Link L's user avatar
  • 135
1 vote
1 answer
78 views

Proof of Constant folding in Coq for IMP using Interaction Trees

Hello Stack Exchange Community, I'm currently working on my thesis which involves using Interaction Trees to define big-step operational semantics for programming languages, particularly the IMP ...
Andrea Tirelli's user avatar
-2 votes
1 answer
46 views

plz any guide me for coq extension in VS code

I am currently exploring Coq development in Visual Studio Code and would like to enhance my experience with suitable extensions. Could you kindly recommend all available Coq extensions for Visual ...
Gul's user avatar
  • 1
0 votes
1 answer
187 views

A Coq program which constructively proves the halting problem

I'm looking for a constructive proof of the halting problem in Coq. The proof sketch described on this wikipedia article is constructively valid. However, I am not sure how to translate this into Coq ...
user avatar
-1 votes
2 answers
70 views

Coq makefile complains about extension points on Windows 10

I installed Coq 8.16.1 on Windows 10 recently. I have a full development previously written in Coq 8.9.0 on Linux and want to upgrade to this. When I run make, I get this error: ...
Daniel Bee's user avatar
0 votes
3 answers
270 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 ...
user avatar
0 votes
1 answer
84 views

What is the difference between these inductive definitions in Coq?

I came up with the following inductive definitions in Coq for an even number: ...
Link L's user avatar
  • 135
1 vote
0 answers
70 views

Unfolding constants while rewriting using rewrite_strat and a hint database

I'm working with a substitution algebra as described by the Autosubst team, and I'm trying to automate some rewritings. As I'm using more than one calculus in my code, I'm trying to use the rewrite ...
paulotorrens's user avatar
4 votes
1 answer
149 views

What is the best way to learn Iris completely independently

I am looking forward to learning Iris by myself, I have essential basic knowledge of Coq and logic but I don't know where to start. Logically, I looked into materials on the project website; the video ...
asha soroushpoor's user avatar
0 votes
0 answers
19 views

reference ospecialize and variable prim_base_irreducible not found in the current environment

Error encountered when trying to make after coq_makefile -f _CoqProject -o Makefile for lambda-rust ...
Sheldon's user avatar
  • 123
0 votes
0 answers
65 views

How to check a Zenon-generated proof with Coq?

I installed zenon (opam package, github) and tried to use it to generate a Coq proof. I couldn't find any documentation for the Zenon's main syntax, so I looked at its test suite. I grabbed this test ...
Greg Nisbet's user avatar
  • 2,711
1 vote
1 answer
97 views

problem with unification

I've faced a problem. I'm not sure how to explain it, so, that is why I'm asking. ...
Andrey's user avatar
  • 215
1 vote
1 answer
76 views

How to express that two equivalence relations can setoid rewrite across each other (Coq)

I am looking for a way to express that two equivalence relations are compatible and can (setoid) rewrite across each other. As an example here's an ordinary proof I wrote that a left inverse implies ...
Chris Henson's user avatar
3 votes
2 answers
211 views

Universe inconsistency errors when using ZF model in Coq

I am trying to use a formal logic system I recently implemented in Coq to study ZF set theory. In order to do this, I need to define a type representing the domain in question, and then prove that ...
Circuit Craft's user avatar
0 votes
1 answer
147 views

Why inductive types (or variants) are so rigid in terms of the set of constructors

An inductive type definition normally carries a set of constructors C, but I am not so sure why the set of constructors C is always once-for-all statically defined. For instance: ...
Tiago Campos's user avatar
2 votes
2 answers
104 views

Continue a section (with context) in coq

So I have a file in coq, which is a bit like the following: ...
Tempestas Ludi's user avatar
2 votes
0 answers
30 views

Problem working with FMapWeakList and Parametrized Records

Consider the following definition of a record R, parametrized over an arbitrary eqType: ...
Felipe's user avatar
  • 63
0 votes
0 answers
81 views

Help with fixing a Coq installation using docker and vscoq

I'm following the logic foundation preface and just began learning. I tried to use the docker with vscoq like the suggested in the book but it didn't work for me and kept asking me to install coq ...
Abde Mojito's user avatar
5 votes
1 answer
176 views

Universe polymorphism and Coq standard library

When developing in Coq with the Universe Polymorphism flag on, the standard library introduces unwelcome universe constraints because it is universe monomorphic. Is there an alternative standard ...
Jon's user avatar
  • 75
1 vote
1 answer
74 views

Use proof irrelevance in cast

I'm working using cast in Coq.Vectors. When trying to rewrite with proofs, I'd like to use the fact of proof irrelevance (Coq.Logic.Eqdep_dec), preferably automatically. I.e., when I have a lemma ...
Adrian L's user avatar
2 votes
2 answers
124 views

Proving that a minimum example exists if any example exists in nat

I'm trying to prove that if a function from nat -> bool is true for any natural number, then there exists a minimum natural number which the function is true for. I've been trying to find a good ...
Tony Peterson's user avatar
7 votes
0 answers
75 views

How do I write a minimal working example (MWE) in Coq to demonstrate some problem?

To get help with some incomplete proof script or definition in Coq, or demonstrate some failing (e.g., Ltac) tactic or command, I am often asked to write a minimal working example (MWE) of Coq ...
palmskog's user avatar
  • 395
2 votes
1 answer
98 views

Eta-equality for records: the case of semigroups

Consider the following definition of a semigroup: ...
Jon's user avatar
  • 75
3 votes
1 answer
97 views

gappa seems to generate bad Coq

I'm using the -Bcoq backend of gappa. The coq file contains dollar signs. So far as I can tell, a coq file should not contain dollar signs. Here is a snippet from -Bcoq : ...
Michael Hennebry's user avatar
2 votes
1 answer
206 views

iris/algebra/auth.vo has bad version number 81700 (expected 81601) for IRIS Coq

...
Sheldon's user avatar
  • 123
6 votes
1 answer
308 views

(Dis)Advantages of basing a proof assistant on CH correspondence?

Major proof assistants like Lean and Coq are fundamentally based on the Curry-Howard correspondence: propositions are encoded as types, quantified propositions are encoded as dependent types, proofs ...
Weier's user avatar
  • 293
0 votes
0 answers
34 views

Why does Program Fixpoint leave behind a temporary_proof2_subproof axiom in this example?

I have reduced my development into the following minimal reproducer: ...
Maya's user avatar
  • 151
1 vote
1 answer
95 views

confused about stlc from Programming Language Foundations

I have two related quetions. I made my way to STLC and Typechecking from Programming Lang Foundations, yet I am more or less mentally stuck at the STLC chapter, hence many things related to it are ...
noCrayCray's user avatar

1
2 3 4 5