# tp4

# Automatic tactics

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.

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.

intros.

auto. auto with arith.

Qed.

Print HintDb arith.

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

intros.

auto. auto with arith.

Qed.

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.

Hint Resolve lemma_name : hintdb.

Require Import Omega.

Lemma test2_auto_arith :

forall m n, m - n <= m.

intros.

auto. auto with arith. omega.

Qed.

Lemma test2_auto_arith :

forall m n, m - n <= m.

intros.

auto. auto with arith. omega.

Qed.

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.

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.

Proof.

intros.

auto with arith. try tauto. intuition auto with arith.

Qed.

forall n p q : nat, n <= p \/ n <= q -> n <= p \/ n <= S q.

Proof.

intros.

auto with arith. try tauto. intuition auto with arith.

Qed.

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.

Proof.

intros.

try ring. unfold square. ring.

Qed.

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.

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.

Proof.

intros.

try ring. unfold square. ring.

Qed.

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.

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.

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.

## Structural induction

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

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.

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.
To go beyond structural induction, we can use well-founded induction.

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

Locate "{ _ | _ }".

Print sig.

Example pos_elt : {x | 3 < x < 5}.

Proof. exists 4. auto with arith. Qed.

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

∀n, (∀m, m < n → div_type m) → div_type n

## 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

Open Scope R_scope.

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.

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
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).
5) Prove associativity and commutativity of addition and mutiplication,
distributivity by using your tactic.
6) Show that C is a metric space.

Arguments f : x%s [x%s ...]

*name*of the scope and not its*key*(e.g. Z_scope and not Z).- 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

end.

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 .

This page has been generated by coqdoc