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
3 votes
0 answers
81 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 ...
user avatar
3 votes
0 answers
55 views

Unfolding expressions in Coq by one layer

Are there any ways to unfold an expression in Coq by a single layer? I have only come up with this obvious solution: ...
user avatar
2 votes
0 answers
46 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....
user avatar
2 votes
4 answers
195 views

I'm stuck trying to prove ∀x : ℕ, 3 | (x + 5x) with Coq

Specifically, I think what's got me is showing that ∀x y z : ℕ, (z|x and z|y) → z|(x + y), or that ∀x y z : ℕ, (x mod y) = 0 → z mod y = (z + x) mod y, depending on how you want to look at it. I know ...
user avatar
11 votes
3 answers
587 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 ...
user avatar
4 votes
0 answers
67 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.
user avatar
4 votes
0 answers
49 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 ...
user avatar
  • 497
12 votes
0 answers
147 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. ...
user avatar
  • 497
9 votes
1 answer
531 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 ...
user avatar
  • 303
13 votes
3 answers
647 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 ...
user avatar
  • 233
5 votes
0 answers
86 views

Prove equality in a record type

I am trying to prove something about monoids an categories. This results in the following (partial) proof: ...
user avatar
3 votes
1 answer
73 views

Found type UU where "?T" was expected

I am trying to solve a couple of exercises in coq. However, with the following code: ...
user avatar
3 votes
3 answers
426 views

How can I prove this theorem with induction in Coq?

Lemma sum_square_p : forall n, 6 * sum_n2 n = n * (n + 1) * (2 * n + 1). where sum_n2 is defined ...
user avatar
6 votes
1 answer
184 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
2 answers
245 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
8 votes
2 answers
650 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 ...
user avatar
  • 2,676
4 votes
1 answer
95 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? ...
user avatar
  • 157
4 votes
1 answer
154 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 ...
user avatar
5 votes
2 answers
64 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 ...
user avatar
  • 157
9 votes
2 answers
367 views

Defining coercion for proof irrelevant equality

Say I would like to define coercion for proof irrelevant equality between types. In Coq I try ...
user avatar
  • 1,662
7 votes
1 answer
80 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 ...
user avatar
  • 419
11 votes
2 answers
325 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 ...
user avatar
  • 213
10 votes
1 answer
484 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 ...
user avatar
  • 1,662
6 votes
1 answer
97 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 ...
user avatar
  • 419
4 votes
1 answer
148 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: ...
user avatar
6 votes
0 answers
108 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 ...
user avatar
11 votes
2 answers
350 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 ...
user avatar
  • 3,355
3 votes
1 answer
85 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? ...
user avatar
16 votes
3 answers
835 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 ...
user avatar
8 votes
2 answers
136 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 ...
user avatar
3 votes
1 answer
91 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 (...
user avatar
  • 2,467
6 votes
1 answer
102 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....
user avatar
  • 157
11 votes
1 answer
148 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 ...
user avatar
  • 2,467
3 votes
1 answer
133 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-...
user avatar
  • 2,467
28 votes
2 answers
560 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 ...
user avatar
2 votes
2 answers
63 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 ...
user avatar
  • 2,467
1 vote
1 answer
60 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 ...
user avatar
  • 2,467
2 votes
1 answer
94 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 ...
user avatar
  • 2,467
4 votes
3 answers
65 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 <...
user avatar
  • 273
4 votes
1 answer
105 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 ...
user avatar
  • 2,467
13 votes
2 answers
166 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 ...
user avatar
4 votes
2 answers
71 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 ...
user avatar
  • 2,467
11 votes
1 answer
107 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 ...
user avatar
  • 497
10 votes
1 answer
115 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 ...
user avatar
  • 203
7 votes
2 answers
137 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 ...
user avatar
  • 273
16 votes
1 answer
229 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 ...
user avatar
  • 165
10 votes
1 answer
157 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 ...
user avatar
  • 2,467
3 votes
3 answers
78 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 ...
user avatar
  • 2,467
24 votes
4 answers
531 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 ...
user avatar
13 votes
2 answers
196 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 ...
user avatar
  • 1,662