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

(** 3) Prove the correctness of your function. **)


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

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

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

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

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

(** 5) Prove associativity and commutativity of addition and mutiplication,
       distributivity by using your tactic. **)

(** 6) Show that C is a metric space. **)
Print Metric_Space.
SearchAbout sqrt.

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