create new hypothesis in coq

• Documentation

The Coq Proof Assistant

A tutorial by mike nahas, introduction, prerequisites, installing coq.

• Get "CoqIDE", the graphical version of Coq. It is available at http://coq.inria.fr/download (If you're running Linux, your package manager may have it.)
• Get "coqtop", the command-line version of Coq. It is available at http://coq.inria.fr/download (If you're running Linux, your package manager may have it.)
• Get "Proof General" Emacs mode. Is is available at http://proofgeneral.inf.ed.ac.uk/
• Install Proof General for Emacs. This is not difficult. Or, at least, it is easier than learning Emacs. The Proof General documentation will tell you how to install it.

Loading this file

Your first proof, dissection of your first proof.

• The "vernacular" language manages definitions, and each of its commands starts with a capital letter: "Theorem", "Proof", and "Qed".
• The "tactics" language is used to write proofs, and its commands start with a lower-case letter: "intros" and "exact".
• The "Gallina" language is used to express what you want to prove, and its expressions use lots of operators and parentheses: "(forall A : Prop, A -> A)".

Seeing where you are in a proof

Your first tactic.

• (forall x : nat, (x < 5) -> (x < 6))
• (forall x y : nat, x + y = y + x)
• (forall A : Prop, A -> A)

Proofs with ->

Proof going forward, proof going backward, proof going backward (large), proof going backward (huge), proof going forward (huge), true and false vs. true and false.

• Capital-F "False" is a Prop with no proofs.
• Capital-T "True" is a Prop that has a single proof called "I". (That's a capital-I, not a number 1.)
• Lastly, "bool" is a Set and "bool" has two elements: lower-case-t "true" and lower-case-f "false".

Capital-T True and Capital-F False

True is provable, unprovability.

• (forall proof_of_A: A, False)
• A -> False

False is unprovable

-> examples, reducto ad absurdium, the return of lower-case true and lower-case false, is_true true is true, is_true called with a complex constant., case with bools.

• (or (x < 5) (x = 7))
• (or True False)
• (or (x = 0) (x = 1))
• or (A B:Prop) : Prop
• declares "or", a function that takes two Props and produces a Prop
• declares "or_introl", a constructor that takes a proof of "A" and returns a proof of "(or A B)"
• declares "or_intror", a constructor that takes a proof of "B" and returns a proof of "(or A B)"
• declares "\/", an operator that is interchangeable with "or"

Or commutes

And commutes, destruct tactic, functions and inductive types.

• andb (b1 b2:bool) : bool
• orb (b1 b2:bool) : bool
• negb (b:bool) : bool
• combining "refine" and "exact" and skipping right over "simpl".

admit tactic

• HINT: Remember "~A" is "A -> False".
• HINT: You can make use of the proof "False_cannot_be_proven"
• HINT: When you get stuck, look at "thm_true_imp_false".

Existence and Equality

• the predicate
• the witness
• a proof of the predicated called with the witness

More existence

Exists and forall.

• we use intros and unfold until we have everything in the context.
• we use "destruct" to extract the witness and the proof of "P witness".
• we call "(forall x, ~(P x))" with the witness, to generate "(P witness) -> False"
• we call "P witness -> False" with "P witness" to get a proof of "False".
• we use the tactic "case" on "proof_of_False"
• we use intros and unfold until our subgoal is "False".
• we use "refine" to call a function whose type ends in "-> False"
• we create something of type "exists" by calling "ex_intro"

Calculating witnesses

Equality is symmetric, equality is transitive, inequality with discriminate, natural numbers and induction, peano arithmetic.

• 0 is a natural number.
• For every natural number n, (S n) is a natural number.
• 1 is (S 0) = (1 + 0)
• 2 is (S (S 0)) = (1+ (1 + 0))
• 3 is (S (S (S 0)) = (1 + (1 + (1 + 0)))
• (plus (S (S O)) (S (S (S O))))
• (S (plus (S O) (S (S (S O)))))
• (S (S (plus O (S (S (S O))))))
• (S (S (S (S (S O))))))
• define a function "P n" that represents "O + n = n"
• prove that the function holds for "P O"
• prove that the function holds for "P (S n)" assuming "P n"
• and then call the function nat_ind with those 3 values.

Addition is Symmetric

Common nat operators.

• "n - m" := (minus n m)
• "n <= m" := (le n m)
• "n < m" := (lt n m)
• "n >= m" := (ge n m)
• "n > m" := (gt n m)
• "x <= y <= z" := (x <= y /\ y <= z)
• "x <= y < z" := (x <= y /\ y < z)
• "x < y < z" := (x < y /\ y < z)
• "x < y <= z" := (x < y /\ y <= z)

Lists and Option

The three forms of hd.

• have "hd" take an additional parameter, which it returns if the list is empty
• have "hd" return a new data structure that may or may not contain the value
• pass "hd" a proof that the list is not empty

hd with additional parameter

Hd returns option, hd with a proof that the list is non-empty, tail of lists, appending lists, vernacular commands.

• "Theorem" starts a proof.
• "Qed" ends a proof.
• "Definition" declares a function.
• "Fixpoint" declares a recursive function.
• "Inductive" declares data types.
• "Notation" creates new operators.
• "Infix" also creates new operators.
• "Show Proof" prints out the current state of the proof.
• "Require Import" reads in definitions from a file.
• "Check" prints out a description of a type.
• "Compute" prints out the result of a function call.

The tactic guide

Recent news.

• Coq 8.9.0 is out
• Coq 8.9+beta1 is out
• Coq 8.8.2 is out

• xhtml valid

A Hands-on Introduction to Coq

Nov 22, 2020 21:00 · 3262 words · 16 minute read ctf cyber-security write-up coq, introduction.

I have been doing quite a bit of functional programming in haskell for the past few months as a part of my university study. That’s why I am delighted to see a relevant challenge come up in this year’s DragonCTF.

The challenge involves proving a few mathematical theorems using Coq , a functional programming language / interactive theorem prover. I have heard of Coq before but have never got the time to learn it. This challenge became the perfect opportunity for me to get to know it and write a hands-on introduction about it :)

The challenge starts out with a few easy proofs for us to first get a hang of Coq.

In this proof, we are asked to prove that for two propositions, (A or B) is the same as (B or A) which is quite trivial.

We can try it first in our local environment using the Coq interactive session coqtop in the terminal:

As you can see we are greeted with a list of subgoals that we need to validate once we input the theorem that we are trying to prove.

We can first introduce A, B and move them into our context using the intros command:

What this does is effectively give a name to A and B and add that to the context. We can certainly use other names for the two propositions as well. Another point to note is that all coq commands need to end with a . just like how every line in C needs to end with ; .

The next step would be to again introduce our hypothesis that A \/ B :

Now with our named propositions A and B and hypothesis H, we can start proving our goal that B \/ A .

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:

Next, we use right to suggest that we want to prove that the right-hand side of B \/ A is true. Because it is an OR statement, we only need to show that one of the two is true, not both. Similarly, left is another valid tactic as well.

Now, we can see that our hypothesis H matches the statement we are trying to prove exactly. We can use exact H to finish this sub-proof:

Now, we only have 1 subgoal left which is when H: B . As you can already tell, this is very similar to our last case. To not repeat ourselves, we can use the auto tactic to solve this case automatically:

Just like that, we finished our first proof in Coq! 🎉🎉🎉

The next few proofs are similar in difficulty:

This proof is so simple that auto can just handle it by itself.

This proof of the commutativity of addition is a bit more involved. We used the induction tactic on m and later rewrote (m+n) as (n+m) in the inductive case utilizing the inductive hypothesis.

