Automatic tactics

trivial - Solves simple goals, a combination of simpl, assumption and reflexivity. easy - Slightly more powerful, can perform introductions and destruct conjunctions.

It is mostly useful in the following notation that ensures that the goal is solved (the notation is already defined in Coq).

auto - Automatically applies lemmas from a lemma database in a Prolog-style fashion. If no arguments are given the database used is "core".

auto with hintdb - Automatically applies tactics and lemmas from the database hintdb given as argument.

We can add lemmas to a database hintdb : new lemmas will be automatically applied.
      Hint Resolve lemma_name : hintdb.
    

We could also add specific tactics instead of lemmas (see the reference manual). Warning! It's easy to create loops, for example with lemmas such as plus_comm : forall m n, m + n = n + m or plus_S : forall n, S n = n + 1. Advice: If you must use auto, create a database of your own instead of adding lemmas to an existing database: it helps with complexity and termination. omega - Solves systems of linear equations and inequalities in Z and nat.

tauto - Solves goals in intuitionistic propositional calculus.

intuition tactic_name - Combines tauto with the tactic given as argument (in fact, we even have tauto = intuition fail). If no argument is given, the default is auto with *.

Dealing with algebraic structures

ring - Solves equalities over a ring or a semi-ring.

field - Solves equalities over a field.

fourier - A kind of omega on real numbers : it solves linear equalities and inequalities on reals.

Integer division

We import the library about natural numbers.

Structural induction

With unary integers (ie nat), we can only define division by subtraction. The most natural way of defining division on integers in Coq is then as follows:

• check if n is 0, in which case division does not make sense
• if m < n, the result is (0, m)
• otherwise, (that is n ≤ m), compute div (m - n) n and add 1 to the quotient.

and then prove the expected properties of division. Here is a tentative definition:
      Fixpoint div m n {struct m} :=
        match n with
          | 0 => (0, 0)
          | S _ => if le_gt_dec n m then let (q,r) := div (m - n) n in (S q, r) else (0, m)
        end.
    

Recall that left and right are the constructors of sumbool, the computational equivalent of disjunction.

1) Try this definition. What is the problem we face here? What happens if we indicate which argument decreases with the construction {struct m}? 2) Find a simple workaround for this last problem. Check your implementation on a few examples. 3) Prove the correctness of your function.

Well-founded induction

To go beyond structural induction, we can use well-founded induction.

It works exactly like a proof by well-founded induction except that we build a function and not a proposition. For that, we need to use a well-founded relation, here <.

Since we will have to deal with well-founded induction, instead of defining only div as a function from nat to nat, we might as well define it together with its full specification. In practice, this means that the return type of the division function will not be a pair of integers but the set of pairs of integers such that the (in)equations we want to the correctness hold.

4) Define the richest (ie most accurate) type for integer division. In order to use well-founded induction, we need to prove that if we know how to compute division for all numbers smaller than n, then we know how to do it for n as well:
    ∀n, (∀m, m < n → div_type m) → div_type n

6) Define such a function (in tactic mode). Wrap up everything to define division.

The Program library

The last solution to define a non structural fixpoint is to use the Program library. 7) Read the page about the Program library.

8) Using Program, define division. Let us now try to compute with our division functions. 9) First, prove the lemma lt_0_3 : 0 < 3. What happens when you do:

• Eval compute in (div1 5 3)
• Eval compute in (div2 5 3 lt_0_3)
• Eval compute in (div3 5 3 lt_0_3)?

Complex numbers

In this last part, we come back to some uses of the automatic tactics presented in the first part.

Complex numbers are pairs of real numbers.

Use the projections fst and snd to acces the components of a complex number. 1) Define oposite, addition, mutiplication on complex numbers. 2) Define some nice notations for your operations. In order to keep theml from interferring with existing notations, we use a specific notation scope C_scope.

To be able to use (...)%C to locally open C_scope.

Each time we have to build an object of type C, the scope C_scope will be open.

You can also open the scope yourself. While we are dealing with scope, note that it is possible to specify the scope s of an argument x (or several at once) of a function f with the command
      Arguments f : x%s [x%s ...]

Note that you must use the name of the scope and not its key (e.g. Z_scope and not Z). 3) Show how equality of complex numbers relates to that of real numbers. 4) Design a tactic that solves equalities on complex numbers. Some reminders on the tactic language (if you want more details, see the reference manual).

• usage:
          Ltac tactic_name tactic_arguments := ...
        
• every time you want to compute something (like applying another tactic to build a term), you need to use a let ... := ... in ...
• if you want to return a term, you need to flag it with constr:(...)
• variables in pattern-matching must be preceeded with a "?"
• you can filter on the goal and on hypotheses: for example
          match goal with
            | [ H1: ~?X, H2: ~?Y |- ~?X /\ ~?Y ] => ...
            | [ |- _ ] => idtac
          end.
        

5) Prove associativity and commutativity of addition and mutiplication, distributivity by using your tactic. 6) Show that C is a metric space.

7) Show that C is a complete metric space. You might find inspiration in the file http://coq.inria.fr/stdlib/Coq.Reals.Rcomplete.html .