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
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 ...
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 (...
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. ...
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 ...
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 ...
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 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$. ...
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 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: ...
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. ...
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 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 ...
0 votes
2 answers
80 views

How to define two mutually recursive functions in Coq?

I make such codes, and cannot preceed. ...
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): ...
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 ...
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.) ...
2 votes
2 answers
63 views

When I destruct record, can I make a hypothesis name without 0?

I made such record. ...
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 ...
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 ...
0 votes
1 answer
83 views

A problem similar to intermediate value problem

My assumption is as follows : ...
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,...
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). ...
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 ...
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: <...
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 ...
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 ...
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 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. ...
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). ...
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: ...
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 ...
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, ...
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, ...
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]. ...
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 ...
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: ...
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": ...
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, ...
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 ...
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: ...
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 ...
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: ...
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 ...
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 ...
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: ...
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 ...
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. ...