Few noteworthy points in this proof include: We can use the assumption tactic in place of exact ??? when the thing we are trying to prove is already in our context When we have A And B , we can use split to break it into two cases of proving A and proving B . Just like how equality can be used to rewrite statements using rewrite , implications can be applied to statements using apply The in keyword allows us to manipulate hypotheses rather than our goal.

Most of the tactics in the proof are introduced before with the exception of exists which simply states that a variable in our context satisfies the goal that we are trying to prove.

This last one is also quite easy to prove. We have two boolean values which only lead to four cases. Using destruct , we can divide-and-conquer each of the cases.

Fun with Math

With the easy ones out of the way, we face a slightly more challenging question:

Here we can see that Arith.Mult. has been imported suggesting that we might need to use some of its properties.

Again, we start with introducing the variables:

Then we can use the distributivity of multiplication in Arith.Mult. and a few other properties on addition to simplify our expression.

At this point, what we really need to prove is that n * m is the same as m * n . We can use cut to state that as a hypothesis and prove it later:

Proof on Lists

As the last question, we are asked to write a proof about lists:

I struggled a lot with this proof and solved it in the end by referencing a similar proof on the standard list type in coq.

Here is my attempt at it:

The basic idea is to do a nested induction on both the index n as well as the list l . However, you need to be careful with the order in which you introduce things otherwise Coq will generate inductive hypotheses not strong enough to prove the theorem.

I really enjoyed getting to know Coq this weekend and managed to catch a glimpse of the full power of Coq as an interactive theorem prover. I really hope this blog post can inspire more people to try Coq and have some fun with it.

Here are some resources that aided me in the process of learning Coq:

• Coq cheat sheet : A great introduction to all the tactics available in Coq and a clear breakdown of when to use what
• Theorem proving with Coq : A wonderful example-based introduction the language that shows the full process of proving things
• Coq Tactics Index : A more in-depth look at the various tactics with some small tricks mixed in

Exploit + Flag

If you care about my exploit script and want to see the flag, here you go:

flag: DrgnS{xxxx_my_c0q_for_4_flag_17bcbc34b7c565a766e335}

Pose proof in Coq

https://stackoverflow.com/q/71768615

I'm trying to prove a theorem in Coq. My current context is:

1 subgoal s, t, x : Entity Pssx : Ps s x Fxs : F x s IPssx : F x s /\ Ps s x Ctss : C t s s Pstx : Ps t x Fxt : F x t ============================ C s s s

F , Ps and C are relations of the theory. I've also Axiom 4:

What I want to do, is to use A4 in the proof, as it will help me to say that s and t are equals. So I've tested: pose proof (A4 x s t). 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). But I don't know what to put instead of Premisses .

I tried several solutions:

composing the hypothesis with /\ , such as pose proof (A4 x s t (Pssx /\ Fxs /\ Pstx /\ Fxt)). but I got the error

The command has indeed failed with message: In environment s, t, x : Entity Pssx : Ps s x Fxs : F x s IPssx : F x s /\ Ps s x Ctss : C t s s Pstx : Ps t x Fxt : F x t The term "Pssx" has type "Ps s x" while it is expected to have type "Prop" .

using the assert command and pose proof (A4 x s t H1). :

assert (H1 := (Ps s x) /\ (F x s) /\ (Ps t x) /\ (F x t)). but I got

The command has indeed failed with message: In environment s, t, x : Entity Pssx : Ps s x Fxs : F x s IPssx : F x s /\ Ps s x Ctss : C t s s Pstx : Ps t x Fxt : F x t H1 : Prop The term "H1" has type "Prop" while it is expected to have type "Ps s x /\ F x s /\ Ps t x /\ F x t" .

assert (H1 := (Pssx) /\ (Fxs) /\ (Pstx) /\ (Fxt)). but I got

The command has indeed failed with message: In environment s, t, x : Entity Pssx : Ps s x Fxs : F x s IPssx : F x s /\ Ps s x Ctss : C t s s Pstx : Ps t x Fxt : F x t H1 : Prop The term "Pssx" has type "Ps s x" while it is expected to have type "Prop" .

So my question is the following: what should I put instead of Premisses for my code to work? Is there a command to create new hypothesis based on other ones? I know how to destruct an hypothesis into two smaller hypothesis, but I don't know how to compose hypothesis to create bigger ones.

The standard in Coq would be to curry your A4 so that instead of receiving one large conjunction as a premise, it receives several different premises:

Then you can do:

s, t, x : Entity Pssx : Ps s x Fxs : F x s IPssx : F x s /\ Ps s x Ctss : C t s s Pstx : Ps t x Fxt : F x t H : s = t C s s s

If you absolutely need A4 with the conjunctions, you can use conj (which you can find with Print "_ /\ _" ):

Navigation Menu

Search code, repositories, users, issues, pull requests..., provide feedback.

We read every piece of feedback, and take your input very seriously.

Saved searches

Use saved searches to filter your results more quickly.

To see all available qualifiers, see our documentation .

• Notifications You must be signed in to change notification settings

Tricks you wish the Coq manual told you [maintainer= @tchajed ]

Licenses found

Coq-community/coq-tricks, folders and files.

Repository files navigation

Tricks in coq.

Some tips, tricks, and features in Coq that are hard to discover.

If you have a trick you've found useful feel free to submit an issue or pull request!

• Tej Chajed (initial)
• Tej Chajed ( @tchajed )
• License: The code in the repository is licensed under the terms of the MIT license . The documentation (including this README) is licensed under the CC0 license .
• Compatible Coq versions: Coq master

To build all the examples in src/ , run make .

