As of May 31, 2023, we have updated our Code of Conduct.

Questions tagged [coq]

Coq is a formal proof management system, semi-interactive theorem prover and functional programming language. Coq is used for software verification, the formalization of programming languages, the formalization of mathematical theorems, teaching, and more. Due to the interactive nature of Coq, we recommend questions to link to executable examples at https://x80.org/collacoq/ if deemed appropriate.

Filter by
Sorted by
Tagged with
0 votes
0 answers
7 views

How to teach `crush` to unfold definitions?

How do I teach crush to unfold automatically def in the following example: Definition P := False. Definition Q := (False \/ False). Definition def := P /\ Q. Axiom solve_P : P = True. Axiom solve_Q : ...
R. Bosman's user avatar
  • 151
-2 votes
0 answers
13 views

How to parse coq statements from a coq .v file the official way?

The parser I wrote doesn't seem to be good enough to go through a coq statement from a coq file. We assumed that a coq statement would always end in a ".\s" with the exception of strings and ...
Charlie Parker's user avatar
1 vote
0 answers
11 views

Including header / footer in a file generated by extraction

I'm using Extraction "foo.ml" main. to extract the relevant parts of my development into an OCaml file, and I'm currently using dune to build everything. For practical reasons, I'm using ...
nobody's user avatar
  • 4,074
0 votes
1 answer
36 views

Implementing variable replacement in a boolean polynomial function in Coq

I have a boolean polynomial function of the form Definition poly (m n : nat) := bv m -> bv n -> C. Where bv dim is simply a boolean list of length dim defined as Definition bv (n : nat) := list ...
epelaez's user avatar
  • 127
0 votes
1 answer
31 views

Is there a way for Coq to recall it already proved a property for the same element in the same proof?

In Coq, I have an inductive property on elements which may appear many times in the same proof. I would like to know if it is possible for Coq to memorize elements for which the property has already ...
Henri_S's user avatar
  • 35
0 votes
2 answers
28 views

Set type Variable to a concrete type inside a definition

Say that we define in Coq: Section bin_trees. Variable T: Type. Inductive bin_tree := | Leaf : bin_tree | Node : T -> bin_tree -> bin_tree -> bin_tree. Within bin_trees section, I ...
shooqie's user avatar
  • 888
0 votes
2 answers
65 views

Replace element in Coq list

I am writing Coq code that needs to modify lists, particularly by accessing an index i, applying a function to that element, and replacing it back. I know I can acces the elemenent of a list by using ...
epelaez's user avatar
  • 127
0 votes
0 answers
55 views

How to use a proof about a datatype within the same datatype definition in Coq?

I have the following Inductive datatype in Coq: Inductive foo : ioh -> Type := | inp : nat -> nat -> foo Input | out : nat -> nat -> string -> foo Output | mat : foo Input -> foo ...
Tilman Zuckmantel's user avatar
1 vote
2 answers
41 views

Importing a Module in Coq

I have the following folder structure: - BaseDefs.v - UsingBaseDefs.v Here, BaseDefs.v contains definitions that I want to use in UsingBaseDefs.v. I tried to use the coqc BaseDefs.v command from the ...
Tilman Zuckmantel's user avatar
1 vote
1 answer
38 views

Non-trivial Fixpoint on nested recursive types

Given two standard definitions of binary trees and arbitrarily branching trees (K-trees) in Coq (nat hardcoded for simplicity): Inductive bintree : Type := | Leaf : bintree | Node : bintree -> ...
shooqie's user avatar
  • 888
0 votes
1 answer
25 views

Coerce rat to realType im math-comp/analysis

Is there a way to coerce a rat into a realType (from the math-comp/analysis library)? For example, the notation for coercing a nat is %:R.
dvr's user avatar
  • 368
0 votes
1 answer
67 views

Ltac tactic that accepts an arbitrary number of quantifiers

I'm trying to write a--my first--Coq tactic. It should split forall x y z ..., A <-> B into two: forall x y z ..., A -> B and forall x y z ..., B -> A. This is my first attempt: Ltac ...
Jay Lee's user avatar
  • 1,592
