(** * TP04: Automatic tactics & integer division *)
(* To build an html version of this exercise sheet, use the command
"coqdoc -utf8 --no-lib-name --no-index --lib-subtitles TP04.v" *)
(***************************)
(** * 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.
intros.
auto. (* -> does not work *)
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]. **)
Require Import Omega.
Lemma test2_auto_arith :
forall m n, m - n <= m.
intros.
auto. (* -> does not work *)
auto with arith. (* -> does not work *)
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.
(** [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. (* -> does not work *)
try tauto. (* -> fails *)
intuition auto with arith.
Qed.
(** ** 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.
Proof.
intros.
try ring. (* -> fails *)
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.
(** [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)
end.
]]
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. **)
Check 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 < n → div_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.
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. **)
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]. **)
Notation "- x" := (Copp x) : C_scope.
Notation "x + y" := (Cadd x y) : 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
end.
]]
**)
(** 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
http://coq.inria.fr/stdlib/Coq.Reals.Rcomplete.html . **)