Questions tagged [coq]
Coq is a formal proof management system. It is often referred to as a proof assistant.
140
questions
46
votes
2
answers
3k
views
What are the main differences between Coq and Lean?
Coq and Lean are two of the most common proof assistants out there (but the question of course applies to other proof assistants too).
What are the main differences between Coq and Lean? Ideally it ...
- 733
35
votes
3
answers
1k
views
What exactly is setoid hell?
One of the only arguments I've heard about why Lean is better than Coq is that you can construct quotients of built-in structures by default. (In Coq, you apparently have to use Setoids instead of ...
- 451
24
votes
4
answers
770
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 ...
- 3,230
20
votes
1
answer
506
views
What is the state of coinductive types and reasoning in Coq?
Ever since the work by Gimenez for his PhD thesis, Coq has supported positive coinductive types. For example, the type of always-infinite streams containing elements of type ...
- 305
18
votes
1
answer
226
views
16
votes
3
answers
871
views
Well-foundedness: classical equivalence of no infinite descent and accessibility
I have often seen the claim that in a classical setting, well-foundedness of a relation > defined as the absence of an infinite descent ...
16
votes
1
answer
879
views
Why not have `Prop : Set` in Coq?
My understanding of Coq is that Prop : Type_1, Set : Type_1, and then Type_1 : Type_2, ...
- 163
15
votes
2
answers
294
views
What are the upsides and downsides of typed vs untyped conversion?
What are the tradeoffs between untyped and type-directed conversion in dependent type theory, and is there any consensus on what's "better"?
Background
Generally speaking, in dependent type ...
- 384
15
votes
1
answer
232
views
How do Coq's bidirectionality hints (`&`) affect type checking?
I have used Coq's bidirectionality hints (placement of & in a call to Arguments) to some effect, mostly by trial and error. ...
- 601
14
votes
3
answers
865
views
How to extract the witness from exists in Coq in function notation/without destructing?
Assuming I have some definition with a forall and an exists like so:
Definition fooable A B P := forall a : A, exists b : B, P a b.
Then on an intuitive level, I ...
- 243
14
votes
1
answer
206
views
Converting between formulations of reals in Coq
While trying to answer more concretely a question on floating points, I tried proving a simple statement using the Flocq library of Coq. However, I got stuck before really exercising it because I am ...
- 482
13
votes
2
answers
278
views
Is eta-equality provable in Coq?
Trying to answer another question, I can't help second guessing myself about whether eta equality is provable in Coq. In particular, can one prove
...
- 2,051
13
votes
3
answers
695
views
Calculus of (inductive) Constructions: Do inductive definitions increase proof strength?
Question
Is CiC stronger than CoC, in terms of proof strength?
Context
To illustrate the kind of confusion I am in, and what I'd like to learn from the answer, here is part of my inner monologue:
If I ...
- 139
13
votes
1
answer
235
views
How do I turn off the aggressive auto-indent in Proof General/Coq
I have installed Proof General via Doom Emacs' coq module, keeping most settings as whatever default that module sets. Sometimes the automatic indentation this ...
- 601
11
votes
2
answers
447
views
How does the formal proof of the four color theorem work?
Over a decade ago, Georges Gonthier, gave a formal proof of the four color theorem. I have a mental picture of how the proof works, and I'd like to see if it is correct.
The original proof of the ...
- 5,748
11
votes
1
answer
553
views
What is the role of impredicativity in program extraction?
Is impredicativity useful for program extraction in Coq? For example is there some kind of realizability argument that depends on impredicativity?
Of course it doesn't seem to be necessary for program ...
- 2,051
11
votes
1
answer
125
views
What are the differences between jsCoq and the versions of Coq that can be downloaded?
I found a site where I can use Coq in my browser: jsCoq Interactive Online System. Are there any major differences between the experience I'm getting on this site and the downloadable version(s)?
- 213
11
votes
2
answers
366
views
Proving uniqueness of an instance of an indexed inductive type
Consider the simple indexed inductive type
Inductive Single : nat -> Set :=
| single_O : Single O
| single_S {n} : Single n -> Single (S n).
Intuitively, I ...
- 213
11
votes
1
answer
138
views
What did Coq 8.15 change about divmod?
I noticed that Coq 8.15 (possibly 8.14) made some significant changes to divmod. In particular, Nat.divmod_0q0 seems to have been removed and the ...
- 213
11
votes
1
answer
188
views
Naming conventions (letter case, underscores, &c) for Coq
Does Coq have an established convention/style for constructors, variables, terms, &c?
An established convention that isn't exceptionless is totally fine. For example, terms should be lowercase ...
- 2,651
10
votes
2
answers
2k
views
How can we formalize a game where each player is a program having access to opponent's code?
How can we define in a proof assistant (eg., Coq) a notion of a 2-player game, where each player is a program that has access to the opponent's source code?
Background: In Open Source Game Theory, we ...
10
votes
1
answer
194
views
Is there a Mizar-like sublanguage for Coq?
Isabelle has the frontend Isar which mimics some features of the Mizar system.
I'm curious if Coq has anything similar, i.e. an alternative to tactic scripts that's designed to be readable or similar ...
- 2,651
9
votes
2
answers
416
views
Learning Math Proof via Proof Assistants
I want to learn proof based mathematics and it looks like a proof assistant like Coq and Lean could be a good way to go about verifying my proofs, without needing a PhD on hand to check through all my ...
- 93
9
votes
1
answer
560
views
What axioms do I need to search the naturals?
Theorem search
{P : nat -> Prop} (dec : forall n, {P n} + {~P n})
: ~~(exists n, P n) -> {n | P n}.
Admitted.
I don't think this is provable in Coq without ...
- 413
9
votes
2
answers
412
views
Defining coercion for proof irrelevant equality
Say I would like to define coercion for proof irrelevant equality between types. In Coq I try
...
- 2,051
9
votes
2
answers
543
views
Is coercion to a higher universe injective?
A type that is a member of a universe can be coerced into a higher universe. Is that coercion injective? That is, if two elements of U1 are equal after being coerced to U2, does that imply they are ...
- 153
8
votes
2
answers
727
views
Explanation of Coq math-comp repositories
How are the Coq math-comp account and repositories related?
Details
One of my side goals is to try to keep the tags on this site meaningful and useful.
Today I ran into this question:
How to prove ...
- 2,796
8
votes
3
answers
235
views
How to prove that addition is commutative for conatural numbers in Coq
I have defined the conatural numbers, bisimulation (extensional equality?) and addition as follows,
...
- 101
8
votes
2
answers
170
views
How to prove `forall m n : nat, m == n -> m = n`?
I am learning Coq with ssreflect. Just to understand things, I've proved forall a b : bool, a == b -> a = b but I can't figure out how to prove ...
- 317
8
votes
2
answers
182
views
Coq: Recursive Smart Constructors and Sigma types, how to avoid axioms
I am using a recursive smart constructor to return a sigma type, which includes the property that the type was constructed in a smart way. This is very basic compared to the smart constructors and ...
- 305
8
votes
3
answers
305
views
Has anyone accidentally "proven" a false theorem using what was later found to be a critical bug?
Critical bugs are periodically found in Coq, and I assume in other proof assistants as well. We are still happy to mostly trust the proof assistants, partly because these critical bugs are relatively ...
- 874
7
votes
4
answers
156
views
Are there any ergonomic ways to deal with finite types in Coq?
I am trying to work with proofs about fixed-size bitvectors, or a map from a finite type to bool. What I'm finding is that "finite type" is actually ...
- 73
7
votes
1
answer
100
views
Tactic unification vs evarconv in Coq
I gather, from practical experience and Zulip hearsay, that Coq has two unification algorithms, known as “tactic unification” and “evarconv”. However, I can't find any documentation on these from a ...
- 601
7
votes
1
answer
92
views
Why Coq's `Include` is designed to instantiate functor with current interactive defining module?
It is surprising for me to see that Coq can Include a functor and will instantiate it with the current interactive module.
Coq Ref Manual:
Command Include ...
- 429
7
votes
0
answers
137
views
What was the first proof assistant with eta equality for records?
The Agda language supports eta equality for (non-(co)inductive) record types:
...
- 421
6
votes
2
answers
2k
views
Why are these two proofs so different?
I was messing around with toy lemmas in Idris and came up with this silly proof.
...
- 328
6
votes
1
answer
245
views
How to replace a function by its body
I have this function:
Definition bexp x y := bexp_r x y [true].
And I have this goal:
value (bexp [] y) = 0 ^ value y
I want ...
user1231
6
votes
2
answers
258
views
Problem proving a binary add function
I'm fairly new to the Coq language and I want to prove a function that does an binary add from numbers represented as a list (least significant bit upfront).
I have created this badd function that ...
user1231
6
votes
1
answer
111
views
Does Coq's Module and Functor type-check incrementally?
I am trying to search the following questions online but I failed:
When applying a functor (parametrized module), will the contents inside the functor be re-type-checked?
Will Coq's command ...
- 429
6
votes
1
answer
143
views
How to set defaults for implicit arguments when they can't be inferred?
If I had a module declared as follows in file A.v:
Section A.
Context {𝒳 : Set}.
Inductive abt := Abt_leaf (x : 𝒳) | Abt_node.
End A.
And in another file, B....
- 157
6
votes
0
answers
82
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 ...
6
votes
0
answers
115
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 ...
- 2,628
5
votes
3
answers
200
views
How do you import part of the standard library in Coq?
How do you import part of the standard library in Coq?
How do you import Nat specifically?
Why is reporting Nat not required to ...
- 2,651
5
votes
1
answer
277
views
Formal description of Coq’s termination checker
Coq’s built-in termination checker accepts some rather intricate recursion patterns with functional values in data types, as shown by this example
...
- 1,614
5
votes
2
answers
161
views
Basics of real numbers in mathcomp (Coq)
I'm trying to play around with the Mathematical Components library in Coq but am having trouble writing basic, concrete statements about real numbers. E.g., I'd like to define
...
- 153
5
votes
3
answers
89
views
Hide the value of a hypothesis introduced by `pose`, show only its type
In proof mode, if I know an expression e of type T, I can write pose foo : T := e to add <...
- 317
5
votes
2
answers
72
views
How to provide a countType when using mathcomp?
The following snippet can't pass type checking.
From mathcomp Require Import choice.
Definition exfn (A:countType) := false.
(* Fail *) Check exfn nat.
Failed with ...
- 157
5
votes
1
answer
124
views
How to implement first-order relational structures in Coq?
I'm trying to define a first-order relational structure in Coq.
I have a way to define a pre-first-order-relational-structure, which is not a standard notion, but seems simple enough.
I also have a ...
- 2,651
5
votes
1
answer
95
views
Unexpected eta expansion in constant definition
Start from this example in section 2.1.14: Polymorphic Universes in Coq's reference maunual (slightly modified):
...
- 90
5
votes
1
answer
176
views
How to fold simplified goal?
I have written a Program Fixpoint called generic_debugging_algorithm with a measure, and I have one obligation left to prove.
To me the obligation reads like:
...
