Questions tagged [coq]

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

41 questions with no upvoted or accepted answers
Filter by
Sorted by
Tagged with
7 votes
0 answers
68 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
7 votes
0 answers
173 views

What was the first proof assistant with eta equality for records?

The Agda language supports eta equality for (non-(co)inductive) record types: ...
Jesper's user avatar
  • 486
6 votes
0 answers
102 views

In VSCoq, how to issue an arbitrary Gallina query via the prompt?

I’m currently trying out Visual Studio + VSCoq, having previously used Emacs + Proof General for Coq, and there’s one part of my usual workflow that I haven’t managed to replicate yet. Is there a way ...
Peter LeFanu Lumsdaine's user avatar
6 votes
0 answers
73 views

What are Generic Arguments in Coq and how are they structured in their OCaml code?

I was trying to figure out why it seems that in a Coq generic argument there seems to be 3 arguments to the constructor GenArg when according to me there should ...
Charlie Parker's user avatar
6 votes
0 answers
170 views

How does one systematically traverse OCaml representations of Coq ASTs terms?

I want to be able to (tree) traverse Coq terms (e.g. in OCaml or using their s-expression representation in any language). My main challenge is to figure out how to do this systematically because I ...
Charlie Parker's user avatar
6 votes
0 answers
127 views

How to write heavily indexed proofs?

I've been playing with hereditary substitution. However, things get very awkward because substitution isn't total unless you index by the environment somehow. In my old approach terms were not indexed ...
Molly Stewart-Gallus's user avatar
5 votes
0 answers
104 views

Display style proofs using Coq

How to display proofs using in Gentzen tree style and (or) Fitch-style, using CoqIDE or JsCoq? PS: I'm rookie used coq.
Valdigleis's user avatar
5 votes
0 answers
127 views

Prove equality in a record type

I am trying to prove something about monoids an categories. This results in the following (partial) proof: ...
Tempestas Ludi's user avatar
4 votes
0 answers
46 views

Using CoqHammer from Ltac2