• The pattern tactic generalizes an expression over a variable. For example, pattern y transforms a goal of P x y z into (fun y => P x y z) y . An especially useful way to use this is to pattern match on eval pattern y in constr:(P x y z) to extract just the function.
• lazymatch is like match but without backtracking on failures inside the match action. If you're not using failures for backtracking (this is often the case), then lazymatch gets better error messages because an error inside the action becomes the overall error message rather than the uninformative "no match" error message. (The semantics of match mean Coq can't do obviously do better - it can't distinguish between a bug in the action and intentionally using the failure to prevent pattern matching.)
• deex (see Deex.v ) is a useful tactic for extracting the witness from an exists hypothesis while preserving the name of the witness and hypothesis.
• Ltac t ::= foo. re-defines the tactic t to foo . This changes the binding , so tactics that refer to t will use the new definition. You can use this for a form of extensibility: write Ltac hook := fail and then use repeat match goal with | (* initial cases *) | _ => hook | (* other cases *) end in your tactic. Now the user can insert an extra case in your tactic's core loop by overriding hook .
• learn approach - see Learn.v for a self-contained example or Clément's thesis for more details
• unshelve tactical, especially useful with an eapply - good example use case is constructing an object by refinement where the obligations end up being your proofs with the values as evars, when you wanted to construct the values by proof
• unfold "+" works
• destruct matches tactic; see coq-tactical's SimplMatch.v
• using instantiate to modify evar environment (thanks to Jonathan Leivent on coq-club)
• eexists ?[x] lets one name an existential variable to be able to refer to it later
• strong induction is in the standard library: Require Import Arith. and use induction n as [n IHn] using lt_wf_ind.
• induction on the length of a list: Require Import Coq.Arith.Wf_nat. and induction xs as [xs IHxs] using (induction_ltof1 _ (@length _)); unfold ltof in IHxs.
• debug auto , debug eauto , and debug trivial give traces, including failed invocations. info_auto , info_eauto , and info_trivial are less verbose ways to debug which only report what the resulting proof includes
• constructor and econstructor backtrack over the constructors over an inductive, which lets you do fun things exploring the constructors of an inductive type. See Constructors.v for some demonstrations.
• There's a way to destruct and maintain an equality: destruct_with_eqn x . You can also do destruct x eqn:H to explicitly name the equality hypothesis. This is similar to case_eq x; intros ; I'm not sure what the practical differences are.
• rew H in t notation to use eq_rect for a (safe) "type cast". Need to import EqNotations - see RewNotation.v for a working example.
• intro -patterns can be combined in a non-trivial way: intros [=->%lemma] -- see IntroPatterns.v .
• change tactic supports patterns ( ?var ): e.g. repeat change (fun x => ?f x) with f would eta-reduce all the functions (of arbitrary arity) in the goal.
• One way to implement a tactic that sleeps for n seconds is in Sleep.v .
• in H1, H2 (just H1 and H2 )
• in H1, H2 |- * ( H1 , H2 , and the goal)
• in * |- (just hypotheses)
• in |- (nowhere)
• in |- * (just the goal, same as leaving the whole thing off)
• in * |- * (everywhere, same as in * ) These forms would be especially useful if occurrence clauses were first-class objects; that is, if tactics could take and pass occurrence clauses. Currently user-defined tactics support occurrence clauses via a set of tactic notations.
• Defining tactics ( Tactic Notation s) that accept multiple optional parameters directly is cumbersome, but it can be done more flexibly using Ltac2. An example can be found in TacticNotationOptionalParams.v .
• You can use notations to shorten repetitive Ltac patterns (much like Haskell's PatternSynonyms ). Define a notation with holes (underscores) and use it in an Ltac match, eg Notation anyplus := (_ + _). and then match goal with | |- context[anyplus] => idtac end I would recommend using Local Notation so the notation isn't available outside the current file.
• You can make all constructors of an inductive hints with Hint Constructors ; you can also do this locally in a proof with eauto using t where t is the name of the inductive.
• The intuition tactic has some unexpected behaviors. It takes a tactic to run on each goal, which is auto with * by default, using hints from all hint databases . intuition idtac or intuition eauto are both much safer. When using these, note that intuition eauto; simpl is parsed as intuition (eauto; simpl) , which is unlikely to be what you want; you'll need to instead write (intuition eauto); simpl .
• The Coq.Program.Tactics library has a number of useful tactics and tactic helpers. Some gems that I like: add_hypothesis is like pose proof but fails if the fact is already in the context (a lightweight version of the learn approach); destruct_one_ex implements the tricky code to eliminate an exists while retaining names (it's a better version of our deex ); on_application matches any application of f by simply handling a large number of arities.
• You can structure your proofs using bullets. You should use them in the order - , + , * so that Proof General indents them correctly. If you need more bullets you can keep going with -- , ++ , ** (although you should rarely need more then three levels of bullets in one proof).
• You can use the set tactic to create shorthand names for expressions. These are special let -bound variables and show up in the hypotheses as v := def . To "unfold" these definitions you can do subst v (note the explicit name is required, subst will not do this by default). This is a good way to make large goals readable, perhaps while figuring out what lemma to extract. It can also be useful if you need to refer these expressions.
• When you write a function in proof mode (useful when dependent types are involved), you probably want to end the proof with Defined instead of Qed . The difference is that Qed makes the proof term opaque and prevents reduction, while Defined will simplify correctly. If you mix computational parts and proof parts (eg, functions which produce sigma types) then you may want to separate the proof into a lemma so that it doesn't get unfolded into a large proof term.
• To make an evar an explicit goal, you can use this trick: unshelve (instantiate (1:=_)) . The way this work is to instantiate the evar with a fresh evar (created due to the _ ) and then unshelve that evar, making it an explicit goal. See UnshelveInstantiate.v for a working example.
• The enough tactic behaves like assert but puts the goal for the stated fact after the current goal rather than before.
• You can use context E [x] to bind a context variable, and then let e := eval context E [y] in ... to substitute back into the context. See Context.v for an example.
• If you have a second-order match (using @?z x , which bind z to a function) and you want to apply the function, there's a trick involving a seemingly useless match. See LtacGallinaApplication.v for an example.
• auto with foo nocore with the pseudo-database nocore disables the default core hint databases and only uses hints from foo (and the context).
• If you need to apply a theorem to a hypothesis and then immediately destruct the result, there's a concise way to do it without repetition: apply thm in H as [x H] , for example, might be used then thm produces an existential for a variable named x .
• If you have a hypothesis H: a = b and need f a = f b , you can use apply (f_equal f) in H . (Strictly speaking this is just using the f_equal theorem in the standard library, but it's also very much like the inverse direction for the f_equal tactic.)
• If you want to both run Ltac and return a constr , you can do so by wrapping the side effect in let _ := match goal with _ => side_effect_tactic end in ... . See https://stackoverflow.com/questions/45949064/check-for-evars-in-a-tactic-that-returns-a-value/46178884#46178884 for Jason Gross's much more thorough explanation.
• If you want lia to help with non-linear arithmetic involving division or modulo (or the similar quot and rem ), you can do that for simple cases with Ltac Zify.zify_post_hook ::= Z.div_mod_to_equations. See DivMod.v for an example and the micromega documentation the full details.
• Coq's admit will force you to use Admitted . If you want to use Qed, you can instead use Axiom falso : False. Ltac admit := destruct falso. This can be useful for debugging Qed errors (say, due to universes) or slow Qeds.

tactics in terms, eg ltac:(eauto) can provide a proof argument

maximally inserted implicit arguments are implicit even when for identifier alone (eg, nil is defined to include the implicit list element type)

maximally inserted arguments can be defined differently for different numbers of arguments - undocumented but eq_refl provides an example

r.(Field) syntax: same as Field r , but convenient when Field is a projection function for the (record) type of r . If you use these, you might also want Set Printing Projections so Coq re-prints calls to projections with the same syntax.

Function vernacular provides a more advanced way to define recursive functions, which removes the restriction of having a structurally decreasing argument; you just need to specify a well-founded relation or a decreasing measure maps to a nat, then prove all necessary obligations to show this function can terminate. See manual and examples in Function.v for more details.

Three alternatives may be considered as drop-in replacements for Function .

• Program Fixpoint may be useful when defining a nested recursive function. See manual and this StackOverflow post .
• CPDT's way of defining general recursive functions with Fix combinator.
• Equations is a plugin which extends Coq with new commands for defining recursive functions, and compiles everything down to eliminators for inductive types, equality and accessibility.

One can pattern-match on tuples under lambdas: Definition fst {A B} : (A * B) -> A := fun '(x,_) => x.

Records fields can be defined with :> , which make that field accessor a coercion. There are three ways to use this (since there are three types of coercion classes). See Coercions.v for some concrete examples.

• If the field is an ordinary type, the record can be used as that type (the field will implicitly be accessed). One good use case for this is whenever a record includes another record; this coercion will make the field accessors of the sub-record work for the outer record as well. (This is vaguely similar to Go embedded structs )
• If the field has a function type, the record can be called.
• If the field is a sort (eg, Type ), then the record can be used as a type.

When a Class field (as opposed to a record) is defined with :> , it becomes a hint for typeclass resolution. This is useful when a class includes a "super-class" requirement as a field. For example, Equivalence has fields for reflexivity, symmetry, and transitivity. The reflexivity field can be used to generically take an Equivalence instance and get a reflexivity instance for free.

The type classes in RelationClasses are useful but can be repetitive to prove. RelationInstances.v goes through a few ways of making these more convenient, and why you would want to do so (basically you can make reflexivity , transitivity , and symmetry more powerful).

The types of inductives can be definitions, as long as they expand to an "arity" (a function type ending in Prop , Set , or Type ). See ArityDefinition.v .

"Views" are a programming pattern that can be used to perform a case analysis only on "relevant" parts of a datatype given the context of the case analysis. See Views.v .

Record fields that are functions can be written in definition-style syntax with the parameters bound after the record name, eg {| func x y := x + y; |} (see RecordFunction.v for a complete example).

If you have a coercion get_function : MyRecord >-> Funclass you can use Add Printing Coercion get_function and then add a notation for get_function so your coercion can be parsed as function application but printed using some other syntax (and maybe you want that syntax to be printing only ).

You can pass implicit arguments explicitly in a keyword-argument-like style, eg nil (A:=nat) . Use About to figure out argument names.

If you do nasty dependent pattern matches or use inversion on a goal and it produces equalities of existT 's, you may benefit from small inversions, described in this blog post . While the small inversion tactic is still not available anywhere I can find, some support is built in to Coq's match return type inference; see SmallInversions.v for examples of how to use that.

You can use tactics-in-terms with notations to write function-like definitions that are written in Ltac. For example, you can use this facility to write macros that inspect and transform Gallina terms, producing theorem statements and optionally their proofs automatically. A simple example is given in DefEquality.v of writing a function that produces an equality for unfolding a definition.

Notations can be dangerous since they by default have global scope and are imported by Import , with no way to selectively import. A pattern I now use by default to make notations controllable is to define every notation in a module with a scope; see NotationModule.v .

This pattern has several advantages:

• notations are only loaded as needed, preventing conflicts when not using the notations
• the notations can be brought into scope everywhere as needed with Import and Local Open Scope , restoring the convenience of a global notation
• if notations conflict, some of them can always be scoped appropriately

Coq has a module system, modeled after ML (eg, the one used in OCaml). You can see some simple examples of using it in Modules.v . In user code, I've found module types and module functors to be more trouble than they're worth 90% of the time - the biggest issue is that once something is in a module type, the only way to extend it is with a new module that wraps an existing module, and the only way to use the extension is to instantiate it. At the same time, you can mostly simulate module types with records.

Coq type class resolution is extremely flexible. There's a hint database called typeclass_instances and typeclass resolution is essentially eauto with typeclass_instances . Normally you add to this database with commands like Instance , but you can add whatever you want to it, including Hint Extern s. See coq-record-update for a practical example.

Classes are a bit special compared to any other type. 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. See the manual on implicit generalization for more details. Note that you don't have to use Class at declaration time to make something a class; you can do it after the fact with Existing Class T .

Set Printing Projections is nice in theory if you use records, but it interacts poorly with classes. See Projections.v .

Other Coq commands

Search vernacular variants; see Search.v for examples.

Search s -Learnt for a search of local hypotheses excluding Learnt

Locate can search for notation, including partial searches.

Optimize Heap (undocumented) runs GC (specifically Gc.compact )

Optimize Proof (undocumented) runs several simplifications on the current proof term (see Proofview.compact )

(in Coq 8.12 and earlier) Generalizable Variable A enables implicit generalization; Definition id `(x:A) := x will implicitly add a parameter A before x . Generalizable All Variables enables implicit generalization for any identifier. Note that this surprisingly allows generalization without a backtick in Instances. Issue #6030 generously requests this behavior be documented, but it should probably require enabling some option. This has been fixed in Coq 8.13; the old behavior requires Set Instance Generalized Output . In Coq 8.14 the option has been removed.

Check supports partial terms, printing a type along with a context of evars. A cool example is Check (id _ _) , where the first underscore must be a function (along with other constraints on the types involved).

The above also works with named existentials. For example, Check ?[x] + ?[y] works.

Unset Intuition Negation Unfolding will cause intuition to stop unfolding not .

Definitions can be normalized (simplified/computed) easily with Definition bar := Eval compute in foo.

Set Uniform Inductive Parameters (in Coq v8.9+beta onwards) allows you to omit the uniform parameters to an inductive in the constructors.

Lemma and Theorem are synonymous, except that coqdoc will not show lemmas. Also synonymous: Corollary , Remark , and Fact . Definition is nearly synonymous, except that Theorem x := def is not supported (you need to use Definition ).

Sections are a powerful way to write a collection of definitions and lemmas that all take the same generic arguments. Here are some tricks for working with sections, which are illustrated in Sections.v :

• Use Context , which is strictly more powerful than Variable - you can declare multiple dependent parameters and get type inference, and can write {A} to make sure a parameter is implicit and maximally inserted.
• Tactics and hints are cleared at the end of a section. This is often annoying but you can take advantage of it by writing one-off tactics like t that are specific to the automation of a file, and callers don't see it. Similarly with adding hints to core with abandon.
• Use notations and implicit types. Say you have a section that defines lists, and you want another file with a bunch of list theorems. You can start with Context (A:Type). Notation list := (List.list A). Implicit Types (l:list). and then in the whole section you basically never need to write type annotations. The notation and implicit type disappears at the end of the section so no worries about leaking it. Furthermore, don't write Theorem foo : forall l, but instead write Theorem foo l : ; you can often also avoid using intros with this trick (though be careful about doing induction and ending up with a weak induction hypothesis).
• If you write a general-purpose tactic t that solves most goals in a section, it gets annoying to write Proof. t. Qed. every time. Instead, define Notation magic := ltac:(t) (only parsing). and write Definition foo l : l = l ++ [] := magic. . You do unfortunately have to write Definition ; Lemma and Theorem do not support := definitions. You don't have to call it magic but of course it's more fun that way. Note that this isn't the best plan because you end up with transparent proofs, which isn't great; ideally Coq would just support Theorem foo := syntax for opaque proofs.

Haskell has an operator f $ x , which is the same as f x except that its parsed differently: f $ 1 + 1 means f (1 + 1) , avoiding parentheses. You can simulate this in Coq with a notation: Notation "f $ x" := (f x) (at level 60, right associativity, only parsing). (from jwiegley/coq-haskell ).

A useful convention for notations is to have them start with a word and an exclamation mark. This is borrowed from @andres-erbsen, who borrowed it from the Rust macro syntax. An example of using this convention is in Macros.v . There are three big advantages to this approach: first, using it consistently alerts readers that a macro is being used, and second, using names makes it much easier to create many macros compared to inventing ASCII syntax, and third, starting every macro with a keyword makes them much easier to get parsing correctly.

To declare an axiomatic instance of a typeclass, use Declare Instance foo : TypeClass . This better than the pattern of Axiom + Existing Instance .

To make Ltac scripts more readable, you can use Set Default Goal Selector "!". , which will enforce that every Ltac command (sentence) be applied to exactly one focused goal. You achieve that by using a combination of bullets and braces. As a result, when reading a script you can always see the flow of where multiple goals are generated and solved.

Arguments foo _ & _ (in Coq 8.11) adds a bidirectionality hint saying that an application of foo should infer a type from its arguments after typing the first argument. See Bidirectional.v for an example and the latest Coq documentation .

Coq 8.11 introduced compiled interfaces, aka vos files (as far as I can tell they are a more principled replacement for vio files). Suppose you make a change deep down to Lib.v and want to start working on Proof.v which imports Lib.v through many dependencies. With vos files, you can recompile all the signatures that Proof.v depends on, skippinng proofs, and keep working. The basic way to use them is to compile Proof.required_vos , a special dependency coqdep generates that will build everything needed to work on Proof.v . Coq natively looks for vos files in interactive mode, and uses empty vos files to indicate that the file is fully compiled in a vo file.

Note that Coq also has vok files; it's possible to check the missing proofs in a vos file, but this does not produce a vo and so all Coq can do is record that the proofs have been checked. They can also be compiled in parallel within a single file, although I don't know how to do that. Compiling vok s lets you fairly confidently check proofs, but to really check everything (particularly universe constraints) you need to build vo files from scratch.

Signature files have one big caveat: if Coq cannot determine the type of a theorem or the proof ends with Defined (and thus might be relevant to later type-checking), it has to run the proof. It does so silently , potentially eliminating any performance benefit. The main reason this happens is due to proofs in a section that don't annotate which section variables are used with Proof using . Generally this can be fixed with Set Default Proof Using "Type" , though only on Coq 8.12+.

Coq 8.12 has a new feature Set Printing Parentheses that prints parentheses as if no notations had an associativity. For example, this will print (1,2,3) as ((1,2),3) . This is much more readable than entirely disabling notations.

You can use Export Set or #[export] Set to set options in a way that affects any file directly importing the file (but not transitively importing, the way Global Set works). This allows a project to locally set up defaults with an options.v file with all of its options, which every file imports. You can use this for basic sanity settings, like Set Default Proof Using "Type". and Set Default Goal Selector "!" without forcing them on all projects that import your project.

You can use all: fail "goals remaining". to assert that a proof is complete. This is useful when you'll use Admitted. but want to document (and check in CI) that the proof is complete other than the admit. tactics used.

You can also use Fail idtac. to assert that a proof is complete, which is shorter than the above but more arcane.

You can use Fail Fail Qed. to really assert that a proof is complete, including doing universe checks, but then still be able to Restart it. I think this is only useful for illustrating small examples but it's amusing that it works. (The new Succeed vernacular in Coq 8.15 is a better replacement, because it preserves error messages on failure.)

Hints can now be set to global, export, or local. Global (the current default) means the hint applies to any module that transitivity imports this one; export makes the hint visible only if the caller imports this module directly. The behavior will eventually change for hints at the top-level so that they become export instead of global (see coq/coq#13384 ), so this might be worth understanding now. HintLocality.v walks through what the three levels do.

The uniform inheritance condition for coercions is gone as of March 2022. This condition required that all the implicit arguments of the target of a coercion could be inferred from the source, so if the source had extra implicit arguments the definition could not be a coercion. This is no longer the case - elaboration will infer the missing arguments. There's still a warning but you can disable it with #[warning="-uniform-inheritance"] on the coercion.

Warnings and options

• You can use Set Warnings "-deprecated-syntactic-definition" to achieve the same effect as -w -deprecated-syntactic-definition from the command line, but from within a Coq file. At least as of Coq 8.19 you can also use #[warning=-"-deprecated-syntactic-definition] to disable the warning for one command.
• You can pass -noinit to coqc or coqtop to avoid loading the standard library.
• Ltac is provided as a plugin loaded by the standard library; if you have -noinit to load it you need Declare ML Module "ltac_plugin". (see NoInit.v ).
• Numeral notations are only provided by the prelude, even if you issue Require Import Coq.Init.Datatypes .
• If you use Coq master, the latest Coq reference manual is built and deployed to https://coq.github.io/doc/master/refman/index.html automatically.
• At Qed, Coq re-checks the proof term, which can take a while. At the same time, Qed rarely fails - some reasons why it might include that there's a universe inconsistency, the coinductive guarded check fails, there's a bug in an OCaml tactic, or there's an incorrect use of exact_no_check . It's not so easy to disable Qed - in Perennial we do so using this disable-qed.sh script, which replaces Qed with Unshelve. Fail idtac. Admitted. . This still ensures there are no goals, but skips the Qed checking. We only skip Qed during CI, but run it regularly locally to have a fully consistent build; another good tradeoff would be to run with Qed checking on a weekly basis but not on every commit.

Contributors 10

• Makefile 0.9%

Coq Cheatsheet

When proving theorems in Coq, knowing what tactics you have at your disposal is vital. In fact, sometimes it’s impossible to complete a proof if you don’t know the right tactic to use!

We provide this tactics cheatsheet as a reference. It contains all the tactics used in the lecture slides, notes, and lab solutions.

Quick Overview

Here is a brief overview of the tactics that we’ve covered. Click on any of the links for more details about how to use them.

Solving simple goals:

• assumption : Solves the goal if it is already assumed in the context.
• reflexivity : Solves the goal if it is a trivial equality.
• trivial : Solves a variety of easy goals.
• auto : Solves a greater variety of easy goals.
• discriminate : Solves the goal if it is a trivial inequality and solves any goal if the context contains a false equality.
• exact : Solves a goal if you know the exact proof term that proves the goal.
• contradiction : Solves any goal if the context contains False or contradictory hypotheses.

Transforming goals:

• intros / intro : Introduces variables appearing with forall as well as the premises (left-hand side) of implications.
• simpl : Simplifies the goal or hypotheses in the context.
• unfold : Unfolds the definitions of terms.
• apply : Uses implications to transform goals and hypotheses.
• rewrite : Replaces a term with an equivalent term if the equivalence of the terms has already been proven.
• inversion : Deduces equalities that must be true given an equality between two constructors.
• left / right : Replaces a goal consisting of a disjunction P \/ Q with just P or Q .
• replace : Replace a term with a equivalent term and generates a subgoal to prove that the equality holds.

Breaking apart goals and hypotheses:

• split : Replaces a goal consisting of a conjunction P /\ Q with two subgoals P and Q .
• destruct (and/or) : Replaces a hypothesis P /\ Q with two hypotheses P and Q . Alternatively, if the hypothesis is a disjunction P \/ Q , generates two subgoals, one where P holds and one where Q holds.
• destruct (case analysis) : Generates a subgoal for every constructor of an inductive type.
• induction : Generates a subgoal for every constructor of an inductive type and provides an induction hypothesis for recursively defined constructors.

Solving specific types of goals:

• ring : Solves goals consisting of addition and multiplication operations.
• tauto : Solves goals consisting of tautologies that hold in constructive logic.
• field : Solves goals consisting of addition, subtraction (the additive inverse), multiplication, and division (the multiplicative inverse).

Tacticals (tactics that act on other tactics):

• ; (semicolon) : Applies the tactic on the right to all subgoals produced by the tactic on the left.
• try : Attempts to apply the given tactic but does not fail even if the given tactic fails.
• || (or) : Tries to apply the tactic on the left; if that fails, tries to apply the tactic on the right.
• all: : Applies the given tactic to all remaining subgoals.
• repeat : Applies the given tactic repeatedly until it fails.

Solving simple goals

The following tactics prove simple goals. Generally, your aim when writing Coq proofs is to transform your goal until it can be solved using one of these tactics.

If the goal is already in your context, you can use the assumption tactic to immediately prove the goal.

After introducing the hypothesis P_holds (which says that P is true) into the context, we can use assumption to complete the proof.

reflexivity

If the goal contains an equality that looks obviously true, the reflexivity tactic can finish off the proof, doing some basic simplification if needed.

Both the left and right sides of the equality in the goal are clearly equal (after simplification), so we use reflexivity .

The trivial tactic can solve a variety of simple goals. It introduces variables and hypotheses into the context and then tries to use various other tactics under the hood to solve the goal.

Any goal that can be solved with assumption or reflexivity can also be solved using trivial .

Unlike most of the other tactics in this section, trivial will not fail even if it cannot solve the goal.

Previously, we proved this theorem using intros and assumption ; however, trivial can actually take care of both those steps in one fell swoop.

The auto tactic is a more advanced version of trivial that performs a recursive proof search.

Any goal that can be solved with trivial can also be solved using auto .

Like trivial , auto never fails even if it cannot do anything.

This proof is too complicated for trivial to handle on its own, but it can be solved with auto !

discriminate

The discriminate tactic proves that different constructors of an inductive type cannot be equal. In other words, if the goal is an inequality consisting of two different constructors, discriminate will solve the goal.

discriminate also has another use: if the context contains a equality between two different constructors (i.e. a false assumption), you can use discriminate to prove any goal.

You may be surprised to learn that auto cannot solve this simple goal! However, discriminate takes care of this proof easily.

Recall that the natural numbers in Coq are defined as an inductive type with constructors O (zero) and S (successor of). The constructors on both sides of the false equality 0 = 1 are different, so we can use discriminate to prove our goal that any proposition P holds.

If you know the exact proof term that proves the goal, you can provide it directly using the exact tactic.

Suppose we know that eq_refl 42 is a term with the type 42 = 42 . Then, we prove that there exists a value that inhabits this type by supplying the term directly using exact , which proves the theorem.

(We could have also used reflexivity or other tactics to prove this goal.)

contradiction

If there is a hypothesis that is equivalent to False or two contradictory hypotheses in the context, you can use the contradiction tactic to prove any goal.

After destructing the hypothesis P /\ ~P , we obtain two hypotheses P and ~P that contradict each other, so we use contradiction to complete the proof.

Transforming goals

While proving a theorem, you will typically need to transform your goal to introduce assumptions into the context, simplify the goal, make use of assumptions, and so on. The following tactics allow you to make progress toward solving a goal.

intros / intro

If there are universally quantified variables in the goal (i.e. forall ), you can introduce those variables into the context using the intros tactic. You can also use intros to introduce all propositions on the left side of an implication as assumptions.

If intros is used by itself, Coq will introduce all the variables and hypotheses that it can, and it will assign names to them automatically. You can provide your own names (or introduce fewer things) by supplying those names in order. See Example 2.

intros also has a sister tactic intro that introduces just one thing.

intros used by itself will never fail, even if there’s nothing to introduce. If you supply some names to intros , however, it will fail if a name is already in use or if there’s not enough stuff left to introduce.

We can introduce the two variables P and Q , as well as the two hypotheses (P -> Q) and ~Q using intros .

The names that Coq chose for the hypotheses H and H0 aren’t very descriptive. We can provide more descriptive names instead. Note that we also have to give names to the two variables after the forall because intros introduces things in order.

The simpl tactic reduces complex terms to simpler forms. You’ll find that it’s not always necessary to use simpl because other tactics (e.g. discriminate ) can do the simplification themselves, but it’s often helpful to try simpl to help you figure out what you, as the writer of the proof, should do next.

You can also use simpl on a hypothesis in the context with the syntax simpl in <hypothesis> .

simpl will never fail, even if no simplification can be done.

Let’s simplify that goal with simpl .

The unfold tactic replaces a defined term in the goal with its definition.

You can also use unfold on a hypothesis in the context with the syntax unfold <term> in <hypothesis> .

This time, nothing happens if we try simpl . However, we can unfold and transform the goal into something that we can then simplify.

We’d like to unfold the ~(P \/ Q) in our context as well, so we use unfold..in.. .

(In thie case, we could have also applied unfold before intros to unfold all the negations at once.)

The apply tactic has a variety of uses.

If your goal is some proposition B and you know that A -> B , then in order to prove that B holds, it suffices to show A holds. apply uses this reasoning to transform the goal from B to A . See Example 1.

apply can also be used on hypotheses. If you have some hypothesis that states that A holds, as well as another hypothesis A -> B , you can use apply to transform the first hypothesis into B . The syntax is apply <term> in <hypothesis> or apply <term> in <hypothesis> as <new-hypothesis> . See Example 2.

You can even apply previously proven theorems. See Example 3.

Since we know that P -> Q , proving that P holds would also prove that Q holds. Therefore, we use apply to transform our goal.

Alternatively, we notice that P holds in our context, and because we know that P -> Q , we can apply that implication to our hypothesis that P holds to transform it.

Note that this replaces our previous hypothesis (and now its name is no longer very applicable)! To prevent this, we can give our new hypothesis its own name using the apply..in..as.. syntax.

We notice that our goal is just an instance of P -> (P -> Q) -> Q , which we already proved is true. Therefore, we can use apply to apply our lemma, which finishes the proof.

Given some known equality a = b , the rewrite tactic lets you replace a with b or vice versa in a goal or hypothesis

The syntax is rewrite -> <equality> to replace a with b in the goal or rewrite <- <equality> to replace b with a . Note that rewrite <equality> is identical to rewrite -> <equality> .

You can also rewrite terms in hypotheses with the rewrite..in.. syntax.

We can try using auto to see if Coq can figure out the rest of the proof for us, but it can’t because it doesn’t know that addition is commutative (that’s what we’re trying to prove!).

However, we can apply our inductive hypothesis x + y = y + x by rewriting the x + y in the goal as y + x using rewrite :

Now you can finish the proof by simply using trivial or auto .

Suppose you have a hypothesis S m = S n , where m and n are nats . The inversion tactic allows you to conclude that m = n . In general, if you have a hypothesis that states an equality between two constructors and the constructors are the same, inversion helps you figure out that all the arguments to those constructors must be equal as well, and it tries to rewrite the goal using that information.

Since S x = S y , we use inversion to extract a new hypothesis that states x = y . inversion actually goes one step further and rewrites the goal using that equality.

left / right

If the goal is a disjunction A \/ B , the left tactic replaces the goal with the left side of the disjunction A , and the right tactic replaces the goal with the right side B .

Since we know that P holds, it makes sense to change the goal to the left side of the disjunction using left .

This time, we know that Q holds, so we replace the goal with its right side using right .

The replace tactic allows you to replace a term in the goal with another term and produces a new subgoal that asks you to prove that those two terms are equal. The syntax is replace <term> with <term> .

We believe that x + 1 and S x are equal, so we can use replace to assert that this equality is true and then prove it later.

Breaking apart goals and hypotheses

The following tactics break apart goals (or hypotheses) into several simpler subgoals (or hypotheses).

If the goal is a conjunction A /\ B , the split tactic replaces the goal with two subgoals A and B .

In order to make progress in the proof, we use split to break up Q /\ R into two subgoals.

destruct (and / or)

If there is a hypothesis containing a conjunction or a disjunction in the context, you can use the destruct tactic to break them apart.

A hypothesis A /\ B means that both A and B hold, so it can be destructed into two new hypotheses A and B . You can also use the destruct..as [...] syntax to give your own name to these new hypotheses. See Example 1.

On the other hand, a hypothesis A \/ B means that at least one of A and B holds, so in order to make use of this hypothesis, you must prove that the goal holds when A is true (and B may not be) and when B is true (and A may not be). You can also use the destruct..as [... | ...] syntax to provide your own names to the hypotheses that are generated (note the presence of the the vertical bar). See Example 2.

Since there’s a conjunction P /\ Q in our context, using destruct on it will give us both P and Q as separate hypotheses.

The names that Coq chose for the new hypotheses aren’t very descriptive, so let’s provide our own.

We can destruct the hypothesis P \/ Q to replace our current goal with two new subgoals P \/ Q with different contexts: one in which P holds and one in which Q holds.

After we’ve proven the first subgoal, we observe that, in the context for the second subgoal, we have the hypothesis that Q holds instead.

destruct (case analysis)

The destruct tactic can also be used for more general case analysis by destructing on a term or variable whose type is an inductive type.

In order to proceed with this proof, we need to prove that it holds for each constructor of element case-by-case, so we use destruct .

Using the induction tactic is the same as using the destruct tactic, except that it also introduces induction hypotheses as appropriate.

Once again, you can use the induction..as [...] syntax to give names to the terms and hypotheses produced in the different cases.

See lecture, notes, and lab 22 for more on induction.

The base case 0 doesn’t produce anything new, so we don’t need to provide any names there. 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!

From here, we can make use of the induction hypothesis with rewrite and then apply auto to knock out the rest of the proof.

Solving specific types of goals

The tactics in this section are automated tactics that are specialized for solving certain types of goals.

The ring tactic can solve any goal that contains only addition and multiplication operations.

You must first use the command Require Import Arith. in order to use ring .

It would be pretty painful to prove this using simpler tactics, but fortunately ring is here to save the day.

The tauto tactic can solve any goal that’s a tautology (in constructive logic). A tautology is a logical formula that’s always true, regardless of the values of the variables in it.

DeMorgan’s law is a tautology, so it can be proven by applying tauto .

The field tactic can solve any goal that contains addition, subtraction (the additive inverse), multiplication, and division (the multiplicative inverse).

Note that field cannot be used on the natural numbers or integers, because integer division is not the inverse of multiplication (e.g. (1 / 2) * 2 does not equal 1).

You must first use the command Require Import Field. in order to use field .

See lecture notes 22 for more information on field .

The following tacticals are “higher-order tactics” that operate on tactics.

; (semicolon)

The ; tactical applies the tactic on the right side of the semicolon to all the subgoals produced by tactic on the left side.

The two subgoals generated by split were solved using the same tactic. We can use ; to make the code more concise.

Many tactics will fail if they are not applicable. The try tactical lets you attempt to use a tactic and allows the tactic to go through even if it fails. This can be particularly useful when chaining tactics together using ; .

We’d like to use discriminate to take care of the second and third subgoals, but we can’t simply write destruct e; discriminate. because discriminate will fail when Coq tries to apply it to the first subgoal. This is where the try tactic comes in handy.

The || tactical first tries the tactic on the left side; if it fails, then it applies the tactic on the right side.

Let’s use this theorem from the last section again. discriminate took care of the other two subgoals, and we know that trivial can solve this one. In other words, we apply either discriminate or trivial to the subgoals generated by destruct e , so we can use || to shorten the proof.

The all: tactical applies a tactic to all the remaining subgoals in the proof.

An alternative proof for the previous theorem using all: .

The repeat tactical repeatedly applies a tactic until it fails.

Note that repeat will never fail, even if it applies the given tactic zero times.

Coq provides a theorem Nat.add_assoc : forall n m p : nat, n + (m + p) = n + m + p in the Arith library that we can make use of two times for this proof.

Acknowledgement: Inspired by the Coq Tactic Index by Joseph Redmon.

Stack Exchange Network

Stack Exchange network consists of 183 Q&A communities including Stack Overflow , the largest, most trusted online community for developers to learn, share their knowledge, and build their careers.

Q&A for work

Connect and share knowledge within a single location that is structured and easy to search.

Applying custom tactic in hypothesis

To avoid tedious repetition I have a tactic that looks something like this:

However, sometimes the expressions I would like to unfold are not in the goal, but in the hypotheses. I can make another tactic

but is there a way to write my tactic so that it can (optionally) be used in hypotheses?

ie. so that I can write unfolds in H. in my proofs

I believe replacing your definition of unfolds' with

Tactic Notation "unfolds" "in" hyp(H) := ... should work. That's how stdpp defines a similar tactic (see line 305 in https://gitlab-10.mpi-sws.org/iris/stdpp/-/blob/master/stdpp/tactics.v. ) You still have to define the tactic twice, once for the goal and once for hypotheses, but you should be able to use it in the way you want.

Your Answer

Sign up or log in, 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 .

Not the answer you're looking for? Browse other questions tagged coq tactic or ask your own question .

• Featured on Meta
• Introducing an accessibility dashboard and some upcoming changes to display...
• We've made changes to our Terms of Service & Privacy Policy - July 2024
• Announcing a change to the data-dump process

Hot Network Questions

• Is there a simple paradox like Russell's paradox that arises if we assume
• Creating specific flash memory area in STM32G0 microcontroller
• Are story points really a good measure for velocity?
• What type of concept is "mad scientist"?
• In Norway, when number ranges are listed 3 times on a sign, what do they mean?
• Iterative mixing problem
• Wall of Fire: Taking damage multiple times by using forced movement on a target
• Simulation Lorenz83 Attractor
• Design patterns - benefits of using with Apex code
• Automatically closing a water valve after a few minutes
• In Europe, are you allowed to enter an intersection on red light in order to allow emergency vehicles to pass?
• How may a Unicode Block font be invoked locally, e.g. by adjusting the following Unicode preamble?
• MPs assuming office on the day of the election
• Why is the completely dark disk of the Moon visible on a new moon if the lunar orbit is at an angle to the Earth’s?
• Normal text and cases
• Does wisdom come with age?
• Grandpa installed this kitchen faucet "once and forever." How do I put in new ball valves?
• Generalized Super-Luhn
• What is “were’t”?
• Why can't I sign into iMessage on OS X 10.9?
• Is threatening to go to the police blackmailing?
• Interview disaster
• What was R' Chanina's Technique to Revive R' Yochanan?
• Self-employed health insurance deduction and insurance just for my kids

Destructing hypothesis

Please see attached file and code.

My question is: why this “destruct” acts like this? what is happening? we have disjunctive pattern with 0 branches here… but destruct works… and changes goal… and leads us to the victory.

AFAIU destruct H with H : A -> B gives A as a new goal and destructs B . Since here B is False , destructing it solves the goal, so only the A part remains to be proved.

Maybe it becomes clearer if you rearrange things a bit:

Theorem not_exists_dist : excluded_middle -> forall (X:Type) (P : X -> Prop), ~(exists x, ~P x) -> (forall x, P x). Proof. intros EM X P H x. unfold not in H. destruct (EM (P x)) as [H2 | H3]. apply H2. assert (exists x : X, P x -> False) as H1. exists x. apply H3. specialize (H H1). destruct H. 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.

Destruct directly applied to H simply automates this a bit and asks you to prove the premise of H.

If you don’t like the destruct H you can also write “exfalso. apply H.” exfalso proves any goal assuming you can prove False in your context. Yet another way of doing this is to writhe “contradiction H” which proves any goal from a hypothesis which is False.

It is so clear now. Thank you.

Related Topics

• Docs »
• Command-line and graphical tools »
• The Coq commands
• Edit on GitHub

The Coq commands ¶

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.

Interactive use (coqtop) ¶

In the interactive mode, also known as the Coq toplevel, the user can develop his theories and proofs step by step. The Coq toplevel is run by the command coqtop .

There are two different binary images of Coq: the byte-code one and the native-code one (if OCaml provides a native-code compiler for your platform, which is supposed in the following). By default, coqtop executes the native-code version; run coqtop.byte to get the byte-code version.

The byte-code toplevel is based on an OCaml toplevel (to allow dynamic linking of tactics). You can switch to the OCaml toplevel with the command Drop. , and come back to the Coq toplevel with the command Coqloop.loop();; .

This flag, off by default, causes coqtop to exit with status code 1 if a command produces an error instead of recovering from it.

Batch compilation (coqc) ¶

The coqc command takes a name file as argument. Then it looks for a file named file .v, and tries to compile it into a file .vo file (See Compiled files ).

The name file should be a regular Coq identifier as defined in Section Lexical conventions . It should contain only letters, digits or underscores (_). For example /bar/foo/toto.v is valid, but /bar/foo/to-to.v is not.

Customization at launch time ¶

By resource file ¶.

When Coq is launched, with either coqtop or coqc , the resource file $XDG_CONFIG_HOME/coq/coqrc.xxx , if it exists, will be implicitly prepended to any document read by Coq, whether it is an interactive session or a file to compile. Here, $XDG_CONFIG_HOME is the configuration directory of the user (by default it's ~/.config ) and xxx is the version number (e.g. 8.8). If this file is not found, then the file $XDG_CONFIG_HOME/coqrc is searched. If not found, it is the file ~/.coqrc.xxx which is searched, and, if still not found, the file ~/.coqrc . If the latter is also absent, no resource file is loaded. You can also specify an arbitrary name for the resource file (see option -init-file below).

The resource file may contain, for instance, Add LoadPath commands to add directories to the load path of Coq. It is possible to skip the loading of the resource file with the option -q .

By environment variables ¶

$COQPATH can be used to specify the load path. It is a list of directories separated by : ( ; on Windows). Coq will also honor $XDG_DATA_HOME and $XDG_DATA_DIRS (see Section Libraries and filesystem ).

Some Coq commands call other Coq commands. In this case, they look for the commands in directory specified by $COQBIN . If this variable is not set, they look for the commands in the executable path.

$COQ_COLORS can be used to specify the set of colors used by coqtop to highlight its output. It uses the same syntax as the $LS_COLORS variable from GNU’s ls, that is, a colon-separated list of assignments of the form name= attr * ; where name is the name of the corresponding highlight tag and each attr is an ANSI escape code. The list of highlight tags can be retrieved with the -list-tags command-line option of coqtop .

The string uses ANSI escape codes to represent attributes. For example:

export COQ_COLORS=”diff.added=4;48;2;0;0;240:diff.removed=41”

sets the highlights for added text in diffs to underlined (the 4) with a background RGB color (0, 0, 240) and for removed text in diffs to a red background. Note that if you specify COQ_COLORS , the predefined attributes are ignored.

$OCAMLRUNPARAM , described here , can be used to specify certain runtime and memory usage parameters. In most cases, experimenting with these settings will likely not cause a significant performance difference and should be harmless.

If the variable is not set, Coq uses the default values , except that space_overhead is set to 120 and minor_heap_size is set to 32Mwords (256MB with 64-bit executables or 128MB with 32-bit executables).

By command line options ¶

The following command-line options are recognized by the commands coqc and coqtop , unless stated otherwise:

Add physical path directory to the OCaml loadpath.

Names of libraries and the command Declare ML Module Section Compiled files .

Add physical path directory to the list of directories where Coq looks for a file and bind it to the logical directory dirpath . The subdirectory structure of directory is recursively available from Coq using absolute names (extending the dirpath prefix) (see Section Qualified identifiers ). Note that only those subdirectories and files which obey the lexical conventions of what is an ident are taken into account. Conversely, the underlying file systems or operating systems may be more restrictive than Coq. While Linux’s ext4 file system supports any Coq recursive layout (within the limit of 255 bytes per filename), the default on NTFS (Windows) or HFS+ (MacOS X) file systems is on the contrary to disallow two files differing only in the case in the same directory.

Section Names of libraries .

Do as -Q directory dirpath but make the subdirectory structure of directory recursively visible so that the recursive contents of physical directory is available from Coq using short or partially qualified names.

Set the toplevel module name to dirpath instead of Top . Not valid for coqc as the toplevel module name is inferred from the name of the output file.

Exclude any subdirectory named directory while processing options such as -R and -Q. By default, only the conventional version control management directories named CVS and_darcs are excluded.

Start from an empty state instead of loading the Init.Prelude module.

Load file as the resource file instead of loading the default resource file from the standard configuration directories.

Do not to load the default resource file.

Load and execute the Coq script from file.v .

Load and execute the Coq script from file.v . Write its contents to the standard output as it is executed.

Load Coq compiled library qualid . This is equivalent to running Require qualid .

Note that the relative order of this command-line option and its variants ( -rfrom , -ri , -re , etc.) and of the -set and -unset options matters since the various Require , Require Import , Require Export , Set and Unset commands will be executed in the order specified on the command-line.

Load Coq compiled library qualid . This is equivalent to running From dirpath Require qualid . See the note above regarding the order of command-line options.

Load Coq compiled library qualid and import it. This is equivalent to running Require Import qualid . See the note above regarding the order of command-line options.

Load Coq compiled library qualid and transitively import it. This is equivalent to running Require Export qualid . See the note above regarding the order of command-line options.

Load Coq compiled library qualid and import it. This is equivalent to running From dirpath Require Import qualid . See the note above regarding the order of command-line options.

Load Coq compiled library qualid and transitively import it. This is equivalent to running From dirpath Require Export qualid . See the note above regarding the order of command-line options.

Exit just after argument parsing. Available for coqtop only.

Output the content of the input file as it is compiled. This option is available for coqc only.

Enable the native_compute reduction machine and precompilation to .cmxs files for future use by native_compute . Setting yes enables native_compute ; it also causes Coq to precompile the native code for future use; all dependencies need to have been precompiled beforehand. Setting no disables native_compute which defaults back to vm_compute ; no files are precompiled. Setting ondemand enables native_compute but disables precompilation; all missing dependencies will be recompiled every time native_compute is called.

Changed in version 8.13: The default value is set at configure time, -config can be used to retrieve it. All this can be summarized in the following table:

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 (produced using -vos ) ¶

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).

Compiled libraries checker (coqchk) ¶

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.

• Stack Overflow for Teams Where developers & technologists share private knowledge with coworkers
• Advertising & Talent Reach devs & technologists worldwide about your product, service or employer brand
• OverflowAI GenAI features for Teams
• OverflowAPI Train & fine-tune LLMs
• Labs The future of collective knowledge sharing
• About the company Visit the blog

Collectives™ on Stack Overflow

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.

In Coq, how do I introduce a variable from an hypothesis into the environment?

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.

Your Answer

Reminder: Answers generated by artificial intelligence tools are not allowed on Stack Overflow. Learn more

Sign up or log in

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 .

Not the answer you're looking for? Browse other questions tagged coq or ask your own question .

• Featured on Meta
• We've made changes to our Terms of Service & Privacy Policy - July 2024
• Introducing an accessibility dashboard and some upcoming changes to display...
• Tag hover experiment wrap-up and next steps

Hot Network Questions

• Simulation Lorenz83 Attractor
• Grandpa installed this kitchen faucet "once and forever." How do I put in new ball valves?
• What was R' Chanina's Technique to Revive R' Yochanan?
• I don't do something AFTER I did something
• Iterative mixing problem
• How does a plane literally "fall from the sky"?
• "Seagulls are gulling away."
• Will lights plugged into cigarette lighter drain the battery to the point that the truck won't start?u
• Is there an English equivalent to the Hindi proverb, "A washerman's dog belongs neither at home nor at the riverbank"?
• Wall of Fire: Taking damage multiple times by using forced movement on a target
• How can flipflops sense the edges of the signals?
• How may a Unicode Block font be invoked locally, e.g. by adjusting the following Unicode preamble?
• Why is the completely dark disk of the Moon visible on a new moon if the lunar orbit is at an angle to the Earth’s?
• Dark, cynical video game taking place in the medieval ages
• MPs assuming office on the day of the election
• Will a spaceship that never stops between earth and mars save fuel?
• In Europe, are you allowed to enter an intersection on red light in order to allow emergency vehicles to pass?
• Can a train/elevator be feasible for scaling huge mountains (modern technology)?
• What are some interesting applications of the theory of covering spaces?
• Emphasizing the decreasing condition in the Integral Test or in the AST (in Calculus II): is it worth the time?
• If a planet or star is composed of gas, the center of mass will have zero gravity but immense pressure? I'm trying to understand fusion in stars
• Interview disaster
• Mathematical Theory of Monotone Transforms
• Solving the "Reverse" Assignment Problem with an Added Constraint?