ArtsAutosBooksBusinessEducationEntertainmentFamilyFashionFoodGamesGenderHealthHolidaysHomeHubPagesPersonal FinancePetsPoliticsReligionSportsTechnologyTravel

Introduction to the Coq Software for Type Theory Part 2: Tactics

Updated on December 9, 2013

So to continue from the last hub I made on the subject, I will here discuss proving statements in Coq from the axioms, functions and definitions you have established. The essential part here is the use of tactics, which allows us to rewrite statements or assert lemmas. As in the previous hub, the examples will be taken from an attempt to build Euclidean geometry in Coq. Let us start with an easy example.

A Simple Example

Theorem ASA_Congruence : Congruence (P,Q,R) (X,Y,Z).


apply SSSImply.

apply ASA_imply_SSS.


This is the last part of a longer proof stating that ASA( that is to say, two angles having to equal angles and one equal line between them) implies Congruence (that the same two triangles have all angles and lines equal) that I split up in several parts. At this point it has been proven that ASA implies SSS (all sides equal), and we have from axiom that SSS implies congruence. So now it is fairly straight forward.

The first line defines what the end goal is :

Theorem ASA_Congruence : Congruence (P,Q,R) (X,Y,Z).

We start with «Theorem», which states that is is a theorem which shall be proven. One might also use «Lemma». Next, we give the theorem a name, which is useful if we want to refer to it later. I gave this proof the name ASA_Congruence.

Then, after the :, we state what we shall prove. I had previously defined P,Q,R,X,Y,Z as having type point, and proven things around them. One might also have used intros here to generalize, which will be discussed later.

So (P,Q,R) and (X,Y,Z) makes two triangles defined by these points.

The next line, proof, simply states that writing out the proof follows.


Here is how Coq looks at this point. The green marker shows what has been checked and confirmed by Cow to be logical. Comparing to regular programming, you might say Coq can compile one line at a time, which is helpful.

The right upper side shows the goals, ie what we are trying to prove right now. At the line we are at, right at the beginning of the proof, it states congruence between the two triangles. The right lower side send messages to the user, for example if there is an error in the proof.

Now, the first line in the proof is

apply SSSImply.

“apply” states that this will prove the statement we are looking for. SSSImply states that triangles which have SSS also have Congruence. apply only works if the end goal of what we are proving matches with the end statement of what we are applying.

In this case, that is true. So now all we have to do is prove the assumptions of SSSImply, that is to say, that the triangles have SSS.

The screen now looks like this.


As you see, the green has gone one line down, and the goal has changed, now we are asked to prove SSS between the triangles. ASA_implies_SSS states exactly this, and so the proof is finished. We end with a Qed, which closes the proof and defines whatever we have proven, so that it can be used later.


in this proof I only used apply, but there are other tactics. Here is a list of some tactics and their uses:

rewrite, is the tactic I use the most. It rewrites the subgoal according to some variable. Some of you might remember mirrorSym from my earlier post, which allows you to change the order of the points defining a triangle while still having the same triangle. By writing

rewrite mirrorSym.

I could have rewritten the the triangles in the subgoals. Often it suffices to write it like this, but sometimes you have to specify what you want rewritten, for example:

rewrite (mirrorSym (X,Y,Z)).

rewrite changes a subgoal, but does not prove it.

Then there is fold and unfold. At the second stage of the proof I was supposed to prove SSS between two triangles. I had a theorem ready for that, but otherwise I would have used unfold. Unfold will unfold a definition, for SSS that would mean that all the lines are equal, and so you would prove that instead. A related one is split, which allows us to split a goal into two smaller subgoals. unfold SSS would first have a product type we would have to prove, EqualLine*EqualLine*EqualLine. Split would then be applied twice to turn it into three EqualLine goals, which we can prove separately.

Fold does the opposite of unfold, it fold something into its definition.

assert lets you add a subgoal which might help you in the other proofs, for example

assert (H : EqualLine X Y).

This little lemma is after being proven called H, and you can use it later in the proof. This is especially useful if you have to use this fact several times.

Not exactly a tactic, I should mention Let. This lets you define a term, for example:

Let A : Angle := (CreateAngle X Y Z).

This means that A is defined as the angle centered in X. You may then fold (CreateAngle X Y Z) which makes things more orderly and is sometimes necessary, if you want to, for example unfold the definition of X (if it has one) but you do not wish the X in the angle to be affected.

Intro lets you get “examples” of what you want to prove. If you want to prove something for all cases of an object, (using forall as in the previous post), intro defines examples of those objects with the right properties, and proving it for the intros is the same as proving it for all objects of that type.

