(** * 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 . **)