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