# Questions tagged [coq]

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

140 questions
Filter by
Sorted by
Tagged with
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 ...
728 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
114 views

### How can I prove has_esp when using mathcomp.analysis?

How can I prove the following goal (which I believe to be true) using mathcomp.analysis? ...
• 157
191 views

### Cannot discriminate 0 = 1

I am just practicing a bit with coq, doing some UniMath exercises and am trying to prove (0 = 1) -> empty. However, for some reason, I seem unable to reason ...
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
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
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
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
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
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
166 views

### Why does this trivial proof fail with structuring tacticals?

Given this: Inductive color := Black | White. Inductive point_state := | Occupied of color | Empty . this works: ...
• 143
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
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,783
114 views

### For functions that are eq_dep equal, are their applications eq_dep equal without axioms?

Is it possible to prove the following theorem without axioms in Coq? Or is the following theorem equivalent to any well known axioms? ...
• 153
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 ...
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 ...
109 views

### List of general purpose Coq sublanguages for defining custom tactics

I've been tweaking the Coq plugin template recently to try to get a feel for writing custom Coq tactics in OCaml. It's tricky. You need to define an .mlg file (...
• 2,651
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
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
173 views

### Coq defining a hierarchy of collections of integers with infinitely many "levels"

I'm trying to formalize a small part of higher-order arithmetic in Coq as an exercise (Wikipedia article for second-order arithmetic). It's straightforward to formalize something resembling second-...
• 2,651
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
75 views

### Coq produce instance of a type {x : T | P x} inside an explicit definition given an x' of type T

I'm trying to formalize a simple type system in Coq as an exercise. I have a type Item and a type {x : Item | IsNormal Item}. If ...
• 2,651
1 vote
112 views

### Form of intros in Coq specifically for forall and explicitly for ->

Are there tactics in Coq that are more limited versions (subtactics?) of intros? I'm curious if there are any specifically for ...
• 2,651
112 views

### Code Review: Proving that a simple propositional logic satisfies Aristotle's Thesis

I'm proving that a simple propositional logic satisfies Aristotle's thesis. I'm curious how to improve the code in question. Here are the things I know that are wrong with it: I'm using ...
• 2,651
90 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
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
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
87 views

### Proof Review: Basic theorem about ternary relations in Coq

I'm proving a simple fact about ternary relations in Coq as an exercise. I'm interested in ternary relations at the moment because they are a simple thing that can represent a finitary consequence ...
• 2,651
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
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
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
507 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
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
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
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 ...
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
226 views

### When to use coinductive types?

One could define streams in the following manner ...
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 ...
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