As it seems most likely to me, due to the special way arguments are evaluated in CoqHammer tactics (I tried to read the source code in OCaml but unfortunately I didn't understand much of it), it is ...
Vladimir Prigodsky's user avatar
3 votes
0 answers
75 views

Coq Typeclass on Functions Gets Confused by Equality

I was trying to use typeclasses to generalize the different notions of homomorphisms, but I’ve run into an annoying issue. Consider this code which demonstrates the issue: ...
sudgy's user avatar
  • 193
3 votes
0 answers
31 views

.CoqMakefile.d required by CoqMakefile but not generated

I am trying to use CoqMakefile to automatically build my Coq project in Coq 8.15.2. When I did this the compilation failed because a file ".CoqMakefile.d" was expected by make but did not ...
Rincewind's user avatar
3 votes
0 answers
77 views

Where is the discriminate tactic defined in Coq?

One can read the Coq documentation about discriminate tactic here. Were is this tactic actually defined?
Jacob woolcutt's user avatar
3 votes
0 answers
116 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 ...
Vladimir Prigodsky's user avatar
3 votes
0 answers
64 views

SSReflect tuple constructor: why not use phantom?

I was reading the mathcomp book learning about canonical structures and following along with the mathcomp source to compare how things were done in practice. Specifically I was looking at sections 6....
wdeweijer's user avatar
2 votes
0 answers
27 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
2 votes
0 answers
46 views

Factoring custom grammar rules for integers and lists in Coq custom entries

Is there a nice way to use custom entries to parse the following grammar? ("nice" meaning ~ "without massive duplication" and ~ "without needing to resort to separate ...
Jason Gross's user avatar
  • 1,447
2 votes
0 answers
61 views

Have Hyperdoctrines been formalized?

I was thinking of formalizing them myself for a project if they haven't been already, and I looked in libraries and couldn't find anything. I was thinking of coq in particular because it's the only ...
Julián's user avatar
  • 143
2 votes
1 answer
77 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 ...
8bc3 457f's user avatar
  • 224
2 votes
0 answers
138 views

Cannot open pixbuf loader module file in Windows

I installed Coq from the 8.15 64-bit installation file in Windows. I ran coqide and got the error message: ...
Moti's user avatar
  • 23
1 vote
0 answers
68 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
1 vote
0 answers
58 views

Injectivity, Surjectivity and Smallness on lists of natural numbers imply each other

Require Import Coq.Lists.List. I have the following properties defined on a list of natural numbers: ...
Agnishom Chattopadhyay's user avatar
1 vote
0 answers
46 views

Why does Coq not allow constructor argument types to be strictly positive mutual inductive types?

Note: Apologies for the wicked mouthful of a title. I'm still getting acquainted with Coq terminology, so I might not have chosen the best words. If you have a better title suggestion, edits are more ...
Kyle Lin's user avatar
  • 143
1 vote
0 answers
45 views

Can you always replace mutually recursive references with parameters?

This is a follow up to a question someone else previously posted: Expressivity of mutual/nested inductives vs. regular inductives. pigworker answered that Adopting Agda-ish notation, the basic ...
Kyle Lin's user avatar
  • 143
1 vote
1 answer
92 views

Defining Kripke models and the canonical model for $S4$ modal logic

I have defined the syntax of modal logic in Coq and now I'm having trouble with the semantics. This is how I defined the Kripke model: ...
Zara's user avatar
  • 111
1 vote
1 answer
140 views

Equivalence Relations COQ

I am also unfamiliar and trying to solve proofs relative to the topic Relations and Divisibility but I would like to solve such COQ proof theorems. I am not quite sure how to solve proofs like this ...
deleted_user0972's user avatar
1 vote
0 answers
44 views

Help with proofs in analysis

I would like to prove this in real analysis, but I’m finding it difficult to do it in Coq. Can someone help me, please. If $f(x_j)$ is non-linear $x_j \geq 0$, and $f(x_j) \geq 0$, and $f(0) = 0$, and ...
Felipe Morelli's user avatar
1 vote
2 answers
192 views

Dependent sum and equality with Coq

I have types B and A n where n:nat. I want to prove that ...
Pavel Shuhray's user avatar
1 vote
0 answers
44 views

How do I prove this property about a factorial specification in Coq?

Notes: This post got pretty long... my apologies but hopefully somebody can take the time to look through it. Also, some of the code below uses terms that are defined elsewhere in my file and not ...
bodacious_bandit's user avatar
1 vote
0 answers
82 views

How to reason about equality between different datatypes?

I am working on a verification project where the specification uses the following inductive datatype to represent bitvectors (MIT's bbv) ...
Felipe's user avatar
  • 63
1 vote
0 answers
25 views

Why does TacArg accepts a value of CAst.t type when it should only accept values of types?

See the argument for TacArg: | TacArg of ('t, 'dtrm, 'p, 'c, 'r, 'n, 'tacexpr, 'l) gen_tactic_arg but the reply has a type CAst.t as an argument for TacArg: <...
Charlie Parker's user avatar
0 votes
0 answers
3 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: process_begin: ...
Daniel Bee's user avatar
0 votes
0 answers
16 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
56 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
0 votes
0 answers
63 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
0 votes
0 answers
31 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
0 votes
0 answers
97 views

Formalization of partial functions for combinatorial counting

I need assistance in defining axioms for partial functions in total function theory that is available in Coq. Specifically, I'm looking for a constructive definition of a partial function that ...
arshiamoeini's user avatar
0 votes
1 answer
45 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 ...
asha soroushpoor's user avatar
0 votes
1 answer
131 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? ...
deleted_user0972's user avatar
0 votes
0 answers
58 views

If I make some new structure like Q, then can I use 'rewrite' tactic for my new structure in Coq?

From $\mathbb{Q}$, the set of all rational numbers, I make some new structure $I$, and also make strict order and (equivalence) equality on $I$. I want to use rewrite tactic for my defined relations (...
with-forest's user avatar
-2 votes
2 answers
79 views

Help with strong induction

I have the following definition of divisibility by 3. ...
deleted_user0972's user avatar
-2 votes
1 answer
192 views

How to write a summation in Coq

I have just started getting acquainted with Coq and I would like to write this sum on it: $\sum_{p=1}^{n} \frac{\mathrm{d}^p}{\mathrm{d}x^p} f(x)$ This is what I have tried: ...
Ícaro Lorran's user avatar