Questions tagged [coq]
Coq is a formal proof management system. It is often referred to as a proof assistant.
140
questions
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 ...
- 90
0
votes
1
answer
84
views
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
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,...
- 285
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
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
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
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:
<...
- 169
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 ...
- 169
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.
...
- 285
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.
...
- 285
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 ...
- 169
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, ...
- 163
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 ...
- 666
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].
...
- 25
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:
...
- 195
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":
...
- 21
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, ...
- 195
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 ...
- 2,628
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,628
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
...
- 1,614
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 ...
- 153
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....
- 31
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 ...
- 63
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
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.
- 51
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:
...
- 225
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:
...
- 225
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
...
- 41
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