1 vote
2 answers
53 views

Software Foundations Basics Exercise - How do I access letter from grade?

I am working through Software Foundations by myself and am trying the exercises, but I am stuck on the exercise for writing the function grade_comparison. Definition grade_comparison (g1 g2 : grade) :...
user21829651's user avatar
-1 votes
1 answer
79 views

How to proof this "Theorem spec0 : forall m n p k, (p <= k) -> (p | n) -> (p | m) -> p <= help m n k." in coq?

I need to create a project on coq for my subject in university I can't understand how proof his equation "S p <= help m n k" p-divider k-(min n m) This project has to count GCD from (min ...
Alexandr's user avatar
1 vote
1 answer
44 views

Recursion and Pattern matching in Coq

I am learning Coq and need to know why the following code does not work in Coq? I am coming from a Haskell background and it is alright there. Require Import List. Require Import Bool. Require Import ...
aaay's user avatar
  • 67
1 vote
0 answers
42 views

`fresh` name: use match result if variable, do something else if it's a constant

In a solver tactic, I'm trying to generate reasonably readable names for the generated hypotheses (so things are at least somewhat readable in cases where the automation fails). fresh is happy with ...
nobody's user avatar
  • 4,074
0 votes
1 answer
62 views

Type coercions in finset

I have this definition, which defines a list of pairs of nats and an element of a subset of some universal type U using the finset library. Definition my_list {U : finType} (E : {set U}) : Type := ...
Bas Laarakker's user avatar
0 votes
2 answers
41 views

Syntax error: '.' expected after [vernac:gallina] (in [vernac_aux]) in Coq when using inductive with integers

So I'm trying to define an inductive set in coq that has integers from 0 to 10: Inductive OD : Set := 0 | 1 | 2 | 3 | 4 | 5 | 6 | 7 | 8 | 9 | 10. I get this message: Syntax error: '.' expected after [...
user12456500's user avatar
0 votes
1 answer
30 views

How to parse a string into a list of lists in Coq?

I was trying to parse a string with double newlines into a list of lists of int in Coq but I'm not able to make it work as expected. Example string: 1 2 3 4 5 The above string needs to be parsed ...
rex's user avatar
  • 124
0 votes
2 answers
49 views

Is there a library for sets that works with bool in Coq?

I am looking to work with mathematical sets and subsets of some universal type. I know this is normally represented as U -> Prop, such as in the Ensembles library. I was wondering if there is ...
Bas Laarakker's user avatar
0 votes
2 answers
28 views

stuck trying to prove sublist of list

i create sublist from list in this way: Fixpoint sublist {X : Type} (n : nat) (m : nat) (lst : list X) : list X := match lst with | [] => [] | h :: t => match m with | O =&...
hch's user avatar
  • 707
0 votes
1 answer
43 views

Use the contrapositive of an hypothesis in Coq

My current hypotheses and goal are: 1 subgoal x : Entity H : ~ P x x -> exists z : Entity, P z x /\ ~ O z x ______________________________________(1/1) P x x I would like to apply the ...
Lepticed's user avatar
  • 325
2 votes
2 answers
94 views

How to write the iota descriptor in Coq?

I'm exercising my proving skills with the book “Mereology” of Cotnoir and Varzi (2021). The first definitions given in the book, after accepting the primitive binary relation P, are : (D1) PPxy := Pxy ...
Lepticed's user avatar
  • 325
0 votes
1 answer
71 views

Morphism signature for dependently-typed vectors in coq

I want to be able to rewrite terms inside the predicate P given to Coq.Vectors.Vector.Forall. The first attempt does not work due to the missing quantification over n. From Coq Require Import Vector ...
pjm's user avatar
  • 259
0 votes
2 answers
39 views

How to deal with lemma only used once in Coq?

I've declared a lemma that I used only for one proof (SoS2_imp_Pos in the code). Is it problematic? How can I do otherwise? I thought about using assert forall s t u, SoS2 u s t -> PoS s u, but I'm ...
Lepticed's user avatar
  • 325
