(** * 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 #<a href="http://coq.inria.fr/distrib/V8.4/refman/Reference-Manual028.html">
       page about the Program library</a>#. **)
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 . **)