Questions tagged [coq]
Coq is a formal proof management system. It is often referred to as a proof assistant.
333
questions
2
votes
1
answer
100
views
How to use Modus Ponens in L axiomatic system
I have copied a system of axioms for L system described in book Mendelson "Introduction into Logics":
...
- 125
2
votes
1
answer
80
views
Is it possible to simplify/normalize nat arithmetic expressions in Coq?
I'm writing a tactic to apply some normalizing rewriting rules on a substitution algebra, similar to the autosubst project. I've made a sigma tactic that applies ...
- 153
3
votes
1
answer
85
views
Extensional sets in Coq and induction
I would like to define the following data type in Coq:
Inductive X : Type :=
| constr : FinSet X -> X.
Here constr should take a single argument, which is a finite set of elements of X. I need this ...
- 31
4
votes
1
answer
384
views
How does Coq guess `i` is decreasing?
As far as I know, fix must be called with a decreasing argument.
In the following code, i is the decreasing argument of ...
- 223
1
vote
1
answer
59
views
Accessing nested typeclasses elegantly
I have a situation where one typeclass is "nested" in another one like this:
...
- 179
2
votes
1
answer
57
views
1
vote
2
answers
61
views
How do I apply a lemma to both sides of an equality hypothesis?
I have the following Coq code:
...
- 13
0
votes
0
answers
43
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
0
votes
0
answers
56
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
1
answer
65
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
1
answer
145
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
3
votes
0
answers
84
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
2
votes
0
answers
68
views
2
votes
2
answers
132
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,105
1
vote
1
answer
82
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 ...
- 179
2
votes
3
answers
266
views
Uniqueness of proofs for inductively defined predicates
In Init/Peano.v the less-than-or-equal predicate is defined as follows:
...
- 127
0
votes
0
answers
54
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):
...
2
votes
2
answers
132
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 ...
- 271
0
votes
1
answer
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
1
answer
51
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
3
votes
2
answers
128
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.
...
- 223
3
votes
2
answers
89
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
2
votes
3
answers
629
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,105
1
vote
1
answer
82
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
5
votes
4
answers
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,105
3
votes
1
answer
221
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
1
answer
40
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,105
1
vote
4
answers
232
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 ...
- 288
1
vote
2
answers
266
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,105
3
votes
1
answer
130
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,105
1
vote
1
answer
60
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
1
answer
105
views
Trying to use 'Equations'
Examples from Chlipala's book
https://mattam82.github.io/Coq-Equations/examples/Examples.MoreDep.html
...
- 127
2
votes
1
answer
72
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,105
1
vote
2
answers
74
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 ...
- 271
0
votes
2
answers
82
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,105
0
votes
1
answer
69
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,105
3
votes
0
answers
125
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
2
votes
1
answer
46
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,105
0
votes
1
answer
88
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,105
0
votes
0
answers
49
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,105
1
vote
1
answer
122
views
1
vote
1
answer
59
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):
...
- 179
3
votes
2
answers
128
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
0
votes
1
answer
36
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
6
votes
3
answers
1k
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 ...
11
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
134
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 ...
- 271
1
vote
2
answers
94
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,105
0
votes
0
answers
31
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
2
votes
0
answers
114
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