(** * 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]. **)
(** [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 div_aux m n k :=
match n, k with
| 0, _ => (0, 0)
| S _, 0 => (0, 0)
| S _, S k' => if le_gt_dec n m then let (q, r) := div_aux (m - n) n k' in (S q, r) else (0, m)
end.
Definition div1 m n := div_aux m n m.
Eval compute in (div1 7 2).
Eval compute in (div1 2 7).
(** In fact, Coq is smarter than I thought because it accepts the
following less ad hoc definition: **)
Fixpoint div1' m n {struct m} :=
match m, n with
| _, 0 => (0, 0)
| 0, S _ => (0, 0)
| S m', S n' => match le_gt_dec n m with
| right _ => (0, m)
| left _ => let (q,r) := div1' (m' - n') n in (S q, r)
end
end.
(** The down side of this solution is that proving its correctness is much
more difficult because there is no real recursion on one argument. **)
(** 3) Prove the correctness of your function. **)
Lemma div_aux_correct1 : forall k m n, m <= k -> 0 < n -> m = fst (div_aux m n k) * n + snd (div_aux m n k).
Proof.
induction k; intros m n Hm Hn.
inversion_clear Hm. now destruct n; compute.
destruct n. now elim (lt_irrefl _ Hn). clear Hn.
destruct m. simpl. reflexivity.
Opaque le_gt_dec. simpl. destruct (le_gt_dec (S n) (S m)); simpl; try reflexivity.
replace (fst (let (q, r) := div_aux (m - n) (S n) k in (S q, r))) with (S (fst (div_aux (m - n) (S n) k)))
by now destruct (div_aux (m - n) (S n) k).
replace (snd (let (q, r) := div_aux (m - n) (S n) k in (S q, r))) with (snd (div_aux (m - n) (S n) k))
by now destruct (div_aux (m - n) (S n) k).
simpl. do 2 rewrite <- plus_Sn_m. rewrite <- plus_assoc. rewrite <- (IHk (m - n) (S n)).
simpl. f_equal. apply le_plus_minus. now apply le_S_n.
transitivity m. apply le_minus. now apply le_S_n.
apply lt_O_Sn.
Qed. Transparent le_gt_dec.
(** The command [Opaque NAME] prevents Coq from unfolding NAME during computation.
The command [Transparent NAME] undoes it. **)
Lemma div_aux_correct2 : forall k m n, m <= k -> 0 < n -> 0 <= snd (div_aux m n k) < n.
Proof.
induction k; intros m n Hm Hn.
destruct n; simpl. now elim (lt_irrefl _ Hn). now split.
destruct n. now elim (lt_irrefl _ Hn). clear Hn. destruct m.
simpl. now auto with arith.
Opaque le_gt_dec. simpl. destruct (le_gt_dec (S n) (S m)); simpl.
replace (snd (let (q, r) := div_aux (m - n) (S n) k in (S q, r))) with (snd (div_aux (m - n) (S n) k))
by now destruct (div_aux (m - n) (S n) k).
apply IHk. transitivity m. apply le_minus. now apply le_S_n. now auto with arith.
now auto with arith.
Qed. Transparent le_gt_dec.
Theorem div1_correct : forall m n, 0 < n -> m = fst (div1 m n) * n + snd (div1 m n) /\ 0 <= snd (div1 m n) < n.
Proof. intros m n. unfold div1. split. now apply div_aux_correct1. now apply div_aux_correct2. 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. **)
(** Two possibilities: either we return a pair with its properties or
we split it up into its components and have two interleaved sets. **)
Definition div_eqn1 m n qr := m = fst qr * n + snd qr /\ 0 <= snd qr < n.
Definition div_type1 m := forall n, 0 < n -> {qr | div_eqn1 m n qr}.
Definition div_eqn2 m n q r := m = q * n + r /\ 0 <= r < n.
Definition div_type2 m := forall n, 0 < n -> {q : nat & {r | div_eqn2 m n q r}}.
(** Of course, they are equivalent: **)
Lemma div_eqn1_eqn2 : forall m n, {qr | div_eqn1 m n qr} -> {q : nat & {r | div_eqn2 m n q r}}.
Proof. intros m n [qr Hqr]. exists (fst qr). exists (snd qr). exact Hqr. Qed.
Lemma div_eqn2_eqn1 : forall m n, {q : nat & {r | div_eqn2 m n q r}} -> {qr | div_eqn1 m n qr}.
Proof. intros m n [q [r Hqr]]. exists (q, r). exact Hqr. Qed.
(** 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.
Definition div_F :
forall x : nat, (forall y : nat, y < x -> div_type1 y) -> div_type1 x.
unfold div_type1 at 2.
intros m div_ref n Hn.
destruct (le_gt_dec n m) as [Hle | Hgt].
(* n ≤ m *)
destruct (div_ref (m - n) (lt_minus m n Hle Hn) n Hn) as [[q r] Hrec].
exists (S q, r). destruct Hrec as [Hq Hr]. split.
rewrite (le_plus_minus n m Hle). rewrite Hq. simpl. ring.
easy.
(* m < n *)
exists (0, m). split. simpl; ring. split; auto with arith.
Defined.
Definition div2 : forall n, div_type1 n := well_founded_induction lt_wf _ div_F.
(** ** 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 the Program library, define division. **)
Program Fixpoint div3 m {measure m} : div_type2 m := fun n Hn =>
match le_gt_dec n m with
| left Hle => match div3 (m - n) (lt_minus m n Hle Hn) n with
| existT q (exist r H) => existT _ (S q) (exist (div_eqn2 (m-n) n q) r _)
end
| right Hgt => existT _ 0 (exist (div_eqn2 m n 0) m _)
end.
Next Obligation.
unfold div_eqn2 in *. destruct H as [H ?]. rewrite (le_plus_minus n m Hle). rewrite H. split. ring. easy.
Defined.
Next Obligation.
unfold div_eqn2. auto with arith.
Defined.
(** 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).
(** For the next two, we need to make the computational definition transparent
by replacing [Qed] with [Defined] in [div_F] and [div3]. **)
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:(...)]
- 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 :=
match goal with
| [H : ?x = ?y |- _] =>
match type of x with
| C => rewrite Ceq_equiv in H; destruct H
| _ => fail
end;Cdec
| [x : C |- _] => destruct x; Cdec
| [|- ?x = ?y] => rewrite Ceq_equiv; split;
unfold Cadd,Cmul,Copp; simpl in *; field
end.
(** 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.
(** Some lemmas about reals **)
Lemma square_pos : forall x, 0 <= x * x.
Proof.
intro x. destruct (Rlt_le_dec x 0).
replace (x*x)%R with ((-x)*(-x))%R by ring. apply Rmult_le_pos; fourier.
now apply Rmult_le_pos.
Qed.
Lemma square_eq_0 : forall x, (x * x = 0 -> x = 0)%R.
Proof. intros x Hx. apply Rmult_integral in Hx. now destruct Hx. Qed.
Lemma square_le : forall x y, 0 <= x -> 0 <= y -> x*x <= y*y -> x <= y.
Proof.
intros x y Hx Hy Hle. setoid_rewrite <- sqrt_square at 1 2; try easy.
now apply sqrt_le_1; try apply square_pos.
Qed.
Lemma Rle_le_plus_eq_0 :
forall x y, (0 <= x -> 0 <= y -> x + y = 0 -> x = 0 /\ y = 0)%R.
Proof.
intros x y Hx Hy Heq. replace (x + y)%R with (x - (- y))%R in Heq by ring.
apply Rminus_diag_uniq in Heq. subst. replace 0%R with (- 0)%R in Hx by ring.
apply Ropp_le_cancel in Hx. assert (y = 0). now apply Rle_antisym. subst.
split; ring.
Qed.
(** Now the reals proofs **)
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.
Lemma Cdist_refl : forall x y : C, Cdist x y = 0 <-> x = y.
Proof.
intros x y. unfold Cdist. split; intro Heq.
- apply sqrt_eq_0 in Heq.
apply Rle_le_plus_eq_0 in Heq; try now apply square_pos.
destruct Heq as [Hreal Him].
apply square_eq_0,Rminus_diag_uniq in Hreal.
apply square_eq_0,Rminus_diag_uniq in Him.
rewrite Ceq_equiv. now split.
now apply Rplus_le_le_0_compat; apply square_pos.
- subst. simpl. rewrite <- sqrt_0. f_equal. now ring.
Qed.
Lemma Cdist_tri : forall x y z : C, Cdist x y <= Cdist x z + Cdist z y.
Proof. Admitted.
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 . **)