diff options
Diffstat (limited to 'theories')
39 files changed, 1510 insertions, 561 deletions
diff --git a/theories/Floats/FloatAxioms.v b/theories/Floats/FloatAxioms.v new file mode 100644 index 0000000000..8ca64aac42 --- /dev/null +++ b/theories/Floats/FloatAxioms.v @@ -0,0 +1,58 @@ +Require Import ZArith Int63 SpecFloat PrimFloat FloatOps. + +(** * Properties of the primitive operators for the Binary64 format *) + +Notation valid_binary := (valid_binary prec emax). + +Definition SF64classify := SFclassify prec. +Definition SF64mul := SFmul prec emax. +Definition SF64add := SFadd prec emax. +Definition SF64sub := SFsub prec emax. +Definition SF64div := SFdiv prec emax. +Definition SF64sqrt := SFsqrt prec emax. +Definition SF64succ := SFsucc prec emax. +Definition SF64pred := SFpred prec emax. + +Axiom Prim2SF_valid : forall x, valid_binary (Prim2SF x) = true. +Axiom SF2Prim_Prim2SF : forall x, SF2Prim (Prim2SF x) = x. +Axiom Prim2SF_SF2Prim : forall x, valid_binary x = true -> Prim2SF (SF2Prim x) = x. + +Theorem Prim2SF_inj : forall x y, Prim2SF x = Prim2SF y -> x = y. + intros. rewrite <- SF2Prim_Prim2SF. symmetry. rewrite <- SF2Prim_Prim2SF. now rewrite H. +Qed. + +Theorem SF2Prim_inj : forall x y, SF2Prim x = SF2Prim y -> valid_binary x = true -> valid_binary y = true -> x = y. + intros. rewrite <- Prim2SF_SF2Prim by assumption. symmetry. rewrite <- Prim2SF_SF2Prim by assumption. rewrite H. reflexivity. +Qed. + +Axiom opp_spec : forall x, Prim2SF (-x)%float = SFopp (Prim2SF x). +Axiom abs_spec : forall x, Prim2SF (abs x) = SFabs (Prim2SF x). + +Axiom eqb_spec : forall x y, (x == y)%float = SFeqb (Prim2SF x) (Prim2SF y). +Axiom ltb_spec : forall x y, (x < y)%float = SFltb (Prim2SF x) (Prim2SF y). +Axiom leb_spec : forall x y, (x <= y)%float = SFleb (Prim2SF x) (Prim2SF y). + +Definition flatten_cmp_opt c := + match c with + | None => FNotComparable + | Some Eq => FEq + | Some Lt => FLt + | Some Gt => FGt + end. +Axiom compare_spec : forall x y, (x ?= y)%float = flatten_cmp_opt (SFcompare (Prim2SF x) (Prim2SF y)). + +Axiom classify_spec : forall x, classify x = SF64classify (Prim2SF x). +Axiom mul_spec : forall x y, Prim2SF (x * y)%float = SF64mul (Prim2SF x) (Prim2SF y). +Axiom add_spec : forall x y, Prim2SF (x + y)%float = SF64add (Prim2SF x) (Prim2SF y). +Axiom sub_spec : forall x y, Prim2SF (x - y)%float = SF64sub (Prim2SF x) (Prim2SF y). +Axiom div_spec : forall x y, Prim2SF (x / y)%float = SF64div (Prim2SF x) (Prim2SF y). +Axiom sqrt_spec : forall x, Prim2SF (sqrt x) = SF64sqrt (Prim2SF x). + +Axiom of_int63_spec : forall n, Prim2SF (of_int63 n) = binary_normalize prec emax (to_Z n) 0%Z false. +Axiom normfr_mantissa_spec : forall f, to_Z (normfr_mantissa f) = Z.of_N (SFnormfr_mantissa prec (Prim2SF f)). + +Axiom frshiftexp_spec : forall f, let (m,e) := frshiftexp f in (Prim2SF m, ((to_Z e) - shift)%Z) = SFfrexp prec emax (Prim2SF f). +Axiom ldshiftexp_spec : forall f e, Prim2SF (ldshiftexp f e) = SFldexp prec emax (Prim2SF f) ((to_Z e) - shift). + +Axiom next_up_spec : forall x, Prim2SF (next_up x) = SF64succ (Prim2SF x). +Axiom next_down_spec : forall x, Prim2SF (next_down x) = SF64pred (Prim2SF x). diff --git a/theories/Floats/FloatClass.v b/theories/Floats/FloatClass.v new file mode 100644 index 0000000000..627cb648f9 --- /dev/null +++ b/theories/Floats/FloatClass.v @@ -0,0 +1,2 @@ +Variant float_class : Set := + | PNormal | NNormal | PSubn | NSubn | PZero | NZero | PInf | NInf | NaN. diff --git a/theories/Floats/FloatLemmas.v b/theories/Floats/FloatLemmas.v new file mode 100644 index 0000000000..81cb7120e0 --- /dev/null +++ b/theories/Floats/FloatLemmas.v @@ -0,0 +1,319 @@ +Require Import ZArith Int63 SpecFloat PrimFloat FloatOps FloatAxioms. +Require Import Psatz. + +(** * Support results involving frexp and ldexp *) + +Lemma shift_value : shift = (2*emax + prec)%Z. + reflexivity. +Qed. + +Theorem frexp_spec : forall f, let (m,e) := frexp f in (Prim2SF m, e) = SFfrexp prec emax (Prim2SF f). + intro. + unfold frexp. + case_eq (frshiftexp f). + intros. + assert (H' := frshiftexp_spec f). + now rewrite H in H'. +Qed. + +Theorem ldexp_spec : forall f e, Prim2SF (ldexp f e) = SFldexp prec emax (Prim2SF f) e. + intros. + unfold ldexp. + rewrite (ldshiftexp_spec f _). + assert (Hv := Prim2SF_valid f). + destruct (Prim2SF f); auto. + unfold SFldexp. + unfold binary_round. + assert (Hmod_elim : forall e, ([| of_Z (Z.max (Z.min e (emax - emin)) (emin - emax - 1) + shift)|]%int63 - shift = Z.max (Z.min e (emax - emin)) (emin - emax - 1))%Z). + { + intro e1. + rewrite of_Z_spec, shift_value. + unfold wB, size; simpl. + unfold Z.pow_pos; simpl. + set (n := Z.max (Z.min _ _) _). + set (wB := 9223372036854775808%Z). (* Z.pow_pos 2 63 *) + assert (-2099 <= n <= 2098)%Z by (unfold n; lia). + rewrite Z.mod_small by (unfold wB; lia). + now rewrite Z.add_simpl_r. + } + rewrite Hmod_elim. + clear Hmod_elim. + revert Hv. + unfold valid_binary, bounded, canonical_mantissa. + unfold fexp. + rewrite Bool.andb_true_iff. + intro H'. + destruct H' as (H1,H2). + apply Zeq_bool_eq in H1. + apply Z.max_case_strong. + apply Z.min_case_strong. + - reflexivity. + - intros He _. + destruct (Z.max_spec (Z.pos (digits2_pos m) + e0 - prec) emin) as [ (H, Hm) | (H, Hm) ]. + + rewrite Hm in H1. + rewrite <- H1. + rewrite !Z.max_l by (revert He; unfold emax, emin, prec; lia). + replace (emin + _)%Z with emax by ring. + unfold shl_align. + rewrite <- H1 in H. + replace (Z.pos _ + _ - _ - _)%Z with (Z.pos (digits2_pos m) - prec)%Z by ring. + remember (Zpos _ - _)%Z as z'. + destruct z' ; [ lia | lia | ]. + unfold binary_round_aux. + unfold shr_fexp. + unfold fexp. + unfold Zdigits2. + unfold shr_record_of_loc, shr. + rewrite !Z.max_l by (revert H He; unfold emax, emin, prec; lia). + replace (_ - _)%Z with (Z.pos (digits2_pos (shift_pos p m)) - prec)%Z by ring. + assert (Hs : (Z.pos (digits2_pos (shift_pos p m)) <= prec)%Z). + { + assert (H' : forall p p', digits2_pos (shift_pos p p') = (digits2_pos p' + p)%positive). + { + induction p0. + intro p'. + simpl. + rewrite IHp0. + rewrite IHp0. + lia. + intro p'. + simpl. + rewrite IHp0. + rewrite IHp0. + lia. + intro p'. + simpl. + lia. + } + rewrite H'. + lia. + } + replace (Z.pos (digits2_pos m) + (emin + e) - prec - (emin + e))%Z with (Z.neg p) by lia. + unfold shr_m, loc_of_shr_record. + unfold round_nearest_even. + remember (Z.pos (digits2_pos (shift_pos p m)) - prec)%Z as ds. + destruct ds. + * rewrite Z.max_l by (revert He; unfold emax, emin, prec; lia). + replace (_ - _)%Z with Z0 by lia. + replace (_ <=? _)%Z with false by (symmetry; rewrite Z.leb_gt; lia). + rewrite Z.max_l by (revert He; unfold emax, emin, prec; lia). + replace (_ - _)%Z with Z0 by lia. + rewrite Z.max_l by (revert He; unfold emax, emin, prec; lia). + replace (_ - _)%Z with Z0 by lia. + replace (_ <=? _)%Z with false by (symmetry; rewrite Z.leb_gt; lia). + reflexivity. + * exfalso; lia. + * rewrite Z.max_l by (revert He; unfold emax, emin, prec; lia). + replace (_ - _)%Z with (Zneg p0) by lia. + replace (_ <=? _)%Z with false by (symmetry; rewrite Z.leb_gt; lia). + rewrite Z.max_l by (revert He; unfold emax, emin, prec; lia). + replace (_ - _)%Z with (Zneg p0) by lia. + rewrite Z.max_l by (revert He; unfold emax, emin, prec; lia). + replace (_ - _)%Z with (Zneg p0) by lia. + replace (_ <=? _)%Z with false by (symmetry; rewrite Z.leb_gt; lia). + reflexivity. + + rewrite !Z.max_l by (revert H He; unfold emax, emin, prec; lia). + rewrite Hm in H1. + clear Hm. + replace (Zpos _ + _ - _)%Z with (e0 + (emax - emin))%Z by (rewrite <- H1 at 1; ring). + replace (Zpos _ + _ - _)%Z with (e0 + e)%Z by (rewrite <- H1 at 1; ring). + unfold shl_align. + replace (_ - _)%Z with Z0 by ring. + replace (e0 + e - _)%Z with Z0 by ring. + unfold binary_round_aux. + unfold shr_fexp. + unfold fexp. + unfold Zdigits2. + rewrite !Z.max_l by (revert H He; unfold emax, emin, prec; lia). + unfold shr_record_of_loc. + unfold shr. + unfold Zdigits2. + replace (Zpos _ + _ - _ - _)%Z with Z0 by lia. + unfold shr_m. + unfold loc_of_shr_record. + unfold round_nearest_even. + rewrite Z.max_l by (revert H He; unfold emax, emin, prec; lia). + replace (Zpos _ + _ - _ - _)%Z with Z0 by lia. + replace (_ <=? _)%Z with false by (symmetry; rewrite Z.leb_gt; lia). + replace (Zpos _ + _ - _ - _)%Z with Z0 by lia. + rewrite Z.max_l by (revert H He; unfold emax, emin, prec; lia). + replace (Zpos _ + _ - _ - _)%Z with Z0 by lia. + replace (_ <=? _)%Z with false by (symmetry; rewrite Z.leb_gt; lia). + reflexivity. + - rewrite Z.min_le_iff. + intro H. + destruct H as [ He | Habs ]; [ | revert Habs; now unfold emin, emax ]. + unfold shl_align. + assert (Hprec : (Z.pos (digits2_pos m) <= prec)%Z). + { + destruct (Z.max_spec (Z.pos (digits2_pos m) + e0 - prec) emin) as [ (Hpi, Hpe) | (Hpi, Hpe) ]; rewrite Hpe in H1; lia. + } + + assert (Hshr : forall p s, Zdigits2 (shr_m (iter_pos shr_1 p s)) = Z.max Z0 (Zdigits2 (shr_m s) - Z.pos p)%Z). + { + assert (Hshr1 : forall s, Zdigits2 (shr_m (shr_1 s)) = Z.max 0 (Zdigits2 (shr_m s) - 1)%Z). + { + intro s0. + destruct s0. + unfold shr_1. + destruct shr_m; try (simpl; lia). + - destruct p; unfold Zdigits2, shr_m, digits2_pos; lia. + - destruct p; unfold Zdigits2, shr_m, digits2_pos; lia. + } + induction p. + simpl. + intro s0. + do 2 rewrite IHp. + rewrite Hshr1. + lia. + intros. + simpl. + do 2 rewrite IHp. + lia. + apply Hshr1. + } + + assert (Hd0 : forall z, Zdigits2 z = 0%Z -> z = 0%Z). + { + intro z. + unfold Zdigits2. + now destruct z. + } + + assert (Hshr_p0 : forall p0, (prec < Z.pos p0)%Z -> shr_m (iter_pos shr_1 p0 {| shr_m := Z.pos m; shr_r := false; shr_s := false |}) = Z0). + { + intros p0 Hp0. + apply Hd0. + rewrite Hshr. + rewrite Z.max_l; [ reflexivity | ]. + unfold shr_m. + unfold Zdigits2. + lia. + } + + assert (Hshr_p0_r : forall p0, (prec < Z.pos p0)%Z -> shr_r (iter_pos shr_1 p0 {| shr_m := Z.pos m; shr_r := false; shr_s := false |}) = false). + { + intros p0 Hp0. + + assert (Hshr_p0m1 : shr_m (iter_pos shr_1 (p0-1) {| shr_m := Z.pos m; shr_r := false; shr_s := false |}) = Z0). + { + apply Hd0. + rewrite Hshr. + rewrite Z.max_l; [ reflexivity | ]. + unfold shr_m. + unfold Zdigits2. + lia. + } + + assert (Hiter_pos : forall A (f : A -> A) p e, iter_pos f (p + 1) e = f (iter_pos f p e)). + { + assert (Hiter_pos' : forall A (f : A -> A) p e, iter_pos f p (f e) = f (iter_pos f p e)). + { + intros A f'. + induction p. + intro e'. + simpl. + now do 2 rewrite IHp. + intro e'. + simpl. + now do 2 rewrite IHp. + intro e'. + now simpl. + } + intros A f'. + induction p. + intros. + simpl. + rewrite <- Pos.add_1_r. + do 2 rewrite IHp. + now do 3 rewrite Hiter_pos'. + intros. + simpl. + now do 2 rewrite Hiter_pos'. + intros. + now simpl. + } + replace p0 with (p0 - 1 + 1)%positive. + rewrite Hiter_pos. + unfold shr_1 at 1. + remember (iter_pos _ _ _) as shr_p0m1. + destruct shr_p0m1. + unfold SpecFloat.shr_m in Hshr_p0m1. + now rewrite Hshr_p0m1. + rewrite Pos.add_1_r. + rewrite Pos.sub_1_r. + apply Pos.succ_pred. + lia. + } + + rewrite Z.leb_le in H2. + + destruct (Z.max_spec (Z.pos (digits2_pos m) + (e0 + (emin - emax - 1)) - prec) emin) as [ (H, Hm) | (H, Hm) ]. + + rewrite Hm. + replace (_ - _)%Z with (emax - e0 + 1)%Z by ring. + remember (emax - e0 + 1)%Z as z'. + destruct z'; [ exfalso; lia | | exfalso; lia ]. + unfold binary_round_aux. + unfold shr_fexp, fexp. + unfold shr, shr_record_of_loc. + unfold Zdigits2. + rewrite Hm. + replace (_ - _)%Z with (Z.pos p) by (rewrite Heqz'; ring). + set (rne := round_nearest_even _ _). + assert (rne = 0%Z). + { + unfold rne. + unfold round_nearest_even. + + assert (Hp0 : (prec < Z.pos p)%Z) by lia. + + unfold loc_of_shr_record. + specialize (Hshr_p0_r _ Hp0). + specialize (Hshr_p0 _ Hp0). + revert Hshr_p0_r Hshr_p0. + set (shr_p0 := iter_pos shr_1 _ _). + destruct shr_p0. + unfold SpecFloat.shr_r, SpecFloat.shr_m. + intros Hshr_r Hshr_m. + rewrite Hshr_r, Hshr_m. + now destruct shr_s. + } + + rewrite H0. + rewrite Z.max_r by (rewrite Heqz'; unfold prec; lia). + replace (_ - _)%Z with 0%Z by lia. + unfold shr_m. + + rewrite Z.max_r by lia. + remember (emin - (e0 + e))%Z as eminmze. + destruct eminmze; [ exfalso; lia | | exfalso; lia ]. + + rewrite Z.max_r by lia. + rewrite <- Heqeminmze. + + set (rne' := round_nearest_even _ _). + assert (Hrne'0 : rne' = 0%Z). + { + unfold rne'. + unfold round_nearest_even. + + assert (Hp1 : (prec < Z.pos p0)%Z) by lia. + + unfold loc_of_shr_record. + specialize (Hshr_p0_r _ Hp1). + specialize (Hshr_p0 _ Hp1). + revert Hshr_p0_r Hshr_p0. + set (shr_p1 := iter_pos shr_1 _ _). + destruct shr_p1. + unfold SpecFloat.shr_r, SpecFloat.shr_m. + intros Hshr_r Hshr_m. + rewrite Hshr_r, Hshr_m. + now destruct shr_s. + } + + rewrite Hrne'0. + rewrite Z.max_r by (rewrite Heqeminmze; unfold prec; lia). + replace (_ - _)%Z with 0%Z by lia. + reflexivity. + + exfalso; lia. +Qed. diff --git a/theories/Floats/FloatOps.v b/theories/Floats/FloatOps.v new file mode 100644 index 0000000000..f0d3bcced9 --- /dev/null +++ b/theories/Floats/FloatOps.v @@ -0,0 +1,48 @@ +Require Import ZArith Int63 SpecFloat PrimFloat. + +(** * Derived operations and mapping between primitive [float]s and [spec_float]s *) + +Definition prec := 53%Z. +Definition emax := 1024%Z. +Notation emin := (emin prec emax). + +Definition shift := 2101%Z. (** [= 2*emax + prec] *) + +Definition frexp f := + let (m, se) := frshiftexp f in + (m, ([| se |] - shift)%Z%int63). + +Definition ldexp f e := + let e' := Z.max (Z.min e (emax - emin)) (emin - emax - 1) in + ldshiftexp f (of_Z (e' + shift)). + +Definition ulp f := ldexp one (fexp prec emax (snd (frexp f))). + +(** [Prim2SF] is an injective function that will be useful to express +the properties of the implemented Binary64 format (see [FloatAxioms]). +*) +Definition Prim2SF f := + if is_nan f then S754_nan + else if is_zero f then S754_zero (get_sign f) + else if is_infinity f then S754_infinity (get_sign f) + else + let (r, exp) := frexp f in + let e := (exp - prec)%Z in + let (shr, e') := shr_fexp prec emax [| normfr_mantissa r |]%int63 e loc_Exact in + match shr_m shr with + | Zpos p => S754_finite (get_sign f) p e' + | Zneg _ | Z0 => S754_zero false (* must never occur *) + end. + +Definition SF2Prim ef := + match ef with + | S754_nan => nan + | S754_zero false => zero + | S754_zero true => neg_zero + | S754_infinity false => infinity + | S754_infinity true => neg_infinity + | S754_finite s m e => + let pm := of_int63 (of_Z (Zpos m)) in + let f := ldexp pm e in + if s then (-f)%float else f + end. diff --git a/theories/Floats/Floats.v b/theories/Floats/Floats.v new file mode 100644 index 0000000000..700c69b99d --- /dev/null +++ b/theories/Floats/Floats.v @@ -0,0 +1,17 @@ +(** The Floats library is split in 6 theories: +- FloatClass: define the [float_class] inductive +- PrimFloat: define the floating-point values and operators as kernel primitives +- SpecFloat: specify the floating-point operators with binary integers +- FloatOps: define conversion functions between [spec_float] and [float] +- FloatAxioms: state properties of the primitive operators w.r.t. [spec_float] +- FloatLemmas: prove a few results involving frexp and ldexp + +For a brief overview of the Floats library, +see {{https://coq.inria.fr/distrib/current/refman/language/coq-library.html#floats-library}} *) + +Require Export FloatClass. +Require Export PrimFloat. +Require Export SpecFloat. +Require Export FloatOps. +Require Export FloatAxioms. +Require Export FloatLemmas. diff --git a/theories/Floats/PrimFloat.v b/theories/Floats/PrimFloat.v new file mode 100644 index 0000000000..bc1727469d --- /dev/null +++ b/theories/Floats/PrimFloat.v @@ -0,0 +1,118 @@ +Require Import Int63 FloatClass. + +(** * Definition of the interface for primitive floating-point arithmetic + +This interface provides processor operators for the Binary64 format of the +IEEE 754-2008 standard. *) + +(** ** Type definition for the co-domain of [compare] *) +Variant float_comparison : Set := FEq | FLt | FGt | FNotComparable. + +Register float_comparison as kernel.ind_f_cmp. + +Register float_class as kernel.ind_f_class. + +(** ** The main type *) +(** [float]: primitive type for Binary64 floating-point numbers. *) +Primitive float := #float64_type. + +(** ** Syntax support *) +Declare Scope float_scope. +Delimit Scope float_scope with float. +Bind Scope float_scope with float. + +Declare ML Module "float_syntax_plugin". + +(** ** Floating-point operators *) +Primitive classify := #float64_classify. + +Primitive abs := #float64_abs. + +Primitive sqrt := #float64_sqrt. + +Primitive opp := #float64_opp. +Notation "- x" := (opp x) : float_scope. + +Primitive eqb := #float64_eq. +Notation "x == y" := (eqb x y) (at level 70, no associativity) : float_scope. + +Primitive ltb := #float64_lt. +Notation "x < y" := (ltb x y) (at level 70, no associativity) : float_scope. + +Primitive leb := #float64_le. +Notation "x <= y" := (leb x y) (at level 70, no associativity) : float_scope. + +Primitive compare := #float64_compare. +Notation "x ?= y" := (compare x y) (at level 70, no associativity) : float_scope. + +Primitive mul := #float64_mul. +Notation "x * y" := (mul x y) : float_scope. + +Primitive add := #float64_add. +Notation "x + y" := (add x y) : float_scope. + +Primitive sub := #float64_sub. +Notation "x - y" := (sub x y) : float_scope. + +Primitive div := #float64_div. +Notation "x / y" := (div x y) : float_scope. + +(** ** Conversions *) + +(** [of_int63]: convert a primitive integer into a float value. + The value is rounded if need be. *) +Primitive of_int63 := #float64_of_int63. + +(** Specification of [normfr_mantissa]: +- If the input is a float value with an absolute value inside $[0.5, 1.)$#[0.5, 1.)#; +- Then return its mantissa as a primitive integer. + The mantissa will be a 53-bit integer with its most significant bit set to 1; +- Else return zero. + +The sign bit is always ignored. *) +Primitive normfr_mantissa := #float64_normfr_mantissa. + +(** ** Exponent manipulation functions *) +(** [frshiftexp]: convert a float to fractional part in $[0.5, 1.)$#[0.5, 1.)# +and integer part. *) +Primitive frshiftexp := #float64_frshiftexp. + +(** [ldshiftexp]: multiply a float by an integral power of 2. *) +Primitive ldshiftexp := #float64_ldshiftexp. + +(** ** Predecesor/Successor functions *) + +(** [next_up]: return the next float towards positive infinity. *) +Primitive next_up := #float64_next_up. + +(** [next_down]: return the next float towards negative infinity. *) +Primitive next_down := #float64_next_down. + +(** ** Special values (needed for pretty-printing) *) +Definition infinity := Eval compute in div (of_int63 1) (of_int63 0). +Definition neg_infinity := Eval compute in opp infinity. +Definition nan := Eval compute in div (of_int63 0) (of_int63 0). + +Register infinity as num.float.infinity. +Register neg_infinity as num.float.neg_infinity. +Register nan as num.float.nan. + +(** ** Other special values *) +Definition one := Eval compute in (of_int63 1). +Definition zero := Eval compute in (of_int63 0). +Definition neg_zero := Eval compute in (-zero)%float. +Definition two := Eval compute in (of_int63 2). + +(** ** Predicates and helper functions *) +Definition is_nan f := negb (f == f)%float. + +Definition is_zero f := (f == zero)%float. (* note: 0 == -0 with floats *) + +Definition is_infinity f := (abs f == infinity)%float. + +Definition is_finite (x : float) := negb (is_nan x || is_infinity x). + +(** [get_sign]: return [true] for [-] sign, [false] for [+] sign. *) +Definition get_sign f := + let f := if is_zero f then (one / f)%float else f in + (f < zero)%float. diff --git a/theories/Floats/SpecFloat.v b/theories/Floats/SpecFloat.v new file mode 100644 index 0000000000..fd0aa5e075 --- /dev/null +++ b/theories/Floats/SpecFloat.v @@ -0,0 +1,416 @@ +Require Import ZArith FloatClass. + +(** * Specification of floating-point arithmetic + +This specification is mostly borrowed from the [IEEE754.Binary] module +of the Flocq library (see {{http://flocq.gforge.inria.fr/}}) *) + +(** ** Inductive specification of floating-point numbers + +Similar to [Flocq.IEEE754.Binary.full_float], but with no NaN payload. *) +Variant spec_float := + | S754_zero (s : bool) + | S754_infinity (s : bool) + | S754_nan + | S754_finite (s : bool) (m : positive) (e : Z). + +(** ** Parameterized definitions + +[prec] is the number of bits of the mantissa including the implicit one; +[emax] is the exponent of the infinities. + +For instance, Binary64 is defined by [prec = 53] and [emax = 1024]. *) +Section FloatOps. + Variable prec emax : Z. + + Definition emin := (3-emax-prec)%Z. + Definition fexp e := Z.max (e - prec) emin. + + Section Zdigits2. + Fixpoint digits2_pos (n : positive) : positive := + match n with + | xH => xH + | xO p => Pos.succ (digits2_pos p) + | xI p => Pos.succ (digits2_pos p) + end. + + Definition Zdigits2 n := + match n with + | Z0 => n + | Zpos p => Zpos (digits2_pos p) + | Zneg p => Zpos (digits2_pos p) + end. + End Zdigits2. + + Section ValidBinary. + Definition canonical_mantissa m e := + Zeq_bool (fexp (Zpos (digits2_pos m) + e)) e. + + Definition bounded m e := + andb (canonical_mantissa m e) (Zle_bool e (emax - prec)). + + Definition valid_binary x := + match x with + | S754_finite _ m e => bounded m e + | _ => true + end. + End ValidBinary. + + Section Iter. + Context {A : Type}. + Variable (f : A -> A). + + Fixpoint iter_pos (n : positive) (x : A) {struct n} : A := + match n with + | xI n' => iter_pos n' (iter_pos n' (f x)) + | xO n' => iter_pos n' (iter_pos n' x) + | xH => f x + end. + End Iter. + + Section Rounding. + Inductive location := loc_Exact | loc_Inexact : comparison -> location. + + Record shr_record := { shr_m : Z ; shr_r : bool ; shr_s : bool }. + + Definition shr_1 mrs := + let '(Build_shr_record m r s) := mrs in + let s := orb r s in + match m with + | Z0 => Build_shr_record Z0 false s + | Zpos xH => Build_shr_record Z0 true s + | Zpos (xO p) => Build_shr_record (Zpos p) false s + | Zpos (xI p) => Build_shr_record (Zpos p) true s + | Zneg xH => Build_shr_record Z0 true s + | Zneg (xO p) => Build_shr_record (Zneg p) false s + | Zneg (xI p) => Build_shr_record (Zneg p) true s + end. + + Definition loc_of_shr_record mrs := + match mrs with + | Build_shr_record _ false false => loc_Exact + | Build_shr_record _ false true => loc_Inexact Lt + | Build_shr_record _ true false => loc_Inexact Eq + | Build_shr_record _ true true => loc_Inexact Gt + end. + + Definition shr_record_of_loc m l := + match l with + | loc_Exact => Build_shr_record m false false + | loc_Inexact Lt => Build_shr_record m false true + | loc_Inexact Eq => Build_shr_record m true false + | loc_Inexact Gt => Build_shr_record m true true + end. + + Definition shr mrs e n := + match n with + | Zpos p => (iter_pos shr_1 p mrs, (e + n)%Z) + | _ => (mrs, e) + end. + + Definition shr_fexp m e l := + shr (shr_record_of_loc m l) e (fexp (Zdigits2 m + e) - e). + + Definition round_nearest_even mx lx := + match lx with + | loc_Exact => mx + | loc_Inexact Lt => mx + | loc_Inexact Eq => if Z.even mx then mx else (mx + 1)%Z + | loc_Inexact Gt => (mx + 1)%Z + end. + + Definition binary_round_aux sx mx ex lx := + let '(mrs', e') := shr_fexp mx ex lx in + let '(mrs'', e'') := shr_fexp (round_nearest_even (shr_m mrs') (loc_of_shr_record mrs')) e' loc_Exact in + match shr_m mrs'' with + | Z0 => S754_zero sx + | Zpos m => if Zle_bool e'' (emax - prec) then S754_finite sx m e'' else S754_infinity sx + | _ => S754_nan + end. + + Definition shl_align mx ex ex' := + match (ex' - ex)%Z with + | Zneg d => (shift_pos d mx, ex') + | _ => (mx, ex) + end. + + Definition binary_round sx mx ex := + let '(mz, ez) := shl_align mx ex (fexp (Zpos (digits2_pos mx) + ex))in + binary_round_aux sx (Zpos mz) ez loc_Exact. + + Definition binary_normalize m e szero := + match m with + | Z0 => S754_zero szero + | Zpos m => binary_round false m e + | Zneg m => binary_round true m e + end. + End Rounding. + + (** ** Define operations *) + + Definition SFopp x := + match x with + | S754_nan => S754_nan + | S754_infinity sx => S754_infinity (negb sx) + | S754_finite sx mx ex => S754_finite (negb sx) mx ex + | S754_zero sx => S754_zero (negb sx) + end. + + Definition SFabs x := + match x with + | S754_nan => S754_nan + | S754_infinity sx => S754_infinity false + | S754_finite sx mx ex => S754_finite false mx ex + | S754_zero sx => S754_zero false + end. + + Definition SFcompare f1 f2 := + match f1, f2 with + | S754_nan , _ | _, S754_nan => None + | S754_infinity s1, S754_infinity s2 => + Some match s1, s2 with + | true, true => Eq + | false, false => Eq + | true, false => Lt + | false, true => Gt + end + | S754_infinity s, _ => Some (if s then Lt else Gt) + | _, S754_infinity s => Some (if s then Gt else Lt) + | S754_finite s _ _, S754_zero _ => Some (if s then Lt else Gt) + | S754_zero _, S754_finite s _ _ => Some (if s then Gt else Lt) + | S754_zero _, S754_zero _ => Some Eq + | S754_finite s1 m1 e1, S754_finite s2 m2 e2 => + Some match s1, s2 with + | true, false => Lt + | false, true => Gt + | false, false => + match Z.compare e1 e2 with + | Lt => Lt + | Gt => Gt + | Eq => Pcompare m1 m2 Eq + end + | true, true => + match Z.compare e1 e2 with + | Lt => Gt + | Gt => Lt + | Eq => CompOpp (Pcompare m1 m2 Eq) + end + end + end. + + Definition SFeqb f1 f2 := + match SFcompare f1 f2 with + | Some Eq => true + | _ => false + end. + + Definition SFltb f1 f2 := + match SFcompare f1 f2 with + | Some Lt => true + | _ => false + end. + + Definition SFleb f1 f2 := + match SFcompare f1 f2 with + | Some Le => true + | _ => false + end. + + Definition SFclassify f := + match f with + | S754_nan => NaN + | S754_infinity false => PInf + | S754_infinity true => NInf + | S754_zero false => NZero + | S754_zero true => PZero + | S754_finite false m _ => + if (digits2_pos m =? Z.to_pos prec)%positive then PNormal + else PSubn + | S754_finite true m _ => + if (digits2_pos m =? Z.to_pos prec)%positive then NNormal + else NSubn + end. + + Definition SFmul x y := + match x, y with + | S754_nan, _ | _, S754_nan => S754_nan + | S754_infinity sx, S754_infinity sy => S754_infinity (xorb sx sy) + | S754_infinity sx, S754_finite sy _ _ => S754_infinity (xorb sx sy) + | S754_finite sx _ _, S754_infinity sy => S754_infinity (xorb sx sy) + | S754_infinity _, S754_zero _ => S754_nan + | S754_zero _, S754_infinity _ => S754_nan + | S754_finite sx _ _, S754_zero sy => S754_zero (xorb sx sy) + | S754_zero sx, S754_finite sy _ _ => S754_zero (xorb sx sy) + | S754_zero sx, S754_zero sy => S754_zero (xorb sx sy) + | S754_finite sx mx ex, S754_finite sy my ey => + binary_round_aux (xorb sx sy) (Zpos (mx * my)) (ex + ey) loc_Exact + end. + + Definition cond_Zopp (b : bool) m := if b then Z.opp m else m. + + Definition SFadd x y := + match x, y with + | S754_nan, _ | _, S754_nan => S754_nan + | S754_infinity sx, S754_infinity sy => + if Bool.eqb sx sy then x else S754_nan + | S754_infinity _, _ => x + | _, S754_infinity _ => y + | S754_zero sx, S754_zero sy => + if Bool.eqb sx sy then x else + S754_zero false + | S754_zero _, _ => y + | _, S754_zero _ => x + | S754_finite sx mx ex, S754_finite sy my ey => + let ez := Z.min ex ey in + binary_normalize (Zplus (cond_Zopp sx (Zpos (fst (shl_align mx ex ez)))) (cond_Zopp sy (Zpos (fst (shl_align my ey ez))))) + ez false + end. + + Definition SFsub x y := + match x, y with + | S754_nan, _ | _, S754_nan => S754_nan + | S754_infinity sx, S754_infinity sy => + if Bool.eqb sx (negb sy) then x else S754_nan + | S754_infinity _, _ => x + | _, S754_infinity sy => S754_infinity (negb sy) + | S754_zero sx, S754_zero sy => + if Bool.eqb sx (negb sy) then x else + S754_zero false + | S754_zero _, S754_finite sy my ey => S754_finite (negb sy) my ey + | _, S754_zero _ => x + | S754_finite sx mx ex, S754_finite sy my ey => + let ez := Z.min ex ey in + binary_normalize (Zminus (cond_Zopp sx (Zpos (fst (shl_align mx ex ez)))) (cond_Zopp sy (Zpos (fst (shl_align my ey ez))))) + ez false + end. + + Definition new_location_even nb_steps k := + if Zeq_bool k 0 then loc_Exact + else loc_Inexact (Z.compare (2 * k) nb_steps). + + Definition new_location_odd nb_steps k := + if Zeq_bool k 0 then loc_Exact + else + loc_Inexact + match Z.compare (2 * k + 1) nb_steps with + | Lt => Lt + | Eq => Lt + | Gt => Gt + end. + + Definition new_location nb_steps := + if Z.even nb_steps then new_location_even nb_steps else new_location_odd nb_steps. + + Definition SFdiv_core_binary m1 e1 m2 e2 := + let d1 := Zdigits2 m1 in + let d2 := Zdigits2 m2 in + let e' := Z.min (fexp (d1 + e1 - (d2 + e2))) (e1 - e2) in + let s := (e1 - e2 - e')%Z in + let m' := + match s with + | Zpos _ => Z.shiftl m1 s + | Z0 => m1 + | Zneg _ => Z0 + end in + let '(q, r) := Z.div_eucl m' m2 in + (q, e', new_location m2 r). + + Definition SFdiv x y := + match x, y with + | S754_nan, _ | _, S754_nan => S754_nan + | S754_infinity sx, S754_infinity sy => S754_nan + | S754_infinity sx, S754_finite sy _ _ => S754_infinity (xorb sx sy) + | S754_finite sx _ _, S754_infinity sy => S754_zero (xorb sx sy) + | S754_infinity sx, S754_zero sy => S754_infinity (xorb sx sy) + | S754_zero sx, S754_infinity sy => S754_zero (xorb sx sy) + | S754_finite sx _ _, S754_zero sy => S754_infinity (xorb sx sy) + | S754_zero sx, S754_finite sy _ _ => S754_zero (xorb sx sy) + | S754_zero sx, S754_zero sy => S754_nan + | S754_finite sx mx ex, S754_finite sy my ey => + let '(mz, ez, lz) := SFdiv_core_binary (Zpos mx) ex (Zpos my) ey in + binary_round_aux (xorb sx sy) mz ez lz + end. + + Definition SFsqrt_core_binary m e := + let d := Zdigits2 m in + let e' := Z.min (fexp (Z.div2 (d + e + 1))) (Z.div2 e) in + let s := (e - 2 * e')%Z in + let m' := + match s with + | Zpos p => Z.shiftl m s + | Z0 => m + | Zneg _ => Z0 + end in + let (q, r) := Z.sqrtrem m' in + let l := + if Zeq_bool r 0 then loc_Exact + else loc_Inexact (if Zle_bool r q then Lt else Gt) in + (q, e', l). + + Definition SFsqrt x := + match x with + | S754_nan => S754_nan + | S754_infinity false => x + | S754_infinity true => S754_nan + | S754_finite true _ _ => S754_nan + | S754_zero _ => x + | S754_finite sx mx ex => + let '(mz, ez, lz) := SFsqrt_core_binary (Zpos mx) ex in + binary_round_aux false mz ez lz + end. + + Definition SFnormfr_mantissa f := + match f with + | S754_finite _ mx ex => + if Z.eqb ex (-prec) then Npos mx else 0%N + | _ => 0%N + end. + + Definition SFldexp f e := + match f with + | S754_finite sx mx ex => binary_round sx mx (ex+e) + | _ => f + end. + + Definition SFfrexp f := + match f with + | S754_finite sx mx ex => + if (Z.to_pos prec <=? digits2_pos mx)%positive then + (S754_finite sx mx (-prec), (ex+prec)%Z) + else + let d := (prec - Z.pos (digits2_pos mx))%Z in + (S754_finite sx (shift_pos (Z.to_pos d) mx) (-prec), (ex+prec-d)%Z) + | _ => (f, (-2*emax-prec)%Z) + end. + + Definition SFone := binary_round false 1 0. + + Definition SFulp x := SFldexp SFone (fexp (snd (SFfrexp x))). + + Definition SFpred_pos x := + match x with + | S754_finite _ mx _ => + let d := + if (mx~0 =? shift_pos (Z.to_pos prec) 1)%positive then + SFldexp SFone (fexp (snd (SFfrexp x) - 1)) + else + SFulp x in + SFsub x d + | _ => x + end. + + Definition SFmax_float := + S754_finite false (shift_pos (Z.to_pos prec) 1 - 1) (emax - prec). + + Definition SFsucc x := + match x with + | S754_zero _ => SFldexp SFone emin + | S754_infinity false => x + | S754_infinity true => SFopp SFmax_float + | S754_nan => x + | S754_finite false _ _ => SFadd x (SFulp x) + | S754_finite true _ _ => SFopp (SFpred_pos (SFopp x)) + end. + + Definition SFpred f := SFopp (SFsucc (SFopp f)). +End FloatOps. diff --git a/theories/Init/Tactics.v b/theories/Init/Tactics.v index ad6f1765a3..6de9f8f88d 100644 --- a/theories/Init/Tactics.v +++ b/theories/Init/Tactics.v @@ -325,9 +325,9 @@ Ltac time_constr tac := (** Useful combinators *) Ltac assert_fails tac := - tryif tac then fail 0 tac "succeeds" else idtac. + tryif (once tac) then gfail 0 tac "succeeds" else idtac. Ltac assert_succeeds tac := - tryif (assert_fails tac) then fail 0 tac "fails" else idtac. + tryif (assert_fails tac) then gfail 0 tac "fails" else idtac. Tactic Notation "assert_succeeds" tactic3(tac) := assert_succeeds tac. Tactic Notation "assert_fails" tactic3(tac) := diff --git a/theories/Numbers/Cyclic/Abstract/CyclicAxioms.v b/theories/Numbers/Cyclic/Abstract/CyclicAxioms.v index daca0ee5dc..44784675b0 100644 --- a/theories/Numbers/Cyclic/Abstract/CyclicAxioms.v +++ b/theories/Numbers/Cyclic/Abstract/CyclicAxioms.v @@ -18,6 +18,7 @@ Set Implicit Arguments. Require Import ZArith. +Require Import Lia. Require Import Znumtheory. Require Import Zpow_facts. Require Import DoubleType. @@ -298,8 +299,7 @@ Module ZnZ. replace (base digits) with (1 * base digits + 0) by ring. rewrite Hp1. apply Z.add_le_mono. - apply Z.mul_le_mono_nonneg; auto with zarith. - case p1; simpl; intros; red; simpl; intros; discriminate. + apply Z.mul_le_mono_nonneg. 1-2, 4: lia. unfold base; auto with zarith. case (spec_to_Z w1); auto with zarith. Qed. @@ -314,7 +314,7 @@ Module ZnZ. forall p, 0 <= p < base digits -> [|of_Z p|] = p. Proof. intros p; case p; simpl; try rewrite spec_0; auto. - intros; rewrite of_pos_correct; auto with zarith. + intros; rewrite of_pos_correct; lia. intros p1 (H1, _); contradict H1; apply Z.lt_nge; red; simpl; auto. Qed. @@ -423,7 +423,7 @@ Lemma eqb_eq : forall x y, eqb x y = true <-> x == y. Proof. intros. unfold eqb, eq. rewrite ZnZ.spec_compare. - case Z.compare_spec; intuition; try discriminate. + case Z.compare_spec; split; (easy || lia). Qed. Lemma eqb_correct : forall x y, eqb x y = true -> x==y. diff --git a/theories/Numbers/Cyclic/Abstract/NZCyclic.v b/theories/Numbers/Cyclic/Abstract/NZCyclic.v index 53a71ce0c9..4fd2cc0564 100644 --- a/theories/Numbers/Cyclic/Abstract/NZCyclic.v +++ b/theories/Numbers/Cyclic/Abstract/NZCyclic.v @@ -15,6 +15,7 @@ Require Import ZArith. Require Import Zpow_facts. Require Import DoubleType. Require Import CyclicAxioms. +Require Import Lia. (** * From [CyclicType] to [NZAxiomsSig] *) @@ -59,7 +60,8 @@ Ltac zcongruence := repeat red; intros; zify; congruence. Instance eq_equiv : Equivalence eq. Proof. -unfold eq. firstorder. + split. 1-2: firstorder. + intros x y z; apply eq_trans. Qed. Local Obligation Tactic := zcongruence. @@ -77,7 +79,7 @@ Qed. Theorem gt_wB_0 : 0 < wB. Proof. -pose proof gt_wB_1; auto with zarith. +pose proof gt_wB_1; lia. Qed. Lemma one_mod_wB : 1 mod wB = 1. @@ -138,8 +140,8 @@ intros n H1 H2 H3. unfold B in *. apply AS in H3. setoid_replace (ZnZ.of_Z (n + 1)) with (S (ZnZ.of_Z n)). assumption. zify. -rewrite 2 ZnZ.of_Z_correct; auto with zarith. -symmetry; apply Zmod_small; auto with zarith. +rewrite 2 ZnZ.of_Z_correct. 2-3: lia. +symmetry; apply Zmod_small; lia. Qed. Theorem Zbounded_induction : @@ -155,8 +157,8 @@ apply natlike_rec2; unfold Q'. destruct (Z.le_gt_cases b 0) as [H | H]. now right. left; now split. intros n H IH. destruct IH as [[IH1 IH2] | IH]. destruct (Z.le_gt_cases (b - 1) n) as [H1 | H1]. -right; auto with zarith. -left. split; [auto with zarith | now apply (QS n)]. +right; lia. +left. split; [ lia | now apply (QS n)]. right; auto with zarith. unfold Q' in *; intros n H1 H2. destruct (H n H1) as [[H3 H4] | H3]. assumption. now apply Z.le_ngt in H3. diff --git a/theories/Numbers/Cyclic/Int31/Cyclic31.v b/theories/Numbers/Cyclic/Int31/Cyclic31.v index e878fa289e..a1e7b2ff85 100644 --- a/theories/Numbers/Cyclic/Int31/Cyclic31.v +++ b/theories/Numbers/Cyclic/Int31/Cyclic31.v @@ -110,7 +110,7 @@ Section Basics. nshiftr x k = 0. Proof. intros. - replace k with ((k-size)+size)%nat by omega. + replace k with ((k-size)+size)%nat by lia. induction (k-size)%nat; auto. rewrite nshiftr_size; auto. simpl; rewrite IHn; auto. @@ -147,7 +147,7 @@ Section Basics. nshiftl x k = 0. Proof. intros. - replace k with ((k-size)+size)%nat by omega. + replace k with ((k-size)+size)%nat by lia. induction (k-size)%nat; auto. rewrite nshiftl_size; auto. simpl; rewrite IHn; auto. @@ -177,7 +177,7 @@ Section Basics. nshiftr x n = 0 -> nshiftr x p = 0. Proof. intros. - replace p with ((p-n)+n)%nat by omega. + replace p with ((p-n)+n)%nat by lia. induction (p-n)%nat. simpl; auto. simpl; rewrite IHn0; auto. @@ -188,7 +188,7 @@ Section Basics. Proof. intros. apply nshiftr_predsize_0_firstl. - apply nshiftr_0_propagates with n; auto; omega. + apply nshiftr_0_propagates with n; auto; lia. Qed. (** * Some induction principles over [int31] *) @@ -207,8 +207,8 @@ Section Basics. rewrite sneakl_shiftr. apply H0. change (P (nshiftr x (S (size - S n)))). - replace (S (size - S n))%nat with (size - n)%nat by omega. - apply IHn; omega. + replace (S (size - S n))%nat with (size - n)%nat by lia. + apply IHn; lia. change x with (nshiftr x (size-size)); auto. Qed. @@ -253,7 +253,7 @@ Section Basics. destruct (iszero (nshiftr x (size - S n))); auto. f_equal. change (shiftr (nshiftr x (size - S n))) with (nshiftr x (S (size - S n))). - replace (S (size - S n))%nat with (size - n)%nat by omega. + replace (S (size - S n))%nat with (size - n)%nat by lia. apply IHn; auto with arith. Qed. @@ -434,8 +434,8 @@ Section Basics. unfold phibis_aux, recrbis_aux; fold recrbis_aux; fold (phibis_aux n (shiftr x)). destruct (firstr x). - specialize IHn with (shiftr x); rewrite Z.double_spec; omega. - specialize IHn with (shiftr x); rewrite Z.succ_double_spec; omega. + specialize IHn with (shiftr x); rewrite Z.double_spec; lia. + specialize IHn with (shiftr x); rewrite Z.succ_double_spec; lia. Qed. Lemma phibis_aux_bounded : @@ -448,16 +448,16 @@ Section Basics. unfold phibis_aux, recrbis_aux; fold recrbis_aux; fold (phibis_aux n (shiftr (nshiftr x (size - S n)))). assert (shiftr (nshiftr x (size - S n)) = nshiftr x (size-n)). - replace (size - n)%nat with (S (size - (S n))) by omega. + replace (size - n)%nat with (S (size - (S n))) by lia. simpl; auto. rewrite H0. - assert (H1 : n <= size) by omega. + assert (H1 : n <= size) by lia. specialize (IHn x H1). set (y:=phibis_aux n (nshiftr x (size - n))) in *. rewrite Nat2Z.inj_succ, Z.pow_succ_r; auto with zarith. case_eq (firstr (nshiftr x (size - S n))); intros. - rewrite Z.double_spec; auto with zarith. - rewrite Z.succ_double_spec; auto with zarith. + rewrite Z.double_spec. lia. + rewrite Z.succ_double_spec; lia. Qed. Lemma phi_nonneg : forall x, (0 <= phi x)%Z. @@ -485,7 +485,7 @@ Section Basics. intros. unfold nshiftr in H; simpl in *. unfold phibis_aux, recrbis_aux. - rewrite H, Z.succ_double_spec; omega. + rewrite H, Z.succ_double_spec; lia. intros. remember (S n) as m. @@ -499,8 +499,8 @@ Section Basics. destruct (firstr x). change (Z.double (phibis_aux (S n) (shiftr x))) with (2*(phibis_aux (S n) (shiftr x)))%Z. - omega. - rewrite Z.succ_double_spec; omega. + lia. + rewrite Z.succ_double_spec; lia. Qed. Lemma phi_lowerbound : @@ -536,7 +536,7 @@ Section Basics. EqShiftL k x y -> EqShiftL k' x y. Proof. unfold EqShiftL; intros. - replace k' with ((k'-k)+k)%nat by omega. + replace k' with ((k'-k)+k)%nat by lia. remember (k'-k)%nat as n. clear Heqn H k'. induction n; simpl; auto. @@ -627,18 +627,18 @@ Section Basics. unfold shiftl; rewrite i2l_sneakl. simpl cstlist. rewrite <- app_comm_cons; f_equal. - rewrite IHn; [ | omega]. + rewrite IHn; [ | lia]. rewrite removelast_app. apply f_equal. - replace (size-n)%nat with (S (size - S n))%nat by omega. + replace (size-n)%nat with (S (size - S n))%nat by lia. rewrite removelast_firstn; auto. - rewrite i2l_length; omega. + rewrite i2l_length; lia. generalize (firstn_length (size-n) (i2l x)). rewrite i2l_length. intros H0 H1. rewrite H1 in H0. - rewrite min_l in H0 by omega. + rewrite min_l in H0 by lia. simpl length in H0. - omega. + lia. Qed. (** [i2l] can be used to define a relation equivalent to [EqShiftL] *) @@ -649,12 +649,12 @@ Section Basics. intros. destruct (le_lt_dec size k) as [Hle|Hlt]. split; intros. - replace (size-k)%nat with O by omega. + replace (size-k)%nat with O by lia. unfold firstn; auto. apply EqShiftL_size; auto. unfold EqShiftL. - assert (k <= size) by omega. + assert (k <= size) by lia. split; intros. assert (i2l (nshiftl x k) = i2l (nshiftl y k)) by (f_equal; auto). rewrite 2 i2l_nshiftl in H1; auto. @@ -679,7 +679,7 @@ Section Basics. rewrite 2 EqShiftL_i2l. unfold twice_plus_one. rewrite 2 i2l_sneakl. - replace (size-k)%nat with (S (size - S k))%nat by omega. + replace (size-k)%nat with (S (size - S k))%nat by lia. remember (size - S k)%nat as n. remember (i2l x) as lx. remember (i2l y) as ly. @@ -688,8 +688,8 @@ Section Basics. split; intros. injection H; auto. f_equal; auto. - subst ly n; rewrite i2l_length; omega. - subst lx n; rewrite i2l_length; omega. + subst ly n; rewrite i2l_length; lia. + subst lx n; rewrite i2l_length; lia. Qed. Lemma EqShiftL_shiftr : forall k x y, EqShiftL k x y -> @@ -704,13 +704,13 @@ Section Basics. rewrite <- sneakl_shiftr. rewrite (EqShiftL_firstr k x y); auto. rewrite <- sneakl_shiftr; auto. - omega. + lia. rewrite <- EqShiftL_twice_plus_one. unfold twice_plus_one; rewrite <- H0. rewrite <- sneakl_shiftr. rewrite (EqShiftL_firstr k x y); auto. rewrite <- sneakl_shiftr; auto. - omega. + lia. Qed. Lemma EqShiftL_incrbis : forall n k x y, n<=size -> @@ -725,13 +725,13 @@ Section Basics. unfold incrbis_aux; simpl; fold (incrbis_aux n (shiftr x)); fold (incrbis_aux n (shiftr y)). - rewrite (EqShiftL_firstr k x y); auto; try omega. + rewrite (EqShiftL_firstr k x y); auto; try lia. case_eq (firstr y); intros. rewrite EqShiftL_twice_plus_one. apply EqShiftL_shiftr; auto. rewrite EqShiftL_twice. - apply IHn; try omega. + apply IHn; try lia. apply EqShiftL_shiftr; auto. Qed. @@ -840,18 +840,18 @@ Section Basics. unfold phibis_aux, recrbis_aux; fold recrbis_aux; fold (phibis_aux n (shiftr (nshiftr x (size-S n)))). assert (shiftr (nshiftr x (size - S n)) = nshiftr x (size-n)). - replace (size - n)%nat with (S (size - (S n))); auto; omega. + replace (size - n)%nat with (S (size - (S n))); auto; lia. rewrite H0. case_eq (firstr (nshiftr x (size - S n))); intros. rewrite phi_inv_double. - rewrite IHn by omega. + rewrite IHn by lia. rewrite <- H0. remember (nshiftr x (size - S n)) as y. destruct y; simpl in H1; rewrite H1; auto. rewrite phi_inv_double_plus_one. - rewrite IHn by omega. + rewrite IHn by lia. rewrite <- H0. remember (nshiftr x (size - S n)) as y. destruct y; simpl in H1; rewrite H1; auto. @@ -928,7 +928,7 @@ Section Basics. (rewrite <- Z.pow_succ_r, <- Zpos_P_of_succ_nat; auto with zarith). rewrite (Z.mul_comm 2). - assert (n<=size)%nat by omega. + assert (n<=size)%nat by lia. destruct p; simpl; [ | | auto]; specialize (IHn p H0); generalize (p2ibis_bounded n p); @@ -937,13 +937,13 @@ Section Basics. change (Zpos p~1) with (2*Zpos p + 1)%Z. rewrite phi_twice_plus_one_firstl, Z.succ_double_spec. rewrite IHn; ring. - apply (nshiftr_0_firstl n); auto; try omega. + apply (nshiftr_0_firstl n); auto; try lia. change (Zpos p~0) with (2*Zpos p)%Z. rewrite phi_twice_firstl. change (Z.double (phi i)) with (2*(phi i))%Z. rewrite IHn; ring. - apply (nshiftr_0_firstl n); auto; try omega. + apply (nshiftr_0_firstl n); auto; try lia. Qed. (** We now prove that this [p2ibis] is related to [phi_inv_positive] *) @@ -959,8 +959,8 @@ Section Basics. specialize IHn with p; destruct (p2ibis n p); simpl @snd in *; simpl phi_inv_positive; rewrite ?EqShiftL_twice_plus_one, ?EqShiftL_twice; - replace (S (size - S n))%nat with (size - n)%nat by omega; - apply IHn; omega. + replace (S (size - S n))%nat with (size - n)%nat by lia; + apply IHn; lia. Qed. (** This gives the expected result about [phi o phi_inv], at least @@ -1008,12 +1008,12 @@ Section Basics. induction n; simpl; auto; intros. destruct p; auto; specialize IHn with p; generalize (p2ibis_bounded n p); - rewrite IHn; try omega; destruct (p2ibis n p); simpl; intros; + rewrite IHn; try lia; destruct (p2ibis n p); simpl; intros; f_equal; auto. apply double_twice_plus_one_firstl. - apply (nshiftr_0_firstl n); auto; omega. + apply (nshiftr_0_firstl n); auto; lia. apply double_twice_firstl. - apply (nshiftr_0_firstl n); auto; omega. + apply (nshiftr_0_firstl n); auto; lia. Qed. Lemma positive_to_int31_phi_inv_positive : forall p, @@ -1046,7 +1046,7 @@ Section Basics. pattern x at 1; rewrite <- (phi_inv_phi x). rewrite <- phi_inv_double. assert (0 <= Z.double (phi x)). - rewrite Z.double_spec; generalize (phi_bounded x); omega. + rewrite Z.double_spec; generalize (phi_bounded x); lia. destruct (Z.double (phi x)). simpl; auto. apply phi_phi_inv_positive. @@ -1060,7 +1060,7 @@ Section Basics. pattern x at 1; rewrite <- (phi_inv_phi x). rewrite <- phi_inv_double_plus_one. assert (0 <= Z.succ_double (phi x)). - rewrite Z.succ_double_spec; generalize (phi_bounded x); omega. + rewrite Z.succ_double_spec; generalize (phi_bounded x); lia. destruct (Z.succ_double (phi x)). simpl; auto. apply phi_phi_inv_positive. @@ -1075,7 +1075,7 @@ Section Basics. rewrite <- phi_inv_incr. assert (0 <= Z.succ (phi x)). change (Z.succ (phi x)) with ((phi x)+1)%Z; - generalize (phi_bounded x); omega. + generalize (phi_bounded x); lia. destruct (Z.succ (phi x)). simpl; auto. apply phi_phi_inv_positive. @@ -1095,7 +1095,7 @@ Section Basics. rewrite incr_twice, phi_twice_plus_one. remember (phi (complement_negative p)) as q. rewrite Z.succ_double_spec. - replace (2*q+1) with (2*(Z.succ q)-1) by omega. + replace (2*q+1) with (2*(Z.succ q)-1) by lia. rewrite <- Zminus_mod_idemp_l, <- Zmult_mod_idemp_r, IHp. rewrite Zmult_mod_idemp_r, Zminus_mod_idemp_l; auto with zarith. @@ -1203,9 +1203,7 @@ Section Int31_Specs. Qed. Lemma spec_more_than_1_digit: 1 < 31. - Proof. - auto with zarith. - Qed. + Proof. reflexivity. Qed. Lemma spec_0 : [| 0 |] = 0. Proof. @@ -1237,7 +1235,7 @@ Section Int31_Specs. assert ((X+Y) mod wB ?= X+Y <> Eq -> [+|C1 (phi_inv (X+Y))|] = X+Y). unfold interp_carry; rewrite phi_phi_inv, Z.compare_eq_iff; intros. destruct (Z_lt_le_dec (X+Y) wB). - contradict H1; auto using Zmod_small with zarith. + contradict H1; apply Zmod_small; lia. rewrite <- (Z_mod_plus_full (X+Y) (-1) wB). rewrite Zmod_small; lia. @@ -1261,7 +1259,7 @@ Section Int31_Specs. assert ((X+Y+1) mod wB ?= X+Y+1 <> Eq -> [+|C1 (phi_inv (X+Y+1))|] = X+Y+1). unfold interp_carry; rewrite phi_phi_inv, Z.compare_eq_iff; intros. destruct (Z_lt_le_dec (X+Y+1) wB). - contradict H1; auto using Zmod_small with zarith. + contradict H1; apply Zmod_small; lia. rewrite <- (Z_mod_plus_full (X+Y+1) (-1) wB). rewrite Zmod_small; lia. @@ -1399,8 +1397,7 @@ Section Int31_Specs. rewrite phi2_phi_inv2. apply Zmod_small. generalize (phi_bounded x)(phi_bounded y); intros. - change (wB^2) with (wB * wB). - auto using Z.mul_lt_mono_nonneg with zarith. + nia. Qed. Lemma spec_mul : forall x y, [|x*y|] = ([|x|] * [|y|]) mod wB. @@ -1424,7 +1421,7 @@ Section Int31_Specs. Proof. unfold div3121; intros. generalize (phi_bounded a1)(phi_bounded a2)(phi_bounded b); intros. - assert ([|b|]>0) by (auto with zarith). + assert ([|b|]>0) by lia. generalize (Z_div_mod (phi2 a1 a2) [|b|] H4) (Z_div_pos (phi2 a1 a2) [|b|] H4). unfold Z.div; destruct (Z.div_eucl (phi2 a1 a2) [|b|]). rewrite ?phi_phi_inv. @@ -1433,19 +1430,19 @@ Section Int31_Specs. change base with wB; change base with wB in H5. change (Z.pow_pos 2 31) with wB; change (Z.pow_pos 2 31) with wB in H. rewrite H5, Z.mul_comm. - replace (z0 mod wB) with z0 by (symmetry; apply Zmod_small; omega). + replace (z0 mod wB) with z0 by (symmetry; apply Zmod_small; lia). replace (z mod wB) with z; auto with zarith. symmetry; apply Zmod_small. split. - apply H7; change base with wB; auto with zarith. - apply Z.mul_lt_mono_pos_r with [|b|]; [omega| ]. + apply H7; change base with wB. nia. + apply Z.mul_lt_mono_pos_r with [|b|]; [lia| ]. rewrite Z.mul_comm. - apply Z.le_lt_trans with ([|b|]*z+z0); [omega| ]. + apply Z.le_lt_trans with ([|b|]*z+z0); [lia| ]. rewrite <- H5. - apply Z.le_lt_trans with ([|a1|]*wB+(wB-1)); [omega | ]. + apply Z.le_lt_trans with ([|a1|]*wB+(wB-1)); [lia | ]. replace ([|a1|]*wB+(wB-1)) with (wB*([|a1|]+1)-1) by ring. - assert (wB*([|a1|]+1) <= wB*[|b|]); try omega. - apply Z.mul_le_mono_nonneg; omega. + assert (wB*([|a1|]+1) <= wB*[|b|]); try lia. + apply Z.mul_le_mono_nonneg; lia. Qed. Lemma spec_div : forall a b, 0 < [|b|] -> @@ -1461,15 +1458,15 @@ Section Int31_Specs. destruct 1; intros. rewrite H1, Z.mul_comm. generalize (phi_bounded a)(phi_bounded b); intros. - replace (z0 mod wB) with z0 by (symmetry; apply Zmod_small; omega). + replace (z0 mod wB) with z0 by (symmetry; apply Zmod_small; lia). replace (z mod wB) with z; auto with zarith. symmetry; apply Zmod_small. - split; auto with zarith. - apply Z.le_lt_trans with [|a|]; auto with zarith. + split. lia. + apply Z.le_lt_trans with [|a|]. 2: lia. rewrite H1. - apply Z.le_trans with ([|b|]*z); try omega. + apply Z.le_trans with ([|b|]*z); try lia. rewrite <- (Z.mul_1_l z) at 1. - apply Z.mul_le_mono_nonneg; auto with zarith. + nia. Qed. Lemma spec_mod : forall a b, 0 < [|b|] -> @@ -1483,7 +1480,7 @@ Section Int31_Specs. rewrite ?phi_phi_inv. destruct 1; intros. generalize (phi_bounded b); intros. - apply Zmod_small; omega. + apply Zmod_small; lia. Qed. Lemma phi_gcd : forall i j, @@ -1498,7 +1495,7 @@ Section Int31_Specs. generalize (phi_bounded j)(phi_bounded i); intros. case_eq [|j|]; intros. simpl; intros. - generalize (Zabs_spec [|i|]); omega. + generalize (Zabs_spec [|i|]); lia. simpl. rewrite IHn, H1; f_equal. rewrite spec_mod, H1; auto. rewrite H1; compute; auto. @@ -1514,9 +1511,9 @@ Section Int31_Specs. unfold Zgcd_bound. generalize (phi_bounded b). destruct [|b|]. - unfold size; auto with zarith. + unfold size; lia. intros (_,H). - cut (Pos.size_nat p <= size)%nat; [ omega | rewrite <- Zpower2_Psize; auto]. + cut (Pos.size_nat p <= size)%nat; [ lia | rewrite <- Zpower2_Psize; auto]. intros (H,_); compute in H; elim H; auto. Qed. @@ -1544,9 +1541,7 @@ Section Int31_Specs. change (iter_nat (S (Z.abs_nat z) + (Z.abs_nat z))%nat A f a = iter_nat (Z.abs_nat (Z.succ_double z)) A f a); f_equal. rewrite Z.succ_double_spec, <- Z.add_diag. - rewrite Zabs2Nat.inj_add; auto with zarith. - rewrite Zabs2Nat.inj_add; auto with zarith. - change (Z.abs_nat 1) with 1%nat; omega. + lia. Qed. Fixpoint addmuldiv31_alt n i j := @@ -1594,7 +1589,7 @@ Section Int31_Specs. symmetry; apply Zdiv_small; apply phi_bounded. simpl addmuldiv31_alt; intros. - rewrite IHn; [ | omega ]. + rewrite IHn; [ | lia ]. case_eq (firstl y); intros. rewrite phi_twice, Z.double_spec. @@ -1606,8 +1601,9 @@ Section Int31_Specs. f_equal. ring. replace (31-Z.of_nat n) with (Z.succ(31-Z.succ(Z.of_nat n))) by ring. - rewrite Z.pow_succ_r, <- Zdiv_Zdiv; auto with zarith. + rewrite Z.pow_succ_r, <- Zdiv_Zdiv. rewrite Z.mul_comm, Z_div_mult; auto with zarith. + lia. auto with zarith. lia. rewrite phi_twice_plus_one, Z.succ_double_spec. rewrite phi_twice; auto. @@ -1622,49 +1618,49 @@ Section Int31_Specs. clear - H. symmetry. apply Zmod_unique with 1; [ | ring ]. generalize (phi_lowerbound _ H) (phi_bounded y). set (wB' := 2^Z.of_nat (pred size)). - replace wB with (2*wB'); [ omega | ]. + replace wB with (2*wB'); [ lia | ]. unfold wB'. rewrite <- Z.pow_succ_r, <- Nat2Z.inj_succ by (auto with zarith). f_equal. rewrite H1. replace wB with (2^(Z.of_nat n)*2^(31-Z.of_nat n)) by - (rewrite <- Zpower_exp; auto with zarith; f_equal; unfold size; ring). + (rewrite <- Zpower_exp by lia; f_equal; unfold size; ring). unfold Z.sub; rewrite <- Z.mul_opp_l. - rewrite Z_div_plus; auto with zarith. + rewrite Z_div_plus. ring_simplify. replace (31+-Z.of_nat n) with (Z.succ(31-Z.succ(Z.of_nat n))) by ring. - rewrite Z.pow_succ_r, <- Zdiv_Zdiv; auto with zarith. + rewrite Z.pow_succ_r, <- Zdiv_Zdiv. rewrite Z.mul_comm, Z_div_mult; auto with zarith. + lia. auto with zarith. lia. + apply Z.lt_gt; apply Z.pow_pos_nonneg; lia. Qed. Lemma shift_unshift_mod_2 : forall n p a, 0 <= p <= n -> ((a * 2 ^ (n - p)) mod (2^n) / 2 ^ (n - p)) mod (2^n) = a mod 2 ^ p. Proof. - intros. + intros n p a H. + assert (2 ^ n > 0 /\ 2 ^ p > 0 /\ 2 ^ (n - p) > 0) as [ X [ Y Z ] ] + by (split; [ | split ]; apply Z.lt_gt, Z.pow_pos_nonneg; lia). rewrite Zmod_small. - rewrite Zmod_eq by (auto with zarith). + rewrite Zmod_eq by assumption. unfold Z.sub at 1. - rewrite Z_div_plus_full_l - by (cut (0 < 2^(n-p)); auto with zarith). + rewrite Z_div_plus_full_l by lia. assert (2^n = 2^(n-p)*2^p). - rewrite <- Zpower_exp by (auto with zarith). - replace (n-p+p) with n; auto with zarith. + rewrite <- Zpower_exp by lia. + replace (n-p+p) with n; lia. rewrite H0. - rewrite <- Zdiv_Zdiv, Z_div_mult by (auto with zarith). + rewrite <- Zdiv_Zdiv, Z_div_mult; auto with zarith. rewrite (Z.mul_comm (2^(n-p))), Z.mul_assoc. rewrite <- Z.mul_opp_l. - rewrite Z_div_mult by (auto with zarith). + rewrite Z_div_mult by assumption. symmetry; apply Zmod_eq; auto with zarith. remember (a * 2 ^ (n - p)) as b. destruct (Z_mod_lt b (2^n)); auto with zarith. split. apply Z_div_pos; auto with zarith. - apply Zdiv_lt_upper_bound; auto with zarith. - apply Z.lt_le_trans with (2^n); auto with zarith. - rewrite <- (Z.mul_1_r (2^n)) at 1. - apply Z.mul_le_mono_nonneg; auto with zarith. - cut (0 < 2 ^ (n-p)); auto with zarith. + apply Zdiv_lt_upper_bound. lia. + nia. Qed. Lemma spec_pos_mod : forall w p, @@ -1676,28 +1672,28 @@ Section Int31_Specs. intros. generalize (phi_bounded w). symmetry; apply Zmod_small. - split; auto with zarith. - apply Z.lt_le_trans with wB; auto with zarith. + split. lia. + apply Z.lt_le_trans with wB. lia. apply Zpower_le_monotone; auto with zarith. intros. case_eq ([|p|] ?= 31); intros; [ apply H; rewrite (Z.compare_eq _ _ H0); auto with zarith | | - apply H; change ([|p|]>31)%Z in H0; auto with zarith ]. + apply H; change ([|p|]>31)%Z in H0; lia ]. change ([|p|]<31) in H0. - rewrite spec_add_mul_div by auto with zarith. + rewrite spec_add_mul_div by lia. change [|0|] with 0%Z; rewrite Z.mul_0_l, Z.add_0_l. generalize (phi_bounded p)(phi_bounded w); intros. assert (31-[|p|]<wB). - apply Z.le_lt_trans with 31%Z; auto with zarith. + apply Z.le_lt_trans with 31%Z. lia. compute; auto. assert ([|31-p|]=31-[|p|]). unfold sub31; rewrite phi_phi_inv. change [|31|] with 31%Z. - apply Zmod_small; auto with zarith. - rewrite spec_add_mul_div by (rewrite H4; auto with zarith). + apply Zmod_small. lia. + rewrite spec_add_mul_div by (rewrite H4; lia). change [|0|] with 0%Z; rewrite Zdiv_0_l, Z.add_0_r. rewrite H4. - apply shift_unshift_mod_2; simpl; auto with zarith. + apply shift_unshift_mod_2; simpl; lia. Qed. @@ -1744,20 +1740,20 @@ Section Int31_Specs. rewrite phi_phi_inv. apply Zmod_small. split. - change 0 with (Z.of_nat O); apply inj_le; omega. + change 0 with (Z.of_nat O); apply inj_le; lia. apply Z.le_lt_trans with (Z.of_nat 31). - apply inj_le; omega. + apply inj_le; lia. compute; auto. case_eq (firstl x); intros; auto. rewrite plus_Sn_m, plus_n_Sm. - replace (S (31 - S n)) with (31 - n)%nat by omega. - rewrite <- IHn; [ | omega | ]. + replace (S (31 - S n)) with (31 - n)%nat by lia. + rewrite <- IHn; [ | lia | ]. f_equal; f_equal. unfold add31. rewrite H1. f_equal. change [|In|] with 1. - replace (31-n)%nat with (S (31 - S n))%nat by omega. + replace (31-n)%nat with (S (31 - S n))%nat by lia. rewrite Nat2Z.inj_succ; ring. clear - H H2. @@ -1774,7 +1770,7 @@ Section Int31_Specs. assert ([|x|]<>0%Z). contradict H. rewrite <- (phi_inv_phi x); rewrite H; auto. - generalize (phi_bounded x); auto with zarith. + generalize (phi_bounded x); lia. Qed. Lemma spec_head0 : forall x, 0 < [|x|] -> @@ -1806,7 +1802,7 @@ Section Int31_Specs. rewrite <- nshiftl_S_tail; auto. change (2^(Z.of_nat 0)) with 1; rewrite Z.mul_1_l. - generalize (phi_bounded x); unfold size; split; auto with zarith. + generalize (phi_bounded x); unfold size; split. 2: lia. change (2^(Z.of_nat 31)/2) with (2^(Z.of_nat (pred size))). apply phi_lowerbound; auto. Qed. @@ -1852,20 +1848,20 @@ Section Int31_Specs. rewrite phi_phi_inv. apply Zmod_small. split. - change 0 with (Z.of_nat O); apply inj_le; omega. + change 0 with (Z.of_nat O); apply inj_le; lia. apply Z.le_lt_trans with (Z.of_nat 31). - apply inj_le; omega. + apply inj_le; lia. compute; auto. case_eq (firstr x); intros; auto. rewrite plus_Sn_m, plus_n_Sm. - replace (S (31 - S n)) with (31 - n)%nat by omega. - rewrite <- IHn; [ | omega | ]. + replace (S (31 - S n)) with (31 - n)%nat by lia. + rewrite <- IHn; [ | lia | ]. f_equal; f_equal. unfold add31. rewrite H1. f_equal. change [|In|] with 1. - replace (31-n)%nat with (S (31 - S n))%nat by omega. + replace (31-n)%nat with (S (31 - S n))%nat by lia. rewrite Nat2Z.inj_succ; ring. clear - H H2. @@ -1905,7 +1901,7 @@ Section Int31_Specs. exists [|shiftr x|]. split. - generalize (phi_bounded (shiftr x)); auto with zarith. + generalize (phi_bounded (shiftr x)); lia. rewrite phi_eqn2; auto. rewrite Z.succ_double_spec; simpl; ring. Qed. @@ -1918,7 +1914,7 @@ Section Int31_Specs. Lemma quotient_by_2 a: a - 1 <= (a/2) + (a/2). Proof. case (Z_mod_lt a 2); auto with zarith. - intros H1; rewrite Zmod_eq_full; auto with zarith. + intros H1; rewrite Zmod_eq_full; lia. Qed. Lemma sqrt_main_trick j k: 0 <= j -> 0 <= k -> @@ -1933,16 +1929,16 @@ Section Int31_Specs. generalize (sqr_pos (Z.succ j / 2)) (quotient_by_2 (Z.succ j)); unfold Z.succ. rewrite Z.pow_2_r, Z.mul_add_distr_r; repeat rewrite Z.mul_add_distr_l. - auto with zarith. + lia. intros k Hk _. replace ((Z.succ j + Z.succ k) / 2) with ((j + k)/2 + 1). generalize (Hrec Hj k Hk) (quotient_by_2 (j + k)). unfold Z.succ; repeat rewrite Z.pow_2_r; repeat rewrite Z.mul_add_distr_r; repeat rewrite Z.mul_add_distr_l. repeat rewrite Z.mul_1_l; repeat rewrite Z.mul_1_r. - auto with zarith. - rewrite Z.add_comm, <- Z_div_plus_full_l; auto with zarith. - apply f_equal2 with (f := Z.div); auto with zarith. + lia. + rewrite Z.add_comm, <- Z_div_plus_full_l by lia. + apply f_equal2 with (f := Z.div); lia. Qed. Lemma sqrt_main i j: 0 <= i -> 0 < j -> i < ((j + (i/j))/2 + 1) ^ 2. @@ -1956,25 +1952,25 @@ Section Int31_Specs. Lemma sqrt_init i: 1 < i -> i < (i/2 + 1) ^ 2. Proof. intros Hi. - assert (H1: 0 <= i - 2) by auto with zarith. - assert (H2: 1 <= (i / 2) ^ 2); auto with zarith. - replace i with (1* 2 + (i - 2)); auto with zarith. - rewrite Z.pow_2_r, Z_div_plus_full_l; auto with zarith. + assert (H1: 0 <= i - 2) by lia. + assert (H2: 1 <= (i / 2) ^ 2). + replace i with (1* 2 + (i - 2)) by lia. + rewrite Z.pow_2_r, Z_div_plus_full_l by lia. generalize (sqr_pos ((i - 2)/ 2)) (Z_div_pos (i - 2) 2). rewrite Z.mul_add_distr_r; repeat rewrite Z.mul_add_distr_l. - auto with zarith. + lia. generalize (quotient_by_2 i). rewrite Z.pow_2_r in H2 |- *; repeat (rewrite Z.mul_add_distr_r || rewrite Z.mul_add_distr_l || rewrite Z.mul_1_l || rewrite Z.mul_1_r). - auto with zarith. + lia. Qed. Lemma sqrt_test_true i j: 0 <= i -> 0 < j -> i/j >= j -> j ^ 2 <= i. Proof. intros Hi Hj Hd; rewrite Z.pow_2_r. - apply Z.le_trans with (j * (i/j)); auto with zarith. + apply Z.le_trans with (j * (i/j)). nia. apply Z_mult_div_ge; auto with zarith. Qed. @@ -1982,7 +1978,7 @@ Section Int31_Specs. Proof. intros Hi Hj H; case (Z.le_gt_cases j ((j + (i/j))/2)); auto. intros H1; contradict H; apply Z.le_ngt. - assert (2 * j <= j + (i/j)); auto with zarith. + assert (2 * j <= j + (i/j)). 2: lia. apply Z.le_trans with (2 * ((j + (i/j))/2)); auto with zarith. apply Z_mult_div_ge; auto with zarith. Qed. @@ -2001,8 +1997,7 @@ Section Int31_Specs. Lemma div31_phi i j: 0 < [|j|] -> [|fst (i/j)%int31|] = [|i|]/[|j|]. intros Hj; generalize (spec_div i j Hj). case div31; intros q r; simpl @fst. - intros (H1,H2); apply Zdiv_unique with [|r|]; auto with zarith. - rewrite H1; ring. + intros (H1,H2); apply Zdiv_unique with [|r|]; lia. Qed. Lemma sqrt31_step_correct rec i j: @@ -2016,24 +2011,27 @@ Section Int31_Specs. assert (Hp2: 0 < [|2|]) by exact (eq_refl Lt). intros Hi Hj Hij H31 Hrec; rewrite sqrt31_step_def. rewrite spec_compare, div31_phi; auto. - case Z.compare_spec; auto; intros Hc; - try (split; auto; apply sqrt_test_true; auto with zarith; fail). + case Z.compare_spec; intros Hc. + 1, 3: split; [ apply sqrt_test_true; lia | assumption ]. assert (E : [|(j + fst (i / j)%int31)|] = [|j|] + [|i|] / [|j|]). - { rewrite spec_add, div31_phi; auto using Z.mod_small with zarith. } - apply Hrec; rewrite !div31_phi, E; auto using sqrt_main with zarith. - split; try apply sqrt_test_false; auto with zarith. + { rewrite spec_add, div31_phi by lia. apply Z.mod_small. split. 2: lia. + generalize (Z.div_pos [|i|] [|j|]); lia. } + apply Hrec; rewrite !div31_phi, E; auto. + 2: apply sqrt_main; lia. + split. 2: apply sqrt_test_false; lia. apply Z.le_succ_l in Hj. change (1 <= [|j|]) in Hj. Z.le_elim Hj. - replace ([|j|] + [|i|]/[|j|]) with (1 * 2 + (([|j|] - 2) + [|i|] / [|j|])) by ring. - rewrite Z_div_plus_full_l; auto with zarith. - assert (0 <= [|i|]/ [|j|]) by auto with zarith. - assert (0 <= ([|j|] - 2 + [|i|] / [|j|]) / [|2|]); auto with zarith. + rewrite Z_div_plus_full_l by lia. + assert (0 <= [|i|]/ [|j|]) by (generalize (Z.div_pos [|i|] [|j|]); lia). + assert (0 <= ([|j|] - 2 + [|i|] / [|j|]) / [|2|]). 2: lia. + apply Z.div_pos; lia. - rewrite <- Hj, Zdiv_1_r. replace (1 + [|i|]) with (1 * 2 + ([|i|] - 1)) by ring. - rewrite Z_div_plus_full_l; auto with zarith. - assert (0 <= ([|i|] - 1) /2) by auto with zarith. - change ([|2|]) with 2; auto with zarith. + rewrite Z_div_plus_full_l by lia. + assert (0 <= ([|i|] - 1) /2) by (apply Z.div_pos; lia). + change [|2|] with 2. lia. Qed. Lemma iter31_sqrt_correct n rec i j: 0 < [|i|] -> 0 < [|j|] -> @@ -2044,18 +2042,16 @@ Section Int31_Specs. [|iter31_sqrt n rec i j|] ^ 2 <= [|i|] < ([|iter31_sqrt n rec i j|] + 1) ^ 2. Proof. revert rec i j; elim n; unfold iter31_sqrt; fold iter31_sqrt; clear n. - intros rec i j Hi Hj Hij H31 Hrec; apply sqrt31_step_correct; auto with zarith. - intros; apply Hrec; auto with zarith. - rewrite Z.pow_0_r; auto with zarith. + intros rec i j Hi Hj Hij H31 Hrec; apply sqrt31_step_correct; auto. + intros; apply Hrec. 2: rewrite Z.pow_0_r. 1-4: lia. intros n Hrec rec i j Hi Hj Hij H31 HHrec. apply sqrt31_step_correct; auto. - intros j1 Hj1 Hjp1; apply Hrec; auto with zarith. + intros j1 Hj1 Hjp1; apply Hrec. 1-4: lia. intros j2 Hj2 H2j2 Hjp2 Hj31; apply Hrec; auto with zarith. intros j3 Hj3 Hpj3. apply HHrec; auto. - rewrite Nat2Z.inj_succ, Z.pow_succ_r. - apply Z.le_trans with (2 ^Z.of_nat n + [|j2|]); auto with zarith. - apply Nat2Z.is_nonneg. + rewrite Nat2Z.inj_succ, Z.pow_succ_r by lia. + apply Z.le_trans with (2 ^Z.of_nat n + [|j2|]); lia. Qed. Lemma spec_sqrt : forall x, @@ -2063,13 +2059,13 @@ Section Int31_Specs. Proof. intros i; unfold sqrt31. rewrite spec_compare. case Z.compare_spec; change [|1|] with 1; - intros Hi; auto with zarith. - repeat rewrite Z.pow_2_r; auto with zarith. - apply iter31_sqrt_correct; auto with zarith. - rewrite div31_phi; change ([|2|]) with 2; auto with zarith. + intros Hi. lia. + 2: case (phi_bounded i); repeat rewrite Z.pow_2_r; auto with zarith. + apply iter31_sqrt_correct. lia. + rewrite div31_phi; change ([|2|]) with 2. 2: lia. replace ([|i|]) with (1 * 2 + ([|i|] - 2))%Z; try ring. - assert (0 <= ([|i|] - 2)/2)%Z by (apply Z_div_pos; auto with zarith). - rewrite Z_div_plus_full_l; auto with zarith. + assert (0 <= ([|i|] - 2)/2)%Z by (apply Z_div_pos; lia). + rewrite Z_div_plus_full_l; lia. rewrite div31_phi; change ([|2|]) with 2; auto with zarith. apply sqrt_init; auto. rewrite div31_phi; change ([|2|]) with 2; auto with zarith. @@ -2078,13 +2074,9 @@ Section Int31_Specs. case (phi_bounded i); auto. intros j2 H1 H2; contradict H2; apply Z.lt_nge. rewrite div31_phi; change ([|2|]) with 2; auto with zarith. - apply Z.le_lt_trans with ([|i|]); auto with zarith. - assert (0 <= [|i|]/2)%Z by (apply Z_div_pos; auto with zarith). - apply Z.le_trans with (2 * ([|i|]/2)); auto with zarith. - apply Z_mult_div_ge; auto with zarith. - case (phi_bounded i); unfold size; auto with zarith. - change [|0|] with 0; auto with zarith. - case (phi_bounded i); repeat rewrite Z.pow_2_r; auto with zarith. + case (phi_bounded i); unfold size; intros X Y. + apply Z.lt_le_trans with ([|i|]). apply Z.div_lt; lia. + lia. Qed. Lemma sqrt312_step_def rec ih il j: @@ -2113,12 +2105,12 @@ Section Int31_Specs. case (phi_bounded j); intros Hbj _. case (phi_bounded il); intros Hbil _. case (phi_bounded ih); intros Hbih Hbih1. - assert ([|ih|] < [|j|] + 1); auto with zarith. + assert ([|ih|] < [|j|] + 1). 2: lia. apply Z.square_lt_simpl_nonneg; auto with zarith. rewrite <- ?Z.pow_2_r; apply Z.le_lt_trans with (2 := H1). apply Z.le_trans with ([|ih|] * wB). - - rewrite ? Z.pow_2_r; auto with zarith. - - unfold phi2. change base with wB; auto with zarith. + - rewrite ? Z.pow_2_r; nia. + - unfold phi2. change base with wB; lia. Qed. Lemma div312_phi ih il j: (2^30 <= [|j|] -> [|ih|] < [|j|] -> @@ -2145,59 +2137,59 @@ Section Int31_Specs. case (phi_bounded il); intros Hil1 _. case (phi_bounded j); intros _ Hj1. assert (Hp3: (0 < phi2 ih il)). - { unfold phi2; apply Z.lt_le_trans with ([|ih|] * base); auto with zarith. - apply Z.mul_pos_pos; auto with zarith. - apply Z.lt_le_trans with (2:= Hih); auto with zarith. } + { unfold phi2; apply Z.lt_le_trans with ([|ih|] * base). 2: lia. + apply Z.mul_pos_pos. lia. auto with zarith. } rewrite spec_compare. case Z.compare_spec; intros Hc1. - split; auto. apply sqrt_test_true; auto. + unfold phi2, base; auto with zarith. + unfold phi2; rewrite Hc1. assert (0 <= [|il|]/[|j|]) by (apply Z_div_pos; auto with zarith). - rewrite Z.mul_comm, Z_div_plus_full_l; auto with zarith. - change base with wB. auto with zarith. + rewrite Z.mul_comm, Z_div_plus_full_l by lia. + change base with wB. lia. - case (Z.le_gt_cases (2 ^ 30) [|j|]); intros Hjj. + rewrite spec_compare; case Z.compare_spec; - rewrite div312_phi; auto; intros Hc; - try (split; auto; apply sqrt_test_true; auto with zarith; fail). + rewrite div312_phi; auto; intros Hc. + 1, 3: split; auto; apply sqrt_test_true; lia. apply Hrec. - * assert (Hf1: 0 <= phi2 ih il/ [|j|]) by auto with zarith. + * assert (Hf1: 0 <= phi2 ih il/ [|j|]). { apply Z.div_pos; lia. } apply Z.le_succ_l in Hj. change (1 <= [|j|]) in Hj. Z.le_elim Hj; [ | contradict Hc; apply Z.le_ngt; - rewrite <- Hj, Zdiv_1_r; auto with zarith ]. + rewrite <- Hj, Zdiv_1_r; lia ]. assert (Hf3: 0 < ([|j|] + phi2 ih il / [|j|]) / 2). { replace ([|j|] + phi2 ih il/ [|j|]) with - (1 * 2 + (([|j|] - 2) + phi2 ih il / [|j|])); try ring. - rewrite Z_div_plus_full_l; auto with zarith. - assert (0 <= ([|j|] - 2 + phi2 ih il / [|j|]) / 2) ; - auto with zarith. } + (1 * 2 + (([|j|] - 2) + phi2 ih il / [|j|])) by ring. + rewrite Z_div_plus_full_l by lia. + assert (0 <= ([|j|] - 2 + phi2 ih il / [|j|]) / 2). + apply Z.div_pos; lia. + lia. } assert (Hf4: ([|j|] + phi2 ih il / [|j|]) / 2 < [|j|]). - { apply sqrt_test_false; auto with zarith. } + { apply sqrt_test_false; lia. } generalize (spec_add_c j (fst (div3121 ih il j))). unfold interp_carry; case add31c; intros r; - rewrite div312_phi; auto with zarith. + rewrite div312_phi by lia. { rewrite div31_phi; change [|2|] with 2; auto with zarith. intros HH; rewrite HH; clear HH; auto with zarith. } { rewrite spec_add, div31_phi; change [|2|] with 2; auto. rewrite Z.mul_1_l; intros HH. - rewrite Z.add_comm, <- Z_div_plus_full_l; auto with zarith. + rewrite Z.add_comm, <- Z_div_plus_full_l by lia. change (phi v30 * 2) with (2 ^ Z.of_nat size). - rewrite HH, Zmod_small; auto with zarith. } + rewrite HH, Zmod_small; lia. } * replace (phi _) with (([|j|] + (phi2 ih il)/([|j|]))/2); - [ apply sqrt_main; auto with zarith | ]. + [ apply sqrt_main; lia | ]. generalize (spec_add_c j (fst (div3121 ih il j))). unfold interp_carry; case add31c; intros r; - rewrite div312_phi; auto with zarith. + rewrite div312_phi by lia. { rewrite div31_phi; auto with zarith. intros HH; rewrite HH; auto with zarith. } { intros HH; rewrite <- HH. change (1 * 2 ^ Z.of_nat size) with (phi (v30) * 2). - rewrite Z_div_plus_full_l; auto with zarith. + rewrite Z_div_plus_full_l by lia. rewrite Z.add_comm. rewrite spec_add, Zmod_small. - rewrite div31_phi; auto. - - split; auto with zarith. + - split. + case (phi_bounded (fst (r/2)%int31)); case (phi_bounded v30); auto with zarith. + rewrite div31_phi; change (phi 2) with 2; auto. @@ -2209,20 +2201,20 @@ Section Int31_Specs. * rewrite Z.mul_comm; apply Z_mult_div_ge; auto with zarith. * case (phi_bounded r); auto with zarith. } + contradict Hij; apply Z.le_ngt. - assert ((1 + [|j|]) <= 2 ^ 30); auto with zarith. + assert ((1 + [|j|]) <= 2 ^ 30). lia. apply Z.le_trans with ((2 ^ 30) * (2 ^ 30)); auto with zarith. - * assert (0 <= 1 + [|j|]); auto with zarith. - apply Z.mul_le_mono_nonneg; auto with zarith. + * assert (0 <= 1 + [|j|]). lia. + apply Z.mul_le_mono_nonneg; lia. * change ((2 ^ 30) * (2 ^ 30)) with ((2 ^ 29) * base). apply Z.le_trans with ([|ih|] * base); - change wB with base in *; auto with zarith. - unfold phi2, base; auto with zarith. + change wB with base in *; + unfold phi2, base; lia. - split; auto. apply sqrt_test_true; auto. + unfold phi2, base; auto with zarith. + apply Z.le_ge; apply Z.le_trans with (([|j|] * base)/[|j|]). - * rewrite Z.mul_comm, Z_div_mult; auto with zarith. - * apply Z.ge_le; apply Z_div_ge; auto with zarith. + * rewrite Z.mul_comm, Z_div_mult; lia. + * apply Z.ge_le; apply Z_div_ge; lia. Qed. Lemma iter312_sqrt_correct n rec ih il j: @@ -2235,17 +2227,15 @@ Section Int31_Specs. Proof. revert rec ih il j; elim n; unfold iter312_sqrt; fold iter312_sqrt; clear n. intros rec ih il j Hi Hj Hij Hrec; apply sqrt312_step_correct; auto with zarith. - intros; apply Hrec; auto with zarith. - rewrite Z.pow_0_r; auto with zarith. + intros; apply Hrec. 2: rewrite Z.pow_0_r. 1-3: lia. intros n Hrec rec ih il j Hi Hj Hij HHrec. apply sqrt312_step_correct; auto. - intros j1 Hj1 Hjp1; apply Hrec; auto with zarith. + intros j1 Hj1 Hjp1; apply Hrec. 1-3: lia. intros j2 Hj2 H2j2 Hjp2; apply Hrec; auto with zarith. intros j3 Hj3 Hpj3. apply HHrec; auto. - rewrite Nat2Z.inj_succ, Z.pow_succ_r. - apply Z.le_trans with (2 ^Z.of_nat n + [|j2|]); auto with zarith. - apply Nat2Z.is_nonneg. + rewrite Nat2Z.inj_succ, Z.pow_succ_r by lia. + lia. Qed. (* Avoid expanding [iter312_sqrt] before variables in the context. *) @@ -2264,18 +2254,18 @@ Section Int31_Specs. assert (Hb: 0 <= base) by (red; intros HH; discriminate). assert (Hi2: phi2 ih il < (phi Tn + 1) ^ 2). { change ((phi Tn + 1) ^ 2) with (2^62). - apply Z.le_lt_trans with ((2^31 -1) * base + (2^31 - 1)); auto with zarith. - 2: simpl; unfold Z.pow_pos; simpl; auto with zarith. + apply Z.le_lt_trans with ((2^31 -1) * base + (2^31 - 1)). + 2: simpl; unfold Z.pow_pos; simpl; lia. case (phi_bounded ih); case (phi_bounded il); intros H1 H2 H3 H4. unfold base, Z.pow, Z.pow_pos in H2,H4; simpl in H2,H4. - unfold phi2. cbn [Z.pow Z.pow_pos Pos.iter]. auto with zarith. } + unfold phi2. nia. } case (iter312_sqrt_correct 31 (fun _ _ j => j) ih il Tn); auto with zarith. change [|Tn|] with 2147483647; auto with zarith. intros j1 _ HH; contradict HH. apply Z.lt_nge. change [|Tn|] with 2147483647; auto with zarith. change (2 ^ Z.of_nat 31) with 2147483648; auto with zarith. - case (phi_bounded j1); auto with zarith. + case (phi_bounded j1); lia. set (s := iter312_sqrt 31 (fun _ _ j : int31 => j) ih il Tn). intros Hs1 Hs2. generalize (spec_mul_c s s); case mul31c. @@ -2287,22 +2277,22 @@ Section Int31_Specs. apply Z.le_trans with (2 ^ Z.of_nat size / 4 * base). simpl; auto with zarith. apply Z.le_trans with ([|ih|] * base); auto with zarith. - unfold phi2; case (phi_bounded il); auto with zarith. + unfold phi2; case (phi_bounded il); lia. intros ih1 il1. change [||WW ih1 il1||] with (phi2 ih1 il1). intros Hihl1. generalize (spec_sub_c il il1). case sub31c; intros il2 Hil2. - rewrite spec_compare; case Z.compare_spec. - unfold interp_carry in *. + - rewrite spec_compare; case Z.compare_spec. + + unfold interp_carry in *. intros H1; split. rewrite Z.pow_2_r, <- Hihl1. unfold phi2; ring[Hil2 H1]. replace [|il2|] with (phi2 ih il - phi2 ih1 il1). rewrite Hihl1. - rewrite <-Hbin in Hs2; auto with zarith. + rewrite <-Hbin in Hs2; lia. unfold phi2; rewrite H1, Hil2; ring. - unfold interp_carry. + + unfold interp_carry. intros H1; contradict Hs1. apply Z.lt_nge; rewrite Z.pow_2_r, <-Hihl1. unfold phi2. @@ -2310,39 +2300,39 @@ Section Int31_Specs. apply Z.lt_le_trans with (([|ih|] + 1) * base + 0). rewrite Z.mul_add_distr_r, Z.add_0_r; auto with zarith. case (phi_bounded il1); intros H3 _. - apply Z.add_le_mono; auto with zarith. - unfold interp_carry in *; change (1 * 2 ^ Z.of_nat size) with base. + nia. + + unfold interp_carry in *; change (1 * 2 ^ Z.of_nat size) with base. rewrite Z.pow_2_r, <- Hihl1, Hil2. intros H1. rewrite <- Z.le_succ_l, <- Z.add_1_r in H1. Z.le_elim H1. - contradict Hs2; apply Z.le_ngt. + * contradict Hs2; apply Z.le_ngt. replace (([|s|] + 1) ^ 2) with (phi2 ih1 il1 + 2 * [|s|] + 1). unfold phi2. case (phi_bounded il); intros Hpil _. assert (Hl1l: [|il1|] <= [|il|]). - { case (phi_bounded il2); rewrite Hil2; auto with zarith. } - assert ([|ih1|] * base + 2 * [|s|] + 1 <= [|ih|] * base); auto with zarith. + { case (phi_bounded il2); rewrite Hil2; lia. } + assert ([|ih1|] * base + 2 * [|s|] + 1 <= [|ih|] * base). 2: lia. case (phi_bounded s); change (2 ^ Z.of_nat size) with base; intros _ Hps. case (phi_bounded ih1); intros Hpih1 _; auto with zarith. - apply Z.le_trans with (([|ih1|] + 2) * base); auto with zarith. + apply Z.le_trans with (([|ih1|] + 2) * base). lia. rewrite Z.mul_add_distr_r. - assert (2 * [|s|] + 1 <= 2 * base); auto with zarith. + nia. rewrite Hihl1, Hbin; auto. - split. + * split. unfold phi2; rewrite <- H1; ring. replace (base + ([|il|] - [|il1|])) with (phi2 ih il - ([|s|] * [|s|])). - rewrite <-Hbin in Hs2; auto with zarith. + rewrite <-Hbin in Hs2; lia. rewrite <- Hihl1; unfold phi2; rewrite <- H1; ring. - unfold interp_carry in Hil2 |- *. + - unfold interp_carry in Hil2 |- *. unfold interp_carry; change (1 * 2 ^ Z.of_nat size) with base. assert (Hsih: [|ih - 1|] = [|ih|] - 1). { rewrite spec_sub, Zmod_small; auto; change [|1|] with 1. case (phi_bounded ih); intros H1 H2. generalize Hih; change (2 ^ Z.of_nat size / 4) with 536870912. - split; auto with zarith. } + lia. } rewrite spec_compare; case Z.compare_spec. - rewrite Hsih. + + rewrite Hsih. intros H1; split. rewrite Z.pow_2_r, <- Hihl1. unfold phi2; rewrite <-H1. @@ -2352,7 +2342,7 @@ Section Int31_Specs. change (2 ^ Z.of_nat size) with base; ring. replace [|il2|] with (phi2 ih il - phi2 ih1 il1). rewrite Hihl1. - rewrite <-Hbin in Hs2; auto with zarith. + rewrite <-Hbin in Hs2; lia. unfold phi2. rewrite <-H1. ring_simplify. @@ -2360,9 +2350,9 @@ Section Int31_Specs. ring. rewrite <-Hil2. change (2 ^ Z.of_nat size) with base; ring. - rewrite Hsih; intros H1. + + rewrite Hsih; intros H1. assert (He: [|ih|] = [|ih1|]). - { apply Z.le_antisymm; auto with zarith. + { apply Z.le_antisymm. lia. case (Z.le_gt_cases [|ih1|] [|ih|]); auto; intros H2. contradict Hs1; apply Z.lt_nge; rewrite Z.pow_2_r, <-Hihl1. unfold phi2. @@ -2371,42 +2361,41 @@ Section Int31_Specs. apply Z.lt_le_trans with (([|ih|] + 1) * base). rewrite Z.mul_add_distr_r, Z.mul_1_l; auto with zarith. case (phi_bounded il1); intros Hpil2 _. - apply Z.le_trans with (([|ih1|]) * base); auto with zarith. } + nia. } rewrite Z.pow_2_r, <-Hihl1; unfold phi2; rewrite <-He. contradict Hs1; apply Z.lt_nge; rewrite Z.pow_2_r, <-Hihl1. unfold phi2; rewrite He. - assert (phi il - phi il1 < 0); auto with zarith. + assert (phi il - phi il1 < 0). 2: lia. rewrite <-Hil2. - case (phi_bounded il2); auto with zarith. - intros H1. + case (phi_bounded il2); lia. + + intros H1. rewrite Z.pow_2_r, <-Hihl1. - assert (H2 : [|ih1|]+2 <= [|ih|]); auto with zarith. + assert (H2 : [|ih1|]+2 <= [|ih|]). lia. Z.le_elim H2. - contradict Hs2; apply Z.le_ngt. + * contradict Hs2; apply Z.le_ngt. replace (([|s|] + 1) ^ 2) with (phi2 ih1 il1 + 2 * [|s|] + 1). unfold phi2. - assert ([|ih1|] * base + 2 * phi s + 1 <= [|ih|] * base + ([|il|] - [|il1|])); - auto with zarith. + assert ([|ih1|] * base + 2 * phi s + 1 <= [|ih|] * base + ([|il|] - [|il1|])). + 2: lia. rewrite <-Hil2. change (-1 * 2 ^ Z.of_nat size) with (-base). case (phi_bounded il2); intros Hpil2 _. - apply Z.le_trans with ([|ih|] * base + - base); auto with zarith. + apply Z.le_trans with ([|ih|] * base + - base). 2: lia. case (phi_bounded s); change (2 ^ Z.of_nat size) with base; intros _ Hps. - assert (2 * [|s|] + 1 <= 2 * base); auto with zarith. - apply Z.le_trans with ([|ih1|] * base + 2 * base); auto with zarith. - assert (Hi: ([|ih1|] + 3) * base <= [|ih|] * base); auto with zarith. - rewrite Z.mul_add_distr_r in Hi; auto with zarith. + assert (2 * [|s|] + 1 <= 2 * base). lia. + apply Z.le_trans with ([|ih1|] * base + 2 * base). lia. + assert (Hi: ([|ih1|] + 3) * base <= [|ih|] * base). nia. lia. rewrite Hihl1, Hbin; auto. - unfold phi2; rewrite <-H2. + * unfold phi2; rewrite <-H2. split. - replace [|il|] with (([|il|] - [|il1|]) + [|il1|]); try ring. + replace [|il|] with (([|il|] - [|il1|]) + [|il1|]) by ring. rewrite <-Hil2. change (-1 * 2 ^ Z.of_nat size) with (-base); ring. replace (base + [|il2|]) with (phi2 ih il - phi2 ih1 il1). rewrite Hihl1. - rewrite <-Hbin in Hs2; auto with zarith. + rewrite <-Hbin in Hs2; lia. unfold phi2; rewrite <-H2. - replace [|il|] with (([|il|] - [|il1|]) + [|il1|]); try ring. + replace [|il|] with (([|il|] - [|il1|]) + [|il1|]) by ring. rewrite <-Hil2. change (-1 * 2 ^ Z.of_nat size) with (-base); ring. Qed. @@ -2436,8 +2425,8 @@ Qed. destruct H; auto with zarith. replace ([|x|] mod 2) with [|r|]. destruct H; auto with zarith. - case Z.compare_spec; auto with zarith. - apply Zmod_unique with [|q|]; auto with zarith. + case Z.compare_spec; lia. + apply Zmod_unique with [|q|]; lia. Qed. (* Bitwise *) diff --git a/theories/Numbers/Cyclic/Int31/Ring31.v b/theories/Numbers/Cyclic/Int31/Ring31.v index 890f42d301..1069a79e76 100644 --- a/theories/Numbers/Cyclic/Int31/Ring31.v +++ b/theories/Numbers/Cyclic/Int31/Ring31.v @@ -13,7 +13,7 @@ (** * Int31 numbers defines Z/(2^31)Z, and can hence be equipped with a ring structure and a ring tactic *) -Require Import Int31 Cyclic31 CyclicAxioms. +Require Import Lia Int31 Cyclic31 CyclicAxioms. Local Open Scope int31_scope. @@ -85,10 +85,11 @@ Qed. Lemma eqb31_eq : forall x y, eqb31 x y = true <-> x=y. Proof. unfold eqb31. intros x y. -rewrite Cyclic31.spec_compare. case Z.compare_spec. -intuition. apply Int31_canonic; auto. -intuition; subst; auto with zarith; try discriminate. -intuition; subst; auto with zarith; try discriminate. +rewrite Cyclic31.spec_compare. +split. +case Z.compare_spec. +intuition. apply Int31_canonic; auto. 1-2: easy. +now intros ->; rewrite Z.compare_refl. Qed. Lemma eqb31_correct : forall x y, eqb31 x y = true -> x=y. diff --git a/theories/Numbers/Cyclic/Int63/Int63.v b/theories/Numbers/Cyclic/Int63/Int63.v index 9e9481341f..febf4fa1be 100644 --- a/theories/Numbers/Cyclic/Int63/Int63.v +++ b/theories/Numbers/Cyclic/Int63/Int63.v @@ -15,6 +15,7 @@ Require Export DoubleType. Require Import Lia. Require Import Zpow_facts. Require Import Zgcd_alt. +Require ZArith. Import Znumtheory. Register bool as kernel.ind_bool. @@ -1354,8 +1355,8 @@ Lemma sqrt_spec : forall x, Proof. intros i; unfold sqrt. rewrite compare_spec. case Z.compare_spec; rewrite to_Z_1; - intros Hi; auto with zarith. - repeat rewrite Z.pow_2_r; auto with zarith. + intros Hi. + lia. apply iter_sqrt_correct; auto with zarith; rewrite lsr_spec, to_Z_1; change (2^1) with 2; auto with zarith. replace [|i|] with (1 * 2 + ([|i|] - 2))%Z; try ring. @@ -1571,12 +1572,11 @@ Lemma sqrt2_spec : forall x y, case (to_Z_bounded il); intros Hpil _. assert (Hl1l: [|il1|] <= [|il|]). case (to_Z_bounded il2); rewrite Hil2; auto with zarith. - assert ([|ih1|] * wB + 2 * [|s|] + 1 <= [|ih|] * wB); auto with zarith. + enough ([|ih1|] * wB + 2 * [|s|] + 1 <= [|ih|] * wB) by lia. case (to_Z_bounded s); intros _ Hps. - case (to_Z_bounded ih1); intros Hpih1 _; auto with zarith. - apply Z.le_trans with (([|ih1|] + 2) * wB); auto with zarith. - rewrite Zmult_plus_distr_l. - assert (2 * [|s|] + 1 <= 2 * wB); auto with zarith. + case (to_Z_bounded ih1); intros Hpih1 _. + apply Z.le_trans with (([|ih1|] + 2) * wB). lia. + auto with zarith. unfold zn2z_to_Z; rewrite <-Hihl1, Hbin; auto. intros H2; split. unfold zn2z_to_Z; rewrite <- H2; ring. @@ -1621,8 +1621,8 @@ Lemma sqrt2_spec : forall x y, case (to_Z_bounded s); intros _ Hps. assert (2 * [|s|] + 1 <= 2 * wB); auto with zarith. apply Z.le_trans with ([|ih1|] * wB + 2 * wB); auto with zarith. - assert (Hi: ([|ih1|] + 3) * wB <= [|ih|] * wB); auto with zarith. - rewrite Zmult_plus_distr_l in Hi; auto with zarith. + assert (Hi: ([|ih1|] + 3) * wB <= [|ih|] * wB) by auto with zarith. + lia. unfold zn2z_to_Z; rewrite <-Hihl1, Hbin; auto. intros H2; unfold zn2z_to_Z; rewrite <-H2. split. diff --git a/theories/Numbers/Cyclic/ZModulo/ZModulo.v b/theories/Numbers/Cyclic/ZModulo/ZModulo.v index 2785e89c5d..cf3e6668a5 100644 --- a/theories/Numbers/Cyclic/ZModulo/ZModulo.v +++ b/theories/Numbers/Cyclic/ZModulo/ZModulo.v @@ -23,6 +23,7 @@ Require Import Znumtheory. Require Import Zpow_facts. Require Import DoubleType. Require Import CyclicAxioms. +Require Import Lia. Local Open Scope Z_scope. @@ -113,7 +114,7 @@ Section ZModulo. Lemma spec_0 : [|zero|] = 0. Proof. unfold to_Z, zero. - apply Zmod_small; generalize wB_pos; auto with zarith. + apply Zmod_small; generalize wB_pos. lia. Qed. Lemma spec_1 : [|one|] = 1. @@ -128,10 +129,10 @@ Section ZModulo. Lemma spec_Bm1 : [|minus_one|] = wB - 1. Proof. unfold to_Z, minus_one. - apply Zmod_small; split; auto with zarith. + apply Zmod_small; split. 2: lia. unfold wB, base. - cut (1 <= 2 ^ Zpos digits); auto with zarith. - apply Z.le_trans with (Zpos digits); auto with zarith. + cut (1 <= 2 ^ Zpos digits). lia. + apply Z.le_trans with (Zpos digits). lia. apply Zpower2_le_lin; auto with zarith. Qed. @@ -162,7 +163,7 @@ Section ZModulo. assert (x mod wB <> 0). unfold eq0, to_Z in H. intro H0; rewrite H0 in H; discriminate. - rewrite Z_mod_nz_opp_full; auto with zarith. + rewrite Z_mod_nz_opp_full; lia. Qed. Lemma spec_opp : forall x, [|opp x|] = (-[|x|]) mod wB. @@ -175,14 +176,14 @@ Section ZModulo. Lemma spec_opp_carry : forall x, [|opp_carry x|] = wB - [|x|] - 1. Proof. intros; unfold opp_carry, to_Z; auto. - replace (- x - 1) with (- 1 - x) by omega. + replace (- x - 1) with (- 1 - x) by lia. rewrite <- Zminus_mod_idemp_r. - replace ( -1 - x mod wB) with (0 + ( -1 - x mod wB)) by omega. + replace ( -1 - x mod wB) with (0 + ( -1 - x mod wB)) by lia. rewrite <- (Z_mod_same_full wB). rewrite Zplus_mod_idemp_l. - replace (wB + (-1 - x mod wB)) with (wB - x mod wB -1) by omega. + replace (wB + (-1 - x mod wB)) with (wB - x mod wB -1) by lia. apply Zmod_small. - generalize (Z_mod_lt x wB wB_pos); omega. + generalize (Z_mod_lt x wB wB_pos); lia. Qed. Definition succ_c x := @@ -221,7 +222,7 @@ Section ZModulo. symmetry. rewrite Z.add_move_r. assert ((x+1) mod wB = 0) by (apply spec_eq0; auto). replace (wB-1) with ((wB-1) mod wB) by - (apply Zmod_small; generalize wB_pos; omega). + (apply Zmod_small; generalize wB_pos; lia). rewrite <- Zminus_mod_idemp_l; rewrite Z_mod_same; simpl; auto. apply Zmod_equal; auto. @@ -231,10 +232,10 @@ Section ZModulo. contradict H0. rewrite Z.add_move_r in H0; simpl in H0. rewrite <- Zplus_mod_idemp_l; rewrite H0. - replace (wB-1+1) with wB; auto with zarith; apply Z_mod_same; auto. + replace (wB-1+1) with wB by lia; apply Z_mod_same; auto. rewrite <- Zplus_mod_idemp_l. apply Zmod_small. - generalize (Z_mod_lt x wB wB_pos); omega. + generalize (Z_mod_lt x wB wB_pos); lia. Qed. Lemma spec_add_c : forall x y, [+|add_c x y|] = [|x|] + [|y|]. @@ -242,10 +243,10 @@ Section ZModulo. intros; unfold add_c, to_Z, interp_carry. destruct Z_lt_le_dec. apply Zmod_small; - generalize (Z_mod_lt x wB wB_pos) (Z_mod_lt y wB wB_pos); omega. + generalize (Z_mod_lt x wB wB_pos) (Z_mod_lt y wB wB_pos); lia. rewrite Z.mul_1_l, Z.add_comm, Z.add_move_r. apply Zmod_small; - generalize (Z_mod_lt x wB wB_pos) (Z_mod_lt y wB wB_pos); omega. + generalize (Z_mod_lt x wB wB_pos) (Z_mod_lt y wB wB_pos); lia. Qed. Lemma spec_add_carry_c : forall x y, [+|add_carry_c x y|] = [|x|] + [|y|] + 1. @@ -253,10 +254,10 @@ Section ZModulo. intros; unfold add_carry_c, to_Z, interp_carry. destruct Z_lt_le_dec. apply Zmod_small; - generalize (Z_mod_lt x wB wB_pos) (Z_mod_lt y wB wB_pos); omega. + generalize (Z_mod_lt x wB wB_pos) (Z_mod_lt y wB wB_pos); lia. rewrite Z.mul_1_l, Z.add_comm, Z.add_move_r. apply Zmod_small; - generalize (Z_mod_lt x wB wB_pos) (Z_mod_lt y wB wB_pos); omega. + generalize (Z_mod_lt x wB wB_pos) (Z_mod_lt y wB wB_pos); lia. Qed. Lemma spec_succ : forall x, [|succ x|] = ([|x|] + 1) mod wB. @@ -299,14 +300,14 @@ Section ZModulo. intros; unfold pred_c, to_Z, interp_carry. case_eq (eq0 x); intros. fold [|x|]; rewrite spec_eq0; auto. - replace ((wB-1) mod wB) with (wB-1); auto with zarith. - symmetry; apply Zmod_small; generalize wB_pos; omega. + replace ((wB-1) mod wB) with (wB-1). lia. + symmetry; apply Zmod_small; generalize wB_pos; lia. assert (x mod wB <> 0). unfold eq0, to_Z in *; now destruct (x mod wB). rewrite <- Zminus_mod_idemp_l. apply Zmod_small. - generalize (Z_mod_lt x wB wB_pos); omega. + generalize (Z_mod_lt x wB wB_pos); lia. Qed. Lemma spec_sub_c : forall x y, [-|sub_c x y|] = [|x|] - [|y|]. @@ -315,12 +316,12 @@ Section ZModulo. destruct Z_lt_le_dec. replace ((wB + (x mod wB - y mod wB)) mod wB) with (wB + (x mod wB - y mod wB)). - omega. + lia. symmetry; apply Zmod_small. - generalize wB_pos (Z_mod_lt x wB wB_pos) (Z_mod_lt y wB wB_pos); omega. + generalize wB_pos (Z_mod_lt x wB wB_pos) (Z_mod_lt y wB wB_pos); lia. apply Zmod_small. - generalize wB_pos (Z_mod_lt x wB wB_pos) (Z_mod_lt y wB wB_pos); omega. + generalize wB_pos (Z_mod_lt x wB wB_pos) (Z_mod_lt y wB wB_pos); lia. Qed. Lemma spec_sub_carry_c : forall x y, [-|sub_carry_c x y|] = [|x|] - [|y|] - 1. @@ -329,12 +330,12 @@ Section ZModulo. destruct Z_lt_le_dec. replace ((wB + (x mod wB - y mod wB - 1)) mod wB) with (wB + (x mod wB - y mod wB -1)). - omega. + lia. symmetry; apply Zmod_small. - generalize wB_pos (Z_mod_lt x wB wB_pos) (Z_mod_lt y wB wB_pos); omega. + generalize wB_pos (Z_mod_lt x wB wB_pos) (Z_mod_lt y wB wB_pos); lia. apply Zmod_small. - generalize wB_pos (Z_mod_lt x wB wB_pos) (Z_mod_lt y wB wB_pos); omega. + generalize wB_pos (Z_mod_lt x wB wB_pos) (Z_mod_lt y wB wB_pos); lia. Qed. Lemma spec_pred : forall x, [|pred x|] = ([|x|] - 1) mod wB. @@ -381,12 +382,12 @@ Section ZModulo. subst h. split. apply Z_div_pos; auto with zarith. - apply Zdiv_lt_upper_bound; auto with zarith. + apply Zdiv_lt_upper_bound. lia. apply Z.mul_lt_mono_nonneg; auto with zarith. clear H H0 H1 H2. case_eq (eq0 h); simpl; intros. case_eq (eq0 l); simpl; intros. - rewrite <- H3, <- H4, (spec_eq0 h), (spec_eq0 l); auto with zarith. + rewrite <- H3, <- H4, (spec_eq0 h), (spec_eq0 l); auto. lia. rewrite H3, H4; auto with zarith. rewrite H3, H4; auto with zarith. Qed. @@ -409,7 +410,7 @@ Section ZModulo. 0 <= [|r|] < [|b|]. Proof. intros; unfold div. - assert ([|b|]>0) by auto with zarith. + assert ([|b|]>0) by lia. assert (Z.div_eucl [|a|] [|b|] = ([|a|]/[|b|], [|a|] mod [|b|])). unfold Z.modulo, Z.div; destruct Z.div_eucl; auto. generalize (Z_div_mod [|a|] [|b|] H0). @@ -417,7 +418,7 @@ Section ZModulo. injection H1 as [= ? ?]. assert ([|r|]=r). apply Zmod_small; generalize (Z_mod_lt b wB wB_pos); fold [|b|]; - auto with zarith. + lia. assert ([|q|]=q). apply Zmod_small. subst q. @@ -426,7 +427,7 @@ Section ZModulo. apply Zdiv_lt_upper_bound; auto with zarith. apply Z.lt_le_trans with (wB*1). rewrite Z.mul_1_r; auto with zarith. - apply Z.mul_le_mono_nonneg; generalize wB_pos; auto with zarith. + apply Z.mul_le_mono_nonneg; generalize wB_pos; lia. rewrite H5, H6; rewrite Z.mul_comm; auto with zarith. Qed. @@ -449,9 +450,9 @@ Section ZModulo. Proof. intros; unfold modulo. apply Zmod_small. - assert ([|b|]>0) by auto with zarith. + assert ([|b|]>0) by lia. generalize (Z_mod_lt [|a|] [|b|] H0) (Z_mod_lt b wB wB_pos). - fold [|b|]; omega. + fold [|b|]; lia. Qed. Lemma spec_modulo_gt : forall a b, [|a|] > [|b|] -> 0 < [|b|] -> @@ -470,19 +471,19 @@ Section ZModulo. destruct H2 as (q,H2); destruct H3 as (q',H3); clear H4. assert (H4:=Z.gcd_nonneg a b). destruct (Z.eq_dec (Z.gcd a b) 0) as [->|Hneq]. - generalize (Zmax_spec a b); omega. + generalize (Zmax_spec a b); lia. assert (0 <= q). - apply Z.mul_le_mono_pos_r with (Z.gcd a b); auto with zarith. + apply Z.mul_le_mono_pos_r with (Z.gcd a b); lia. destruct (Z.eq_dec q 0). subst q; simpl in *; subst a; simpl; auto. - generalize (Zmax_spec 0 b) (Zabs_spec b); omega. + generalize (Zmax_spec 0 b) (Zabs_spec b); lia. apply Z.le_trans with a. rewrite H2 at 2. rewrite <- (Z.mul_1_l (Z.gcd a b)) at 1. - apply Z.mul_le_mono_nonneg; auto with zarith. - generalize (Zmax_spec a b); omega. + apply Z.mul_le_mono_nonneg; lia. + generalize (Zmax_spec a b); lia. Qed. Lemma spec_gcd : forall a b, Zis_gcd [|a|] [|b|] [|gcd a b|]. @@ -497,7 +498,7 @@ Section ZModulo. apply Z.gcd_nonneg. apply Z.le_lt_trans with (Z.max [|a|] [|b|]). apply Zgcd_bound; auto with zarith. - generalize (Zmax_spec [|a|] [|b|]); omega. + generalize (Zmax_spec [|a|] [|b|]); lia. Qed. Lemma spec_gcd_gt : forall a b, [|a|] > [|b|] -> @@ -519,7 +520,7 @@ Section ZModulo. intros; unfold div21. generalize (Z_mod_lt a1 wB wB_pos); fold [|a1|]; intros. generalize (Z_mod_lt a2 wB wB_pos); fold [|a2|]; intros. - assert ([|b|]>0) by auto with zarith. + assert ([|b|]>0) by lia. remember ([|a1|]*wB+[|a2|]) as a. assert (Z.div_eucl a [|b|] = (a/[|b|], a mod [|b|])). unfold Z.modulo, Z.div; destruct Z.div_eucl; auto. @@ -528,18 +529,17 @@ Section ZModulo. injection H4 as [= ? ?]. assert ([|r|]=r). apply Zmod_small; generalize (Z_mod_lt b wB wB_pos); fold [|b|]; - auto with zarith. + lia. assert ([|q|]=q). apply Zmod_small. subst q. split. - apply Z_div_pos; auto with zarith. - subst a; auto with zarith. - apply Zdiv_lt_upper_bound; auto with zarith. + apply Z_div_pos. lia. + subst a. nia. + apply Zdiv_lt_upper_bound; nia. subst a. replace (wB*[|b|]) with (([|b|]-1)*wB + wB) by ring. - apply Z.lt_le_trans with ([|a1|]*wB+wB); auto with zarith. - rewrite H8, H9; rewrite Z.mul_comm; auto with zarith. + lia. Qed. Definition add_mul_div p x y := @@ -573,7 +573,7 @@ Section ZModulo. if is_even x then [|x|] mod 2 = 0 else [|x|] mod 2 = 1. Proof. intros; unfold is_even; destruct Z.eq_dec; auto. - generalize (Z_mod_lt [|x|] 2); omega. + generalize (Z_mod_lt [|x|] 2); lia. Qed. Definition sqrt x := Z.sqrt [|x|]. @@ -611,33 +611,33 @@ Section ZModulo. simpl zn2z_to_Z. remember ([|x|]*wB+[|y|]) as z. destruct z. - auto with zarith. - generalize (Z.sqrtrem_spec (Zpos p)). - destruct Z.sqrtrem as (s,r); intros [U V]; auto with zarith. + - auto with zarith. + - generalize (Z.sqrtrem_spec (Zpos p)). + destruct Z.sqrtrem as (s,r); intros [U V]. lia. assert (s < wB). + { destruct (Z_lt_le_dec s wB); auto. assert (wB * wB <= Zpos p). - rewrite U. - apply Z.le_trans with (s*s); try omega. - apply Z.mul_le_mono_nonneg; generalize wB_pos; auto with zarith. + apply Z.le_trans with (s*s). 2: lia. + apply Z.mul_le_mono_nonneg; generalize wB_pos; lia. assert (Zpos p < wB*wB). rewrite Heqz. replace (wB*wB) with ((wB-1)*wB+wB) by ring. - apply Z.add_le_lt_mono; auto with zarith. - apply Z.mul_le_mono_nonneg; auto with zarith. - generalize (spec_to_Z x); auto with zarith. - generalize wB_pos; auto with zarith. - omega. - replace [|s|] with s by (symmetry; apply Zmod_small; auto with zarith). + apply Z.add_le_lt_mono. 2: auto with zarith. + apply Z.mul_le_mono_nonneg. 1, 3-5: auto with zarith. + generalize wB_pos; lia. + generalize (spec_to_Z x); lia. + } + replace [|s|] with s by (symmetry; apply Zmod_small; lia). destruct Z_lt_le_dec; unfold interp_carry. - replace [|r|] with r by (symmetry; apply Zmod_small; auto with zarith). - rewrite Z.pow_2_r; auto with zarith. - replace [|r-wB|] with (r-wB) by (symmetry; apply Zmod_small; auto with zarith). - rewrite Z.pow_2_r; omega. + replace [|r|] with r by (symmetry; apply Zmod_small; lia). + rewrite Z.pow_2_r; lia. + replace [|r-wB|] with (r-wB) by (symmetry; apply Zmod_small; lia). + rewrite Z.pow_2_r; lia. - assert (0<=Zneg p). - rewrite Heqz; generalize wB_pos; auto with zarith. - compute in H0; elim H0; auto. + - assert (0<=Zneg p). + generalize (spec_to_Z x) (spec_to_Z y); nia. + lia. Qed. Lemma two_p_power2 : forall x, x>=0 -> two_p x = 2 ^ x. @@ -669,12 +669,12 @@ Section ZModulo. intros. assert (0 <= zdigits - Z.log2 (Zpos p) - 1 < wB) as Hrange. split. - cut (Z.log2 (Zpos p) < zdigits). omega. + cut (Z.log2 (Zpos p) < zdigits). lia. unfold zdigits. unfold wB, base in *. apply Z.log2_lt_pow2; intuition. apply Z.lt_trans with zdigits. - omega. + lia. unfold zdigits, wB, base; apply Zpower2_lt_lin; auto with zarith. unfold to_Z; rewrite (Zmod_small _ _ Hrange). @@ -728,7 +728,7 @@ Section ZModulo. rewrite Z.mul_comm. rewrite <- Z.pow_succ_r; auto with zarith. rewrite H1; auto. - rewrite <- H1; omega. + rewrite <- H1; lia. Qed. Definition tail0 x := diff --git a/theories/QArith/QArith_base.v b/theories/QArith/QArith_base.v index 54d35cded2..4239943d03 100644 --- a/theories/QArith/QArith_base.v +++ b/theories/QArith/QArith_base.v @@ -8,7 +8,7 @@ (* * (see LICENSE file for the text of the license) *) (************************************************************************) -Require Export ZArith. +Require Export ZArith_base. Require Export ZArithRing. Require Export Morphisms Setoid Bool. diff --git a/theories/QArith/Qround.v b/theories/QArith/Qround.v index 8d68038582..35f113e226 100644 --- a/theories/QArith/Qround.v +++ b/theories/QArith/Qround.v @@ -9,6 +9,7 @@ (************************************************************************) Require Import QArith. +Import Zdiv. Lemma Qopp_lt_compat: forall p q : Q, p < q -> - q < - p. Proof. @@ -38,7 +39,7 @@ Proof. intros z. unfold Qceiling. simpl. -rewrite Zdiv_1_r. +rewrite Z.div_1_r. apply Z.opp_involutive. Qed. @@ -50,8 +51,7 @@ unfold Qle. simpl. replace (n*1)%Z with n by ring. rewrite Z.mul_comm. -apply Z_mult_div_ge. -auto with *. +now apply Z.mul_div_le. Qed. Hint Resolve Qfloor_le : qarith. diff --git a/theories/Reals/Cos_plus.v b/theories/Reals/Cos_plus.v index d09b3248ef..b411c4953a 100644 --- a/theories/Reals/Cos_plus.v +++ b/theories/Reals/Cos_plus.v @@ -14,7 +14,7 @@ Require Import SeqSeries. Require Import Rtrigo_def. Require Import Cos_rel. Require Import Max. -Require Import Omega. +Require Import Lia. Local Open Scope nat_scope. Local Open Scope R_scope. @@ -213,7 +213,7 @@ Proof. apply le_n_S. apply plus_le_compat_l; assumption. rewrite pred_of_minus. - omega. + lia. apply Rle_trans with (sum_f_R0 (fun k:nat => @@ -236,7 +236,7 @@ Proof. apply Rmult_le_compat_l. left; apply Rinv_0_lt_compat; apply INR_fact_lt_0. apply C_maj. - omega. + lia. right. unfold Rdiv; rewrite Rmult_comm. unfold Binomial.C. @@ -248,7 +248,7 @@ Proof. unfold Rsqr; reflexivity. apply INR_fact_neq_0. apply INR_fact_neq_0. - omega. + lia. apply INR_fact_neq_0. unfold Rdiv; rewrite Rmult_comm. unfold Binomial.C. @@ -258,7 +258,7 @@ Proof. replace (2 * S (N + n) - 2 * S (n0 + n))%nat with (2 * (N - n0))%nat. rewrite mult_INR. reflexivity. - omega. + lia. apply INR_fact_neq_0. apply Rle_trans with (sum_f_R0 (fun k:nat => INR N / INR (fact (S N)) * C ^ (4 * N)) (pred N)). @@ -279,7 +279,7 @@ Proof. apply Rmult_le_compat_l. apply Rle_0_sqr. apply le_INR. - omega. + lia. rewrite Rmult_comm; unfold Rdiv; apply Rmult_le_compat_l. apply pos_INR. apply Rle_trans with (/ INR (fact (S (N + n)))). @@ -458,7 +458,7 @@ Proof. (2 * (N - n0) + 1 + (2 * S (n0 + n) + 1))%nat. repeat rewrite pow_add. ring. - omega. + lia. apply INR_fact_neq_0. apply INR_fact_neq_0. apply Rle_ge; left; apply Rinv_0_lt_compat. @@ -517,7 +517,7 @@ Proof. replace (2 * S (S (n0 + n)))%nat with (S (2 * S (n0 + n) + 1)). apply le_n_Sn. ring. - omega. + lia. right. unfold Rdiv; rewrite Rmult_comm. unfold Binomial.C. @@ -529,7 +529,7 @@ Proof. unfold Rsqr; reflexivity. apply INR_fact_neq_0. apply INR_fact_neq_0. - omega. + lia. apply INR_fact_neq_0. unfold Rdiv; rewrite Rmult_comm. unfold Binomial.C. @@ -540,7 +540,7 @@ Proof. (2 * (N - n0) + 1)%nat. rewrite mult_INR. reflexivity. - omega. + lia. apply INR_fact_neq_0. apply Rle_trans with (sum_f_R0 (fun k:nat => INR N / INR (fact (S (S N))) * C ^ (4 * S N)) @@ -563,8 +563,8 @@ Proof. apply Rle_0_sqr. replace (S (pred (N - n))) with (N - n)%nat. apply le_INR. - omega. - omega. + lia. + lia. rewrite Rmult_comm; unfold Rdiv; apply Rmult_le_compat_l. apply pos_INR. apply Rle_trans with (/ INR (fact (S (S (N + n))))). @@ -592,7 +592,7 @@ Proof. rewrite Rmult_1_r. apply le_INR. apply fact_le. - omega. + lia. apply INR_fact_neq_0. apply INR_fact_neq_0. rewrite sum_cte. diff --git a/theories/Reals/Cos_rel.v b/theories/Reals/Cos_rel.v index d5086db6cf..4ce5cd6b1c 100644 --- a/theories/Reals/Cos_rel.v +++ b/theories/Reals/Cos_rel.v @@ -12,7 +12,7 @@ Require Import Rbase. Require Import Rfunctions. Require Import SeqSeries. Require Import Rtrigo_def. -Require Import OmegaTactic. +Require Import Lia. Local Open Scope R_scope. Definition A1 (x:R) (N:nat) : R := @@ -149,13 +149,13 @@ unfold Wn. apply Rmult_eq_compat_l. replace (2 * S i - S (2 * i0))%nat with (S (2 * (i - i0))). reflexivity. -omega. +lia. apply sum_eq; intros. unfold Wn. apply Rmult_eq_compat_l. replace (2 * S i - 2 * i0)%nat with (2 * (S i - i0))%nat. reflexivity. -omega. +lia. replace (- sum_f_R0 @@ -211,7 +211,7 @@ replace (S (2 * i0)) with (2 * i0 + 1)%nat; [ apply Rmult_eq_compat_l | ring ]. replace (2 * S i - (2 * i0 + 1))%nat with (2 * (i - i0) + 1)%nat. reflexivity. -omega. +lia. apply INR_fact_neq_0. apply INR_fact_neq_0. apply INR_fact_neq_0. @@ -240,7 +240,7 @@ rewrite Rmult_1_l. rewrite Rinv_mult_distr. replace (2 * i - 2 * i0)%nat with (2 * (i - i0))%nat. reflexivity. -omega. +lia. apply INR_fact_neq_0. apply INR_fact_neq_0. apply INR_fact_neq_0. diff --git a/theories/Reals/DiscrR.v b/theories/Reals/DiscrR.v index 9205df1bb7..2ae93c8705 100644 --- a/theories/Reals/DiscrR.v +++ b/theories/Reals/DiscrR.v @@ -9,7 +9,7 @@ (************************************************************************) Require Import RIneq. -Require Import Omega. +Require Import Lia. Local Open Scope R_scope. Lemma Rlt_R0_R2 : 0 < 2. @@ -49,7 +49,7 @@ Ltac omega_sup := repeat rewrite <- plus_IZR || rewrite <- mult_IZR || rewrite <- Ropp_Ropp_IZR || rewrite Z_R_minus; - apply IZR_lt; omega. + apply IZR_lt; lia. Ltac prove_sup := match goal with diff --git a/theories/Reals/Exp_prop.v b/theories/Reals/Exp_prop.v index 1636d81d25..2c822da055 100644 --- a/theories/Reals/Exp_prop.v +++ b/theories/Reals/Exp_prop.v @@ -17,7 +17,7 @@ Require Import PSeries_reg. Require Import Div2. Require Import Even. Require Import Max. -Require Import Omega. +Require Import Lia. Local Open Scope nat_scope. Local Open Scope R_scope. @@ -488,8 +488,8 @@ Proof. rewrite div2_S_double. apply S_pred with 0%nat; apply H3. reflexivity. - omega. - omega. + lia. + lia. rewrite H2. replace (pred (S (2 * N0))) with (2 * N0)%nat; [ idtac | reflexivity ]. replace (S (S (2 * N0))) with (2 * S N0)%nat. @@ -549,15 +549,15 @@ Proof. rewrite H6. replace (pred (2 * N1)) with (S (2 * pred N1)). rewrite div2_S_double. - omega. - omega. + lia. + lia. assert (0 < n)%nat. apply lt_le_trans with 2%nat. apply lt_O_Sn. apply le_trans with (max (2 * S N0) 2). apply le_max_r. apply H3. - omega. + lia. rewrite H6. replace (pred (S (2 * N1))) with (2 * N1)%nat. rewrite div2_double. diff --git a/theories/Reals/Machin.v b/theories/Reals/Machin.v index 08bc38a085..d5a39f527f 100644 --- a/theories/Reals/Machin.v +++ b/theories/Reals/Machin.v @@ -8,7 +8,7 @@ (* * (see LICENSE file for the text of the license) *) (************************************************************************) -Require Import Omega. +Require Import Lia. Require Import Lra. Require Import Rbase. Require Import Rtrigo1. @@ -163,8 +163,8 @@ assert (cv : Un_cv PI_2_3_7_tg 0). rewrite <- (Rmult_0_r 2), <- Ropp_mult_distr_r_reverse. rewrite <- Rmult_plus_distr_l, Rabs_mult, (Rabs_pos_eq 2);[|lra]. rewrite Rmult_assoc; apply Rmult_lt_compat_l;[lra | ]. - apply (Pn1 n); omega. - apply (Pn2 n); omega. + apply (Pn1 n); lia. + apply (Pn2 n); lia. rewrite Machin_2_3_7. rewrite !atan_eq_ps_atan; try (split; lra). unfold ps_atan; destruct (in_int (/3)); destruct (in_int (/7)); diff --git a/theories/Reals/RIneq.v b/theories/Reals/RIneq.v index 7813c7b975..229e6018ca 100644 --- a/theories/Reals/RIneq.v +++ b/theories/Reals/RIneq.v @@ -19,7 +19,7 @@ Require Export Raxioms. Require Import Rpow_def. Require Import Zpower. Require Export ZArithRing. -Require Import Omega. +Require Import Lia. Require Export RealField. Local Open Scope Z_scope. @@ -1875,7 +1875,7 @@ Lemma eq_IZR : forall n m:Z, IZR n = IZR m -> n = m. Proof. intros z1 z2 H; generalize (Rminus_diag_eq (IZR z1) (IZR z2) H); rewrite (Z_R_minus z1 z2); intro; generalize (eq_IZR_R0 (z1 - z2) H0); - intro; omega. + intro; lia. Qed. (**********) @@ -1913,21 +1913,21 @@ Qed. Lemma IZR_ge : forall n m:Z, (n >= m)%Z -> IZR n >= IZR m. Proof. intros m n H; apply Rnot_lt_ge; red; intro. - generalize (lt_IZR m n H0); intro; omega. + generalize (lt_IZR m n H0); intro; lia. Qed. Lemma IZR_le : forall n m:Z, (n <= m)%Z -> IZR n <= IZR m. Proof. intros m n H; apply Rnot_gt_le; red; intro. - unfold Rgt in H0; generalize (lt_IZR n m H0); intro; omega. + unfold Rgt in H0; generalize (lt_IZR n m H0); intro; lia. Qed. Lemma IZR_lt : forall n m:Z, (n < m)%Z -> IZR n < IZR m. Proof. intros m n H; cut (m <= n)%Z. intro H0; elim (IZR_le m n H0); intro; auto. - generalize (eq_IZR m n H1); intro; exfalso; omega. - omega. + generalize (eq_IZR m n H1); intro; exfalso; lia. + lia. Qed. Lemma IZR_neq : forall z1 z2:Z, z1 <> z2 -> IZR z1 <> IZR z2. @@ -1954,7 +1954,7 @@ Lemma one_IZR_r_R1 : forall r (n m:Z), r < IZR n <= r + 1 -> r < IZR m <= r + 1 -> n = m. Proof. intros r z x [H1 H2] [H3 H4]. - cut ((z - x)%Z = 0%Z); auto with zarith. + cut ((z - x)%Z = 0%Z). lia. apply one_IZR_lt1. rewrite <- Z_R_minus; split. replace (-1) with (r - (r + 1)). diff --git a/theories/Reals/R_Ifp.v b/theories/Reals/R_Ifp.v index 5365e04000..5f0747d869 100644 --- a/theories/Reals/R_Ifp.v +++ b/theories/Reals/R_Ifp.v @@ -14,7 +14,7 @@ (**********************************************************) Require Import Rbase. -Require Import Omega. +Require Import Lia. Local Open Scope R_scope. (*********************************************************) @@ -60,7 +60,7 @@ Proof. apply lt_IZR in H1. rewrite <- minus_IZR in H2. apply le_IZR in H2. - omega. + lia. Qed. (**********) @@ -230,7 +230,7 @@ Proof. rewrite <- (plus_IZR (Int_part r1 - Int_part r2) 1) in H; generalize (up_tech (r1 - r2) (Int_part r1 - Int_part r2) H0 H); intros; clear H H0; unfold Int_part at 1; - omega. + lia. Qed. (**********) @@ -314,7 +314,7 @@ Proof. in H0; fold (IZR (Int_part r1) - IZR (Int_part r2) - 1) in H0; rewrite (Z_R_minus (Int_part r1) (Int_part r2)) in H0; rewrite (Z_R_minus (Int_part r1) (Int_part r2)) in H; - auto with zarith real. + auto with real. change (_ + -1) with (IZR (Int_part r1 - Int_part r2) - 1) in H; rewrite (Z_R_minus (Int_part r1 - Int_part r2) 1) in H; rewrite (Z_R_minus (Int_part r1 - Int_part r2) 1) in H0; @@ -323,7 +323,7 @@ Proof. intro; clear H; generalize (up_tech (r1 - r2) (Int_part r1 - Int_part r2 - 1) H1 H0); intros; clear H0 H1; unfold Int_part at 1; - omega. + lia. Qed. (**********) @@ -430,14 +430,14 @@ Proof. clear a b; change 2 with (1 + 1) in H0; rewrite <- (Rplus_assoc (IZR (Int_part r1) + IZR (Int_part r2)) 1 1) in H0; - auto with zarith real. + auto with real. rewrite <- (plus_IZR (Int_part r1) (Int_part r2)) in H; rewrite <- (plus_IZR (Int_part r1) (Int_part r2)) in H0; rewrite <- (plus_IZR (Int_part r1 + Int_part r2) 1) in H; rewrite <- (plus_IZR (Int_part r1 + Int_part r2) 1) in H0; rewrite <- (plus_IZR (Int_part r1 + Int_part r2 + 1) 1) in H0; generalize (up_tech (r1 + r2) (Int_part r1 + Int_part r2 + 1) H H0); - intro; clear H H0; unfold Int_part at 1; omega. + intro; clear H H0; unfold Int_part at 1; lia. Qed. (**********) @@ -499,7 +499,7 @@ Proof. rewrite <- (plus_IZR (Int_part r1 + Int_part r2) 1) in H1; generalize (up_tech (r1 + r2) (Int_part r1 + Int_part r2) H0 H1); intro; clear H0 H1; unfold Int_part at 1; - omega. + lia. Qed. (**********) @@ -522,7 +522,7 @@ Proof. rewrite (Rplus_assoc (r1 + r2) (- (IZR (Int_part r1) + IZR (Int_part r2))) (-(1))) ; rewrite <- (Ropp_plus_distr (IZR (Int_part r1) + IZR (Int_part r2)) 1); - trivial with zarith real. + trivial with real. Qed. (**********) diff --git a/theories/Reals/Ranalysis2.v b/theories/Reals/Ranalysis2.v index 7a838f2772..3f560f202e 100644 --- a/theories/Reals/Ranalysis2.v +++ b/theories/Reals/Ranalysis2.v @@ -11,7 +11,6 @@ Require Import Rbase. Require Import Rfunctions. Require Import Ranalysis1. -Require Import Omega. Local Open Scope R_scope. (**********) diff --git a/theories/Reals/Ranalysis5.v b/theories/Reals/Ranalysis5.v index ca82222c25..11835bd24a 100644 --- a/theories/Reals/Ranalysis5.v +++ b/theories/Reals/Ranalysis5.v @@ -16,7 +16,7 @@ Require Import Lra. Require Import RiemannInt. Require Import SeqProp. Require Import Max. -Require Import Omega. +Require Import Lia. Require Import Lra. Local Open Scope R_scope. @@ -1095,11 +1095,11 @@ assert (Main : Rabs ((f (x+h) - fn N (x+h)) - (f x - fn N x) + (fn N (x+h) - fn apply Rlt_trans with (Rabs h * eps / 4 + Rabs (f x - fn N x) + Rabs h * Rabs (fn' N c - g x)). apply Rplus_lt_compat_r ; apply Rplus_lt_compat_r ; unfold R_dist in fnxh_CV_fxh ; rewrite Rabs_minus_sym ; apply fnxh_CV_fxh. - unfold N; omega. + unfold N; lia. apply Rlt_trans with (Rabs h * eps / 4 + Rabs h * eps / 4 + Rabs h * Rabs (fn' N c - g x)). apply Rplus_lt_compat_r ; apply Rplus_lt_compat_l. unfold R_dist in fnx_CV_fx ; rewrite Rabs_minus_sym ; apply fnx_CV_fx. - unfold N ; omega. + unfold N ; lia. replace (fn' N c - g x) with ((fn' N c - g c) + (g c - g x)) by field. apply Rle_lt_trans with (Rabs h * eps / 4 + Rabs h * eps / 4 + Rabs h * Rabs (fn' N c - g c) + Rabs h * Rabs (g c - g x)). @@ -1113,7 +1113,7 @@ assert (Main : Rabs ((f (x+h) - fn N (x+h)) - (f x - fn N x) + (fn N (x+h) - fn apply Rplus_lt_compat_r; apply Rplus_lt_compat_l; apply Rmult_lt_compat_l. apply Rabs_pos_lt ; assumption. rewrite Rabs_minus_sym ; apply fn'c_CVU_gc. - unfold N ; omega. + unfold N ; lia. assert (t : Boule x delta c). destruct P. apply Rabs_def2 in xhinbxdelta; destruct xhinbxdelta. @@ -1201,11 +1201,11 @@ assert (Main : Rabs ((f (x+h) - fn N (x+h)) - (f x - fn N x) + (fn N (x+h) - fn apply Rlt_trans with (Rabs h * eps / 4 + Rabs (f x - fn N x) + Rabs h * Rabs (fn' N c - g x)). apply Rplus_lt_compat_r ; apply Rplus_lt_compat_r ; unfold R_dist in fnxh_CV_fxh ; rewrite Rabs_minus_sym ; apply fnxh_CV_fxh. - unfold N; omega. + unfold N; lia. apply Rlt_trans with (Rabs h * eps / 4 + Rabs h * eps / 4 + Rabs h * Rabs (fn' N c - g x)). apply Rplus_lt_compat_r ; apply Rplus_lt_compat_l. unfold R_dist in fnx_CV_fx ; rewrite Rabs_minus_sym ; apply fnx_CV_fx. - unfold N ; omega. + unfold N ; lia. replace (fn' N c - g x) with ((fn' N c - g c) + (g c - g x)) by field. apply Rle_lt_trans with (Rabs h * eps / 4 + Rabs h * eps / 4 + Rabs h * Rabs (fn' N c - g c) + Rabs h * Rabs (g c - g x)). @@ -1219,7 +1219,7 @@ assert (Main : Rabs ((f (x+h) - fn N (x+h)) - (f x - fn N x) + (fn N (x+h) - fn apply Rplus_lt_compat_r; apply Rplus_lt_compat_l; apply Rmult_lt_compat_l. apply Rabs_pos_lt ; assumption. rewrite Rabs_minus_sym ; apply fn'c_CVU_gc. - unfold N ; omega. + unfold N ; lia. assert (t : Boule x delta c). destruct P. apply Rabs_def2 in xhinbxdelta; destruct xhinbxdelta. diff --git a/theories/Reals/Ratan.v b/theories/Reals/Ratan.v index 57bc89b7e5..e822b87cc6 100644 --- a/theories/Reals/Ratan.v +++ b/theories/Reals/Ratan.v @@ -20,7 +20,7 @@ Require Import SeqProp. Require Import Ranalysis5. Require Import SeqSeries. Require Import PartSum. -Require Import Omega. +Require Import Lia. Local Open Scope R_scope. @@ -76,30 +76,30 @@ clear. intros [ | n] P Hs Ho;[solve[apply Ho, Hs] | apply Hs; auto with arith]. intros N; pattern N; apply WLOG; clear N. intros [ | N] Npos n decr to0 cv nN. - clear -Npos; elimtype False; omega. + lia. assert (decr' : Un_decreasing (fun i => f (S N + i)%nat)). intros k; replace (S N+S k)%nat with (S (S N+k)) by ring. apply (decr (S N + k)%nat). assert (to' : Un_cv (fun i => f (S N + i)%nat) 0). intros eps ep; destruct (to0 eps ep) as [M PM]. - exists M; intros k kM; apply PM; omega. + exists M; intros k kM; apply PM; lia. assert (cv' : Un_cv (sum_f_R0 (tg_alt (fun i => ((-1) ^ S N * f(S N + i)%nat)))) (l - sum_f_R0 (tg_alt f) N)). intros eps ep; destruct (cv eps ep) as [M PM]; exists M. intros n' nM. match goal with |- ?C => set (U := C) end. - assert (nM' : (n' + S N >= M)%nat) by omega. + assert (nM' : (n' + S N >= M)%nat) by lia. generalize (PM _ nM'); unfold R_dist. rewrite (tech2 (tg_alt f) N (n' + S N)). assert (t : forall a b c, (a + b) - c = b - (c - a)) by (intros; ring). rewrite t; clear t; unfold U, R_dist; clear U. - replace (n' + S N - S N)%nat with n' by omega. + replace (n' + S N - S N)%nat with n' by lia. rewrite <- (sum_eq (tg_alt (fun i => (-1) ^ S N * f(S N + i)%nat))). tauto. intros i _; unfold tg_alt. rewrite <- Rmult_assoc, <- pow_add, !(plus_comm i); reflexivity. - omega. + lia. assert (cv'' : Un_cv (sum_f_R0 (tg_alt (fun i => f (S N + i)%nat))) ((-1) ^ S N * (l - sum_f_R0 (tg_alt f) N))). apply (Un_cv_ext (fun n => (-1) ^ S N * @@ -118,7 +118,7 @@ intros [ | N] Npos n decr to0 cv nN. rewrite neven. destruct (alternated_series_ineq _ _ p' decr to0 cv) as [D E]. unfold R_dist; rewrite Rabs_pos_eq;[ | lra]. - assert (dist : (p <= p')%nat) by omega. + assert (dist : (p <= p')%nat) by lia. assert (t := decreasing_prop _ _ _ (CV_ALT_step1 f decr) dist). apply Rle_trans with (sum_f_R0 (tg_alt f) (2 * p) - l). unfold Rminus; apply Rplus_le_compat_r; exact t. @@ -129,7 +129,7 @@ intros [ | N] Npos n decr to0 cv nN. rewrite nodd; destruct (alternated_series_ineq _ _ p' decr to0 cv) as [D E]. unfold R_dist; rewrite <- Rabs_Ropp, Rabs_pos_eq, Ropp_minus_distr; [ | lra]. - assert (dist : (p <= p')%nat) by omega. + assert (dist : (p <= p')%nat) by lia. apply Rle_trans with (l - sum_f_R0 (tg_alt f) (S (2 * p))). unfold Rminus; apply Rplus_le_compat_l, Ropp_le_contravar. solve[apply Rge_le, (growing_prop _ _ _ (CV_ALT_step0 f decr) dist)]. @@ -142,11 +142,11 @@ intros [ | N] Npos n decr to0 cv nN. rewrite neven; destruct (alternated_series_ineq _ _ p' decr to0 cv) as [D E]. unfold R_dist; rewrite Rabs_pos_eq;[ | lra]. - assert (dist : (S p < S p')%nat) by omega. + assert (dist : (S p < S p')%nat) by lia. apply Rle_trans with (sum_f_R0 (tg_alt f) (2 * S p) - l). unfold Rminus; apply Rplus_le_compat_r, (decreasing_prop _ _ _ (CV_ALT_step1 f decr)). - omega. + lia. rewrite keep, tech5; unfold tg_alt at 2; rewrite <- keep, pow_1_even. lra. rewrite nodd; destruct (alternated_series_ineq _ _ p' decr to0 cv) as [D E]. @@ -154,7 +154,7 @@ intros [ | N] Npos n decr to0 cv nN. rewrite Ropp_minus_distr. apply Rle_trans with (l - sum_f_R0 (tg_alt f) (S (2 * p))). unfold Rminus; apply Rplus_le_compat_l, Ropp_le_contravar, Rge_le, - (growing_prop _ _ _ (CV_ALT_step0 f decr)); omega. + (growing_prop _ _ _ (CV_ALT_step0 f decr)); lia. generalize C; rewrite keep, tech5; unfold tg_alt. rewrite <- keep, pow_1_even. assert (t : forall a b c, a <= b + 1 * c -> a - b <= c) by (intros; lra). @@ -166,7 +166,7 @@ clear WLOG; intros Hyp [ | n] decr to0 cv _. intros [A B]; rewrite Rabs_pos_eq; lra. apply Rle_trans with (f 1%nat). apply (Hyp 1%nat (le_n 1) (S n) decr to0 cv). - omega. + lia. solve[apply decr]. Qed. @@ -746,7 +746,7 @@ intros x Hx n. apply Rlt_le. apply Rinv_0_lt_compat. apply lt_INR_0. - omega. + lia. destruct (proj1 Hx) as [Hx1|Hx1]. destruct (proj2 Hx) as [Hx2|Hx2]. (* . 0 < x < 1 *) @@ -762,7 +762,7 @@ intros x Hx n. rewrite Rmult_1_r. exact Hx1. exact Hx2. - omega. + lia. apply Rgt_not_eq. exact Hx1. (* . x = 1 *) @@ -771,13 +771,13 @@ intros x Hx n. apply Rle_refl. (* . x = 0 *) rewrite <- Hx1. - do 2 (rewrite pow_i ; [ idtac | omega ]). + do 2 (rewrite pow_i ; [ idtac | lia ]). apply Rle_refl. apply Rlt_le. apply Rinv_lt_contravar. - apply Rmult_lt_0_compat ; apply lt_INR_0 ; omega. + apply Rmult_lt_0_compat ; apply lt_INR_0 ; lia. apply lt_INR. - omega. + lia. Qed. Lemma Ratan_seq_converging : forall x, (0 <= x <= 1)%R -> Un_cv (Ratan_seq x) 0. @@ -808,7 +808,7 @@ intros x Hx eps Heps. apply Rlt_le. apply Rinv_0_lt_compat. apply lt_INR_0. - omega. + lia. apply pow_incr. exact Hx. rewrite pow1. @@ -817,15 +817,15 @@ intros x Hx eps Heps. rewrite Rmult_1_l. apply Rinv_le_contravar. apply lt_INR_0. - omega. + lia. apply le_INR. - omega. + lia. rewrite <- (Rinv_involutive eps). apply Rinv_lt_contravar. apply Rmult_lt_0_compat. auto with real. apply lt_INR_0. - omega. + lia. apply Rlt_trans with (INR N). destruct (archimed (/ eps)) as (H,_). assert (0 < up (/ eps))%Z. @@ -837,7 +837,7 @@ intros x Hx eps Heps. rewrite INR_IZR_INZ, positive_nat_Z. exact HN. apply lt_INR. - omega. + lia. apply Rgt_not_eq. exact Heps. apply Rle_ge. @@ -848,7 +848,7 @@ intros x Hx eps Heps. apply Rlt_le. apply Rinv_0_lt_compat. apply lt_INR_0. - omega. + lia. Qed. Definition ps_atan_exists_01 (x : R) (Hx:0 <= x <= 1) : @@ -1045,7 +1045,7 @@ intros x n x_lb ; unfold Datan_seq ; induction n. apply Rmult_gt_0_compat. replace (x^2) with (x*x) by field ; apply Rmult_gt_0_compat ; assumption. assumption. - replace (2 * S n)%nat with (S (S (2 * n))) by intuition. + replace (2 * S n)%nat with (S (S (2 * n))) by lia. simpl ; field. Qed. @@ -1067,8 +1067,7 @@ Lemma Datan_seq_increasing : forall x y n, (n > 0)%nat -> 0 <= x < y -> Datan_se Proof. intros x y n n_lb x_encad ; assert (x_pos : x >= 0) by intuition. assert (y_pos : y > 0). apply Rle_lt_trans with (r2:=x) ; intuition. - induction n. - apply False_ind ; intuition. + induction n. lia. clear -x_encad x_pos y_pos ; induction n ; unfold Datan_seq. case x_pos ; clear x_pos ; intro x_pos. simpl ; apply Rmult_gt_0_lt_compat ; intuition. lra. @@ -1077,14 +1076,14 @@ intros x y n n_lb x_encad ; assert (x_pos : x >= 0) by intuition. simpl ; field. intuition. assert (Hrew : forall a, a^(2 * S (S n)) = (a ^ 2) * (a ^ (2 * S n))). - clear ; intro a ; replace (2 * S (S n))%nat with (S (S (2 * S n)))%nat by intuition. + clear ; intro a ; replace (2 * S (S n))%nat with (S (S (2 * S n)))%nat by lia. simpl ; field. case x_pos ; clear x_pos ; intro x_pos. rewrite Hrew ; rewrite Hrew. apply Rmult_gt_0_lt_compat ; intuition. apply Rmult_gt_0_lt_compat ; intuition ; lra. rewrite x_pos. - rewrite pow_i ; intuition. + rewrite pow_i. intuition. lia. Qed. Lemma Datan_seq_decreasing : forall x, -1 < x -> x < 1 -> Un_decreasing (Datan_seq x). @@ -1101,7 +1100,7 @@ assert (intabs : 0 <= Rabs x < 1). split;[apply Rabs_pos | apply Rabs_def1]; tauto. apply (pow_lt_1_compat (Rabs x) 2) in intabs. tauto. -omega. +lia. Qed. Lemma Datan_seq_CV_0 : forall x, -1 < x -> x < 1 -> Un_cv (Datan_seq x) 0. @@ -1112,7 +1111,7 @@ assert (x_ub2 : Rabs (x^2) < 1). rewrite <- pow2_abs. assert (H: 0 <= Rabs x < 1) by (split;[apply Rabs_pos | apply Rabs_def1; auto]). - apply (pow_lt_1_compat _ 2) in H;[tauto | omega]. + apply (pow_lt_1_compat _ 2) in H;[tauto | lia]. elim (pow_lt_1_zero (x^2) x_ub2 eps eps_pos) ; intros N HN ; exists N ; intros n Hn. unfold R_dist, Datan_seq. replace (x ^ (2 * n) - 0) with ((x ^ 2) ^ n). apply HN ; assumption. @@ -1130,7 +1129,7 @@ assert (Tool2 : / (1 + x ^ 2) > 0). apply Rinv_0_lt_compat ; tauto. assert (x_ub2' : 0<= Rabs (x^2) < 1). rewrite Rabs_pos_eq, <- pow2_abs;[ | apply pow2_ge_0]. - apply pow_lt_1_compat;[split;[apply Rabs_pos | ] | omega]. + apply pow_lt_1_compat;[split;[apply Rabs_pos | ] | lia]. apply Rabs_def1; assumption. assert (x_ub2 : Rabs (x^2) < 1) by tauto. assert (eps'_pos : ((1+x^2)*eps) > 0). @@ -1164,7 +1163,7 @@ assert (tool : forall a b c, 0 < b -> a < b * c -> a * / b < c). assumption. field; apply Rgt_not_eq; exact bp. apply tool;[exact Tool1 | ]. -apply HN; omega. +apply HN; lia. Qed. Lemma Datan_CVU_prelim : forall c (r : posreal), Rabs c + r < 1 -> @@ -1187,7 +1186,7 @@ apply (Alt_CVU (fun x n => Datan_seq n x) intros x [ | n] inb. solve[unfold Datan_seq; apply Rle_refl]. rewrite <- (Datan_seq_Rabs x); apply Rlt_le, Datan_seq_increasing. - omega. + lia. apply Boule_lt in inb; intuition. solve[apply Rabs_pos]. apply Datan_seq_CV_0. @@ -1212,7 +1211,7 @@ assert (Tool : forall N, (-1) ^ (S (2 * N)) = - 1). rewrite <- pow_add. replace (2 + S (2 * n))%nat with (S (2 * S n))%nat. reflexivity. - intuition. + lia. intros N x x_lb x_ub. induction N. unfold Datan_seq, Ratan_seq, tg_alt ; simpl. @@ -1251,10 +1250,10 @@ intros N x x_lb x_ub. apply Rabs_pos_lt ; assumption. rewrite Rabs_right. replace 1 with (/1) by field. - apply Rinv_1_lt_contravar ; intuition. + apply Rinv_1_lt_contravar. lra. apply lt_1_INR; lia. apply Rgt_ge ; replace (INR (2 * S N + 1)) with (INR (2*S N) + 1) ; [apply RiemannInt.RinvN_pos | ]. - replace (2 * S N + 1)%nat with (S (2 * S N))%nat by intuition ; + replace (2 * S N + 1)%nat with (S (2 * S N))%nat by lia. rewrite S_INR ; reflexivity. apply Hdelta ; assumption. rewrite Rmult_minus_distr_l. @@ -1266,7 +1265,7 @@ intros N x x_lb x_ub. - (x ^ (2 * S N + 1) / INR (2 * S N + 1))) / h)) by intuition. apply Rplus_eq_compat_l. field. split ; [apply Rgt_not_eq|] ; intuition. - clear ; replace (pred (2 * S N + 1)) with (2 * S N)%nat by intuition. + clear ; replace (pred (2 * S N + 1)) with (2 * S N)%nat by lia. field ; apply Rgt_not_eq ; intuition. field ; split ; [apply Rgt_not_eq |] ; intuition. elim (Main (eps/3) eps_3_pos) ; intros delta2 Hdelta2. @@ -1314,7 +1313,7 @@ apply (Alt_CVU (fun i r => Ratan_seq r i) ps_atan PI_tg (/2) pos_half); intros x n b; apply Boule_half_to_interval in b. rewrite <- (Rmult_1_l (PI_tg n)); unfold Ratan_seq, PI_tg. apply Rmult_le_compat_r. - apply Rlt_le, Rinv_0_lt_compat, (lt_INR 0); omega. + apply Rlt_le, Rinv_0_lt_compat, (lt_INR 0); lia. rewrite <- (pow1 (2 * n + 1)); apply pow_incr; assumption. exact PI_tg_cv. Qed. @@ -1458,10 +1457,10 @@ rewrite Rplus_assoc ; apply Rabs_triang. apply Halpha ; split. unfold D_x, no_cond ; split ; [ | apply Rgt_not_eq ] ; intuition. intuition. - apply HN2; unfold N; omega. + apply HN2; unfold N; lia. lra. rewrite <- Rabs_Ropp, Ropp_minus_distr; apply HN1. - unfold N; omega. + unfold N; lia. lra. assumption. field. diff --git a/theories/Reals/Rderiv.v b/theories/Reals/Rderiv.v index effbc3a404..69a41db4db 100644 --- a/theories/Reals/Rderiv.v +++ b/theories/Reals/Rderiv.v @@ -17,7 +17,7 @@ Require Import Rbase. Require Import Rfunctions. Require Import Rlimit. Require Import Lra. -Require Import Omega. +Require Import Lia. Local Open Scope R_scope. (*********) @@ -341,7 +341,7 @@ Proof. rewrite cond in H2; rewrite cond; simpl in H2; simpl; cut (1 + x0 * 1 * 0 = 1 * 1); [ intro A; rewrite A in H2; assumption | ring ]. - cut (n0 <> 0%nat -> S (n0 - 1) = n0); [ intro | omega ]; + cut (n0 <> 0%nat -> S (n0 - 1) = n0); [ intro | lia ]; rewrite (H3 cond) in H2; rewrite (Rmult_comm (x0 ^ n0) (INR n0)) in H2; rewrite (tech_pow_Rplus x0 n0 n0) in H2; assumption. Qed. diff --git a/theories/Reals/Rfunctions.v b/theories/Reals/Rfunctions.v index 17b39d22cb..7f9e019c5b 100644 --- a/theories/Reals/Rfunctions.v +++ b/theories/Reals/Rfunctions.v @@ -25,7 +25,7 @@ Require Export R_sqr. Require Export SplitAbsolu. Require Export SplitRmult. Require Export ArithProp. -Require Import Omega. +Require Import Lia. Require Import Zpower. Local Open Scope nat_scope. Local Open Scope R_scope. @@ -122,7 +122,7 @@ Hint Resolve pow_lt: real. Lemma Rlt_pow_R1 : forall (x:R) (n:nat), 1 < x -> (0 < n)%nat -> 1 < x ^ n. Proof. intros x n; elim n; simpl; auto with real. - intros H' H'0; exfalso; omega. + intros H' H'0; exfalso; lia. intros n0; case n0. simpl; rewrite Rmult_1_r; auto. intros n1 H' H'0 H'1. @@ -262,14 +262,14 @@ Proof. elim (IZN (up (b * / (Rabs x - 1))) H2); intros; exists x0; apply (Rge_trans (INR x0) (IZR (up (b * / (Rabs x - 1)))) (b * / (Rabs x - 1))). - rewrite INR_IZR_INZ; apply IZR_ge; omega. + rewrite INR_IZR_INZ; apply IZR_ge; lia. unfold Rge; left; assumption. exists 0%nat; apply (Rge_trans (INR 0) (IZR (up (b * / (Rabs x - 1)))) (b * / (Rabs x - 1))). - rewrite INR_IZR_INZ; apply IZR_ge; simpl; omega. + rewrite INR_IZR_INZ; apply IZR_ge; simpl; lia. unfold Rge; left; assumption. - omega. + lia. Qed. Lemma pow_ne_zero : forall n:nat, n <> 0%nat -> 0 ^ n = 0. @@ -745,7 +745,7 @@ Proof. - now simpl; rewrite Rmult_1_l. - now rewrite <- !pow_powerRZ, Rpow_mult_distr. - destruct Hmxy as [H|H]. - + assert(m = 0) as -> by now omega. + + assert(m = 0) as -> by now lia. now rewrite <- Hm, Rmult_1_l. + assert(x0 <> 0)%R by now intros ->; apply H; rewrite Rmult_0_l. assert(y0 <> 0)%R by now intros ->; apply H; rewrite Rmult_0_r. @@ -808,7 +808,7 @@ Proof. ring. rewrite Rmult_plus_distr_r; rewrite Hrecn; cut ((n + 1)%nat = S n). intro H; rewrite H; simpl; ring. - omega. + lia. Qed. Lemma sum_f_R0_triangle : diff --git a/theories/Reals/Rprod.v b/theories/Reals/Rprod.v index 15ec7891f7..ed2c953449 100644 --- a/theories/Reals/Rprod.v +++ b/theories/Reals/Rprod.v @@ -14,7 +14,7 @@ Require Import Rfunctions. Require Import Rseries. Require Import PartSum. Require Import Binomial. -Require Import Omega. +Require Import Lia. Local Open Scope R_scope. (** TT Ak; 0<=k<=N *) @@ -34,16 +34,16 @@ Lemma prod_SO_split : prod_f_R0 An k * prod_f_R0 (fun l:nat => An (k +1+l)%nat) (n - k -1). Proof. intros; induction n as [| n Hrecn]. - absurd (k < 0)%nat; omega. - cut (k = n \/ (k < n)%nat);[intro; elim H0; intro|omega]. - replace (S n - k - 1)%nat with O; [rewrite H1; simpl|omega]. + absurd (k < 0)%nat; lia. + cut (k = n \/ (k < n)%nat);[intro; elim H0; intro|lia]. + replace (S n - k - 1)%nat with O; [rewrite H1; simpl|lia]. replace (n+1+0)%nat with (S n); ring. - replace (S n - k-1)%nat with (S (n - k-1));[idtac|omega]. + replace (S n - k-1)%nat with (S (n - k-1));[idtac|lia]. simpl; replace (k + S (n - k))%nat with (S n). replace (k + 1 + S (n - k - 1))%nat with (S n). rewrite Hrecn; [ ring | assumption ]. - omega. - omega. + lia. + lia. Qed. (**********) @@ -116,11 +116,11 @@ Proof. assert (forall (n:nat), (0 < n)%nat -> (if eq_nat_dec n 0 then 1 else INR n) = INR n). intros n; case (eq_nat_dec n 0); auto with real. - intros; absurd (0 < n)%nat; omega. + intros; absurd (0 < n)%nat; lia. intros; unfold Rsqr; repeat rewrite fact_prodSO. cut ((k=N)%nat \/ (k < N)%nat \/ (N < k)%nat). intro H2; elim H2; intro H3. - rewrite H3; replace (2*N-N)%nat with N;[right; ring|omega]. + rewrite H3; replace (2*N-N)%nat with N;[right; ring|lia]. case H3; intro; clear H2 H3. rewrite (prod_SO_split (fun l:nat => if eq_nat_dec l 0 then 1 else INR l) (2 * N - k) N). rewrite Rmult_assoc; apply Rmult_le_compat_l. @@ -133,12 +133,12 @@ Proof. apply prod_SO_Rle; intros; split; auto. rewrite H0. rewrite H0. - apply le_INR; omega. - omega. - omega. + apply le_INR; lia. + lia. + lia. assumption. - omega. - omega. + lia. + lia. rewrite <- (Rmult_comm (prod_f_R0 (fun l:nat => if eq_nat_dec l 0 then 1 else INR l) k)); rewrite (prod_SO_split (fun l:nat => @@ -154,13 +154,13 @@ Proof. apply prod_SO_Rle; intros; split; auto. rewrite H0. rewrite H0. - apply le_INR; omega. - omega. - omega. - omega. - omega. + apply le_INR; lia. + lia. + lia. + lia. + lia. assumption. - omega. + lia. Qed. @@ -192,5 +192,5 @@ Proof. reflexivity. rewrite mult_INR; apply prod_neq_R0; apply INR_fact_neq_0. apply prod_neq_R0; apply INR_fact_neq_0. - omega. + lia. Qed. diff --git a/theories/Reals/Rsigma.v b/theories/Reals/Rsigma.v index 2a9c6953c5..7577c4b7b0 100644 --- a/theories/Reals/Rsigma.v +++ b/theories/Reals/Rsigma.v @@ -12,7 +12,7 @@ Require Import Rbase. Require Import Rfunctions. Require Import Rseries. Require Import PartSum. -Require Import Omega. +Require Import Lia. Local Open Scope R_scope. Set Implicit Arguments. @@ -57,12 +57,12 @@ Section Sigma. ring. replace (high - S (S k))%nat with (high - S k - 1)%nat. apply pred_of_minus. - omega. + lia. unfold sigma; replace (S k - low)%nat with (S (k - low)). pattern (S k) at 1; replace (S k) with (low + S (k - low))%nat. symmetry ; apply (tech5 (fun i:nat => f (low + i))). - omega. - omega. + lia. + lia. rewrite <- H2; unfold sigma; rewrite <- minus_n_n; simpl; replace (high - S low)%nat with (pred (high - low)). replace (sum_f_R0 (fun k0:nat => f (S (low + k0))) (pred (high - low))) with @@ -73,7 +73,7 @@ Section Sigma. apply sum_eq; intros; replace (S (low + i)) with (low + S i)%nat. reflexivity. ring. - omega. + lia. inversion H; [ right; reflexivity | left; assumption ]. Qed. diff --git a/theories/Reals/Rtrigo1.v b/theories/Reals/Rtrigo1.v index 0df1442f46..c2651d4120 100644 --- a/theories/Reals/Rtrigo1.v +++ b/theories/Reals/Rtrigo1.v @@ -18,7 +18,7 @@ Require Export Cos_rel. Require Export Cos_plus. Require Import ZArith_base. Require Import Zcomplements. -Import Omega. +Require Import Lia. Require Import Lra. Require Import Ranalysis1. Require Import Rsqrt_def. @@ -1741,7 +1741,7 @@ Proof. replace (3*(PI/2)) with (PI/2 + PI) in GT by field. rewrite Rplus_comm in GT. now apply Rplus_lt_reg_l in GT. } - omega. + lia. Qed. Lemma cos_eq_0_2PI_1 (x:R) : diff --git a/theories/Reals/SeqProp.v b/theories/Reals/SeqProp.v index d73f6ce0f3..34ea323a95 100644 --- a/theories/Reals/SeqProp.v +++ b/theories/Reals/SeqProp.v @@ -12,7 +12,7 @@ Require Import Rbase. Require Import Rfunctions. Require Import Rseries. Require Import Max. -Require Import Omega. +Require Import Lia. Local Open Scope R_scope. (*****************************************************************) @@ -1155,7 +1155,7 @@ Proof. rewrite Rmult_1_r; apply Rle_trans with (INR M_nat). left; rewrite INR_IZR_INZ. rewrite <- H4; assert (H8 := archimed (Rabs x)); elim H8; intros; assumption. - apply le_INR; omega. + apply le_INR; lia. apply INR_fact_neq_0. apply INR_fact_neq_0. ring. diff --git a/theories/Setoids/Setoid.v b/theories/Setoids/Setoid.v index 2f8be5de12..ddc9967bfa 100644 --- a/theories/Setoids/Setoid.v +++ b/theories/Setoids/Setoid.v @@ -12,6 +12,8 @@ Require Export Coq.Classes.SetoidTactics. Export Morphisms.ProperNotations. +Require Coq.ssr.ssrsetoid. + (** For backward compatibility *) Definition Setoid_Theory := @Equivalence. diff --git a/theories/Structures/OrderedTypeEx.v b/theories/Structures/OrderedTypeEx.v index cc216b21f8..e889150d92 100644 --- a/theories/Structures/OrderedTypeEx.v +++ b/theories/Structures/OrderedTypeEx.v @@ -9,7 +9,7 @@ (************************************************************************) Require Import OrderedType. -Require Import ZArith. +Require Import ZArith_base. Require Import PeanoNat. Require Import Ascii String. Require Import NArith Ndec. diff --git a/theories/ZArith/Zdigits.v b/theories/ZArith/Zdigits.v index 056e67db83..4896301aa7 100644 --- a/theories/ZArith/Zdigits.v +++ b/theories/ZArith/Zdigits.v @@ -15,11 +15,11 @@ Require Import Bvector. Require Import ZArith. Require Export Zpower. -Require Import Omega. +Require Import Lia. (** The evaluation of boolean vector is done both in binary and two's complement. The computed number belongs to Z. - We hence use Omega to perform computations in Z. + We hence use lia to perform computations in Z. Moreover, we use functions [2^n] where [n] is a natural number (here the vector length). *) @@ -155,10 +155,10 @@ Section Z_BRIC_A_BRAC. forall (n:nat) (bv:Bvector n), (binary_value n bv >= 0)%Z. Proof. induction bv as [| a n v IHbv]; cbn. - omega. + lia. - destruct a; destruct (binary_value n v); simpl; auto. - auto with zarith. + destruct a; destruct (binary_value n v); auto. + discriminate. Qed. Lemma two_compl_value_Sn : @@ -203,7 +203,7 @@ Section Z_BRIC_A_BRAC. auto. destruct p; auto. - simpl; intros; omega. + simpl; intros; lia. intro H; elim H; trivial. Qed. @@ -214,11 +214,11 @@ Section Z_BRIC_A_BRAC. (z < two_power_nat (S n))%Z -> (Z.div2 z < two_power_nat n)%Z. Proof. intros. - enough (2 * Z.div2 z < 2 * two_power_nat n)%Z by omega. + enough (2 * Z.div2 z < 2 * two_power_nat n)%Z by lia. rewrite <- two_power_nat_S. destruct (Zeven.Zeven_odd_dec z) as [Heven|Hodd]; intros. rewrite <- Zeven.Zeven_div2; auto. - generalize (Zeven.Zodd_div2 z Hodd); omega. + generalize (Zeven.Zodd_div2 z Hodd); lia. Qed. Lemma Z_to_two_compl_Sn_z : @@ -253,9 +253,9 @@ Section Z_BRIC_A_BRAC. intros n z; rewrite (two_power_nat_S n). generalize (Zmod2_twice z). destruct (Zeven.Zeven_odd_dec z) as [H| H]. - rewrite (Zeven_bit_value z H); intros; omega. + rewrite (Zeven_bit_value z H); intros; lia. - rewrite (Zodd_bit_value z H); intros; omega. + rewrite (Zodd_bit_value z H); intros; lia. Qed. Lemma Zlt_two_power_nat_S : @@ -265,9 +265,9 @@ Section Z_BRIC_A_BRAC. intros n z; rewrite (two_power_nat_S n). generalize (Zmod2_twice z). destruct (Zeven.Zeven_odd_dec z) as [H| H]. - rewrite (Zeven_bit_value z H); intros; omega. + rewrite (Zeven_bit_value z H); intros; lia. - rewrite (Zodd_bit_value z H); intros; omega. + rewrite (Zodd_bit_value z H); intros; lia. Qed. End Z_BRIC_A_BRAC. @@ -309,7 +309,7 @@ Section COHERENT_VALUE. (z < two_power_nat n)%Z -> binary_value n (Z_to_binary n z) = z. Proof. induction n as [| n IHn]. - unfold two_power_nat, shift_nat; simpl; intros; omega. + unfold two_power_nat, shift_nat; simpl; intros; lia. intros; rewrite Z_to_binary_Sn_z. rewrite binary_value_Sn. @@ -328,13 +328,13 @@ Section COHERENT_VALUE. Proof. induction n as [| n IHn]. unfold two_power_nat, shift_nat; simpl; intros. - assert (z = (-1)%Z \/ z = 0%Z). omega. + assert (z = (-1)%Z \/ z = 0%Z). lia. intuition; subst z; trivial. intros; rewrite Z_to_two_compl_Sn_z. rewrite two_compl_value_Sn. rewrite IHn. - generalize (Zmod2_twice z); omega. + generalize (Zmod2_twice z); lia. apply Zge_minus_two_power_nat_S; auto. diff --git a/theories/ZArith/Zgcd_alt.v b/theories/ZArith/Zgcd_alt.v index 0cc137ef5d..da2df40572 100644 --- a/theories/ZArith/Zgcd_alt.v +++ b/theories/ZArith/Zgcd_alt.v @@ -25,7 +25,7 @@ Require Import ZArith_base. Require Import ZArithRing. Require Import Zdiv. Require Import Znumtheory. -Require Import Omega. +Require Import Lia. Open Scope Z_scope. @@ -76,8 +76,7 @@ Open Scope Z_scope. Z.abs a < Z.of_nat n -> Zis_gcd a b (Zgcdn n a b). Proof. induction n. - simpl; intros. - exfalso; generalize (Z.abs_nonneg a); omega. + intros; lia. destruct a; intros; simpl; [ generalize (Zis_gcd_0_abs b); intuition | | ]; unfold Z.modulo; @@ -85,8 +84,7 @@ Open Scope Z_scope. destruct (Z.div_eucl b (Zpos p)) as (q,r); intros (H0,H1); rewrite Nat2Z.inj_succ in H; simpl Z.abs in H; - (assert (H2: Z.abs r < Z.of_nat n) by - (rewrite Z.abs_eq; auto with zarith)); + (assert (H2: Z.abs r < Z.of_nat n) by lia); assert (IH:=IHn r (Zpos p) H2); clear IHn; simpl in IH |- *; rewrite H0. @@ -108,15 +106,11 @@ Open Scope Z_scope. Lemma fibonacci_pos : forall n, 0 <= fibonacci n. Proof. enough (forall N n, (n<N)%nat -> 0<=fibonacci n) by eauto. - induction N. - inversion 1. + induction N. intros; lia. + intros [ | [ | n ] ]. 1-2: simpl; lia. intros. - destruct n. - simpl; auto with zarith. - destruct n. - simpl; auto with zarith. change (0 <= fibonacci (S n) + fibonacci n). - generalize (IHN n) (IHN (S n)); omega. + generalize (IHN n) (IHN (S n)); lia. Qed. Lemma fibonacci_incr : @@ -129,7 +123,7 @@ Open Scope Z_scope. destruct m. simpl; auto with zarith. change (fibonacci (S m) <= fibonacci (S m)+fibonacci m). - generalize (fibonacci_pos m); omega. + generalize (fibonacci_pos m); lia. Qed. (** 3) We prove that fibonacci numbers are indeed worst-case: @@ -144,8 +138,8 @@ Open Scope Z_scope. fibonacci (S (S n)) <= b. Proof. induction n. - intros [|a|a]; intros; simpl; omega. - intros [|a|a] b (Ha,Ha'); [simpl; omega | | easy ]. + intros [|a|a]; intros; simpl; lia. + intros [|a|a] b (Ha,Ha'); [simpl; lia | | easy ]. remember (S n) as m. rewrite Heqm at 2. simpl Zgcdn. unfold Z.modulo; generalize (Z_div_mod b (Zpos a) eq_refl). @@ -161,20 +155,13 @@ Open Scope Z_scope. apply Zis_gcd_sym. apply Zis_gcd_for_euclid2; auto. apply Zis_gcd_sym; auto. - + split; auto. - rewrite EQ. - apply Z.add_le_mono; auto. - apply Z.le_trans with (Zpos a * 1); auto. - now rewrite Z.mul_1_r. - apply Z.mul_le_mono_nonneg_l; auto with zarith. - change 1 with (Z.succ 0). apply Z.le_succ_l. - destruct q; auto with zarith. - assert (Zpos a * Zneg p < 0) by now compute. omega. + + split. auto. + destruct q. lia. 1-2: nia. - (* r = 0 *) clear IHn EQ Hr'; intros _. subst r; simpl; rewrite Heqm. destruct n. - + simpl. omega. + + simpl. lia. + now destruct 1. Qed. @@ -184,7 +171,7 @@ Open Scope Z_scope. 0 < a < b -> a < fibonacci (S n) -> Zis_gcd a b (Zgcdn n a b). Proof. - destruct a; [ destruct 1; exfalso; omega | | destruct 1; discriminate]. + destruct a. 1,3 : intros; lia. cut (forall k n b, k = (S (Pos.to_nat p) - n)%nat -> 0 < Zpos p < b -> Zpos p < fibonacci (S n) -> @@ -192,22 +179,17 @@ Open Scope Z_scope. destruct 2; eauto. clear n; induction k. intros. - assert (Pos.to_nat p < n)%nat by omega. apply Zgcdn_linear_bound. - simpl. - generalize (inj_le _ _ H2). - rewrite Nat2Z.inj_succ. - rewrite positive_nat_Z; auto. - omega. + lia. intros. generalize (Zgcdn_worst_is_fibonacci n (Zpos p) b H0); intros. assert (Zis_gcd (Zpos p) b (Zgcdn (S n) (Zpos p) b)). apply IHk; auto. - omega. + lia. replace (fibonacci (S (S n))) with (fibonacci (S n)+fibonacci n) by auto. - generalize (fibonacci_pos n); omega. + generalize (fibonacci_pos n); lia. replace (Zgcdn n (Zpos p) b) with (Zgcdn (S n) (Zpos p) b); auto. - generalize (H2 H3); clear H2 H3; omega. + generalize (H2 H3); clear H2 H3; lia. Qed. (** 4) The proposed bound leads to a fibonacci number that is big enough. *) @@ -215,7 +197,7 @@ Open Scope Z_scope. Lemma Zgcd_bound_fibonacci : forall a, 0 < a -> a < fibonacci (Zgcd_bound a). Proof. - destruct a; [omega| | intro H; discriminate]. + destruct a; [lia| | intro H; discriminate]. intros _. induction p; [ | | compute; auto ]; simpl Zgcd_bound in *; @@ -224,10 +206,10 @@ Open Scope Z_scope. assert (n <> O) by (unfold n; destruct p; simpl; auto). destruct n as [ |m]; [elim H; auto| ]. - generalize (fibonacci_pos m); rewrite Pos2Z.inj_xI; omega. + generalize (fibonacci_pos m); rewrite Pos2Z.inj_xI; lia. destruct n as [ |m]; [elim H; auto| ]. - generalize (fibonacci_pos m); rewrite Pos2Z.inj_xO; omega. + generalize (fibonacci_pos m); rewrite Pos2Z.inj_xO; lia. Qed. (* 5) the end: we glue everything together and take care of @@ -265,10 +247,10 @@ Open Scope Z_scope. Z.le_elim H1. + apply Zgcdn_ok_before_fibonacci; auto. apply Z.lt_le_trans with (fibonacci (S m)); - [ omega | apply fibonacci_incr; auto]. + [ lia | apply fibonacci_incr; auto]. + subst r; simpl. - destruct m as [ |m]; [exfalso; omega| ]. - destruct n as [ |n]; [exfalso; omega| ]. + destruct m as [ |m]; [ lia | ]. + destruct n as [ |n]; [ lia | ]. simpl; apply Zis_gcd_sym; apply Zis_gcd_0. Qed. @@ -277,7 +259,7 @@ Open Scope Z_scope. Proof. destruct a. - simpl; intros. - destruct n; [exfalso; omega | ]. + destruct n; [ lia | ]. simpl; generalize (Zis_gcd_0_abs b); intuition. - apply Zgcdn_is_gcd_pos. - rewrite <- Zgcd_bound_opp, <- Zgcdn_opp. diff --git a/theories/ZArith/Zpow_facts.v b/theories/ZArith/Zpow_facts.v index e65eb7cdc7..a669429ffa 100644 --- a/theories/ZArith/Zpow_facts.v +++ b/theories/ZArith/Zpow_facts.v @@ -8,7 +8,7 @@ (* * (see LICENSE file for the text of the license) *) (************************************************************************) -Require Import ZArith_base ZArithRing Omega Zcomplements Zdiv Znumtheory. +Require Import ZArith_base ZArithRing Lia Zcomplements Zdiv Znumtheory. Require Export Zpower. Local Open Scope Z_scope. @@ -49,7 +49,7 @@ Proof. intros. now apply Z.pow_le_mono_r. Qed. Theorem Zpower_lt_monotone a b c : 1 < a -> 0 <= b < c -> a^b < a^c. -Proof. intros. apply Z.pow_lt_mono_r; auto with zarith. Qed. +Proof. intros. apply Z.pow_lt_mono_r; lia. Qed. Theorem Zpower_gt_1 x y : 1 < x -> 0 < y -> 1 < x^y. Proof. apply Z.pow_gt_1. Qed. @@ -87,10 +87,10 @@ Proof. assert (Hn := Nat2Z.is_nonneg n). destruct p; simpl Pos.size_nat. - specialize IHn with p. - rewrite Pos2Z.inj_xI, Nat2Z.inj_succ, Z.pow_succ_r; omega. + rewrite Nat2Z.inj_succ, Z.pow_succ_r; lia. - specialize IHn with p. - rewrite Pos2Z.inj_xO, Nat2Z.inj_succ, Z.pow_succ_r; omega. - - split; auto with zarith. + rewrite Nat2Z.inj_succ, Z.pow_succ_r; lia. + - split. lia. intros _. apply Z.pow_gt_1. easy. now rewrite Nat2Z.inj_succ, Z.lt_succ_r. Qed. @@ -103,8 +103,8 @@ Proof. intros Hn; destruct (Z.le_gt_cases 0 q) as [H1|H1]. - pattern q; apply natlike_ind; trivial. clear q H1. intros q Hq Rec. rewrite !Z.pow_succ_r; trivial. - rewrite Z.mul_mod_idemp_l; auto with zarith. - rewrite Z.mul_mod, Rec, <- Z.mul_mod; auto with zarith. + rewrite Z.mul_mod_idemp_l by lia. + rewrite Z.mul_mod, Rec, <- Z.mul_mod by lia. reflexivity. - rewrite !Z.pow_neg_r; auto with zarith. Qed. @@ -163,7 +163,7 @@ Qed. Lemma Zpower_divide p q : 0 < q -> (p | p ^ q). Proof. exists (p^(q - 1)). - rewrite Z.mul_comm, <- Z.pow_succ_r; f_equal; auto with zarith. + rewrite Z.mul_comm, <- Z.pow_succ_r by lia; f_equal; lia. Qed. Theorem rel_prime_Zpower_r i p q : @@ -190,7 +190,7 @@ Proof. - simpl; intros. assert (2<=p) by (apply prime_ge_2; auto). assert (p<=1) by (apply Z.divide_pos_le; auto with zarith). - omega. + lia. - intros n Hn Rec. rewrite Z.pow_succ_r by trivial. intros. assert (2<=p) by (apply prime_ge_2; auto). @@ -213,11 +213,11 @@ Proof. exists 1; rewrite Z.pow_1_r; apply prime_power_prime with n; auto. case not_prime_divide with (2 := Hpr); auto. intros p1 ((Hp1, Hpq1),(q1,->)). - assert (Hq1 : 0 < q1) by (apply Z.mul_lt_mono_pos_r with p1; auto with zarith). - destruct (IH p1) with p n as (r1,Hr1); auto with zarith. + assert (Hq1 : 0 < q1) by (apply Z.mul_lt_mono_pos_r with p1; lia). + destruct (IH p1) with p n as (r1,Hr1). 3-4: assumption. 1-2: lia. transitivity (q1 * p1); trivial. exists q1; auto with zarith. - destruct (IH q1) with p n as (r2,Hr2); auto with zarith. - split; auto with zarith. + destruct (IH q1) with p n as (r2,Hr2). 3-4: assumption. 2: lia. + split. lia. rewrite <- (Z.mul_1_r q1) at 1. apply Z.mul_lt_mono_pos_l; auto with zarith. transitivity (q1 * p1); trivial. exists p1; auto with zarith. diff --git a/theories/ZArith/Zquot.v b/theories/ZArith/Zquot.v index fea7db7921..b3e7fff7d6 100644 --- a/theories/ZArith/Zquot.v +++ b/theories/ZArith/Zquot.v @@ -63,6 +63,7 @@ Hint Resolve Zrem_0_l Zrem_0_r Zquot_0_l Zquot_0_r Z.quot_1_r Z.rem_1_r Ltac zero_or_not a := destruct (Z.eq_decidable a 0) as [->|?]; [rewrite ?Zquot_0_l, ?Zrem_0_l, ?Zquot_0_r, ?Zrem_0_r; + try lia; auto with zarith|]. Lemma Z_rem_same a : Z.rem a a = 0. @@ -100,7 +101,6 @@ Proof. zero_or_not b. now apply Z.rem_opp_opp. Qed. Theorem Zrem_sgn a b : 0 <= Z.sgn (Z.rem a b) * Z.sgn a. Proof. zero_or_not b. - - apply Z.square_nonneg. - zero_or_not (Z.rem a b). rewrite Z.rem_sign_nz; trivial. apply Z.square_nonneg. Qed. @@ -203,18 +203,18 @@ Qed. (* Division of positive numbers is positive. *) Lemma Z_quot_pos a b : 0 <= a -> 0 <= b -> 0 <= a÷b. -Proof. intros. zero_or_not b. apply Z.quot_pos; auto with zarith. Qed. +Proof. intros. zero_or_not b. apply Z.quot_pos; lia. Qed. (** As soon as the divisor is greater or equal than 2, the division is strictly decreasing. *) Lemma Z_quot_lt a b : 0 < a -> 2 <= b -> a÷b < a. -Proof. intros. apply Z.quot_lt; auto with zarith. Qed. +Proof. intros. apply Z.quot_lt; lia. Qed. (** [<=] is compatible with a positive division. *) Lemma Z_quot_monotone a b c : 0<=c -> a<=b -> a÷c <= b÷c. -Proof. intros. zero_or_not c. apply Z.quot_le_mono; auto with zarith. Qed. +Proof. intros. zero_or_not c. apply Z.quot_le_mono; lia. Qed. (** With our choice of division, rounding of (a÷b) is always done toward 0: *) @@ -228,12 +228,12 @@ Proof. intros. zero_or_not b. apply Z.mul_quot_ge; auto with zarith. Qed. iff the modulo is zero. *) Lemma Z_quot_exact_full a b : a = b*(a÷b) <-> Z.rem a b = 0. -Proof. intros. zero_or_not b. intuition. apply Z.quot_exact; auto. Qed. +Proof. intros. zero_or_not b. apply Z.quot_exact; auto. Qed. (** A modulo cannot grow beyond its starting point. *) Theorem Zrem_le a b : 0 <= a -> 0 <= b -> Z.rem a b <= a. -Proof. intros. zero_or_not b. apply Z.rem_le; auto with zarith. Qed. +Proof. intros. zero_or_not b. apply Z.rem_le; lia. Qed. (** Some additional inequalities about Zdiv. *) @@ -357,7 +357,7 @@ Qed. Theorem Zquot_mult_le: forall a b c, 0<=a -> 0<=b -> 0<=c -> c*(a÷b) <= (c*a)÷b. -Proof. intros. zero_or_not b. apply Z.quot_mul_le; auto with zarith. Qed. +Proof. intros. zero_or_not b. apply Z.quot_mul_le; lia. Qed. (** Z.rem is related to divisibility (see more in Znumtheory) *) @@ -376,7 +376,7 @@ Lemma Zquot2_odd_remainder : forall a, Proof. intros [ |p|p]. simpl. left. simpl. auto with zarith. - left. destruct p; simpl; auto with zarith. + left. destruct p; simpl; lia. right. destruct p; simpl; split; now auto with zarith. Qed. @@ -414,10 +414,10 @@ Theorem Zquotrem_Zdiv_eucl_pos : forall a b:Z, 0 <= a -> 0 < b -> Proof. intros. apply Zdiv_mod_unique with b. - apply Zrem_lt_pos; auto with zarith. - rewrite Z.abs_eq; auto with *; apply Z_mod_lt; auto with *. - rewrite <- Z_div_mod_eq; auto with *. - symmetry; apply Z.quot_rem; auto with *. + apply Zrem_lt_pos; lia. + rewrite Z.abs_eq by lia. apply Z_mod_lt; lia. + rewrite <- Z_div_mod_eq by lia. + symmetry; apply Z.quot_rem; lia. Qed. Theorem Zquot_Zdiv_pos : forall a b, 0 <= a -> 0 <= b -> diff --git a/theories/ZArith/Zwf.v b/theories/ZArith/Zwf.v index 853ec951ae..ca04bb4c8f 100644 --- a/theories/ZArith/Zwf.v +++ b/theories/ZArith/Zwf.v @@ -10,7 +10,7 @@ Require Import ZArith_base. Require Export Wf_nat. -Require Import Omega. +Require Import Lia. Local Open Scope Z_scope. (** Well-founded relations on Z. *) @@ -39,20 +39,19 @@ Section wf_proof. clear a; simple induction n; intros. (** n= 0 *) case H; intros. - case (lt_n_O (f a)); auto. + lia. apply Acc_intro; unfold Zwf; intros. - assert False; omega || contradiction. + lia. (** inductive case *) case H0; clear H0; intro; auto. apply Acc_intro; intros. apply H. unfold Zwf in H1. - case (Z.le_gt_cases c y); intro; auto with zarith. + case (Z.le_gt_cases c y); intro. 2: lia. left. - red in H0. apply lt_le_trans with (f a); auto with arith. unfold f. - apply Zabs2Nat.inj_lt; omega. + lia. apply (H (S (f a))); auto. Qed. @@ -83,9 +82,7 @@ Section wf_proof_up. Proof. apply well_founded_lt_compat with (f := f). unfold Zwf_up, f. - intros. - apply Zabs2Nat.inj_lt; try (apply Z.le_0_sub; intuition). - now apply Z.sub_lt_mono_l. + lia. Qed. End wf_proof_up. |