Require Import Arith.

Lemma use_hyp_in_auto :
  forall P : nat -> Prop,
  (forall x y, P x -> P y -> P (x + y)) ->
  forall a b c d, P a -> P b -> P c -> P d ->
  P (a + ((b + c)) + d).
Proof.
auto.
Qed.

Lemma use_hyp_in_firstorder :
  forall P : nat -> Prop,
  (forall x y, P x -> P y -> P (x + y)) ->
  forall a b c, P a /\ P b /\ P c ->
  P (a + (b + c)).
Proof.
auto 30.
firstorder.
Qed.

(* Hint can also use existing theorems, which must have been
  added into a database. *)
#[export]
Hint Resolve Nat.Even_Even_add : ev_base.

#[export]
Hint Resolve Nat.Even_mul_r : ev_base.

#[export]
Hint Resolve Nat.Even_mul_l : ev_base.

Lemma Even2 : Nat.Even 2. Proof. exists 1. reflexivity. Qed.

#[export]
Hint Resolve Even2 : ev_base.

Lemma use_thms_in_auto n m :
  Nat.Even ((((2 * n + m * 2) + (2 * n + m * 2)) + 
            ((2 * n + m * 2) + (2 * n + m * 2))) +
            (((2 * n + m * 2) + (2 * n + m * 2)) + 
            ((2 * n + m * 2) + (2 * n + 2)))).
Proof.
auto 6 with ev_base.
Qed.

Lemma use_hyp_in_auto2 :
  forall P : nat -> Prop,
  (forall x y, P x -> P y -> P (x + y)) ->
  forall a b c, P a -> P b -> P c ->
  P ((a + ((a + (b + c)) + b + c)) + a + (b + c)).
Proof.
Fail now auto.
auto 10.
Qed.

Lemma big_cmp : 3 <= 100 /\ 
                97 <= 100 /\ 
                20 <= 100.
Proof.
split.
  now auto with arith.
split.
  info_auto with arith.
Fail now auto with arith.
(* It did not solve this one. *)
Show Proof.
Check Nat.le_add_r.
match goal with
  | |- ?x <= ?y => 
    apply (Nat.le_add_r x (y - x))
end.
Qed.

#[local]
Hint Extern 0 (_ <= _) =>
  (match goal with | |- ?x <= ?y => 
        apply (Nat.le_add_r x (y - x)) end) : arith.

Lemma try_hint_extern : 25 <= 75.
Proof.
info_auto with arith.
Qed.

Require Import ZArith.
Open Scope Z_scope.

Lemma quartic_add a b :
  (a + b) ^ 4 =
  a ^ 4 + 4 * a * b ^ 3 + 6 * a ^ 2 * b ^ 2 +
  4 * a ^ 3 * b + b ^ 4.
Proof.
ring.
Qed.

Lemma quartic_sub a b :
  (a - b) ^ 4 =
  a ^ 4 - 4 * a * b ^ 3 + 6 * a ^ 2 * b ^ 2 -
  4 * a ^ 3 * b + b ^ 4.
Proof.
ring.
Qed.

Close Scope Z_scope.

Lemma quartic_add_nat (a b : nat) :
  (a + b) ^ 4 =
  a ^ 4 + 4 * a * b ^ 3 + 6 * a ^ 2 * b ^ 2 + 4 * a ^ 3 * b + b ^ 4.
Proof.
Fail ring.
cbv [Nat.pow].
ring.
Qed.

Lemma quartic_sub_nat (a b : nat) :
  (a - b) ^ 4 =
  a ^ 4 - 4 * a * b ^ 3 + 6 * a ^ 2 * b ^ 2 - 4 * a ^ 3 * b + b ^ 4.
Proof.
Fail ring.
cbv [Nat.pow].
Fail ring.
(* The statement is not true, no wonder it can't be proved. *)
assert (~(forall a b : nat,
             (a - b) ^ 4 =
              a ^ 4 - 4 * a * b ^ 3 + 6 * a ^ 2 * b ^ 2
              - 4 * a ^ 3 * b + b ^ 4)).
  intros abs.
  assert (abs' : 0 = 1).
    exact (abs 0 1).
  (* this is due to the irregular behavior of natural number subtraction. *)
  discriminate.
Abort.

Require Import Reals Lra.

Open Scope R_scope.

Lemma sum_step n : n * (n + 1) / 2 + (n + 1) = (n + 1) * (n + 2) / 2.
Proof.
field.
Qed.

Lemma gen_sum_step n f : f <> 0 ->
  n * (n + 1) / f + (n + 1) = 
  (n + 1) * (n + f) / f.
Proof.
intros fn0.
field.
auto.
Qed.

Lemma example_linear_arithmetic x y :
  (x * x) / 2 + 1 <= y ->
  y <= - 2 * (x * (x * 1)) + 1 ->
  y <= (x * x) + 10 ->
  (x * x) <= y.
Proof.
intros half_plane_1 half_plane_2 half_plane_3.
lra.
Qed.

Require Import Reals Lra.
From Interval Require Import Tactic.

Open Scope R_scope.

Lemma example_with_PI x : PI <= x -> x < 4 * x.
Proof.
intros xgepi.
Fail lra.
interval_intro PI.
lra.
Qed.

Lemma approx_pi : 3.14 <= PI <= 3.15.
Proof.
interval.
Qed.

Require Import Reals Lra.
From Coquelicot Require Import Coquelicot.

Open Scope R_scope.

Lemma is_derive_test a y :
  0 < a ->
  Derive (fun x => 1 / sqrt (a + x ^ 2)) y =
  - y / ((a + y ^ 2) * sqrt (a + y ^ 2)).
Proof.
intros a_positive.
apply is_derive_unique.
(* Looking ahead at the conditions produced by 
  auto_derive, we will need to guarantee that
  the following formula is positive.  We do it
  once and for all so that later uses of nra use
  it. *)
assert (tmp : 0 < sqrt (a + y * (y * 1))).
  apply sqrt_lt_R0; nra.
auto_derive.
  split.
    nra.
  split.
    nra.
  easy.
rewrite sqrt_def;[ | nra].
simpl; field; nra.
Qed.

From Interval Require Import Plot.

Definition p1 := ltac:(plot (fun x => sin(1/x)) 0.01 4).

Plot p1.

Plot ltac:(plot (fun x => sqrt (1 - x^2) * sin (x * 200)) (-1) 1
  with (i_degree 3, i_size 500 1500)).