0 votes
1 answer
56 views

'coqc' does not find findlib.conf

~ % coqc Error: Anomaly "Uncaught exception Failure("Config file not found - neither /usr/local/etc/findlib.conf nor the directory /usr/local/etc/findlib.conf.d")." Please report ...
Mohan Radhakrishnan's user avatar
0 votes
2 answers
64 views

What is a way to represent non-disjoint union in Coq?

In Coq, A+B is the disjoint sum of types A and B. Is there any way to introduce a (possibly) non-disjoint sum of two types? For example, what if possibly A = B? I could not find any information on ...
Bas Laarakker's user avatar
0 votes
3 answers
72 views

How to proof recursively defined functions' prop in Coq

I am trying to prove a lemma called alignof_correct in Coq, which verifies that the alignof function I defined for a type returns a positive value. I have defined the types and the function, and ...
Max's user avatar
  • 19
0 votes
2 answers
44 views

Why do these theorems of propositional logic allow for the same proof in Coq?

I find it mystifying why, in the following proofs, the same sequence left; right; left serves to prove each theorem, when in a proof in propositional logic (in all proof systems I know of) these two ...
user65526's user avatar
  • 685
0 votes
2 answers
100 views

How to formally verify a compiler (frontend and/or backend)?

For a project I am about to begin, I was exploring formal verification of a compiler. I came across the CompCert C Compiler which is an ACM awarded, formally verified C compiler. When I read further, ...
anurag's user avatar
  • 1,635
-2 votes
2 answers
55 views

The apply rule in proof by cases

