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
1 vote
1 answer
50 views

Non-dependent implicit argument instantiation in Coq's reference manual does not work

Consider the following definition Definition foo1 (A : Type) {_ : A} := A. I was wondering whether there is a way to instantiate the non-dependent implicit ...
0 votes
1 answer
84 views

A problem similar to intermediate value problem

My assumption is as follows : ...
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): ...
0 votes
1 answer
60 views

Define a function using another function

I want to define a translation function g from another function f. Definition trans (f g : Q -> Q) (t : Q) := forall q : Q, f (q + t) == g q. In the above code,...
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 ...
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 ...
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 ...
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 ...
1 vote
0 answers
22 views

Why does TacArg accepts a value of CAst.t type when it should only accept values of types?

See the argument for TacArg: | TacArg of ('t, 'dtrm, 'p, 'c, 'r, 'n, 'tacexpr, 'l) gen_tactic_arg but the reply has a type CAst.t as an argument for TacArg: <...
5 votes
0 answers
56 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 ...
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
3 votes
1 answer
119 views

How to prove "$x \le y$" or "$\text{not} (x \le y)$" for rational numbers $x$ and $y$ in Coq?

I have made the following code, and I'm in stuck. ...
1 vote
1 answer
31 views

How to Deal with Qle_bool in the progress of proving in Coq

I want to prove the following theorem in Coq. Please give me an advice if possible. ...
5 votes
0 answers
136 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 ...
3 votes
0 answers
68 views

Where is the discriminate tactic defined in Coq?

One can read the Coq documentation about discriminate tactic here. Were is this tactic actually defined?
3 votes
1 answer
121 views

How to convince Coq this dependent pattern match is exhaustive?

The stack definition and a test function to work with it are given below. The code works (when compiling example you will see an error, it is my problem). ...
  • 203
4 votes
3 answers
126 views

Why use records for non-empty lists rather than inductively defined non-empty lists?

I've come across two main ways to do non-empty lists: ...
  • 141
1 vote
1 answer
144 views

dependent pattern matching and kind of inversion

The stack definition and a test function to work with it are defined below. (Maybe) only the nicety is that I need 2-levels of types (see in code). The code works (example can be compiled). ...
  • 203
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, ...
4 votes
1 answer
178 views

Dependent pattern matching

upd. What I would like to do is to put a = RedNode' .. into current context (when using refine). I found this technique here ...
  • 203
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
3 votes
1 answer
102 views

Equivalent of `range` in Coq

There is a function which is usually called range in other languages: it takes a natural n, and returns a list of naturals ...
2 votes
1 answer
171 views

How to prove these 2 theorems with the help of the function below?

First, the function [foldc] should be defined, using the supplementary [eqfx]. ...
1 vote
1 answer
212 views

Strong induction for nat in Coq

I'm doing some exercises on Coq and trying to prove the strong induction principle for nat: ...
2 votes
1 answer
347 views

Problem with rewrite

I've just started with Coq and I don't understand why it does not accept rewrite in the next situation. The following exercise is from "Coq in hurry": ...
0 votes
1 answer
139 views

Equational reasoning in Coq

I've been doing some exercises on Coq, and have stuck for the next problem: Let T: Set with 2 operations f, ...
2 votes
2 answers
82 views

Coq inductive type with vector parameter lacks sufficient inductive principle

Background/Setting of Problem I am trying to encode first-order logic in Coq, and have defined a Term as: ...
  • 1,439
3 votes
1 answer
97 views

Obligation Tactic := intros. results in the Program Fixpoint with measure not being defined

I have a Program Fixpoint with measure for which I have proved all obligations. When I try to check it, it fails: Error: The reference trivial_program_fixpoint2 was not found in the current ...
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: ...
3 votes
1 answer
155 views

Why do record based inductive types with primitive projections lack an eta law?

In Coq there is ongoing work to shore up some weaknesses in subject reduction and coinductive types. Primitive projections are part of that effort for better behaviour. I get why there might be ...
1 vote
1 answer
178 views

Axiomization of Peano arithmetic in constructive first-order logic

I've been playing with axiomising systems of first-order logic in Coq. I've started to develop the beginning of a framework. As an example I give a minimal phrasing of Peano arithmetic in Coq in the ...
2 votes
1 answer
76 views

Why does my previously defined function expands/computes to itself?

Problem I have a function leb defined in one of the (transitively) imported file: Types.v. However, calling it in my current ...
  • 350
4 votes
2 answers
248 views

Why is my recursive definition of list_min ill-formed?

I'm new to Coq and I'm on my own (self-learning). Question: Define a function list_min that takes a list of natural numbers and returns the least element of the list. Source My solution: ...
  • 350
5 votes
1 answer
100 views

How to evaluate proof terms through opaque definitions?

Is there is a way to force computation over opaque terms, for the purposes of debugging/meta-analysis of proof scripts. I understand why Coq doesn’t do this by default, and guess it would probably ...
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 ...
2 votes
1 answer
101 views

Can a Prop show that all entries of a list equal Type@{U} for any U?

In Coq, is it possible to write a predicate (list Type -> Prop) that is only provable if all entries of the list are of the form ...
3 votes
0 answers
103 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 ...
5 votes
0 answers
122 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: ...
3 votes
0 answers
60 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....
3 votes
4 answers
384 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 ...
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 ...
5 votes
0 answers
85 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.
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
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
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
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
5 votes
0 answers
111 views

Prove equality in a record type

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

Found type UU where "?T" was expected

I am trying to solve a couple of exercises in coq. However, with the following code: ...
3 votes
4 answers
526 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 ...
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 ...
user avatar