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
59 votes
2 answers
5k 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 ...
Ricky's user avatar
  • 908
40 votes
3 answers
2k 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 ...
setholopolus's user avatar
25 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 ...
Meven Lennon-Bertrand's user avatar
22 votes
1 answer
765 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 ...
palmskog's user avatar
  • 395
18 votes
1 answer
267 views

When to use coinductive types?

One could define streams in the following manner ...
Agnishom Chattopadhyay's user avatar
16 votes
3 answers
958 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 ...
Théo Winterhalter's user avatar
16 votes
1 answer
958 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, ...
Emma Hudson's user avatar
16 votes
2 answers
343 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 ...
Blaisorblade's user avatar
15 votes
1 answer
279 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. ...
James Wood's user avatar
14 votes
4 answers
1k 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 ...
Sacchan's user avatar
  • 243
14 votes
1 answer
242 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 ...
Bruno Le Floch's user avatar
13 votes
2 answers
370 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 ...
Couchy's user avatar
  • 2,171
13 votes
3 answers
759 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 ...
Max Kubierschky's user avatar
13 votes
1 answer
350 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 ...
James Wood's user avatar
12 votes
1 answer
243 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 ...
Greg Nisbet's user avatar
  • 2,711
11 votes
1 answer
592 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 ...
Couchy's user avatar
  • 2,171
11 votes
2 answers
523 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 ...
Jason Rute's user avatar
  • 7,240
11 votes
1 answer
145 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)?
Laurel's user avatar
  • 213
11 votes
2 answers
389 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 ...
L. F.'s user avatar
  • 213
11 votes
1 answer
151 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 ...
Rand00's user avatar
  • 213
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 ...
Matthias Georg Mayer's user avatar
10 votes
1 answer
229 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 ...
Greg Nisbet's user avatar
  • 2,711
9 votes
2 answers
688 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 ...
quidproquo's user avatar
9 votes
1 answer
586 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 ...
HTNW's user avatar
  • 458
9 votes
2 answers
432 views

Defining coercion for proof irrelevant equality

Say I would like to define coercion for proof irrelevant equality between types. In Coq I try ...
Couchy's user avatar
  • 2,171
9 votes
2 answers
551 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 ...
Kyle Stemen's user avatar
8 votes
2 answers
790 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 ...
Guy Coder's user avatar
  • 2,826
8 votes
4 answers
239 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 ...
Ben Little's user avatar
8 votes
3 answers
324 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, ...
Daigo's user avatar
  • 101
8 votes
2 answers
197 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 ...
CrabMan's user avatar
  • 317
8 votes
2 answers
220 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 ...
Walter Schulze's user avatar
7 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. ...
Nathan's user avatar
  • 348
7 votes
2 answers
1k views

Is it possible to make a proof assistant program based on ZFC?

I heard that many proof assistant programs are made based on the type theory. For me, as a mathematician, when I met Coq at first, it is difficult to accustomed with it. So I have a question. Is it ...
with-forest's user avatar
7 votes
1 answer
115 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 ...
James Wood's user avatar
7 votes
1 answer
96 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 ...
Ende Jin's user avatar
  • 429
7 votes
3 answers
372 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 ...
Ana Borges's user avatar
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
4 answers
626 views

Inductive vs. recursive definitions

In Coq there are two ways to define a new type on an inductive type: Using Inductive and using Fixpoint. What are pros and cons ...
8bc3 457f's user avatar
  • 224
6 votes
1 answer
287 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 ...
user avatar
6 votes
1 answer
355 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 ...
Joachim Breitner's user avatar
6 votes
2 answers
268 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 ...
user avatar
6 votes
1 answer
125 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 ...
Ende Jin's user avatar
  • 429
6 votes
2 answers
208 views

Is there a formalism of "coinductive" data types with negative occurrences?

Consider the following program in Haskell: ...
Sebastian Graf's user avatar
6 votes
1 answer
248 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
  • 273
6 votes
1 answer
209 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....
lyfeng's user avatar
  • 157
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

1
2 3 4 5