Questions tagged [coq-plugin]
12 questions
5
votes
1 answer
OCaml and preprocessor have incompatible versions error when installing tcoq
I was trying to install tcoq and I had the following error:
"/Users/pinocchio/.opam/4.05.0/bin/ocamlfind" ocamlc -rectypes -w -3-52-56 -c grammar/compat5.ml
OCAMLC -c -pp grammar/gramCompat.mlp
>> Fatal error: OCaml and preprocessor have…
Charlie Parker
- 5,884
- 57
- 198
- 323
5
votes
2 answers
Using forall within recursive Function definition
I'm trying to use Function to define a recursive definition using a measure, and I'm getting the error:
Error: find_call_occs : Prod
I'm posting the whole source code at the bottom, but my function is
Function kripke_sat (M : kripke) (s : U) (p :…
Maty
- 223
- 1
- 7
3
votes
1 answer
How to setup Coq as theorem prover for First Order Logic
As far as I understand, then Coq have built-in First Order Logic https://coq.inria.fr/tutorial/1-basic-predicate-calculus. But Coq is not theorem prover, Coq is proof assistant and that means that user is required to provide some hints what…
TomR
- 2,696
- 6
- 34
- 87
2
votes
1 answer
How to get the name of a named goal in the coq api
I'm currently working on an ocaml program, which will be using the coq api to extract information about proofs and their goals.
For this, I want to extract the name given to a goal, when a "refine ?[name]" or some other tactic to name a goal, was…
KöniglichePM
- 21
- 1
1
vote
1 answer
Paramcoq: Free theorems in Coq
How can I prove the following free theorem with the plugin Paramcoq?
Lemma id_free (f : forall A : Type, A -> A) (X : Type) (x : X), f X x = x.
If it is not possible, then what is the purpose of this plugin?
Bob
- 1,713
- 10
- 23
1
vote
0 answers
Coq: Port a Ltac tactic using CPS style to an ML tactic (OCaml plugin)
I'm trying to port a Coq tactic (currently written in Ltac) to OCaml, in order to be able to extend that tactic more easily (and avoid the hacks I needed to emulate in Ltac some data structures that are otherwise quite standard in OCaml).
I am…
ErikMD
- 13,377
- 3
- 35
- 71
1
vote
1 answer
rewrite works for integer but not for rationals for Coq aac_tactics
I was testing Coq rewrite tactics modulo associativity and commutativity (aac_tactics). The following example works for integer (Z), but generates an error when integers are replaced by rationals (Q).
Require Import ZArith.
Import…
thor
- 21,418
- 31
- 87
- 173
1
vote
1 answer
where is Coq aac_tactics installed?
I was testing the AAC tactics library for rewrites modulo associativity and commutativity. According to a Coq website, one should:
Depending on your installation, either modify the following two lines,
or add them to your .coqrc files, replacing…
thor
- 21,418
- 31
- 87
- 173
0
votes
1 answer
What are standard practices for developing Coq code in Atom Editor?
I wanted to develop some Coq code in Atom. I wanted to be able to check my code line by line as usual just like with CoqIDE or emacs proof general. Is there something like that for atom or how do people develop Coq code in Atom editor?
some…
Charlie Parker
- 5,884
- 57
- 198
- 323
0
votes
1 answer
How to customize colors for Command and Tactic in ProofGeneral when using Coq in Emacs?
I want to color some specific command and tactic into different color, e.g. I want "Print" and "Locate" command to be gray, and "induction" to be some special color different from other tactics.
Is this possible in ProofGeneral? If it is not…
luochen1990
- 3,689
- 1
- 22
- 37
0
votes
1 answer
How to do higher-order term rewriting in Coq?
This question is based on my question https://cs.stackexchange.com/questions/96533/how-to-transform-lambda-function-to-multi-argument-lambda-function-and-how-to-re There are two functions and two terms in that question:
Functions:
is:…
TomR
- 2,696
- 6
- 34
- 87
0
votes
1 answer
How to use Coq aac tactics to prove equalities in the goal?
I am guessing that Coq aac_tactics (8.5p1) should be able to deal with assoc. and commutativity. But I can't figure out how to use it prove simple equalities such as
2 + y + 5 = 7 + y
For example:
Require Import AAC_tactics.AAC.
Require Import…
thor
- 21,418
- 31
- 87
- 173