Stack Overflow
Stack Overflow

Questions tagged [coqide]

Graphical interface (IDE) for Coq. It is written in OCaml.

103 questions
10
votes
2 answers

Agda-like programming in Coq/Proof General?

Unlike Agda, Coq tends to separate proofs from functions. The tactics Coq gives are great for writing proofs, but I'm wondering if there is a way to replicate some Agda-mode functionality. Specifically, I'd like: Some equivalent of Agda's ? or…
jmite
  • 8,171
  • 6
  • 40
  • 81
9
votes
3 answers

can I force Coq to print parentheses?

I'm new to Coq, working on set-theoretic proof writing. I realized that parentheses are omitted, and it makes difficult for me to read the formula. For example, 1 subgoal A, B : {set T} H : B \subset A ______________________________________(1/1) A…
Pengin
  • 771
  • 1
  • 10
  • 16
7
votes
1 answer

The reference "X" was not found in the current environment

I'm using CoqIDE to complete the exercises in the Software Foundations book about Coq. I can successfully compile Basics.v, resulting in Basics.vo and Basics.glob in my directory. When I try to run Induction.v, it works. When I try to compile it, it…
RaptorDotCpp
  • 1,425
  • 14
  • 26
7
votes
2 answers

How do you look up where identifiers are defined in Coq efficiently?

In most IDEs or text editors, you can right-click a term and it takes you to the file where that term is defined. CoqIDE doesn't seem to have that, so I've been doing coqdoc myfile.v --html, then going to the generated HTML docs. But the only…
Lance
  • 75,200
  • 93
  • 289
  • 503
7
votes
1 answer

CoqIDE loadpath error for ssreflect

I am a Coq newbie and therefore to improve my understanding of proof checking I am trying to use the Ssreflect library. I have installed Ssreflect v 1.5 on a Mac OS v 10.10.3 ( Yosemite ) which runs at the Terminal. However when I tried to load…
David
  • 439
  • 1
  • 4
  • 15
6
votes
1 answer

How to step through semicolons separated tactics sequence in coqide?

when constructing proof in coqide, I didn't find a way to step though T1; T2; T3; ...; Tn. one tactic by one tactic. So it became very difficult to construct correct proof like the code above. So my question is Is there a way to step through the…
lambda
  • 63
  • 3
4
votes
2 answers

Coq: Strong specification of haskell's Replicate function

I'm having a bit of trouble understanding the difference between strong and weak specification in Coq. For instance, if I wanted to write the replicate function (given a number n and a value x, it creates a list of length n, with all elements equal…
Cris Teller
  • 99
  • 5
4
votes
1 answer

Coq module "Cannot find a physical path bound to logical path matching suffix <> and prefix" and "not found in the loadpath"

I'm reading logical foundations and have downloaded the coq scripts which come with it. I'm using coq v8.8.1, install via opam. I'm getting the two errors in the title, and I am not sure how I should go about debugging them. The full error message…
Peeyush Kushwaha
  • 3,453
  • 8
  • 35
  • 69
4
votes
1 answer

CoqIDE error with exporting modules in the same library

I am running CoqIDE to use read the textbook series "Software Foundations", I am currently reading the volume "Logical Foundations". I just started Chapter 2 (Induction), but when I try to run the line From LF Require Import Basics. I get an error…
Roquentin
  • 177
  • 2
  • 12
4
votes
2 answers

Coq makefile "Top." Prefix

I am using the automatic Coq 8.5 makefile generator. This makefile prefixes all modules by "Top." . Now let's say you run a lot of files by make and then want to change/debug some file in the IDE. Then the annoying fact is that Coq complains it…
Cryptostasis
  • 1,166
  • 6
  • 15
4
votes
2 answers

Vim plugin does not recognize existing Perl support

I've been using the CoqIDE plugin for Vim on Linux machines for editing Coq files. Now I'm trying to install it on Windows 8. But when I try to source the plugin, I get Your vim doesn't support Perl. Install it before using CoqIDE mode. which is…
user287393
  • 1,221
  • 8
  • 13
3
votes
1 answer

How to do induction on the end of a list in Coq

In the standart way I have induction for list like this Approval is performed for lst Proving for x::lst But I want: Approval is performed for lst Proving for lst ++ x::nil For me, the place of x in the list is important. I tried to write…
he11boy
  • 71
  • 3
3
votes
1 answer

Coq: Issue with Require Export

my issue seems to be a common one, but none of the found answers could solve it. I am following the software foundations course on Coq, and so I come to the command: > From LF Require Export Basics. Whatever I try, I get always the following…
Henri_S
  • 47
  • 6
3
votes
1 answer

In Coq is it necessary to add the current directory to the load path to access compiled files there for imports or exports?

I recently switched from Windows to Mac and now CoqIde is not behaving as I'm used to. I'm using Coq 8.9.1 and I don't remember the version I used to use, but it was last updated fall 2018. On my old machine, I could compile a file (e.g. file1.v to…
lady.corvus
  • 95
  • 6
3
votes
1 answer

Development of the Coq library. (Add LoadPath solution is not good enough.)

I am adding some theorems to the library https://github.com/coq-contribs/zfc But there is a not very good thing. While I developing the code in the CoqIDE I have to add Add LoadPath "/home/user/0my/GITHUB/". and to rename all Require Import…
ged
  • 687
  • 7
  • 19
1
2 3 4 5 6 7