outcome
requirements
yes
yes (default)
native_compute
of deps
yes
no
vm_compute
none
none
yes
ondemand
native_compute
none
none
no
yes, no, ondemand
vm_compute
none
none
ondemand
yes
native_compute
of deps
ondemand
no
vm_compute
none
none
ondemand
ondemand (default)
native_compute
none
none
Set the directory in which to put the aforementioned .cmxs for native_compute . Defaults to .coq-native .
Indicate Coq to skip the processing of opaque proofs (i.e., proofs ending with Qed or Admitted ), output a .vos files instead of a .vo file, and to load .vos files instead of .vo files when interpreting Require commands.
Indicate Coq to check a file completely, to load .vos files instead of .vo files when interpreting Require commands, and to output an empty .vok files upon success instead of writing a .vo file.
Configure the display of warnings. This option expects all, none or a comma-separated list of warning names or categories (see Section Controlling display ).
Coqtop only . Enable or disable color output. Default is auto, meaning color is shown only if the output channel supports ANSI escape sequences.
Coqtop only . Controls highlighting of differences between proof steps. on highlights added tokens, removed highlights both added and removed tokens. Requires that -color is enabled. (see Section Showing differences between proof steps ).
Pretty-print each command to file.beautified when compiling file.v , in order to get old-fashioned syntax/definitions/notations.
Start a special toplevel to communicate with a specific IDE.
Change the logical theory of Coq by declaring the sort Set impredicative.
This is known to be inconsistent with some standard axioms of classical mathematics such as the functional axiom of choice or the principle of description.
Collapse the universe hierarchy of Coq.
This makes the logic inconsistent.
Experimental. Do not depend on this option. Replace Coq's auto-generated name scheme with names of the form ident0 , ident1 , etc. Within Coq, the Mangle Names flag turns this behavior on, and the Mangle Names Prefix option sets the prefix to use. This feature is intended to be used as a linter for developments that want to be robust to changes in the auto-generated name scheme. The options are provided to facilitate tracking down problems.
Enable flags and set options. string should be setting_name =value , the value is interpreted according to the type of the option. For flags setting_name is equivalent to setting_name =true . For instance -set "Universe Polymorphism" will enable Universe Polymorphism . Note that the quotes are shell syntax, Coq does not see them. See the note above regarding the order of command-line options.
As -set but used to disable options and flags. string must be " setting_name " . See the note above regarding the order of command-line options.
Load a file that sets a few options to maintain partial backward-compatibility with a previous version. This is equivalent to Require Import Coq.Compat.CoqXXX with XXX one of the last three released versions (including the current version). Note that the explanations above regarding the order of command-line options apply, and this could be relevant if you are resetting some of the compatibility options.
Dump references for global names in file file (to be used by coqdoc, see Documenting Coq files with coqdoc ). By default, if file.v is being compiled, file.glob is used.
Disable the dumping of references for global names.
Set the binary image to be used by coqc to be file instead of the standard one. Not of general use.
Set the directory containing Coq binaries to be used by coqc . It is equivalent to doing export COQBIN= directory before launching coqc .
Print the location of Coq’s standard library and exit.
Print the locations of Coq’s binaries, dependencies, and libraries, then exit.
Print the list of command line arguments that coqtop has recognized as options and exit.
Print Coq’s version and exit.
Print the highlight tags known by Coq as well as their currently associated color and exit.
Print a short usage and exit.
Compiled interfaces help saving time while developing Coq formalizations, by compiling the formal statements exported by a library independently of the proofs that it contains.
Warning Compiled interfaces should only be used for development purposes. At the end of the day, one still needs to proof check all files by producing standard .vo files. (Technically, when using -vos , fewer universe constraints are collected.) Moreover, this feature is still experimental, it may be subject to change without prior notice.
The compilation using coqc -vos foo.v produces a file called foo.vos , which is similar to foo.vo except that all opaque proofs are skipped in the compilation process.
The compilation using coqc -vok foo.v checks that the file foo.v correctly compiles, including all its opaque proofs. If the compilation succeeds, then the output is a file called foo.vok , with empty contents. This file is only a placeholder indicating that foo.v has been successfully compiled. (This placeholder is useful for build systems such as make .)
When compiling a file bar.v that depends on foo.v (for example via a Require Foo. command), if the compilation command is coqc -vos bar.v or coqc -vok bar.v , then the file foo.vos gets loaded (instead of foo.vo ). A special case is if file foo.vos exists and has empty contents, and foo.vo exists, then foo.vo is loaded.
Appart from the aforementioned case where foo.vo can be loaded in place of foo.vos , in general the .vos and .vok files live totally independently from the .vo files.
Dependencies generated by ``coq_makefile``.
The files foo.vos and foo.vok both depend on foo.v .
Furthermore, if a file foo.v requires bar.v , then foo.vos and foo.vok also depend on bar.vos .
Note, however, that foo.vok does not depend on bar.vok . Hence, as detailed further, parallel compilation of proofs is possible.
In addition, coq_makefile generates for a file foo.v a target foo.required_vos which depends on the list of .vos files that foo.vos depends upon (excluding foo.vos itself). As explained next, the purpose of this target is to be able to request the minimal working state for editing interactively the file foo.v .
When writing a custom build system, be aware that coqdep only produces dependencies related to .vos and .vok if the -vos command line flag is passed. This is to maintain compatibility with dune (see ocaml/dune#2642 on github ).
Typical compilation of a set of file using a build system.
Assume a file foo.v that depends on two files f1.v and f2.v . The command make foo.required_vos will compile f1.v and f2.v using the option -vos to skip the proofs, producing f1.vos and f2.vos . At this point, one is ready to work interactively on the file foo.v , even though it was never needed to compile the proofs involved in the files f1.v and f2.v .
Assume a set of files f1.v ... fn.v with linear dependencies. The command make vos enables compiling the statements (i.e. excluding the proofs) in all the files. Next, make -j vok enables compiling all the proofs in parallel. Thus, calling make -j vok directly enables taking advantage of a maximal amount of parallelism during the compilation of the set of files.
Note that this comes at the cost of parsing and typechecking all definitions twice, once for the .vos file and once for the .vok file. However, if files contain nontrivial proofs, or if the files have many linear chains of dependencies, or if one has many cores available, compilation should be faster overall.
Need for ``Proof using``
When a theorem is part of a section, typechecking the statement of this theorem might be insufficient for deducing the type of this statement as of at the end of the section. Indeed, the proof of the theorem could make use of section variables or section hypotheses that are not mentioned in the statement of the theorem.
For this reason, proofs inside section should begin with Proof using instead of Proof , where after the using clause one should provide the list of the names of the section variables that are required for the proof but are not involved in the typechecking of the statement. Note that it is safe to write Proof using. instead of Proof. also for proofs that are not within a section.
If Coq is invoked using the -vos option, whenever it finds the command Proof. inside a section, it will compile the proof, that is, refuse to skip it, and it will raise a warning. To disable the warning, one may pass the flag -w -proof-without-using-in-section .
Interaction with standard compilation
When compiling a file foo.v using coqc in the standard way (i.e., without -vos nor -vok ), an empty file foo.vos and an empty file foo.vok are created in addition to the regular output file foo.vo . If coqc is subsequently invoked on some other file bar.v using option -vos or -vok , and that bar.v requires foo.v , if Coq finds an empty file foo.vos , then it will load foo.vo instead of foo.vos .
The purpose of this feature is to allow users to benefit from the -vos option even if they depend on libraries that were compiled in the traditional manner (i.e., never compiled using the -vos option).
The coqchk command takes a list of library paths as argument, described either by their logical name or by their physical filename, which must end in .vo . The corresponding compiled libraries ( .vo files) are searched in the path, recursively processing the libraries they depend on. The content of all these libraries is then type checked. The effect of coqchk is only to return with normal exit code in case of success, and with positive exit code if an error has been found. Error messages are not deemed to help the user understand what is wrong. In the current version, it does not modify the compiled libraries to mark them as successfully checked.
Note that non-logical information is not checked. By logical information, we mean the type and optional body associated with names. It excludes for instance anything related to the concrete syntax of objects (customized syntax rules, association between short and long names), implicit arguments, etc.
This tool can be used for several purposes. One is to check that a compiled library provided by a third-party has not been forged and that loading it cannot introduce inconsistencies 1 . Another point is to get an even higher level of security. Since coqtop can be extended with custom tactics, possibly ill-typed code, it cannot be guaranteed that the produced compiled libraries are correct. coqchk is a standalone verifier, and thus it cannot be tainted by such malicious code.
Command-line options -Q , -R , -where and -impredicative-set are supported by coqchk and have the same meaning as for coqtop . As there is no notion of relative paths in object files -Q and -R have exactly the same meaning.
Check module but do not check its dependencies.
Do not check module and any of its dependencies, unless explicitly required.
At exit, print a summary about the context. List the names of all assumptions and variables (constants without body).
Do not write progress information to the standard output.
Environment variable $COQLIB can be set to override the location of the standard library.
The algorithm for deciding which modules are checked or admitted is the following: assuming that coqchk is called with argument M , option -norec N , and -admit A . Let us write \(\overline{S}\) for the set of reflexive transitive dependencies of set \(S\) . Then:
Modules \(C = \overline{M} \backslash \overline{A} \cup M \cup N\) are loaded and type checked before being added to the context.
And \(M \cup N \backslash C\) is the set of modules that are loaded and added to the context without type checking. Basic integrity checks (checksums) are nonetheless performed.
As a rule of thumb, -admit can be used to tell Coq that some libraries have already been checked. So coqchk A B can be split in coqchk A && coqchk B -admit A without type checking any definition twice. Of course, the latter is slightly slower since it makes more disk access. It is also less secure since an attacker might have replaced the compiled library A after it has been read by the first command, but before it has been read by the second command.
Ill-formed non-logical information might for instance bind Coq.Init.Logic.True to short name False, so apparently False is inhabited, but using fully qualified names, Coq.Init.Logic.False will always refer to the absurd proposition, what we guarantee is that there is no proof of this latter constant.
Find centralized, trusted content and collaborate around the technologies you use most.
Q&A for work
Connect and share knowledge within a single location that is structured and easy to search.
Get early access and see previews of new features.
Let's say I have made an Hypothesis about the existance of a value. How do I name that variable in the environment?
Now I want to introduce c and the fact that d*c = n into the environment, so I don't have to start my proof by destructing H every time, like this:
There is no way of doing what you want, as far as I know. I think it would be a bit complicated to implement because of the restrictions governing Prop elimination.
In this particular case, one thing you could do would be to name n / d as c in your context, and then prove an auxiliary lemma, using your hypothesis, saying that n = c * d . Then you would still have your hypothesis in the statement of your lemmas, but wouldn't have to destruct it all the time.
Reminder: Answers generated by artificial intelligence tools are not allowed on Stack Overflow. Learn more
Post as a guest.
Required, but never shown
By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy .
IMAGES
COMMENTS
1. Since your lemma x contains an inner universal quantification (the forall k part at the end), Coq does not manage to guess which natural number you want to use. By applying x to H, you only provide i and j. You have two solutions: provide the relevant k by hand using the apply x with (k := foo) in H syntax.
ains b, replace b. with a in your goal.rewrite H1 in H2. Given H1 : a = b and another hypothesis H2 t. at contains replace. with in a, a b H2.rewr. te <-H1. in H2. Replace b with a in H2.with b. If your goal contains a, t already have a hypothesis stating= b or one stating b = a, you will h. ve to com.
2 →Q, Coq will create subgoals for each assumption P 1 and P 2. If the lemma has no assumptions, then then applyH finishes the goal. ... assertPasHbytac Create new hypothesis H: P after proving subgoal P using tac assert(G:=H) Duplicate hypothesis cutP Split goal Q into two subgoals P →Q and P
The inductive case `S x` produces a new term `x` and a new hypothesis, so we give those names. The vertical bar separates the two cases. After proving the base case, we move on to the inductive case. Hey, Coq came up with the correct induction hypothesis for us. Thanks, Coq! Theorem n_plus_n : forall (n : nat), n + n = n * 2. Proof.
Then, to apply a tactic tac to the first goal only, you can write 1:tac. Using value ! enforces that all tactics are used either on a single focused goal or with a local selector (''strict focusing mode''). Although other selectors are available, only all, ! or a single natural number are valid default goal selectors.
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. H1 : x < z which follows from H and H0 using Z.lt_trans. Is there a better way to do this than the following? assert (H1 : x < z). { apply Z.lt_trans with y. exact H. exact H0.
The only way to create a proof of type "eq" is to use the only constructor "eq_refl". It takes a value of "x" of type "A" and returns "@eq A x x", that is, that "x" is equal to itself. (The "@" prevents Coq from inferring values, like the type "A".) The name "eq_refl" comes from the reflexive property of equality.
Introduction and Contents. This is the reference manual of Coq. Coq is an interactive theorem prover. It lets you formalize mathematical concepts and then helps you interactively generate machine-checked proofs of theorems. Machine checking gives users much more confidence that the proofs are correct compared to human-generated and -checked proofs.
We can use the destruct keyword or tactic as it's commonly called in Coq. What it does is that it breaks down hypothesis H : A \/ B into two cases: one with H: A and one with H : B and we can prove those two separately as two subgoals: problem0 < destruct H. 2 subgoals. A, B : Prop. H : A.
A new hypothesis is added: H : Ps s x /\ F x s /\ Ps t x /\ F x t -> s = t. I know I can destruct the hypothesis H, prove the premisses and use the conclusion. But I also know that I can give the premisses directly in the pose proof command. I want to do something like pose proof (A4 x s t Premisses).
First of all, in (_ : T x1 x2) Coq will only trigger type class resolution to fill the hole when T is a class. Second, classes get special implicit generalization behavior; specifically, you can write {T} and Coq will automatically generalize the arguments to T, which you don't even have to write down.
Theorem noworks : forall (X : Type) (P : X → Prop) (A : Prop) (x' : X), A → (A → (A → P x')) → P x'. Then apply Himp in HA would work and generate a second goal, asking for a proof of A. However when it comes to quantifiers, apply does not generate goals for them, hence the failure. You can instead use eapply (where the e stands ...
The abstracting tactic is called generalize_eqs and it takes as argument a hypothesis to generalize. It uses the JMeq datatype defined in Coq.Logic.JMeq, hence we need to require it before. For example, revisiting the first example of the inversion documentation: Require Import Coq.Logic.JMeq.
The inductive case S x produces a new term x and a new hypothesis, so we give those names. The vertical bar separates the two cases. After proving the base case, we move on to the inductive case. Hey, Coq came up with the correct induction hypothesis for us. Thanks, Coq! Theorem n_plus_n : forall (n : nat), n + n = n * 2. Proof. induction n as ...
Explore Teams Create a free Team. Teams. ... Coq cannot `simple apply reflexivity` in custom tactic. ... Coq sublanguages for defining custom tactics. 1. Proving that applicative functors compose. 4. Ltac - run tactic for each hypothesis of given pattern. 7. Examples of theories where tactic language is required for simple proofs. 1.
Qed. So you first assert the premise of H and prove it. Then you specialize H with the proven premise and all what remains in H is False. Destruct H then asks you to solve the goal for all possible cases in which H can be constructed. For False there is no way to construct it, so you have to solve the goal for 0 cases.
There are three Coq commands: coqtop: the Coq toplevel (interactive mode); coqc: the Coq compiler (batch compilation); coqchk: the Coq checker (validation of compiled libraries). The options are (basically) the same for the first two commands, and roughly described below. You can also look at the man pages of coqtop and coqc for more details.
I'm doing a Coq proof. I have P -> Q as a hypothesis, and (P -> Q) -> (~Q -> ~P) as a lemma. ... Take a conjunction of two hypotheses and create a new hypothesis in Coq. 0. How to specialize nested hypotheses in Coq? 0. Coq : replace hypothesis into implication. Hot Network Questions
Note that simpl here doesn't work because it's not really a tactic to simplify hypotheses in the usual sense, it's really just a tactic to apply some computation rules, it basically evaluates the goal or the hypothesis you apply it on. True -> P does not reduce to P because it would then take one fewer argument. edited Mar 24, 2020 at 15:26.
Definition divides d n := exists c, d*c = n. Section divisor. Variables (d n a:Z). Hypothesis H: divides d n. Now I want to introduce c and the fact that d*c = n into the environment, so I don't have to start my proof by destructing H every time, like this: Lemma div4: divides (a*d) (a*n). destruct H as [c H'].