fix compatibility with 9.2; still compatible with 8.17

Author: jmadiot

Arith/Nk_ind.v

@@ -21,6 +21,7 @@ USA.
 
 Require Import PeanoNat.
 Require Import Compare.
+Require Import Lia.
 Open Scope nat_scope.
 
 (* begin hide *)
@@ -141,11 +142,7 @@ reflexivity.
 intro.
 unfold kth_S. fold kth_S.
 rewrite IHk.
-assert (n + S k + 1=S k + n +1).
-auto with arith.
-rewrite H. clear H.
-simpl.
-auto with arith.
+lia.
 Qed.
 
 (** introduction of [next_P_k] *)

Complex/CFsequence_facts.v

@@ -418,8 +418,8 @@ Proof.
   replace (sum_f_R0 An N + sum_f_R0 (fun l:nat => An (S N + l)%nat) n)%R with
   (sum_f_R0 An (S (N + n)))%R.
   apply HN' ; intuition lia.
-  assert (N_pos : (0 <= N)%nat) by intuition.
-  assert (N_ub : (N < S (N + n))%nat) by intuition.
+  assert (N_pos : (0 <= N)%nat) by auto with arith.
+  assert (N_ub : (N < S (N + n))%nat) by auto with arith.
   intros; assert (H := sigma_split An N_pos N_ub) ; unfold sigma in H.
   do 2 rewrite Nat.sub_0_r in H.
   replace (sum_f_R0 An (S (N + n))) with
@@ -441,8 +441,8 @@ Proof.
       replace ((CFpartial_sum (fun n0 : nat => fn n0 x) N + sum_f_C0 (fun l:nat => fn (S N + l)%nat x) n))
       with (CFpartial_sum (fun n0 : nat => fn n0 x) (S N + n)%nat).
   apply HN' ; intuition lia.
-  assert (N_pos : (0 <= N)%nat) by intuition.
-  assert (N_ub : (N < S (N + n))%nat) by intuition.
+  assert (N_pos : (0 <= N)%nat) by auto with arith.
+  assert (N_ub : (N < S (N + n))%nat) by auto with arith.
   intros; assert (H := Csigma_split (fun n => fn n x) O (S (N + n)) N N_pos N_ub) ; unfold Csigma in H.
   do 2 rewrite Nat.sub_0_r in H.
   replace (CFpartial_sum (fun n0 : nat => fn n0 x) (S N + n)) with
@@ -464,8 +464,8 @@ Proof.
   replace (sum_f_R0 An N + sum_f_R0 (fun l:nat => An (S N + l)%nat) n)%R with
   (sum_f_R0 An (S (N + n)))%R.
   apply HN' ; intuition lia.
-  assert (N_pos : (0 <= N)%nat) by intuition.
-  assert (N_ub : (N < S (N + n))%nat) by intuition.
+  assert (N_pos : (0 <= N)%nat) by auto with arith.
+  assert (N_ub : (N < S (N + n))%nat) by auto with arith.
   intros; assert (H := sigma_split An N_pos N_ub) ; unfold sigma in H.
   do 2 rewrite Nat.sub_0_r in H.
   replace (sum_f_R0 An (S (N + n))) with
@@ -487,8 +487,8 @@ Proof.
       replace ((CFpartial_sum (fun n0 : nat => fn n0 x) N + sum_f_C0 (fun l:nat => fn (S N + l)%nat x) n))
       with (CFpartial_sum (fun n0 : nat => fn n0 x) (S N + n)%nat).
   apply HN' ; intuition lia.
-  assert (N_pos : (0 <= N)%nat) by intuition.
-  assert (N_ub : (N < S (N + n))%nat) by intuition.
+  assert (N_pos : (0 <= N)%nat) by auto with arith.
+  assert (N_ub : (N < S (N + n))%nat) by auto with arith.
   intros; assert (H := Csigma_split (fun n => fn n x) O (S (N + n)) N N_pos N_ub) ; unfold Csigma in H.
   do 2 rewrite Nat.sub_0_r in H.
   replace (CFpartial_sum (fun n0 : nat => fn n0 x) (S N + n)) with

Complex/Canalysis_deriv.v

