TP04: Automatic tactics & integer division

Automatic tactics

trivial - Solves simple goals, a combination of simpl, assumption and reflexivity and uses the hint database.
easy - Slightly more powerful, can perform introductions and destruct conjunctions.
Print Ltac easy.

It is mostly useful in the following notation that ensures that the goal is solved (the notation is already defined in Coq).
Tactic Notation "now" tactic(t) := t; easy.

Lemma and_comm : forall P Q, P /\ Q -> Q /\ P.
Proof. intros. now split. Qed.

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

auto with hintdb - Automatically applies tactics and lemmas from the database hintdb given as argument.
Require Import Arith.
Print HintDb arith.

Lemma test_auto_arith : forall m n, m <= n -> S m <= S n.
auto. auto with arith.

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.
Require Import Omega.

Lemma test2_auto_arith :
  forall m n, m - n <= m.
auto. auto with arith. omega.

tauto - Solves goals in intuitionistic propositional calculus.
Lemma test1_tauto : forall P Q, P /\ Q -> P \/ Q.
Proof. intros. tauto. Qed.

Lemma test2_tauto : forall P Q, (P -> ~~Q) -> ~~(P -> Q).
Proof. intros. tauto. Qed.

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 *.
Lemma test_intuition :
  forall n p q : nat, n <= p \/ n <= q -> n <= p \/ n <= S q.
auto with arith. try tauto. intuition auto with arith.

Dealing with algebraic structures

ring - Solves equalities over a ring or a semi-ring.
Require Import ZArith.
Open Local Scope Z_scope.

Theorem ring_example1 : forall x y : Z, (x+y) * (x+y) = x*x + 2*x*y + y*y.
Proof. intros; ring. Qed.

Definition square (z : Z) := z*z.
Theorem ring_example2 :
  forall x y : Z, square (x+y) = square x + 2*x*y + square y.
try ring. unfold square. ring.

Theorem ring_example3 :
  forall x y : nat, ((x+y)*(x+y) = x*x + 2*x*y + y*y)%nat.
Proof. intros; ring. Qed.

Require Import Reals.
Open Scope R_scope.

Theorem ring_example4 : forall x y : R, (x+y)*(x+y) = x*x + 2*x*y + y*y.
Proof. intros x y; ring. Qed.

field - Solves equalities over a field.
Theorem field_example : forall x y : R, y <> 0 -> (x+y)/y = 1+(x/y).
Proof. intros. field. easy. Qed.

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

Theorem fourier_example1 : forall x y : R, x - y > 1 -> x-2*y < 0 -> x > 1.
Proof. intros. fourier. Qed.

Close Scope R_scope.
Close Scope Z_scope.

Integer division

We import the library about natural numbers.
Require Import Arith.

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)
Recall that left and right are the constructors of sumbool, the computational equivalent of disjunction.
Print sumbool.
Check le_gt_dec.

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 <.
Check lt_wf.

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.
Locate "{ _ | _ }".
Print sig.
Example pos_elt : {x | 3 < x < 5}.
Proof. exists 4. auto with arith. Qed.

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 < ndiv_type m) → div_type n
6) Define such a function (in tactic mode). Wrap up everything to define division.
Check lt_minus.
Check le_plus_minus.

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.
Require Import Program.

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)?
Lemma lt_0_3 : 0 < 3.
Proof. omega. Qed.

Complex numbers

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

Complex numbers are pairs of real numbers.
Definition C := (R * R)%type.
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.
Delimit Scope C_scope with C.
To be able to use (...)%C to locally open C_scope.

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

Open Scope C_scope.
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:(...)
  • you can use match type of t to handle types
  • 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
5) Prove associativity and commutativity of addition and mutiplication, distributivity by using your tactic.
6) Show that C is a metric space.
Print Metric_Space.
SearchAbout sqrt.

7) Show that C is a complete metric space.
You might find inspiration in the file .

This page has been generated by coqdoc