(* Warning: the last lines of this file are unsuitable for use in JsCoq,
  which does not provide Coquelicot or Interval *)
Require Import ZArith Lia.

Open Scope Z_scope.

Fail Fixpoint Zfact (x : Z) :=
  if x <=? 0 then 1 else x * Zfact (x - 1).

Fixpoint fact_fuel (x : Z) (fuel : nat) :=
match fuel with
| 0%nat => 0
| S p => if x <=? 0 then 1 else x * fact_fuel (x - 1) p
end.

Definition Zfact (x : Z) := fact_fuel x (S (Z.to_nat x)).

Compute Zfact 3.

Lemma fact_fuel_correct n x :
  0 <= x < Z.of_nat n ->
  (fact_fuel x n) = Z.of_nat (fact (Z.to_nat x)).
Proof.
revert x.
induction n as [ | p Ih].
  intros x xint; lia.
intros x xint.
simpl.
rewrite Z.leb_compare.
destruct (x ?= 0) eqn: test.
    apply Z.compare_eq in test; rewrite test.
    simpl.
    easy.
  rewrite Z.compare_lt_iff in test; lia.
rewrite Z.compare_gt_iff in test.
assert (st : 0 <= x - 1) by lia.
assert (stepx : Z.to_nat x = S (Z.to_nat (x - 1))).
  apply Z2Nat.inj_succ in st.
  rewrite <- st, <- Z.add_1_r; apply f_equal; lia.
assert (fuel_cnd : (Z.to_nat (x - 1) < p)%nat) by lia.
rewrite stepx; cbv [fact]; fold fact; rewrite <- stepx.
rewrite Nat2Z.inj_mul.
rewrite Z2Nat.id;[ | lia].
apply f_equal.
apply Ih; lia.
Qed.

Lemma Zfact_correct x : 0 <= x -> Zfact x = Z.of_nat (fact (Z.to_nat x)).
Proof.
intros xge0; unfold Zfact; apply fact_fuel_correct.
lia.
Qed.

Compute Zfact 25.

Require Program.

From Equations Require Import Equations.
Require Import Wellfounded.

#[local]
Instance zltwf x : 
   WellFounded (fun n m => x <= n < m) := (Z.lt_wf x).

Equations Zfact'(x : Z) : Z by wf x (fun n m => 0 <= n < m) :=
  Zfact' x with (Z_le_dec x 0) := {
  | left _ => 1
  | right xnle0 => x * Zfact' (x - 1)
  }.
Next Obligation.
lia.
Qed.

Definition inspect {A} (a : A) : {b | a = b} :=
  exist _ a eq_refl.

Notation "x 'eqn:' p" := (exist _ x p) (only parsing, at level 20).


Equations Zfact2 (x : Z) : Z by wf x (fun n m => 0 <= n < m) :=
  Zfact2 x with inspect (x <=? 0) := {
  | true eqn: eq1 => 1
  | false eqn: eq1 => x * Zfact2 (x - 1)
  }.
Next Obligation.
lia.
Qed.

Lemma Zfact'3 : Zfact' 3 = 6.
Proof.
repeat (rewrite Zfact'_equation_1; simpl).
reflexivity.
Qed.

Check (Zfact'_equation_1
     : forall x : Z, Zfact' x =
       Zfact'_unfold_clause_1 x (Z_le_dec x 0)).

Fact check2 : Zfact'_unfold_clause_1 =
fun (x : Z) (refine : {x <= 0} + {~ x <= 0}) =>
if refine then 1 else x * Zfact' (x - 1).
Proof. reflexivity.  Qed.

Lemma Zfact'_main (x : Z) :
  Zfact' x = if x <=? 0 then 1 else x * Zfact' (x - 1).
Proof.
rewrite Zfact'_equation_1; simpl.
case (Z_le_dec x 0); intros test; simpl.
  destruct (Z.leb_spec x 0); lia.
destruct (Z.leb_spec x 0); lia.
Qed.

Lemma Zfact2_main (x : Z) :
  Zfact2 x = if x <=? 0 then 1 else x * Zfact2 (x - 1).
Proof.
rewrite Zfact2_equation_1; simpl.
destruct (x <=? 0); auto.
Qed.

Extraction Zfact2.
Extraction inspect.
Extraction Inline inspect.
Extraction Zfact'.
Extract Inductive bool => bool [true false].
Extraction Zfact'.

(*************************************************************************)

Require Import Reals Lra.

Search cos.
Print Assumptions derivable_cos.
Print cos.
Check exist_cos.
Print cos_in.
Print cos_n.
Print cos_term.
Print infinite_sum.

Print PI.
Print PI2.
Check PI_2_aux.

Open Scope R_scope.

Compute PI.

Print PI.

Check PI_2_aux.

Lemma comp_ex1 a b : 0 < a -> 3 * a < 4 * b -> 3 * a < 5 * b.
Proof.
lra.
Qed.

From Coquelicot Require Import Coquelicot.

Lemma RInt_x_1_2 : RInt (fun x => x) 1 2 = 3 / 2.
Proof.
assert (der_cond:  forall x,
  Rmin 1 2 <= x <= Rmax 1 2 -> is_derive (fun x0 : R => x0 ^ 2 / 2) x x).
  intros x _.
  auto_derive.
    easy.
  now field.
assert (cont_cond :
  forall x, Rmin 1 2 <= x <= Rmax 1 2 -> continuous (fun x => x) x).
  intros x _.
  now apply continuous_id.
assert (tmp := is_RInt_derive (fun x => x ^ 2 / 2) (fun x => x) 1 2
           der_cond cont_cond).
apply is_RInt_unique in tmp.
rewrite tmp.
unfold minus, plus, opp; simpl; field.
Qed.

From Interval Require Import Tactic.

Lemma RInt_x_1_2' : RInt (fun x => x) 1 2 = 3 / 2.
Proof.
integral_intro (RInt (fun x => x) 1 2) with (i_prec 3) as val.
lra.
Qed.

Lemma RInt_cos_0_PI_approx : -1 /256 < RInt cos 0 PI < 1/256.
Proof.
integral_intro (RInt cos 0 PI) with (i_prec 200, i_decimal).
lra.
Qed.

Lemma RInt_cos_0_PI : RInt cos 0 PI = 0.
Proof.
assert (der_cond:  forall x,
  Rmin 0 PI <= x <= Rmax 0 PI -> is_derive sin x (cos x)).
  intros x _.
  auto_derive.
    easy.
  now field.
assert (cont_cond :
  forall x, Rmin 0 PI <= x <= Rmax 0 PI -> continuous cos x).
  intros x _.
  now apply continuous_cos.
assert (tmp := is_RInt_derive _ _ 0 PI der_cond cont_cond).
apply is_RInt_unique in tmp.
rewrite tmp.
unfold minus, plus, opp; simpl.
rewrite sin_0, sin_PI.
lra.
Qed.

Close Scope R_scope.
Close Scope Z_scope.