(** * 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 file.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. **)
Fixpoint divaux m n k {struct k} :=
match n, k with
| 0, _ | _, 0 => (0, 0)
| S _, S k' => if le_gt_dec n m then let (q,r) := divaux (m - n) n k' in (S q, r) else (0, m)
end.
Definition div1 m n := divaux m n m.
Eval compute in div1 7 2.
Eval compute in div1 2 7.
(** 3) Prove the correctness of your function. **)
Lemma divaux_bound : forall c, forall a b, 0 < b -> a <= c ->
let (q, r) := divaux a b c in r < b.
Proof.
intros c; induction c; intros a b nzb ac.
inversion ac.
destruct b; simpl. congruence. auto with arith.
simpl.
destruct b. congruence.
destruct (le_gt_dec (S b) a); auto.
specialize (IHc (a - S b) (S b) nzb).
remember (divaux (a - S b) (S b) c) as x.
destruct x.
apply IHc.
auto with *.
Qed.
Lemma divaux_correct : forall c, forall a b, 0 < b -> a <= c ->
fst (divaux a b c) * b + snd (divaux a b c) = a.
Proof.
intros c; induction c; intros a b nzb ac.
inversion ac.
destruct b; simpl. congruence. auto with arith.
simpl.
destruct b. inversion nzb.
destruct (le_gt_dec (S b) a); auto.
specialize (IHc (a - S b) (S b) nzb).
remember (divaux (a - S b) (S b) c) as x.
destruct x.
simpl in *.
auto with *.
Qed.
(* with the "let" another proof. *)
Lemma divaux_correct' : forall c, forall a b, 0 < b -> a <= c ->
let (q, r) := divaux a b c in q * b + r = a /\ r < b.
Proof.
intros c; induction c; intros a b nzb ac.
inversion ac.
destruct b; simpl; eauto.
simpl.
destruct b. inversion nzb.
destruct (le_gt_dec (S b) a); auto.
specialize (IHc (a - S b) (S b) nzb).
remember (divaux (a - S b) (S b) c) as x.
destruct x.
simpl in *.
auto with *.
Qed.
Theorem div1_correct : forall a b, 0 < b ->
let (q, r) := div1 a b in q * b + r = a /\ r < b.
Proof.
intros a b nzb; unfold div1.
pose proof divaux_correct a a b nzb.
pose proof divaux_bound a a b nzb.
remember (divaux a b a) as x; destruct x as (q, r).
simpl in *.
auto.
Qed.
(** ** 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.
(*
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. **)
Definition Copp (x : C) : C := (-fst x, -snd x).
Definition Cadd (x : C) (y : C) : C := (fst x + fst y, snd x + snd y).
Definition Cmul (x : C) (y : C) : C := (fst x * fst y - snd x * snd y, fst x * snd y + snd x * fst y).
(** 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.
Notation "x * y" := (Cmul 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. **)
Lemma Ceq_equiv : forall (x y : C), x = y <-> fst x = fst y /\ snd x = snd y.
Proof.
intros [x₁ x₂] [y₁ y₂].
split; intro Heq.
inversion Heq. now subst.
simpl in Heq. destruct Heq. now subst.
Qed.
(** 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.
]]
**)
Ltac Cdec :=
lazymatch goal with
| [ H : ?x = ?y |- _ ] => match type of x with C => rewrite Ceq_equiv in H; destruct H; Cdec | _ => fail end
| [ x : C |- _ ] => destruct x; simpl in *; Cdec
| [ |- ?x = ?y ] =>
apply Ceq_equiv; unfold Cadd,Cmul,Copp; simpl in *; split; subst;
field ||
pose proof Rplus_eq_reg_l;
pose proof Rplus_comm;
intuition eauto with *
end.
(*
Lemma Cdec_test : forall x y z : C, (1,1) + x = (1,1) + y -> x + z = z + y.
raté
*)
(** 5) Prove associativity and commutativity of addition and mutiplication,
distributivity by using your tactic. **)
Lemma Cadd_comm : forall x y : C, x + y = y + x.
Proof. intros. Cdec. Qed.
Lemma Cadd_assoc : forall x y z : C, (x + y) + z = x + (y + z).
Proof. intros. Cdec. Qed.
Lemma Cmul_comm : forall x y : C, x * y = y * x.
Proof. intros. Cdec. Qed.
Lemma Cmul_assoc : forall x y z : C, (x * y) * z = x * (y * z).
Proof. intros. Cdec. Qed.
Lemma Cmul_add_distr : forall x y z : C, x * (y + z) = x * y + x * z.
Proof. intros. Cdec. Qed.
(** 6) Show that C is a metric space. **)
Print Metric_Space.
SearchAbout sqrt.
Definition Cdist (x y : C) : R :=
sqrt ((fst x - fst y) * (fst x - fst y) + (snd x - snd y) * (snd x - snd y)).
Lemma Cdist_pos : forall x y : C, Cdist x y >= 0.
Proof.
intros x y.
apply Rle_ge.
apply sqrt_pos.
Qed.
Lemma Cdist_sym : forall x y, Cdist x y = Cdist y x.
Proof.
intros x y.
unfold Cdist.
f_equal.
ring.
Qed.
(** Lemmas about real numbers *)
Lemma sqr_pos : forall x : R, 0 <= x * x.
Proof.
pose proof Rmult_le_pos.
intros x; destruct Rle_lt_dec with 0 x; auto.
replace (x * x)%R with (-x * -x)%R by ring.
apply H; fourier.
Qed.
Lemma sqrdiff_zero : forall x y, ((x - y) * (x - y) = 0 -> x = y)%R.
Proof.
intros x y E.
apply Rminus_diag_uniq.
apply Rmult_integral in E.
intuition.
Qed.
Lemma Cdist_refl : forall x y : C, Cdist x y = 0 <-> x = y.
Proof.
pose proof sqr_pos.
pose proof Rplus_le_le_0_compat.
intros [a b] [c d]; unfold Cdist; split; intros E; simpl in *.
apply sqrt_eq_0, Rplus_eq_R0 in E; auto with *.
f_equal; apply sqrdiff_zero; intuition.
injection E; intros; subst.
unfold Rminus; repeat rewrite Rplus_opp_r.
rewrite Rmult_0_l, Rplus_0_l, sqrt_0; auto.
Qed.
Lemma Cdist_tri : forall x y z : C, Cdist x y <= Cdist x z + Cdist z y.
Proof.
assert (P: forall x y, 0 <= x * x + y * y).
intros; apply Rplus_le_le_0_compat; apply sqr_pos.
intros [a b] [c d] [e f].
apply Rsqr_incr_0_var; [ | (apply Rplus_le_le_0_compat; apply sqrt_pos) ].
rewrite Rsqr_plus; unfold Cdist; simpl.
repeat rewrite Rsqr_sqrt; auto.
rewrite Rmult_assoc.
assert (G: forall x y a b, (a <= b -> x = y + 2 * a -> x <= y + 2 * b)%R).
intros; fourier.
eapply G.
(* we use the magic inequality sqrt_cauchy ... *)
pose proof sqrt_cauchy as U; unfold Rsqr in U.
apply U.
ring.
Qed.
Definition C_met : Metric_Space :=
Build_Metric_Space C Cdist Cdist_pos Cdist_sym Cdist_refl Cdist_tri.
(** 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 . **)