(**************************************************************************)
(*       ___                                                              *)
(*      ||M||                                                             *)
(*      ||A||       A project by Andrea Asperti                           *)
(*      ||T||                                                             *)
(*      ||I||       Developers:                                           *)
(*      ||T||         The HELM team.                                      *)
(*      ||A||         http://helm.cs.unibo.it                             *)
(*      \   /                                                             *)
(*       \ /        This file is distributed under the terms of the       *)
(*        v         GNU General Public License Version 2                  *)
(*                                                                        *)
(**************************************************************************)

include "nat/plus.ma".
include "nat/orders.ma".
include "nat/compare.ma".

axiom R: Type.
axiom R0: R.
axiom R1: R.
axiom Rplus: R→R→R.
axiom Rmult: R→R→R.

notation "0" with precedence 89
for @{ 'zero }.
interpretation "Rzero" 'zero = (R0).
interpretation "Nzero" 'zero = (O).

notation "1" with precedence 89
for @{ 'one }.
interpretation "Rone" 'one = (R1).
interpretation "None" 'one = (S O).

interpretation "Rplus" 'plus x y = (Rplus x y).

interpretation "Rmult" 'middot x y = (Rmult x y).

definition Fplus ≝
 λf,g:R→R.λx:R.f x + g x.
 
definition Fmult ≝
 λf,g:R→R.λx:R.f x · g x.

interpretation "Fplus" 'plus x y = (Fplus x y).
interpretation "Fmult" 'middot x y = (Fmult x y).

notation "2" with precedence 89
for @{ 'two }.
interpretation "Rtwo" 'two = (Rplus R1 R1).
interpretation "Ntwo" 'two = (S (S O)).

let rec Rpower (x:R) (n:nat) on n ≝
 match n with
  [ O ⇒ 1
  | S n ⇒ x · (Rpower x n)
  ].

interpretation "Rpower" 'exp x n = (Rpower x n).

let rec inj (n:nat) on n : R ≝
 match n with
  [ O ⇒ 0
  | S n ⇒
     match n with
      [ O ⇒ 1
      | S m ⇒ 1 + inj n
      ]
  ].

coercion inj.

axiom Rplus_Rzero_x: ∀x:R.0+x=x.
axiom Rplus_comm: symmetric ? Rplus.
axiom Rplus_assoc: associative ? Rplus.
axiom Rmult_Rone_x: ∀x:R.1 · x=x.
axiom Rmult_Rzero_x: ∀x:R.0 · x=0.
axiom Rmult_assoc: associative ? Rmult.
axiom Rmult_comm: symmetric ? Rmult.
axiom Rmult_Rplus_distr: distributive ? Rmult Rplus.

alias symbol "middot" = "Rmult".
alias symbol "plus" = "natural plus".

definition monomio ≝
 λn.λx:R.x\sup n.

definition costante : nat → R → R ≝
 λa:nat.λx:R.inj a.

coercion costante with 1.

axiom f_eq_extensional:
 ∀f,g:R→R.(∀x:R.f x = g x) → f=g.

lemma Fmult_one_f: ∀f:R→R.1·f=f.
 intro;
 unfold Fmult;
 simplify;
 apply f_eq_extensional;
 intro;
 autobatch.
qed.

lemma Fmult_zero_f: ∀f:R→R.0·f=0.
 intro;
 unfold Fmult;
 simplify;
 apply f_eq_extensional;
 intro;
 autobatch.
qed.

lemma Fmult_commutative: symmetric ? Fmult.
 unfold;
 intros;
 unfold Fmult;
 apply f_eq_extensional;
 intros;
 autobatch.
qed.

lemma Fmult_associative: associative ? Fmult.
 unfold;
 intros;
 unfold Fmult;
 unfold Fmult;
 apply f_eq_extensional;
 intros;
 autobatch.
qed.

lemma Fmult_Fplus_distr: distributive ? Fmult Fplus.
 unfold;
 intros;
 unfold Fmult;
 unfold Fplus;
 apply f_eq_extensional;
 intros;
 simplify;
 autobatch.
qed.

lemma monomio_product:
 ∀n,m.monomio (n+m) = monomio n · monomio m.
 intros;
 unfold monomio;
 unfold Fmult;
 simplify;
 elim n;
  [ simplify;
    apply f_eq_extensional;
    intro;
    autobatch
  | simplify;
    apply f_eq_extensional;
    intro;
    cut (x\sup (n1+m) = x \sup n1 · x \sup m);
     [ rewrite > Hcut;
       autobatch
     | change in ⊢ (? ? % ?) with ((λx:R.x\sup(n1+m)) x);
       rewrite > H;
       reflexivity
     ]
  ].
qed.

lemma costante_sum:
 ∀n,m.costante n + costante m = costante (n+m).
 intros;
 unfold Fplus;
 unfold costante;
 apply f_eq_extensional;
 intros;
 elim n;
  [ simplify;
    autobatch
  | simplify;
    clear x;
    clear H;
    clear n;
    elim n1;
     [ simplify;
       elim m;
        [ simplify;
          autobatch
        | simplify;
          rewrite < H;
          autobatch
        ]
     | simplify;
       rewrite < H;
       clear H;
       elim n;
        [ simplify;
          autobatch
        | simplify;
          autobatch
        ]
     ]
   ].
qed.

axiom derivative: (R→R) → R → R.

notation "hvbox('D'[f])"
  non associative with precedence 90
for @{ 'derivative $f }.

interpretation "Rderivative" 'derivative f = (derivative f).

(*  FG: we definitely do not want 'x' as a keyward! 
 *  Any file that includes this one can not use 'x' as an identifier
 *)  
notation "hvbox('X' \sup n)"
  non associative with precedence 60
for @{ 'monomio $n }.

notation "hvbox('X')"
  non associative with precedence 60
for @{ 'monomio 1 }.

interpretation "Rmonomio" 'monomio n = (monomio n).

axiom derivative_x0: D[X \sup 0] = 0.
axiom derivative_x1: D[X] = 1.

axiom derivative_mult: ∀f,g:R→R. D[f·g] = D[f]·g + f·D[g].

alias symbol "middot" = "Fmult".

theorem derivative_power: ∀n:nat. D[X \sup n] = n·X \sup (pred n).
 assume n:nat.
 (*we proceed by induction on n to prove
 (D[X \sup n] = n · X \sup (pred n)).*)
 elim n 0.
 case O.
   the thesis becomes (D[X \sup 0] = 0·X \sup (pred 0)).
  done.
 case S (m:nat).
  by induction hypothesis we know
   (D[X \sup m] = m·X \sup (pred m)) (H).
  the thesis becomes
   (D[X \sup (1+m)] = (1+m) · X \sup m).
  we need to prove
   (m · (X \sup (1+ pred m)) = m · X \sup m) (Ppred).
   lapply depth=0 le_n;
   we proved (0 < m ∨ 0=m) (cases).
   we proceed by induction on cases
   to prove (m · (X \sup (1+ pred m)) = m · X \sup m).
    case left.
      suppose (0 < m) (m_pos).
      using (S_pred ? m_pos) we proved (m = 1 + pred m) (H1).
      by H1 done.
    case right.
      suppose (0=m) (m_zero). 
    by m_zero, Fmult_zero_f done.
  conclude
     (D[X \sup (1+m)])
   = (D[X · X \sup m]).
   = (D[X] · X \sup m + X · D[X \sup m]).
   = (X \sup m + X · (m · X \sup (pred m))). 
   lapply depth=0 Fmult_associative;
   lapply depth=0 Fmult_commutative;
   = (X \sup m + m · (X · X \sup (pred m))) by Fmult_associative, Fmult_commutative.
   = (X \sup m + m · (X \sup (1 + pred m))).
   = (X \sup m + m · X \sup m).
   = ((1+m) · X \sup m) by Fmult_one_f, Fmult_commutative, Fmult_Fplus_distr, costante_sum
  done.
qed.

(*
notation "hvbox(\frac 'd' ('d' ident i) break p)"
  right associative with precedence 90
for @{ 'derivative ${default
  @{\lambda ${ident i} : $ty. $p)}
  @{\lambda ${ident i} . $p}}}.

interpretation "Rderivative" 'derivative \eta.f = (derivative f).
*)

notation "hvbox(\frac 'd' ('d' 'X') break p)" with precedence 90
for @{ 'derivative $p}.

interpretation "Rderivative" 'derivative f = (derivative f).

theorem derivative_power': ∀n:nat. D[X \sup (1+n)] = (1+n) · X \sup n.
 assume n:nat.
 (*we proceed by induction on n to prove
 (D[X \sup (1+n)] = (1+n) · X \sup n).*) elim n 0.
 case O.
   the thesis becomes (D[X \sup 1] = 1 · X \sup 0).
  done.
 case S (m:nat).
  by induction hypothesis we know
   (D[X \sup (1+m)] = (1+m) · X \sup m) (H).
  the thesis becomes
   (D[X \sup (2+m)] = (2+m) · X \sup (1+m)).
  conclude
     (D[X \sup (2+m)])
   = (D[X · X \sup (1+m)]).
   = (D[X] · X \sup (1+m) + X · D[X \sup (1+m)]).
   = (X \sup (1+m) + X · (costante (1+m) · X \sup m)).
   = (X \sup (1+m) + costante (1+m) · X \sup (1+m)).
   = ((2+m) · X \sup (1+m)) timeout=30 by Fmult_one_f, Fmult_commutative,
       Fmult_Fplus_distr, assoc_plus, plus_n_SO, costante_sum
  done.
qed.