And finally, symmetry and reflexivity. You might remember that we have the identity function for all types, and that Coq says the identity function has symmetry and reflexivity. This is how you state that for Coq to understand, so if you goal is EqualPoint A A, you can simple state


and the goal is finished. Symmetry changes the order of the two terms in an equality-goal.

These are the tactics I have used, although there are many more. These have however been enough to establish all I have proven so far in Euclidean geometry.


    0 of 8192 characters used
    Post Comment

    No comments yet.


    This website uses cookies

    As a user in the EEA, your approval is needed on a few things. To provide a better website experience, uses cookies (and other similar technologies) and may collect, process, and share personal data. Please choose which areas of our service you consent to our doing so.

    For more information on managing or withdrawing consents and how we handle data, visit our Privacy Policy at:

    Show Details
    HubPages Device IDThis is used to identify particular browsers or devices when the access the service, and is used for security reasons.
    LoginThis is necessary to sign in to the HubPages Service.
    Google RecaptchaThis is used to prevent bots and spam. (Privacy Policy)
    AkismetThis is used to detect comment spam. (Privacy Policy)
    HubPages Google AnalyticsThis is used to provide data on traffic to our website, all personally identifyable data is anonymized. (Privacy Policy)
    HubPages Traffic PixelThis is used to collect data on traffic to articles and other pages on our site. Unless you are signed in to a HubPages account, all personally identifiable information is anonymized.
    Amazon Web ServicesThis is a cloud services platform that we used to host our service. (Privacy Policy)
    CloudflareThis is a cloud CDN service that we use to efficiently deliver files required for our service to operate such as javascript, cascading style sheets, images, and videos. (Privacy Policy)
    Google Hosted LibrariesJavascript software libraries such as jQuery are loaded at endpoints on the or domains, for performance and efficiency reasons. (Privacy Policy)
    Google Custom SearchThis is feature allows you to search the site. (Privacy Policy)
    Google MapsSome articles have Google Maps embedded in them. (Privacy Policy)
    Google ChartsThis is used to display charts and graphs on articles and the author center. (Privacy Policy)
    Google AdSense Host APIThis service allows you to sign up for or associate a Google AdSense account with HubPages, so that you can earn money from ads on your articles. No data is shared unless you engage with this feature. (Privacy Policy)
    Google YouTubeSome articles have YouTube videos embedded in them. (Privacy Policy)
    VimeoSome articles have Vimeo videos embedded in them. (Privacy Policy)
    PaypalThis is used for a registered author who enrolls in the HubPages Earnings program and requests to be paid via PayPal. No data is shared with Paypal unless you engage with this feature. (Privacy Policy)
    Facebook LoginYou can use this to streamline signing up for, or signing in to your Hubpages account. No data is shared with Facebook unless you engage with this feature. (Privacy Policy)
    MavenThis supports the Maven widget and search functionality. (Privacy Policy)
    Google AdSenseThis is an ad network. (Privacy Policy)
    Google DoubleClickGoogle provides ad serving technology and runs an ad network. (Privacy Policy)
    Index ExchangeThis is an ad network. (Privacy Policy)
    SovrnThis is an ad network. (Privacy Policy)
    Facebook AdsThis is an ad network. (Privacy Policy)
    Amazon Unified Ad MarketplaceThis is an ad network. (Privacy Policy)
    AppNexusThis is an ad network. (Privacy Policy)
    OpenxThis is an ad network. (Privacy Policy)
    Rubicon ProjectThis is an ad network. (Privacy Policy)
    TripleLiftThis is an ad network. (Privacy Policy)
    Say MediaWe partner with Say Media to deliver ad campaigns on our sites. (Privacy Policy)
    Remarketing PixelsWe may use remarketing pixels from advertising networks such as Google AdWords, Bing Ads, and Facebook in order to advertise the HubPages Service to people that have visited our sites.
    Conversion Tracking PixelsWe may use conversion tracking pixels from advertising networks such as Google AdWords, Bing Ads, and Facebook in order to identify when an advertisement has successfully resulted in the desired action, such as signing up for the HubPages Service or publishing an article on the HubPages Service.
    Author Google AnalyticsThis is used to provide traffic data and reports to the authors of articles on the HubPages Service. (Privacy Policy)
    ComscoreComScore is a media measurement and analytics company providing marketing data and analytics to enterprises, media and advertising agencies, and publishers. Non-consent will result in ComScore only processing obfuscated personal data. (Privacy Policy)
    Amazon Tracking PixelSome articles display amazon products as part of the Amazon Affiliate program, this pixel provides traffic statistics for those products (Privacy Policy)