Questions tagged [coq]
Coq is a formal proof management system. It is often referred to as a proof assistant.
104
questions
3
votes
0
answers
20
views
.CoqMakefile.d required by CoqMakefile but not generated
I am trying to use CoqMakefile to automatically build my Coq project in Coq 8.15.2.
When I did this the compilation failed because a file ".CoqMakefile.d" was expected by make but did not ...
- 2,916
0
votes
0
answers
47
views
If I make some new structure like Q, then can I use 'rewrite' tactic for my new structure in Coq?
From $\mathbb{Q}$, the set of all rational numbers, I make some new structure $I$, and also make strict order and (equivalence) equality on $I$.
I want to use rewrite tactic for my defined relations (...
- 285
1
vote
1
answer
111
views
Can I unfold not all things but only one thing in Coq?
For example,
Example example (a b c : Q) :
(a * b) * c == a * (b * c).
Proof.
unfold Qmult.
This code show me this screen.
...
- 46
8
votes
3
answers
254
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 ...
- 111
0
votes
1
answer
40
views
How can I correspond a hypothesis to a decidable axiom in match (in Coq)?
I made some record structure $I$ with addition and equality. And I made an axiom.
Axiom I_dec :
forall a : I, ({0 < a} + {a < 0}) + {a == 0}.
With this ...
- 2,419
1
vote
1
answer
79
views
How do I prove this property in Coq?
I am working on a variant of an example by Christine Paulin-Mohring. It represents in Coq the Needham-Schroeder protocol in the (flawed) public key version. I would like to prove that the protocol is ...
- 1,162
1
vote
1
answer
49
views
How can I use a (three terms) decidable axiom in a case analysis?
In Coq, I made some record structure $I$ and also make a strict order and equality $<$ and $==$.
And I showed that $a < b$ or $a == b$ or $b < a$ for every $a, b \in I$.
...
- 446
2
votes
1
answer
92
views
Natural deduction with coq assistant prover
I want to mimic natural deduction proofs in coq ; for instance the proof I made for "A /\ B -> B /\ A" is for now
...
- 4,690
4
votes
1
answer
75
views
How can I search only all of the lemmas in a different module (in Coq)?
I usually import QArith.
If I write
Search "max" "id".
Then I can see something like this:
...
- 109
1
vote
2
answers
324
views
What is the remaining goals on the shelf?
When I prove a theorem in Coq, I made a hypothesis that is 'False',
and by using 'contradiction' tactics, I finish my proof.
However, the coq program show some words for me.
...
- 2,419
3
votes
2
answers
106
views
Coq: can `tauto` be used to prove classical tautologies?
When I experiment, I get inconsistent results.
Running the following code (with a proof included to double-check that it's provable)
...
- 5,920
5
votes
0
answers
119
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 ...
- 136
0
votes
2
answers
80
views
How to define two mutually recursive functions in Coq?
I make such codes, and cannot preceed.
...
- 446
5
votes
1
answer
83
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):
...
- 2,419
8
votes
2
answers
288
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 ...
- 61
1
vote
1
answer
105
views
Can I prove this axiom without using excluded-middle property?
I define the following axiom.
(First, I want to prove it, and make it Theorem.
However, I can not find how to start.)
...
- 5,920
2
votes
2
answers
63
views
1
vote
2
answers
52
views
Is there a tactic in Coq to make a hypothesis from applying two hypotheses?
Suppose in Coq we have the following hypotheses:
x, y, z: Z
H : x < y
H0 : y < z
and I would like to introduce also the hypothesis
...
- 5,920
1
vote
1
answer
49
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 ...
- 839
0
votes
1
answer
83
views
3
votes
4
answers
498
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
...
0
votes
1
answer
44
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,...
- 446
1
vote
1
answer
136
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).
...
CommunityBot
- 1
9
votes
2
answers
531
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 ...
- 2,422
6
votes
0
answers
69
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
21
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:
<...
- 161
5
votes
0
answers
49
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 ...
- 4,690
5
votes
2
answers
112
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
...
- 46
3
votes
1
answer
116
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,258
1
vote
1
answer
30
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.
...
- 446
3
votes
0
answers
61
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
102
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
108
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:
...
- 2,422
4
votes
1
answer
145
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
14
votes
1
answer
812
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, ...
- 2,056
8
votes
3
answers
188
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,
...
- 1,258
2
votes
1
answer
164
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
3
votes
1
answer
76
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 ...
- 839
1
vote
1
answer
89
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
323
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":
...
- 340
0
votes
1
answer
132
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, ...
- 5,920
2
votes
1
answer
99
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,237
2
votes
2
answers
69
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:
...
- 2,422
3
votes
1
answer
66
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 ...
- 1,162
5
votes
1
answer
143
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:
...
- 839
2
votes
1
answer
164
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 ...
- 839
2
votes
1
answer
74
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 ...
- 839
4
votes
2
answers
221
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:
...
- 446
5
votes
1
answer
62
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 ...
- 2,422
15
votes
1
answer
213
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