diff options
32 files changed, 591 insertions, 478 deletions
diff --git a/Makefile.checker b/Makefile.checker index 5c55ccf489..90c73a496d 100644 --- a/Makefile.checker +++ b/Makefile.checker @@ -43,7 +43,7 @@ checker/check.cmxa $(LIBCOQRUN) checker/coqchk.mli checker/coqchk.ml $(CODESIGN_HIDE) $@ else $(CHICKEN): $(CHICKENBYTE) - cp $< $@ + rm -f $@ && cp $< $@ endif $(CHICKENBYTE): config/config.cma clib/clib.cma lib/lib.cma kernel/kernel.cma \ diff --git a/Makefile.ide b/Makefile.ide index 39c6c8ad1e..bd72494289 100644 --- a/Makefile.ide +++ b/Makefile.ide @@ -110,7 +110,7 @@ $(COQIDE): $(LINKIDEOPT) $(STRIP_HIDE) $@ else $(COQIDE): $(COQIDEBYTE) - cp $< $@ + rm -f $@ && cp $< $@ endif $(COQIDEBYTE): $(LINKIDE) @@ -119,9 +119,7 @@ $(COQIDEBYTE): $(LINKIDE) -linkpkg -package str,unix,dynlink,threads,lablgtk3-sourceview3 $(IDEFLAGS) $(IDECDEPSFLAGS) $^ ide/coqide_os_specific.ml: ide/coqide_$(IDEINT).ml.in config/Makefile - @rm -f $@ - cp $< $@ - @chmod a-w $@ + rm -f $@ && cp $< $@ && chmod a-w $@ ide/%.cmi: ide/%.mli $(SHOW)'OCAMLC $<' @@ -150,7 +148,7 @@ IDETOPCMX:=$(IDETOPCMA:.cma=.cmxa) # Special rule for coqidetop $(IDETOPEXE): $(IDETOP:.opt=.$(BEST)) - cp $< $@ + rm -f $@ && cp $< $@ $(IDETOP): ide/idetop.ml $(LINKCMX) $(LIBCOQRUN) $(IDETOPCMX) $(SHOW)'COQMKTOP -o $@' diff --git a/doc/changelog/02-specification-language/10997-unsupport-atts-warn.rst b/doc/changelog/02-specification-language/10997-unsupport-atts-warn.rst new file mode 100644 index 0000000000..43a748b365 --- /dev/null +++ b/doc/changelog/02-specification-language/10997-unsupport-atts-warn.rst @@ -0,0 +1,3 @@ +- The unsupported attribute error is now an error-by-default warning, + meaning it can be disabled (`#10997 + <https://github.com/coq/coq/pull/10997>`_, by Gaëtan Gilbert). diff --git a/doc/changelog/03-notations/09883-numeral-notations-sorts.rst b/doc/changelog/03-notations/09883-numeral-notations-sorts.rst new file mode 100644 index 0000000000..abc5a516ae --- /dev/null +++ b/doc/changelog/03-notations/09883-numeral-notations-sorts.rst @@ -0,0 +1,4 @@ +- Numeral Notations now support sorts in the input to printing + functions (e.g., numeral notations can be defined for terms + containing things like `@cons Set nat nil`). (`#9883 + <https://github.com/coq/coq/pull/9883>`_, by Jason Gross). diff --git a/doc/sphinx/language/gallina-specification-language.rst b/doc/sphinx/language/gallina-specification-language.rst index ae9d284661..dd65d4aeb3 100644 --- a/doc/sphinx/language/gallina-specification-language.rst +++ b/doc/sphinx/language/gallina-specification-language.rst @@ -1556,6 +1556,11 @@ the following attributes names are recognized: now foo. Abort. +.. warn:: Unsupported attribute + + This warning is an error by default. It is caused by using a + command with some attribute it does not understand. + .. [1] This is similar to the expression “*entry* :math:`\{` sep *entry* :math:`\}`” in standard BNF, or “*entry* :math:`(` sep *entry* diff --git a/doc/sphinx/user-extensions/syntax-extensions.rst b/doc/sphinx/user-extensions/syntax-extensions.rst index a28ce600ca..02910e603a 100644 --- a/doc/sphinx/user-extensions/syntax-extensions.rst +++ b/doc/sphinx/user-extensions/syntax-extensions.rst @@ -1442,8 +1442,8 @@ Numeral notations of the resulting term will be refreshed. Note that only fully-reduced ground terms (terms containing only - function application, constructors, inductive type families, and - primitive integers) will be considered for printing. + function application, constructors, inductive type families, + sorts, and primitive integers) will be considered for printing. .. cmdv:: Numeral Notation @ident__1 @ident__2 @ident__3 : @scope (warning after @num). @@ -1592,8 +1592,8 @@ String notations of the resulting term will be refreshed. Note that only fully-reduced ground terms (terms containing only - function application, constructors, inductive type families, and - primitive integers) will be considered for printing. + function application, constructors, inductive type families, + sorts, and primitive integers) will be considered for printing. .. exn:: Cannot interpret this string as a value of type @type diff --git a/interp/notation.ml b/interp/notation.ml index 70d3e4175e..c157cf43fb 100644 --- a/interp/notation.ml +++ b/interp/notation.ml @@ -503,6 +503,9 @@ let rec constr_of_glob env sigma g = match DAst.get g with let sigma,cl = List.fold_left_map (constr_of_glob env) sigma gcl in sigma,mkApp (c, Array.of_list cl) | Glob_term.GInt i -> sigma, mkInt i + | Glob_term.GSort gs -> + let sigma,c = Evd.fresh_sort_in_family sigma (Glob_ops.glob_sort_family gs) in + sigma,mkSort c | _ -> raise NotAValidPrimToken @@ -516,6 +519,10 @@ let rec glob_of_constr token_kind ?loc env sigma c = match Constr.kind c with | Ind (ind, _) -> DAst.make ?loc (Glob_term.GRef (GlobRef.IndRef ind, None)) | Var id -> DAst.make ?loc (Glob_term.GRef (GlobRef.VarRef id, None)) | Int i -> DAst.make ?loc (Glob_term.GInt i) + | Sort Sorts.SProp -> DAst.make ?loc (Glob_term.GSort (Glob_term.UNamed [Glob_term.GSProp, 0])) + | Sort Sorts.Prop -> DAst.make ?loc (Glob_term.GSort (Glob_term.UNamed [Glob_term.GProp, 0])) + | Sort Sorts.Set -> DAst.make ?loc (Glob_term.GSort (Glob_term.UNamed [Glob_term.GSet, 0])) + | Sort (Sorts.Type _) -> DAst.make ?loc (Glob_term.GSort (Glob_term.UAnonymous {rigid=true})) | _ -> Loc.raise ?loc (PrimTokenNotationError(token_kind,env,sigma,UnexpectedTerm c)) let no_such_prim_token uninterpreted_token_kind ?loc ty = diff --git a/test-suite/output/NumeralNotations.out b/test-suite/output/NumeralNotations.out index 460c77879c..505dc52ebe 100644 --- a/test-suite/output/NumeralNotations.out +++ b/test-suite/output/NumeralNotations.out @@ -180,3 +180,41 @@ let v := 4%Zlike in v : Zlike : Zlike 0%Zlike : Zlike +let v := 0%kt in v : ty + : ty +let v := 1%kt in v : ty + : ty +let v := 2%kt in v : ty + : ty +let v := 3%kt in v : ty + : ty +let v := 4%kt in v : ty + : ty +let v := 5%kt in v : ty + : ty +The command has indeed failed with message: +Cannot interpret this number as a value of type ty + = 0%kt + : ty + = 1%kt + : ty + = 2%kt + : ty + = 3%kt + : ty + = 4%kt + : ty + = 5%kt + : ty +let v : ty := Build_ty Empty_set zero in v : ty + : ty +let v : ty := Build_ty unit one in v : ty + : ty +let v : ty := Build_ty bool two in v : ty + : ty +let v : ty := Build_ty Prop prop in v : ty + : ty +let v : ty := Build_ty Set set in v : ty + : ty +let v : ty := Build_ty Type type in v : ty + : ty diff --git a/test-suite/output/NumeralNotations.v b/test-suite/output/NumeralNotations.v index 44805ad09d..c306b15ef3 100644 --- a/test-suite/output/NumeralNotations.v +++ b/test-suite/output/NumeralNotations.v @@ -391,3 +391,68 @@ Module Test19. Check {| summands := (cons 1 (cons 2 (cons (-1) nil)))%Z |}. Check {| summands := nil |}. End Test19. + +Module Test20. + (** Test Sorts *) + Local Set Universe Polymorphism. + Inductive known_type : Type -> Type := + | prop : known_type Prop + | set : known_type Set + | type : known_type Type + | zero : known_type Empty_set + | one : known_type unit + | two : known_type bool. + + Existing Class known_type. + Existing Instances zero one two prop. + Existing Instance set | 2. + Existing Instance type | 4. + + Record > ty := { t : Type ; kt : known_type t }. + + Definition ty_of_uint (x : Decimal.uint) : option ty + := match Nat.of_uint x with + | 0 => @Some ty zero + | 1 => @Some ty one + | 2 => @Some ty two + | 3 => @Some ty prop + | 4 => @Some ty set + | 5 => @Some ty type + | _ => None + end. + Definition uint_of_ty (x : ty) : Decimal.uint + := Nat.to_uint match kt x with + | prop => 3 + | set => 4 + | type => 5 + | zero => 0 + | one => 1 + | two => 2 + end. + + Declare Scope kt_scope. + Delimit Scope kt_scope with kt. + + Numeral Notation ty ty_of_uint uint_of_ty : kt_scope. + + Check let v := 0%kt in v : ty. + Check let v := 1%kt in v : ty. + Check let v := 2%kt in v : ty. + Check let v := 3%kt in v : ty. + Check let v := 4%kt in v : ty. + Check let v := 5%kt in v : ty. + Fail Check let v := 6%kt in v : ty. + Eval cbv in (_ : known_type Empty_set) : ty. + Eval cbv in (_ : known_type unit) : ty. + Eval cbv in (_ : known_type bool) : ty. + Eval cbv in (_ : known_type Prop) : ty. + Eval cbv in (_ : known_type Set) : ty. + Eval cbv in (_ : known_type Type) : ty. + Local Set Printing All. + Check let v := 0%kt in v : ty. + Check let v := 1%kt in v : ty. + Check let v := 2%kt in v : ty. + Check let v := 3%kt in v : ty. + Check let v := 4%kt in v : ty. + Check let v := 5%kt in v : ty. +End Test20. 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..72c496d56d 100644 --- a/theories/Numbers/Cyclic/Int63/Int63.v +++ b/theories/Numbers/Cyclic/Int63/Int63.v @@ -1354,8 +1354,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 +1571,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 +1620,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/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/vernac/attributes.ml b/vernac/attributes.ml index 6af454eee5..b7a3b002bd 100644 --- a/vernac/attributes.ml +++ b/vernac/attributes.ml @@ -18,13 +18,17 @@ and vernac_flag_value = | VernacFlagLeaf of string | VernacFlagList of vernac_flags +let warn_unsupported_attributes = + CWarnings.create ~name:"unsupported-attributes" ~category:"parsing" ~default:CWarnings.AsError + (fun atts -> + let keys = List.map fst atts in + let keys = List.sort_uniq String.compare keys in + let conj = match keys with [_] -> "this attribute: " | _ -> "these attributes: " in + Pp.(str "This command does not support " ++ str conj ++ prlist str keys ++ str".")) + let unsupported_attributes = function | [] -> () - | atts -> - let keys = List.map fst atts in - let keys = List.sort_uniq String.compare keys in - let conj = match keys with [_] -> "this attribute: " | _ -> "these attributes: " in - user_err Pp.(str "This command does not support " ++ str conj ++ prlist str keys ++ str".") + | atts -> warn_unsupported_attributes atts type 'a key_parser = 'a option -> vernac_flag_value -> 'a |