@@ -178,7 +178,7 @@ intros f x Hf_deriv eps eps_pos ; destruct Hf_deriv as (l, Hl).
   destruct (Hl (eps / 2)%R eps_2_pos) as ([alpha alpha_pos], Halpha) ;
   exists (Rmin (1/2) alpha) ; split ; [apply Rmin_pos ; lra|] ;
   intros x' [_ x'_bd] ; simpl ; simpl in Halpha ; unfold C_dist in *.
-  pose (h := x' - x) ; replace x' with (x + h) by (unfold h ; intuition).
+  pose (h := x' - x) ; replace x' with (x + h) by (unfold h; auto with complex).
    case (Ceq_or_neq_C0 h) ; intro Hh_0.
    rewrite Hh_0, Cadd_0_r, Cminus_diag_eq ; [| reflexivity] ;
    rewrite Cnorm_C0 ; assumption.
@@ -195,7 +195,7 @@ intros f x Hf_deriv eps eps_pos ; destruct Hf_deriv as (l, Hl).
    apply Rlt_trans with ((Rmin (1/2) alpha) * eps)%R.
    apply Rmult_lt_compat_r ; assumption.
    apply Rle_lt_trans with (eps / 2)%R.
-   unfold Rdiv ; rewrite Rmult_comm ; apply Rmult_le_compat_l ; intuition ;
+   unfold Rdiv ; rewrite Rmult_comm ; apply Rmult_le_compat_l ; auto with real;
    apply Rle_trans with (1 * /2)%R ; [apply Rmin_l | right ; field].
    lra.
    assert (eps_2_pos : eps / 2 > 0) by lra ; 
@@ -209,7 +209,7 @@ intros f x Hf_deriv eps eps_pos ; destruct Hf_deriv as (l, Hl).
   apply Rgt_not_eq ; apply Cnorm_pos_lt ; assumption.
   apply Rmin_pos ; lra.
  intros x' [_ x'_bd] ; simpl ; unfold C_dist.
-  pose (h := x' - x) ; replace x' with (x+h) by (unfold h ; intuition) ;
+  pose (h := x' - x) ; replace x' with (x+h) by (unfold h ; intuition auto with complex) ;
   case (Ceq_or_neq_C0 h) ; intro Hh_0.
   rewrite Hh_0, Cadd_0_r, Cminus_diag_eq ; [| reflexivity] ;
   rewrite Cnorm_C0 ; assumption.

Complex/Cexp.v

@@ -66,7 +66,7 @@ intro n ; unfold exp_seq, An_deriv, Cseq_shift, Cseq_mult.
  replace (fact (S n))%nat with ((S n) * fact n)%nat by reflexivity.
  rewrite mult_INC, Cinv_mult_distr, <- Cmult_assoc, Cinv_r, Cmult_1_l ;
  [reflexivity | | |] ; replace C0 with (INC O) by reflexivity ; apply not_INC ;
- try apply fact_neq_0 ; intuition.
+ try apply fact_neq_0 ; intuition auto with *.
 Qed.
 
 (** * This power serie has a radius of convergence that is infinite *)
@@ -90,11 +90,11 @@ assert (t : (1 > 0)%nat) by constructor ;
  apply Rle_trans with (R_dist ((/ Rseq_shift (Rseq_poly 1))%Rseq (N + n)%nat) 0).
  right ; unfold R_dist, Rseq_shift, Rseq_poly, pow ; apply Rabs_eq_compat ;
  rewrite Rminus_0_r, <- (Rmult_1_r (INR (S (N + n)))) ; reflexivity.
- left ; apply HN ; intuition.
- apply not_0_INR ; intuition.
+ left ; apply HN ; intuition auto with *.
+ apply not_0_INR ; intuition auto with *.
 
 unfold M ; rewrite Rinv_involutive ; [| apply Rgt_not_eq ; apply Rplus_le_lt_0_compat ;
- [apply Rabs_pos | apply Rlt_0_1]] ; intuition.
+ [apply Rabs_pos | apply Rlt_0_1]] ; intuition auto with *.
 Qed.
 
 Definition Cexp (z : C) := sum  _ exp_infinite_cv_radius z.
@@ -156,7 +156,7 @@ Lemma Cre_Cpow_2 : forall (a : R) (n : nat), Cre ((0 +i a) ^ (2 * n)) = ((-1) ^
 Proof.
 intros a n ; induction n.
  simpl ; ring.
- replace (2 * S n)%nat with (S (S (2 * n))) by intuition.
+ replace (2 * S n)%nat with (S (S (2 * n))) by intuition auto with *.
  do 2 rewrite Cpow_S, Cre_mul ; rewrite IHn.
  rewrite Cim_mul.
  replace (Cre (0 +i a)) with R0 by reflexivity.
@@ -167,7 +167,7 @@ Lemma Cim_Cpow_2 : forall (a : R) (n : nat), Cim ((0 +i a) ^ (2 * n)) = R0.
 Proof.
 intros a n ; induction n.
  simpl ; ring.
- replace (2 * S n)%nat with (S (S (2 * n))) by intuition.
+ replace (2 * S n)%nat with (S (S (2 * n))) by intuition auto with *.
  do 2 rewrite Cpow_S, Cim_mul ; rewrite IHn.
  rewrite Cre_mul.
  replace (Cre (0 +i a)) with R0 by reflexivity.
@@ -178,7 +178,7 @@ Lemma Cre_Cpow_S2 : forall (a : R) (p : nat), Cre ((0 +i  a) ^ S (2 * p)) = R0.
 Proof.
 intros a n ; induction n.
  simpl ; ring.
- replace (2 * S n)%nat with (S (S (2 * n))) by intuition.
+ replace (2 * S n)%nat with (S (S (2 * n))) by intuition auto with *.
  do 2 rewrite Cpow_S, Cre_mul ; rewrite IHn.
  rewrite Cim_mul.
  replace (Cre (0 +i a)) with R0 by reflexivity.
@@ -189,7 +189,7 @@ Lemma Cim_Cpow_S2 : forall (a : R) (n : nat), Cim ((0 +i a) ^ (S (2 * n))) = ((-
 Proof.
 intros a n ; induction n.
  simpl ; ring.
- replace (2 * S n)%nat with (S (S (2 * n))) by intuition.
+ replace (2 * S n)%nat with (S (S (2 * n))) by intuition auto with *.
  do 2 rewrite Cpow_S, Cim_mul ; rewrite IHn.
  rewrite Cre_mul.
  replace (Cre (0 +i a)) with R0 by reflexivity.
@@ -214,18 +214,18 @@ intros a ; rewrite <- Ceq ; split ; simpl ;
 
 clear ; induction p.
  simpl ; field.
- replace (2 * S p)%nat with (S (S (2 * p)))%nat by intuition.
+ replace (2 * S p)%nat with (S (S (2 * p)))%nat by intuition auto with *.
  do 2 rewrite sum_f_C0_simpl ; rewrite tech5 ; do 2 rewrite<- Cre_add_compat ;
  rewrite <- IHp, Rplus_assoc ; apply Rplus_eq_compat_l.
  replace ((-1) ^ S p / INR (fact (2 * S p)) * a² ^ S p)%R
  with (Cre (gt_pser exp_seq (0 +i  a) (S (S (2 * p))))).
  replace (Cre (gt_pser exp_seq (0 +i  a) (S (2 * p))))%R with R0.
  symmetry ; apply Rplus_0_l.
  unfold_gt ; unfold exp_seq ; rewrite Cre_mul.
- replace (S (S (2 * p))) with (2 * S p)%nat by intuition.
+ replace (S (S (2 * p))) with (2 * S p)%nat by intuition auto with *.
  rewrite Cim_inv_INC, Rmult_0_l, Cre_Cpow_S2 ; ring.
  unfold_gt ; unfold exp_seq ; rewrite Cre_mul.
- replace (S (S (2 * p))) with (2 * S p)%nat by intuition.
+ replace (S (S (2 * p))) with (2 * S p)%nat by intuition auto with *.
  rewrite Cre_Cpow_2, Cim_Cpow_2, INC_inv_Cre_INR.
  unfold Rsqr ; rewrite pow_mult, Rmult_0_r, Rminus_0_r.
  rewrite Rmult_comm ; unfold Rdiv ; do 2 rewrite Rmult_assoc ;
@@ -240,18 +240,18 @@ clear ; induction p.
 
 clear ; induction p.
  simpl ; field.
- replace (2 * S p)%nat with (S (S (2 * p)))%nat by intuition.
+ replace (2 * S p)%nat with (S (S (2 * p)))%nat by intuition auto with *.
  do 2 rewrite sum_f_C0_simpl ; rewrite tech5 ; do 2 rewrite<- Cre_add_compat ;
  rewrite <- IHp, Rplus_assoc ; apply Rplus_eq_compat_l.
  replace ((-1) ^ S p / INR (fact (2 * S p)) * a² ^ S p)%R
  with (Cre (gt_pser exp_seq (0 +i  a) (S (S (2 * p))))).
  replace (Cre (gt_pser exp_seq (0 +i  a) (S (S (S (2 * p))))))%R with R0.
  symmetry ; apply Rplus_0_r.
  unfold_gt ; unfold exp_seq ; rewrite Cre_mul.
- replace (S (S (2 * p))) with (2 * S p)%nat by intuition.
+ replace (S (S (2 * p))) with (2 * S p)%nat by intuition auto with *.
  rewrite Cim_inv_INC, Rmult_0_l, Cre_Cpow_S2 ; ring.
  unfold_gt ; unfold exp_seq ; rewrite Cre_mul.
- replace (S (S (2 * p))) with (2 * S p)%nat by intuition.
+ replace (S (S (2 * p))) with (2 * S p)%nat by intuition auto with *.
  rewrite Cre_Cpow_2, Cim_Cpow_2, INC_inv_Cre_INR.
  unfold Rsqr ; rewrite pow_mult, Rmult_0_r, Rminus_0_r.
  rewrite Rmult_comm ; unfold Rdiv ; do 2 rewrite Rmult_assoc ;
@@ -272,8 +272,8 @@ clear ; induction p.
  simpl ; field.
  rewrite sum_f_C0_simpl, <- Cim_add_compat, IHn, Rplus_0_l ;
  unfold gt_pser ; replace (0 +i 0) with C0 by reflexivity.
- unfold Cseq_mult ; rewrite C0_pow, Cmult_0_r ; simpl ; intuition.
- intuition.
+ unfold Cseq_mult ; rewrite C0_pow, Cmult_0_r ; simpl ; intuition auto with *.
+ intuition auto with *.
 
 pose (eps' := (eps / Rabs a)%R) ; assert (eps'_pos : 0 < eps').
  unfold eps', Rdiv ; apply Rlt_mult_inv_pos ; [| apply Rabs_pos_lt] ; assumption.
@@ -292,7 +292,7 @@ destruct (Hl' _ eps'_pos) as [N HN] ; exists (S (2 * N))%nat ;
   clear ; induction p.
   simpl ; field.
 
- replace (2 * S (S p))%nat with (S (S (2 * S p))) by intuition.
+ replace (2 * S (S p))%nat with (S (S (2 * S p))) by intuition auto with *.
  rewrite tech5 ; do 2 rewrite sum_f_C0_simpl, <- Cim_add_compat.
  rewrite IHp, Rplus_assoc ; apply Rplus_eq_compat_l.
  replace (Cim (gt_pser exp_seq (0 +i  a) (S (S (2 * S p)))))%R with R0.
@@ -302,7 +302,7 @@ destruct (Hl' _ eps'_pos) as [N HN] ; exists (S (2 * N))%nat ;
  unfold Rsqr.
  rewrite INC_inv_Cre_INR.
  replace (a ^ S (2 * S p))%R with (a * (a ^ 2) ^ (S p))%R.
- replace (2 * S p + 1)%nat with (S (2 * S p)) by intuition.
+ replace (2 * S p + 1)%nat with (S (2 * S p)) by intuition auto with *.
  rewrite (Rmult_comm (/ INR (fact (S (2 * S p)))) _) ; unfold Rdiv ;
  repeat rewrite Rmult_assoc ; apply Rmult_eq_compat_l.
  rewrite Rmult_comm, <- Rmult_assoc ; apply Rmult_eq_compat_r.
@@ -311,7 +311,7 @@ destruct (Hl' _ eps'_pos) as [N HN] ; exists (S (2 * N))%nat ;
  rewrite <- pow_mult ; simpl ; reflexivity.
  apply fact_neq_0.
 unfold_gt ; unfold exp_seq ; rewrite Cim_mul ;
-replace ( S (S (2 * S p))) with (2 * (S (S p)))%nat by intuition ;
+replace ( S (S (2 * S p))) with (2 * (S (S p)))%nat by (intuition auto with *) ;
 rewrite Cim_Cpow_2, INC_inv_Cim_INR.
 do 2 rewrite Rmult_0_r ; ring.
 apply fact_neq_0.
@@ -325,18 +325,18 @@ apply fact_neq_0.
   clear ; induction p.
   simpl ; field.
 
- replace (2 * (S p))%nat with (S (S (2 * p))) by intuition.
+ replace (2 * (S p))%nat with (S (S (2 * p))) by intuition auto with *.
  rewrite tech5 ; do 2 rewrite sum_f_C0_simpl, <- Cim_add_compat.
  rewrite IHp, Rplus_assoc ; apply Rplus_eq_compat_l.
  replace (Cim (gt_pser exp_seq (0 +i  a) (S (S (2 * p)))))%R with R0.
  unfold_gt ; unfold exp_seq.
- replace (S (S (S (2 * p)))) with (S (2 * (S p))) by intuition.
+ replace (S (S (S (2 * p)))) with (S (2 * (S p))) by intuition auto with *.
  rewrite Cim_mul, Cre_Cpow_S2, Cim_Cpow_S2, Rmult_0_l,
  Rplus_0_l, Rplus_0_r.
  unfold Rsqr.
  rewrite INC_inv_Cre_INR.
  replace (a ^ S (2 * S p))%R with (a * (a ^ 2) ^ (S p))%R.
- replace (2 * S p + 1)%nat with (S (2 * S p)) by intuition.
+ replace (2 * S p + 1)%nat with (S (2 * S p)) by intuition auto with *.
  rewrite (Rmult_comm (/ INR (fact (S (2 * S p)))) _) ; unfold Rdiv ;
  repeat rewrite Rmult_assoc ; apply Rmult_eq_compat_l.
  rewrite Rmult_comm, <- Rmult_assoc ; apply Rmult_eq_compat_r.
@@ -345,15 +345,15 @@ apply fact_neq_0.
  rewrite <- pow_mult ; simpl ; reflexivity.
  apply fact_neq_0.
 unfold_gt ; unfold exp_seq ; rewrite Cim_mul ;
-replace (S (S (2 * p))) with (2 * (S p))%nat by intuition ;
+replace (S (S (2 * p))) with (2 * (S p))%nat by (intuition auto with *) ;
 rewrite Cim_Cpow_2, INC_inv_Cim_INR.
 do 2 rewrite Rmult_0_r ; ring.
 apply fact_neq_0.
 Qed.
 
 Lemma Cexp_abs_cv : forall z, {l | Cser_abs_cv (gt_pser exp_seq z) l}.
 Proof.
-intro z ; assert (z_bd : Cnorm z < Cnorm z + 1) by intuition ;
+intro z ; assert (z_bd : Cnorm z < Cnorm z + 1) by (intuition  auto with *);
  destruct (Cpser_abel2_prelim _ _ (exp_infinite_cv_radius (Cnorm z + 1)%R) _ z_bd) as [l Hl].
  unfold Cpser_norm in Hl.
  exists (Cre l) ; unfold Cser_abs_cv.

Complex/Cpow_plus.v

@@ -122,7 +122,7 @@ Proof.
 intros n zR zI.
 apply sum_f_C0_eq_seq.
 intros n0 H.
-replace (zR +i zI) with ((zR, 0%R) + (0%R, zI)) by (rewrite <- Ceq ; simpl ; intuition).
+replace (zR +i zI) with ((zR, 0%R) + (0%R, zI)) by (rewrite <- Ceq ; simpl ; intuition auto with *).
 generalize equi_binom_add. intro Hn1. unfold Cdiv in *. apply Hn1. exact H. 
 Qed.
 (* end hide *)
@@ -175,8 +175,8 @@ field.
 split ; try split ; apply not_0_INC ; try apply fact_neq_0 ; intuition lia.
 }
 ring_simplify.
-replace (S n - S n)%nat with O by intuition.
-replace (S (S n) - S (S n))%nat with O by intuition.
+replace (S n - S n)%nat with O by intuition auto with *.
+replace (S (S n) - S (S n))%nat with O by intuition auto with *.
 repeat rewrite fact_simpl.
 repeat rewrite mult_INC. simpl (INC 0).
 field_simplify. unfold Cdiv. repeat rewrite Cmult_0_r. rewrite Cmult_0_l. reflexivity.