I entered the following attempted proof into CoqIde Theorem choice_reverse : (P -> R) /\ (Q -> R)->((P \/ Q) -> R). Proof. intros H [h' |h'']. destruct H as [PthenR QthenR]. apply PthenR. ...
user65526's user avatar
  • 685
0 votes
2 answers
44 views

How to distribute an AND operator in Coq?

I have this hypothesis: H : (x = s \/ x = t) /\ OoS v x. My current goal is OoS v s \/ OoS v t. So, my idea to solve it was to distribute the AND operator in H to get H : (x = s /\ OoS v x) \/ (x = t /...
Lepticed's user avatar
  • 325
1 vote
1 answer
37 views

Proving n + S n = S (n + n) without n + S m = S (n + m)

Is it possible to prove forall n, n + S n = S (n + n) (with or without induction) without using forall n m, n + S m = S (n + m)? Looking at the proof, if I start by using induction on n, we end up in ...
Yousef Alhessi's user avatar
0 votes
1 answer
40 views

Disjunction and the error `No product after head reduction'

In CoqIde I entered the following code: Theorem or_left : P -> P \/ Q. Proof. intros S V S_holds. This produces the error No product even after head-reduction. What is the problem and what does ...
user65526's user avatar
  • 685
0 votes
2 answers
44 views

How to create a custom Ltac to recursively destruct conjunctions?

I quite often have to deal with complex conjunctions such as (Q /\ W) /\ (E /\ R). I am quite sick of destructing them manually and guessing how to arrange square brackets so I don't accidentally ...
radrow's user avatar
  • 6,299
0 votes
1 answer
47 views

How can I write a filter function for sequences represented as functions in Coq?

Given that we have the types T1, T2 and T_Union, as well as functions proj1 : T_Union -> option T1 and proj2 : T_Union -> option T2, and a sequence represented as nat -> T_Union, how can you ...
Bas Laarakker's user avatar
0 votes
1 answer
27 views

Unclear error message regarding format and notation

In CoqId I have written the following: Parameter i: Type. (* Type for worlds *) Parameter u: Type. (* Type for individuals *) Definition o := i -> Prop. (* Type of modal propositions *) Parameter ...
user65526's user avatar
  • 685
0 votes
0 answers
31 views

Definite description operator in Coq

I have entered the following code in CoqIde: Require Export Classical. Require Export Description. Inductive pbool : Type := T : pbool | F : pbool | U : pbool. Variables s p e t f: ...
user65526's user avatar
  • 685
0 votes
1 answer
35 views

Activating nested proof

I have entered the following code in CoqIde: Require Export Classical. Require Export Description. Theorem excluded_middle_informative : forall P:Prop, {P} + {~ P}. Theorem ...
user65526's user avatar
  • 685
0 votes
1 answer
30 views

Complete Atomic Boolean algebras in Coq

In CoqId I have entered Variables s p e t f: Type. I now want the set of elements which interpret terms of type e to have the structure of a Complete Atomic Boolean algebra. Of course, for this to be ...
user65526's user avatar
  • 685
0 votes
1 answer
21 views

Understanding a message on CoqIde

I typed Eval cbv in id. in CoqIde and received the message = fun x : ?a => x : ?a -> ?a` What does this mean? What does the question mark mean?
user65526's user avatar
  • 685
1 vote
1 answer
52 views

How to break up an implication into two subgoals in Coq?

Say I have the following: Lemma my_lemma : forall a b c, a -> (b -> c) -> d. Proof. intros. Then, above the line, I get: X : a X0 : b -> c Let's say that in my proof, I know I'm ...
markasoftware's user avatar
1 vote
1 answer
51 views

How to overload the "+" notation in Coq?

I'm trying to overload the notation for +. The following doesn't work: Definition my_add (n m :nat):= n + m. Fail Notation "x + y":= (my_add x y) (at level 50, y at next level). Fails with ...
user2506946's user avatar
1 vote
1 answer
27 views

Fail to `destruct` due to ill-typedness and even cannot give an exact term in Coq

I tried to implement the following Coq code: Set Implicit Arguments. Inductive fun_eq A B (f : A -> B) : forall C D, (C -> D) -> Prop := fun_eqrefl : forall g : A -> B, f = g -> ...
Lomega's user avatar
  • 15
0 votes
1 answer
18 views

What is the tag for menhir for coq 8.12 when installing it with opam install -y?

I want to install opam menhir but make the install explicit for coq 8.12 to make my script explicit + robust to installation. But when I ask it to show me it show the dev tag, which I assume might ...
Charlie Parker's user avatar
0 votes
0 answers
27 views

How does one install coq-serapi for coq 8.10 using opam pin and ideally using a commit from coq-serapi?

I tried finding the version compatible with coq 8.10 and installing it via opam pin but it's output is odd: opam pin add -y coq-serapi git+https://github.com/ejgallego/coq-serapi.git#...
Charlie Parker's user avatar
0 votes
3 answers
142 views

How does one pin/freeze a version of the dependencies of an opam project/package and then install the project with such specified dependencies?

How do we freeze an entire dependency tree/chain from an already working opam install? I have a bunch of coq projects installed via opam right now. I'd like to figure out what commit they are using ...
Charlie Parker's user avatar
1 vote
1 answer
47 views

How do I install ocamlfind first properly before other opam packages without root permissions?

I was trying to install some coq packages with opam but have this hack: # coq-equations seems to rely on ocamlfind for it's build, but doesn't # list it as a dependency, so opam sometimes tries to ...
Charlie Parker's user avatar
0 votes
1 answer
27 views

How does one make sure that coq project installed correctly when it doesn't seem to appear on opam list?

I tried installing lin-alg-8.10 using the instructions I was told from proverbot's repo using coq 8.10: # - Create the 8.10 switch opam switch opam switch create coq-8.10 4.07.1 eval $(opam env --...
Charlie Parker's user avatar
1 vote
1 answer
83 views

Does `∃! x, ∃! y, P (x, y)` imply `∃! xy, P (fst xy) (snd xy)`?

It is comparatively easy to prove the following (Coq): Goal forall A (P : A -> A -> Prop), (exists! xy, P (fst xy) (snd xy)) -> (exists! x, exists! y, P x y). The question I am puzzled with: ...
Zazaeil's user avatar
  • 3,767

1
2 3 4 5
57