All Questions
Tagged with coq proof-general
31
questions
0
votes
2
answers
251
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 ...
- 132
0
votes
2
answers
326
views
Proving Binary Tree Properties
As an exercise for myself, I'm trying to define and prove a few properties on binary trees.
Here's my btree definition:
Inductive tree : Type :=
| Leaf
| Node (x : nat) (t1 : tree) (t2 : tree).
The ...
- 157
3
votes
2
answers
194
views
How can I get C-c C-n to format the current line in proof-general coq-mode-map
I'm using proof-general to write Coq proofs.
When I use C-c C-n in a proof, my cursor is moved to the next line, but the current line is not formatted. So for instance, if I type:
intros n. <C-c C-...
- 486
1
vote
1
answer
191
views
SF Volume 1: Logic: How to prove tr_rev <-> rev?
From Software Foundations Volume 1, chapter Logic we see a tail recursive definition of list reversal. It goes like so:
Fixpoint rev_append {X} (l1 l2 : list X) : list X :=
match l1 with
| [] =>...
- 157
0
votes
1
answer
509
views
Software Foundations Volume 1: Tactics: injection_ex3
Could some explain how to complete this proof? (please don't give the actual answer, just some guidance :)
The exercise is from SF volume1, as stated in the title and it goes like this:
(** **** ...
- 157
2
votes
1
answer
987
views
"Symbol's value as variable is void" when adding a path to coqtop when opening emacs
I am trying to run emacs with proof generale to open Coq files. However, when I open emacs I get the following error message:
Symbol's value as variable is void: “/Users/myusername/.opam/default/bin/...
- 23
2
votes
1
answer
145
views
what is [...] in proof general and why can't I delete it
When I try and copy paste proof code, sometimes a [...] will show up (even though I did not copy anything of the kind) and I cannot delete it. I have to undo the copy in order to get rid of it. What ...
- 437
3
votes
1
answer
1k
views
Unicode symbols fail for Proof-general while writing Coq
I use Coq 8.11 in Ubuntu with Proof-general. I write:
Ltac example1 :=
fail.
and succeed. Say I want to use unicode symbols:
Proof-General -> Display -> Quick Options -> Unicode Tokens
then ...
- 2,600
4
votes
1
answer
817
views
How to change Coq Version in Proof General?
I have some code that only compiles coq code in Coq 8.09.0 . The version that I normally use is the most up-to-date version now which is Coq 8.11.0. I was able to create a new environment using opam ...
- 473
2
votes
1
answer
158
views
Unable to set up Certified Programming with Dependent Types
I am working with the book Certified Programming with Dependent Types but each time I'm finding a different error. It seems to me that the error comes from a mismatch between the compilation process ...
- 2,600
0
votes
1
answer
484
views
Avoid printing notation in Coq with Proof General
In lecture 6 of the DeepSpec 2018, the lecturer Checks the definition of
string_dec
obtaining:
string_dec
: forall s1 s2 : string, {s1 = s2} + {s1 <> s2}
Then he goes on to see the ...
- 2,600
0
votes
1
answer
184
views
SSreflect not working with Emacs, Coq and ProofGeneral. How to install SSreflect in MacOS?
If I do something like - From mathcomp Require Import ssreflect. it gives me the following error.
Error: Cannot load mathcomp.ssreflect.ssreflect: no physical path bound to
mathcomp.ssreflect
But if ...
1
vote
0
answers
219
views
Why is Proof General so slow in Windows 10?
I open emacs and then a .v file so that Proof General is triggered. However, one this is done the IDE is very slow and it takes ages to scroll up and down the proof. Any idea on why this might be ...
- 2,600
0
votes
1
answer
99
views
Browse definition in Coq-IDE
In the Isabelle proof assistant, one can click Ctrl+click on a term and the IDE redirects him to the relevant definition.
Can this be done with CoqIde? With Proof-General?
- 2,600
0
votes
1
answer
163
views
proof Lemma which based on Fixpoint definitions
Trying to prove following Lemma:
I have tried unfold nth_error and nth in the goal but I cannot figure out a way to tell Coq to break the Fixpoint definition of these two functions. I have also tried ...
- 157