diff options
| author |  Benjamin Barenblat <bbaren@debian.org> | 2019-02-02 19:29:23 -0500 |
|---|---|---|
| committer | Benjamin Barenblat <bbaren@debian.org> | 2019-02-02 19:29:23 -0500 |
| commit | 9ebf44d84754adc5b64fcf612c6816c02c80462d (patch) | |
| tree | bf5e06a28488e0e06a2f2011ff0d110e2e02f8fc /theories | |
| parent | 9043add656177eeac1491a73d2f3ab92bec0013c (diff) | |
Imported Upstream version 8.9.0upstream/8.9.0upstream
Diffstat (limited to 'theories')
70 files changed, 1373 insertions, 535 deletions
diff --git a/theories/Arith/Compare_dec.v b/theories/Arith/Compare_dec.v index 713aef85..6f220f20 100644 --- a/theories/Arith/Compare_dec.v +++ b/theories/Arith/Compare_dec.v @@ -135,10 +135,10 @@ Qed. See now [Nat.compare] and its properties. In scope [nat_scope], the notation for [Nat.compare] is "?=" *) -Notation nat_compare := Nat.compare (compat "8.6"). +Notation nat_compare := Nat.compare (compat "8.7"). -Notation nat_compare_spec := Nat.compare_spec (compat "8.6"). -Notation nat_compare_eq_iff := Nat.compare_eq_iff (compat "8.6"). +Notation nat_compare_spec := Nat.compare_spec (compat "8.7"). +Notation nat_compare_eq_iff := Nat.compare_eq_iff (compat "8.7"). Notation nat_compare_S := Nat.compare_succ (only parsing). Lemma nat_compare_lt n m : n<m <-> (n ?= m) = Lt. diff --git a/theories/Bool/Bool.v b/theories/Bool/Bool.v index edf78ed5..66a82008 100644 --- a/theories/Bool/Bool.v +++ b/theories/Bool/Bool.v @@ -814,3 +814,10 @@ Defined. (** Reciprocally, from a decidability, we could state a [reflect] as soon as we have a [bool_of_sumbool]. *) + +(** For instance, we could state the correctness of [Bool.eqb] via [reflect]: *) + +Lemma eqb_spec (b b' : bool) : reflect (b = b') (eqb b b'). +Proof. + destruct b, b'; now constructor. +Qed. diff --git a/theories/Compat/Coq88.v b/theories/Compat/Coq88.v index 4142af05..950cd824 100644 --- a/theories/Compat/Coq88.v +++ b/theories/Compat/Coq88.v @@ -9,3 +9,19 @@ (************************************************************************) (** Compatibility file for making Coq act similar to Coq v8.8 *) +Require Export Coq.Compat.Coq89. + +(** In Coq 8.9, prim token notations follow [Import] rather than + [Require]. So we make all of the relevant notations accessible in + compatibility mode. *) +Require Coq.Strings.Ascii Coq.Strings.String. +Require Coq.ZArith.BinIntDef Coq.PArith.BinPosDef Coq.NArith.BinNatDef. +Require Coq.Reals.Rdefinitions. +Require Coq.Numbers.Cyclic.Int31.Int31. +Declare ML Module "string_syntax_plugin". +Declare ML Module "ascii_syntax_plugin". +Declare ML Module "r_syntax_plugin". +Declare ML Module "int31_syntax_plugin". +Numeral Notation BinNums.Z BinIntDef.Z.of_int BinIntDef.Z.to_int : Z_scope. +Numeral Notation BinNums.positive BinPosDef.Pos.of_int BinPosDef.Pos.to_int : positive_scope. +Numeral Notation BinNums.N BinNatDef.N.of_int BinNatDef.N.to_int : N_scope. diff --git a/theories/Compat/Coq86.v b/theories/Compat/Coq89.v index 666be207..d2567188 100644 --- a/theories/Compat/Coq86.v +++ b/theories/Compat/Coq89.v @@ -8,8 +8,4 @@ (* * (see LICENSE file for the text of the license) *) (************************************************************************) -(** Compatibility file for making Coq act similar to Coq v8.6 *) -Require Export Coq.Compat.Coq87. - -Require Export Coq.extraction.Extraction. -Require Export Coq.funind.FunInd. +(** Compatibility file for making Coq act similar to Coq v8.9 *) diff --git a/theories/FSets/FMapFacts.v b/theories/FSets/FMapFacts.v index 99705966..2d5a7983 100644 --- a/theories/FSets/FMapFacts.v +++ b/theories/FSets/FMapFacts.v @@ -26,7 +26,7 @@ Hint Extern 1 (Equivalence _) => constructor; congruence. Module WFacts_fun (E:DecidableType)(Import M:WSfun E). -Notation option_map := option_map (compat "8.6"). +Notation option_map := option_map (compat "8.7"). Notation eq_dec := E.eq_dec. Definition eqb x y := if eq_dec x y then true else false. diff --git a/theories/FSets/FMapFullAVL.v b/theories/FSets/FMapFullAVL.v index 34529678..c0db8646 100644 --- a/theories/FSets/FMapFullAVL.v +++ b/theories/FSets/FMapFullAVL.v @@ -27,7 +27,7 @@ *) -Require Import FunInd Recdef FMapInterface FMapList ZArith Int FMapAVL ROmega. +Require Import FunInd Recdef FMapInterface FMapList ZArith Int FMapAVL Lia. Set Implicit Arguments. Unset Strict Implicit. @@ -39,7 +39,7 @@ Import Raw.Proofs. Local Open Scope pair_scope. Local Open Scope Int_scope. -Ltac omega_max := i2z_refl; romega with Z. +Ltac omega_max := i2z_refl; lia. Section Elt. Variable elt : Type. @@ -697,7 +697,7 @@ Module IntMake_ord (I:Int)(X: OrderedType)(D : OrderedType) <: end. Proof. intros; unfold cardinal_e_2; simpl; - abstract (do 2 rewrite cons_cardinal_e; romega with * ). + abstract (do 2 rewrite cons_cardinal_e; lia ). Defined. Definition Cmp c := diff --git a/theories/FSets/FSetEqProperties.v b/theories/FSets/FSetEqProperties.v index 56844f47..59b2f789 100644 --- a/theories/FSets/FSetEqProperties.v +++ b/theories/FSets/FSetEqProperties.v @@ -333,7 +333,7 @@ Proof. auto with set. Qed. -(* caracterisation of [union] via [subset] *) +(* characterisation of [union] via [subset] *) Lemma union_subset_1: subset s (union s s')=true. Proof. @@ -408,7 +408,7 @@ intros; apply equal_1; apply inter_add_2. rewrite not_mem_iff; auto. Qed. -(* caracterisation of [union] via [subset] *) +(* characterisation of [union] via [subset] *) Lemma inter_subset_1: subset (inter s s') s=true. Proof. diff --git a/theories/Init/Datatypes.v b/theories/Init/Datatypes.v index 05b741f0..1e6843d5 100644 --- a/theories/Init/Datatypes.v +++ b/theories/Init/Datatypes.v @@ -12,7 +12,6 @@ Set Implicit Arguments. Require Import Notations. Require Import Logic. -Declare ML Module "nat_syntax_plugin". (********************************************************************) (** * Datatypes with zero and one element *) diff --git a/theories/Init/Decimal.v b/theories/Init/Decimal.v index 57163b1b..1ff00ec1 100644 --- a/theories/Init/Decimal.v +++ b/theories/Init/Decimal.v @@ -42,10 +42,10 @@ Notation zero := (D0 Nil). Inductive int := Pos (d:uint) | Neg (d:uint). -Delimit Scope uint_scope with uint. -Bind Scope uint_scope with uint. -Delimit Scope int_scope with int. -Bind Scope int_scope with int. +Delimit Scope dec_uint_scope with uint. +Bind Scope dec_uint_scope with uint. +Delimit Scope dec_int_scope with int. +Bind Scope dec_int_scope with int. (** This representation favors simplicity over canonicity. For normalizing numbers, we need to remove head zero digits, @@ -161,3 +161,9 @@ with succ_double d := end. End Little. + +(** Pseudo-conversion functions used when declaring + Numeral Notations on [uint] and [int]. *) + +Definition uint_of_uint (i:uint) := i. +Definition int_of_int (i:int) := i. diff --git a/theories/Init/Logic.v b/theories/Init/Logic.v index 15ca5abc..9d60cf54 100644 --- a/theories/Init/Logic.v +++ b/theories/Init/Logic.v @@ -29,6 +29,13 @@ Definition not (A:Prop) := A -> False. Notation "~ x" := (not x) : type_scope. +(** Create the "core" hint database, and set its transparent state for + variables and constants explicitely. *) + +Create HintDb core. +Hint Variables Opaque : core. +Hint Constants Opaque : core. + Hint Unfold not: core. (** [and A B], written [A /\ B], is the conjunction of [A] and [B] diff --git a/theories/Init/Nat.v b/theories/Init/Nat.v index ad1bc717..eb4ba0e5 100644 --- a/theories/Init/Nat.v +++ b/theories/Init/Nat.v @@ -24,6 +24,10 @@ Definition t := nat. (** ** Constants *) +Local Notation "0" := O. +Local Notation "1" := (S O). +Local Notation "2" := (S (S O)). + Definition zero := 0. Definition one := 1. Definition two := 2. diff --git a/theories/Init/Peano.v b/theories/Init/Peano.v index d5322d09..65e5e76a 100644 --- a/theories/Init/Peano.v +++ b/theories/Init/Peano.v @@ -31,6 +31,7 @@ Require Import Logic. Require Coq.Init.Nat. Open Scope nat_scope. +Local Notation "0" := O. Definition eq_S := f_equal S. Definition f_equal_nat := f_equal (A:=nat). diff --git a/theories/Init/Prelude.v b/theories/Init/Prelude.v index 802f18c0..6d98bcb3 100644 --- a/theories/Init/Prelude.v +++ b/theories/Init/Prelude.v @@ -19,9 +19,24 @@ Require Export Peano. Require Export Coq.Init.Wf. Require Export Coq.Init.Tactics. Require Export Coq.Init.Tauto. -(* Initially available plugins - (+ nat_syntax_plugin loaded in Datatypes) *) +(* Some initially available plugins. See also: + - ltac_plugin (in Notations) + - tauto_plugin (in Tauto). +*) Declare ML Module "cc_plugin". Declare ML Module "ground_plugin". +Declare ML Module "numeral_notation_plugin". + +(* Parsing / printing of decimal numbers *) +Arguments Nat.of_uint d%dec_uint_scope. +Arguments Nat.of_int d%dec_int_scope. +Numeral Notation Decimal.uint Decimal.uint_of_uint Decimal.uint_of_uint + : dec_uint_scope. +Numeral Notation Decimal.int Decimal.int_of_int Decimal.int_of_int + : dec_int_scope. + +(* Parsing / printing of [nat] numbers *) +Numeral Notation nat Nat.of_uint Nat.to_uint : nat_scope (abstract after 5000). + (* Default substrings not considered by queries like SearchAbout *) Add Search Blacklist "_subproof" "_subterm" "Private_". diff --git a/theories/Init/Specif.v b/theories/Init/Specif.v index b6afba29..76632312 100644 --- a/theories/Init/Specif.v +++ b/theories/Init/Specif.v @@ -745,16 +745,16 @@ Hint Resolve exist exist2 existT existT2: core. (* Compatibility *) -Notation sigS := sigT (compat "8.6"). -Notation existS := existT (compat "8.6"). -Notation sigS_rect := sigT_rect (compat "8.6"). -Notation sigS_rec := sigT_rec (compat "8.6"). -Notation sigS_ind := sigT_ind (compat "8.6"). -Notation projS1 := projT1 (compat "8.6"). -Notation projS2 := projT2 (compat "8.6"). - -Notation sigS2 := sigT2 (compat "8.6"). -Notation existS2 := existT2 (compat "8.6"). -Notation sigS2_rect := sigT2_rect (compat "8.6"). -Notation sigS2_rec := sigT2_rec (compat "8.6"). -Notation sigS2_ind := sigT2_ind (compat "8.6"). +Notation sigS := sigT (compat "8.7"). +Notation existS := existT (compat "8.7"). +Notation sigS_rect := sigT_rect (compat "8.7"). +Notation sigS_rec := sigT_rec (compat "8.7"). +Notation sigS_ind := sigT_ind (compat "8.7"). +Notation projS1 := projT1 (compat "8.7"). +Notation projS2 := projT2 (compat "8.7"). + +Notation sigS2 := sigT2 (compat "8.7"). +Notation existS2 := existT2 (compat "8.7"). +Notation sigS2_rect := sigT2_rect (compat "8.7"). +Notation sigS2_rec := sigT2_rec (compat "8.7"). +Notation sigS2_ind := sigT2_ind (compat "8.7"). diff --git a/theories/Logic/Berardi.v b/theories/Logic/Berardi.v index c6836a1c..ed4d69ab 100644 --- a/theories/Logic/Berardi.v +++ b/theories/Logic/Berardi.v @@ -82,7 +82,7 @@ End Retracts. (** This lemma is basically a commutation of implication and existential quantification: (EX x | A -> P(x)) <=> (A -> EX x | P(x)) which is provable in classical logic ( => is already provable in - intuitionnistic logic). *) + intuitionistic logic). *) Lemma L1 : forall A B:Prop, retract_cond (pow A) (pow B). Proof. @@ -136,7 +136,7 @@ trivial. Qed. -Theorem classical_proof_irrelevence : T = F. +Theorem classical_proof_irrelevance : T = F. Proof. generalize not_has_fixpoint. unfold Not_b. @@ -148,4 +148,7 @@ intros not_true is_true. elim not_true; trivial. Qed. + +Notation classical_proof_irrelevence := classical_proof_irrelevance (compat "8.8"). + End Berardis_paradox. diff --git a/theories/Logic/Diaconescu.v b/theories/Logic/Diaconescu.v index 3317766c..66e82ddb 100644 --- a/theories/Logic/Diaconescu.v +++ b/theories/Logic/Diaconescu.v @@ -234,8 +234,6 @@ Qed. (** An alternative more concise proof can be done by directly using the guarded relational choice *) -Declare Implicit Tactic auto. - Lemma proof_irrel_rel_choice_imp_eq_dec' : a1=a2 \/ ~a1=a2. Proof. assert (decide: forall x:A, x=a1 \/ x=a2 -> diff --git a/theories/Logic/EqdepFacts.v b/theories/Logic/EqdepFacts.v index d938b315..8e59941f 100644 --- a/theories/Logic/EqdepFacts.v +++ b/theories/Logic/EqdepFacts.v @@ -125,7 +125,7 @@ Proof. apply eq_dep_intro. Qed. -Notation eq_sigS_eq_dep := eq_sigT_eq_dep (compat "8.6"). (* Compatibility *) +Notation eq_sigS_eq_dep := eq_sigT_eq_dep (compat "8.7"). (* Compatibility *) Lemma eq_dep_eq_sigT : forall (U:Type) (P:U -> Type) (p q:U) (x:P p) (y:P q), diff --git a/theories/MSets/MSetEqProperties.v b/theories/MSets/MSetEqProperties.v index 1ee098cb..4f2fdcf9 100644 --- a/theories/MSets/MSetEqProperties.v +++ b/theories/MSets/MSetEqProperties.v @@ -333,7 +333,7 @@ Proof. auto with set. Qed. -(* caracterisation of [union] via [subset] *) +(* characterisation of [union] via [subset] *) Lemma union_subset_1: subset s (union s s')=true. Proof. @@ -408,7 +408,7 @@ intros; apply equal_1; apply inter_add_2. rewrite not_mem_iff; auto. Qed. -(* caracterisation of [union] via [subset] *) +(* characterisation of [union] via [subset] *) Lemma inter_subset_1: subset (inter s s') s=true. Proof. diff --git a/theories/NArith/BinNat.v b/theories/NArith/BinNat.v index 5d3ec5ab..92c124ec 100644 --- a/theories/NArith/BinNat.v +++ b/theories/NArith/BinNat.v @@ -930,6 +930,8 @@ Bind Scope N_scope with N.t N. (** Exportation of notations *) +Numeral Notation N N.of_uint N.to_uint : N_scope. + Infix "+" := N.add : N_scope. Infix "-" := N.sub : N_scope. Infix "*" := N.mul : N_scope. @@ -964,33 +966,33 @@ Notation N_ind := N_ind (only parsing). Notation N0 := N0 (only parsing). Notation Npos := N.pos (only parsing). -Notation Ndiscr := N.discr (compat "8.6"). +Notation Ndiscr := N.discr (compat "8.7"). Notation Ndouble_plus_one := N.succ_double (only parsing). -Notation Ndouble := N.double (compat "8.6"). -Notation Nsucc := N.succ (compat "8.6"). -Notation Npred := N.pred (compat "8.6"). -Notation Nsucc_pos := N.succ_pos (compat "8.6"). -Notation Ppred_N := Pos.pred_N (compat "8.6"). +Notation Ndouble := N.double (compat "8.7"). +Notation Nsucc := N.succ (compat "8.7"). +Notation Npred := N.pred (compat "8.7"). +Notation Nsucc_pos := N.succ_pos (compat "8.7"). +Notation Ppred_N := Pos.pred_N (compat "8.7"). Notation Nplus := N.add (only parsing). Notation Nminus := N.sub (only parsing). Notation Nmult := N.mul (only parsing). -Notation Neqb := N.eqb (compat "8.6"). -Notation Ncompare := N.compare (compat "8.6"). -Notation Nlt := N.lt (compat "8.6"). -Notation Ngt := N.gt (compat "8.6"). -Notation Nle := N.le (compat "8.6"). -Notation Nge := N.ge (compat "8.6"). -Notation Nmin := N.min (compat "8.6"). -Notation Nmax := N.max (compat "8.6"). -Notation Ndiv2 := N.div2 (compat "8.6"). -Notation Neven := N.even (compat "8.6"). -Notation Nodd := N.odd (compat "8.6"). -Notation Npow := N.pow (compat "8.6"). -Notation Nlog2 := N.log2 (compat "8.6"). +Notation Neqb := N.eqb (compat "8.7"). +Notation Ncompare := N.compare (compat "8.7"). +Notation Nlt := N.lt (compat "8.7"). +Notation Ngt := N.gt (compat "8.7"). +Notation Nle := N.le (compat "8.7"). +Notation Nge := N.ge (compat "8.7"). +Notation Nmin := N.min (compat "8.7"). +Notation Nmax := N.max (compat "8.7"). +Notation Ndiv2 := N.div2 (compat "8.7"). +Notation Neven := N.even (compat "8.7"). +Notation Nodd := N.odd (compat "8.7"). +Notation Npow := N.pow (compat "8.7"). +Notation Nlog2 := N.log2 (compat "8.7"). Notation nat_of_N := N.to_nat (only parsing). Notation N_of_nat := N.of_nat (only parsing). -Notation N_eq_dec := N.eq_dec (compat "8.6"). +Notation N_eq_dec := N.eq_dec (compat "8.7"). Notation Nrect := N.peano_rect (only parsing). Notation Nrect_base := N.peano_rect_base (only parsing). Notation Nrect_step := N.peano_rect_succ (only parsing). @@ -999,11 +1001,11 @@ Notation Nrec := N.peano_rec (only parsing). Notation Nrec_base := N.peano_rec_base (only parsing). Notation Nrec_succ := N.peano_rec_succ (only parsing). -Notation Npred_succ := N.pred_succ (compat "8.6"). +Notation Npred_succ := N.pred_succ (compat "8.7"). Notation Npred_minus := N.pred_sub (only parsing). -Notation Nsucc_pred := N.succ_pred (compat "8.6"). +Notation Nsucc_pred := N.succ_pred (compat "8.7"). Notation Ppred_N_spec := N.pos_pred_spec (only parsing). -Notation Nsucc_pos_spec := N.succ_pos_spec (compat "8.6"). +Notation Nsucc_pos_spec := N.succ_pos_spec (compat "8.7"). Notation Ppred_Nsucc := N.pos_pred_succ (only parsing). Notation Nplus_0_l := N.add_0_l (only parsing). Notation Nplus_0_r := N.add_0_r (only parsing). @@ -1011,7 +1013,7 @@ Notation Nplus_comm := N.add_comm (only parsing). Notation Nplus_assoc := N.add_assoc (only parsing). Notation Nplus_succ := N.add_succ_l (only parsing). Notation Nsucc_0 := N.succ_0_discr (only parsing). -Notation Nsucc_inj := N.succ_inj (compat "8.6"). +Notation Nsucc_inj := N.succ_inj (compat "8.7"). Notation Nminus_N0_Nle := N.sub_0_le (only parsing). Notation Nminus_0_r := N.sub_0_r (only parsing). Notation Nminus_succ_r:= N.sub_succ_r (only parsing). @@ -1021,29 +1023,29 @@ Notation Nmult_1_r := N.mul_1_r (only parsing). Notation Nmult_comm := N.mul_comm (only parsing). Notation Nmult_assoc := N.mul_assoc (only parsing). Notation Nmult_plus_distr_r := N.mul_add_distr_r (only parsing). -Notation Neqb_eq := N.eqb_eq (compat "8.6"). +Notation Neqb_eq := N.eqb_eq (compat "8.7"). Notation Nle_0 := N.le_0_l (only parsing). -Notation Ncompare_refl := N.compare_refl (compat "8.6"). +Notation Ncompare_refl := N.compare_refl (compat "8.7"). Notation Ncompare_Eq_eq := N.compare_eq (only parsing). Notation Ncompare_eq_correct := N.compare_eq_iff (only parsing). -Notation Nlt_irrefl := N.lt_irrefl (compat "8.6"). -Notation Nlt_trans := N.lt_trans (compat "8.6"). +Notation Nlt_irrefl := N.lt_irrefl (compat "8.7"). +Notation Nlt_trans := N.lt_trans (compat "8.7"). Notation Nle_lteq := N.lt_eq_cases (only parsing). -Notation Nlt_succ_r := N.lt_succ_r (compat "8.6"). -Notation Nle_trans := N.le_trans (compat "8.6"). -Notation Nle_succ_l := N.le_succ_l (compat "8.6"). -Notation Ncompare_spec := N.compare_spec (compat "8.6"). +Notation Nlt_succ_r := N.lt_succ_r (compat "8.7"). +Notation Nle_trans := N.le_trans (compat "8.7"). +Notation Nle_succ_l := N.le_succ_l (compat "8.7"). +Notation Ncompare_spec := N.compare_spec (compat "8.7"). Notation Ncompare_0 := N.compare_0_r (only parsing). Notation Ndouble_div2 := N.div2_double (only parsing). Notation Ndouble_plus_one_div2 := N.div2_succ_double (only parsing). -Notation Ndouble_inj := N.double_inj (compat "8.6"). +Notation Ndouble_inj := N.double_inj (compat "8.7"). Notation Ndouble_plus_one_inj := N.succ_double_inj (only parsing). -Notation Npow_0_r := N.pow_0_r (compat "8.6"). -Notation Npow_succ_r := N.pow_succ_r (compat "8.6"). -Notation Nlog2_spec := N.log2_spec (compat "8.6"). -Notation Nlog2_nonpos := N.log2_nonpos (compat "8.6"). -Notation Neven_spec := N.even_spec (compat "8.6"). -Notation Nodd_spec := N.odd_spec (compat "8.6"). +Notation Npow_0_r := N.pow_0_r (compat "8.7"). +Notation Npow_succ_r := N.pow_succ_r (compat "8.7"). +Notation Nlog2_spec := N.log2_spec (compat "8.7"). +Notation Nlog2_nonpos := N.log2_nonpos (compat "8.7"). +Notation Neven_spec := N.even_spec (compat "8.7"). +Notation Nodd_spec := N.odd_spec (compat "8.7"). Notation Nlt_not_eq := N.lt_neq (only parsing). Notation Ngt_Nlt := N.gt_lt (only parsing). diff --git a/theories/NArith/BinNatDef.v b/theories/NArith/BinNatDef.v index 5de75537..be12fffa 100644 --- a/theories/NArith/BinNatDef.v +++ b/theories/NArith/BinNatDef.v @@ -13,6 +13,10 @@ Require Import BinPos. Local Open Scope N_scope. +Local Notation "0" := N0. +Local Notation "1" := (Npos 1). +Local Notation "2" := (Npos 2). + (**********************************************************************) (** * Binary natural numbers, definitions of operations *) (**********************************************************************) @@ -398,4 +402,9 @@ Definition to_uint n := Definition to_int n := Decimal.Pos (to_uint n). +Numeral Notation N of_uint to_uint : N_scope. + End N. + +(** Re-export the notation for those who just [Import NatIntDef] *) +Numeral Notation N N.of_uint N.to_uint : N_scope. diff --git a/theories/NArith/Ndec.v b/theories/NArith/Ndec.v index 67c30f22..e2b2b490 100644 --- a/theories/NArith/Ndec.v +++ b/theories/NArith/Ndec.v @@ -22,8 +22,8 @@ Local Open Scope N_scope. (** Obsolete results about boolean comparisons over [N], kept for compatibility with IntMap and SMC. *) -Notation Peqb := Pos.eqb (compat "8.6"). -Notation Neqb := N.eqb (compat "8.6"). +Notation Peqb := Pos.eqb (compat "8.7"). +Notation Neqb := N.eqb (compat "8.7"). Notation Peqb_correct := Pos.eqb_refl (only parsing). Notation Neqb_correct := N.eqb_refl (only parsing). Notation Neqb_comm := N.eqb_sym (only parsing). diff --git a/theories/NArith/Ndigits.v b/theories/NArith/Ndigits.v index 3ccaa721..a2a2430e 100644 --- a/theories/NArith/Ndigits.v +++ b/theories/NArith/Ndigits.v @@ -517,6 +517,23 @@ Definition N2Bv (n:N) : Bvector (N.size_nat n) := | Npos p => P2Bv p end. +Fixpoint P2Bv_sized (m : nat) (p : positive) : Bvector m := + match m with + | O => [] + | S m => + match p with + | xI p => true :: P2Bv_sized m p + | xO p => false :: P2Bv_sized m p + | xH => true :: Bvect_false m + end + end. + +Definition N2Bv_sized (m : nat) (n : N) : Bvector m := + match n with + | N0 => Bvect_false m + | Npos p => P2Bv_sized m p + end. + Fixpoint Bv2N (n:nat)(bv:Bvector n) : N := match bv with | Vector.nil _ => N0 @@ -561,6 +578,7 @@ Qed. (** To state nonetheless a second result about composition of conversions, we define a conversion on a given number of bits : *) +#[deprecated(since = "8.9.0", note = "Use N2Bv_sized instead.")] Fixpoint N2Bv_gen (n:nat)(a:N) : Bvector n := match n return Bvector n with | 0 => Bnil @@ -670,3 +688,28 @@ rewrite H. destruct a, b, (Bv2N n v1), (Bv2N n v2); simpl; auto. Qed. + +Lemma N2Bv_sized_Nsize (n : N) : + N2Bv_sized (N.size_nat n) n = N2Bv n. +Proof with simpl; auto. + destruct n... + induction p... + all: rewrite IHp... +Qed. + +Lemma N2Bv_sized_Bv2N (n : nat) (v : Bvector n) : + N2Bv_sized n (Bv2N n v) = v. +Proof with simpl; auto. + induction v... + destruct h; + unfold N2Bv_sized; + destruct (Bv2N n v) as [|[]]; + rewrite <- IHv... +Qed. + +Lemma N2Bv_N2Bv_sized_above (a : N) (k : nat) : + N2Bv_sized (N.size_nat a + k) a = N2Bv a ++ Bvect_false k. +Proof with auto. + destruct a... + induction p; simpl; f_equal... +Qed. diff --git a/theories/NArith/Ndiv_def.v b/theories/NArith/Ndiv_def.v index 7c9fd869..885c0d48 100644 --- a/theories/NArith/Ndiv_def.v +++ b/theories/NArith/Ndiv_def.v @@ -24,10 +24,10 @@ Lemma Pdiv_eucl_remainder a b : snd (Pdiv_eucl a b) < Npos b. Proof. now apply (N.pos_div_eucl_remainder a (Npos b)). Qed. -Notation Ndiv_eucl := N.div_eucl (compat "8.6"). -Notation Ndiv := N.div (compat "8.6"). +Notation Ndiv_eucl := N.div_eucl (compat "8.7"). +Notation Ndiv := N.div (compat "8.7"). Notation Nmod := N.modulo (only parsing). Notation Ndiv_eucl_correct := N.div_eucl_spec (only parsing). Notation Ndiv_mod_eq := N.div_mod' (only parsing). -Notation Nmod_lt := N.mod_lt (compat "8.6"). +Notation Nmod_lt := N.mod_lt (compat "8.7"). diff --git a/theories/NArith/Nsqrt_def.v b/theories/NArith/Nsqrt_def.v index e771fe91..f0433283 100644 --- a/theories/NArith/Nsqrt_def.v +++ b/theories/NArith/Nsqrt_def.v @@ -13,8 +13,8 @@ Require Import BinNat. (** Obsolete file, see [BinNat] now, only compatibility notations remain here. *) -Notation Nsqrtrem := N.sqrtrem (compat "8.6"). -Notation Nsqrt := N.sqrt (compat "8.6"). -Notation Nsqrtrem_spec := N.sqrtrem_spec (compat "8.6"). +Notation Nsqrtrem := N.sqrtrem (compat "8.7"). +Notation Nsqrt := N.sqrt (compat "8.7"). +Notation Nsqrtrem_spec := N.sqrtrem_spec (compat "8.7"). Notation Nsqrt_spec := (fun n => N.sqrt_spec n (N.le_0_l n)) (only parsing). -Notation Nsqrtrem_sqrt := N.sqrtrem_sqrt (compat "8.6"). +Notation Nsqrtrem_sqrt := N.sqrtrem_sqrt (compat "8.7"). diff --git a/theories/Numbers/AltBinNotations.v b/theories/Numbers/AltBinNotations.v new file mode 100644 index 00000000..c7e39996 --- /dev/null +++ b/theories/Numbers/AltBinNotations.v @@ -0,0 +1,69 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) + +(** * Alternative Binary Numeral Notations *) + +(** Faster but less safe parsers and printers of [positive], [N], [Z]. *) + +(** By default, literals in types [positive], [N], [Z] are parsed and + printed via the [Numeral Notation] command, by conversion from/to + the [Decimal.int] representation. When working with numbers with + thousands of digits and more, conversion from/to [Decimal.int] can + become significantly slow. If that becomes a problem for your + development, this file provides some alternative [Numeral + Notation] commmands that use [Z] as bridge type. To enable these + commands, just be sure to [Require] this file after other files + defining numeral notations. + + Note: up to Coq 8.8, literals in types [positive], [N], [Z] were + parsed and printed using a native ML library of arbitrary + precision integers named bigint.ml. From 8.9, the default is to + parse and print using a Coq library converting sequences of + digits, hence reducing the amount of ML code to trust. But this + method is slower. This file then gives access to the legacy + method, trading efficiency against a larger ML trust base relying + on bigint.ml. *) + +Require Import BinNums. + +(** [positive] *) + +Definition pos_of_z z := + match z with + | Zpos p => Some p + | _ => None + end. + +Definition pos_to_z p := Zpos p. + +Numeral Notation positive pos_of_z pos_to_z : positive_scope. + +(** [N] *) + +Definition n_of_z z := + match z with + | Z0 => Some N0 + | Zpos p => Some (Npos p) + | Zneg _ => None + end. + +Definition n_to_z n := + match n with + | N0 => Z0 + | Npos p => Zpos p + end. + +Numeral Notation N n_of_z n_to_z : N_scope. + +(** [Z] *) + +Definition z_of_z (z:Z) := z. + +Numeral Notation Z z_of_z z_of_z : Z_scope. diff --git a/theories/Numbers/BinNums.v b/theories/Numbers/BinNums.v index f8b3d9e1..3ba9d1f5 100644 --- a/theories/Numbers/BinNums.v +++ b/theories/Numbers/BinNums.v @@ -12,13 +12,11 @@ Set Implicit Arguments. -Declare ML Module "z_syntax_plugin". - (** [positive] is a datatype representing the strictly positive integers in a binary way. Starting from 1 (represented by [xH]), one can add a new least significant digit via [xO] (digit 0) or [xI] (digit 1). - Numbers in [positive] can also be denoted using a decimal notation; - e.g. [6%positive] abbreviates [xO (xI xH)] *) + Numbers in [positive] will also be denoted using a decimal notation; + e.g. [6%positive] will abbreviate [xO (xI xH)] *) Inductive positive : Set := | xI : positive -> positive @@ -32,8 +30,8 @@ Arguments xI _%positive. (** [N] is a datatype representing natural numbers in a binary way, by extending the [positive] datatype with a zero. - Numbers in [N] can also be denoted using a decimal notation; - e.g. [6%N] abbreviates [Npos (xO (xI xH))] *) + Numbers in [N] will also be denoted using a decimal notation; + e.g. [6%N] will abbreviate [Npos (xO (xI xH))] *) Inductive N : Set := | N0 : N @@ -47,8 +45,8 @@ Arguments Npos _%positive. An integer is either zero or a strictly positive number (coded as a [positive]) or a strictly negative number (whose opposite is stored as a [positive] value). - Numbers in [Z] can also be denoted using a decimal notation; - e.g. [(-6)%Z] abbreviates [Zneg (xO (xI xH))] *) + Numbers in [Z] will also be denoted using a decimal notation; + e.g. [(-6)%Z] will abbreviate [Zneg (xO (xI xH))] *) Inductive Z : Set := | Z0 : Z diff --git a/theories/Numbers/Cyclic/Int31/Cyclic31.v b/theories/Numbers/Cyclic/Int31/Cyclic31.v index bd4f0279..4a1f24b9 100644 --- a/theories/Numbers/Cyclic/Int31/Cyclic31.v +++ b/theories/Numbers/Cyclic/Int31/Cyclic31.v @@ -21,9 +21,7 @@ Require Import Znumtheory. Require Import Zgcd_alt. Require Import Zpow_facts. Require Import CyclicAxioms. -Require Import ROmega. - -Declare ML Module "int31_syntax_plugin". +Require Import Lia. Local Open Scope nat_scope. Local Open Scope int31_scope. @@ -128,7 +126,7 @@ Section Basics. Lemma nshiftl_S_tail : forall n x, nshiftl x (S n) = nshiftl (shiftl x) n. - Proof. + Proof. intros n; elim n; simpl; intros; now f_equal. Qed. @@ -1239,7 +1237,7 @@ Section Int31_Specs. destruct (Z_lt_le_dec (X+Y) wB). contradict H1; auto using Zmod_small with zarith. rewrite <- (Z_mod_plus_full (X+Y) (-1) wB). - rewrite Zmod_small; romega. + rewrite Zmod_small; lia. generalize (Z.compare_eq ((X+Y) mod wB) (X+Y)); intros Heq. destruct Z.compare; intros; @@ -1263,7 +1261,7 @@ Section Int31_Specs. destruct (Z_lt_le_dec (X+Y+1) wB). contradict H1; auto using Zmod_small with zarith. rewrite <- (Z_mod_plus_full (X+Y+1) (-1) wB). - rewrite Zmod_small; romega. + rewrite Zmod_small; lia. generalize (Z.compare_eq ((X+Y+1) mod wB) (X+Y+1)); intros Heq. destruct Z.compare; intros; @@ -1301,8 +1299,8 @@ Section Int31_Specs. unfold interp_carry; rewrite phi_phi_inv, Z.compare_eq_iff; intros. destruct (Z_lt_le_dec (X-Y) 0). rewrite <- (Z_mod_plus_full (X-Y) 1 wB). - rewrite Zmod_small; romega. - contradict H1; apply Zmod_small; romega. + rewrite Zmod_small; lia. + contradict H1; apply Zmod_small; lia. generalize (Z.compare_eq ((X-Y) mod wB) (X-Y)); intros Heq. destruct Z.compare; intros; @@ -1320,8 +1318,8 @@ Section Int31_Specs. unfold interp_carry; rewrite phi_phi_inv, Z.compare_eq_iff; intros. destruct (Z_lt_le_dec (X-Y-1) 0). rewrite <- (Z_mod_plus_full (X-Y-1) 1 wB). - rewrite Zmod_small; romega. - contradict H1; apply Zmod_small; romega. + rewrite Zmod_small; lia. + contradict H1; apply Zmod_small; lia. generalize (Z.compare_eq ((X-Y-1) mod wB) (X-Y-1)); intros Heq. destruct Z.compare; intros; @@ -1358,7 +1356,7 @@ Section Int31_Specs. change [|1|] with 1; change [|0|] with 0. rewrite <- (Z_mod_plus_full (0-[|x|]) 1 wB). rewrite Zminus_mod_idemp_l. - rewrite Zmod_small; generalize (phi_bounded x); romega. + rewrite Zmod_small; generalize (phi_bounded x); lia. Qed. Lemma spec_pred_c : forall x, [-|sub31c x 1|] = [|x|] - 1. diff --git a/theories/Numbers/Cyclic/Int31/Int31.v b/theories/Numbers/Cyclic/Int31/Int31.v index 9f8da831..927f430f 100644 --- a/theories/Numbers/Cyclic/Int31/Int31.v +++ b/theories/Numbers/Cyclic/Int31/Int31.v @@ -15,11 +15,15 @@ Require Import Wf_nat. Require Export ZArith. Require Export DoubleType. +Declare ML Module "int31_syntax_plugin". + +Local Unset Elimination Schemes. + (** * 31-bit integers *) (** This file contains basic definitions of a 31-bit integer arithmetic. In fact it is more general than that. The only reason - for this use of 31 is the underlying mecanism for hardware-efficient + for this use of 31 is the underlying mechanism for hardware-efficient computations by A. Spiwack. Apart from this, a switch to, say, 63-bit integers is now just a matter of replacing every occurrences of 31 by 63. This is actually made possible by the use of @@ -48,6 +52,10 @@ Inductive int31 : Type := I31 : digits31 int31. Register digits as int31 bits in "coq_int31" by True. Register int31 as int31 type in "coq_int31" by True. +Scheme int31_ind := Induction for int31 Sort Prop. +Scheme int31_rec := Induction for int31 Sort Set. +Scheme int31_rect := Induction for int31 Sort Type. + Delimit Scope int31_scope with int31. Bind Scope int31_scope with int31. Local Open Scope int31_scope. diff --git a/theories/Numbers/DecimalString.v b/theories/Numbers/DecimalString.v index 1a3220f6..591024ba 100644 --- a/theories/Numbers/DecimalString.v +++ b/theories/Numbers/DecimalString.v @@ -94,7 +94,7 @@ Definition int_of_string s := match s with | EmptyString => Some (Pos Nil) | String a s' => - if ascii_dec a "-" then option_map Neg (uint_of_string s') + if Ascii.eqb a "-" then option_map Neg (uint_of_string s') else option_map Pos (uint_of_string s) end. @@ -131,8 +131,8 @@ Proof. - unfold int_of_string. destruct (string_of_uint d) eqn:Hd. + now destruct d. - + destruct ascii_dec; subst. - * now destruct d. + + case Ascii.eqb_spec. + * intros ->. now destruct d. * rewrite <- Hd, usu; auto. - rewrite usu; auto. Qed. @@ -141,8 +141,8 @@ Lemma sis s d : int_of_string s = Some d -> string_of_int d = s. Proof. destruct s; [intros [= <-]| ]; simpl; trivial. - destruct ascii_dec; subst; simpl. - - destruct (uint_of_string s) eqn:Hs; simpl; intros [= <-]. + case Ascii.eqb_spec. + - intros ->. destruct (uint_of_string s) eqn:Hs; simpl; intros [= <-]. simpl; f_equal. now apply sus. - destruct d; [ | now destruct uint_of_char]. simpl string_of_int. @@ -178,7 +178,7 @@ Definition int_of_string s := match s with | EmptyString => None | String a s' => - if ascii_dec a "-" then option_map Neg (uint_of_string s') + if Ascii.eqb a "-" then option_map Neg (uint_of_string s') else option_map Pos (uint_of_string s) end. @@ -228,8 +228,8 @@ Proof. unfold int_of_string. destruct (string_of_uint d) eqn:Hd. + now destruct d. - + destruct ascii_dec; subst. - * now destruct d. + + case Ascii.eqb_spec. + * intros ->. now destruct d. * rewrite <- Hd, usu; auto. now intros ->. - intros _ H. rewrite usu; auto. now intros ->. @@ -253,8 +253,8 @@ Lemma sis s d : int_of_string s = Some d -> string_of_int d = s. Proof. destruct s; [intros [=]| ]; simpl. - destruct ascii_dec; subst; simpl. - - destruct (uint_of_string s) eqn:Hs; simpl; intros [= <-]. + case Ascii.eqb_spec. + - intros ->. destruct (uint_of_string s) eqn:Hs; simpl; intros [= <-]. simpl; f_equal. now apply sus. - destruct d; [ | now destruct uint_of_char]. simpl string_of_int. diff --git a/theories/Numbers/Integer/Abstract/ZBits.v b/theories/Numbers/Integer/Abstract/ZBits.v index 2da44528..4aabda77 100644 --- a/theories/Numbers/Integer/Abstract/ZBits.v +++ b/theories/Numbers/Integer/Abstract/ZBits.v @@ -80,7 +80,7 @@ Proof. now apply testbit_even_succ. Qed. -(** Alternative caracterisations of [testbit] *) +(** Alternative characterisations of [testbit] *) (** This concise equation could have been taken as specification for testbit in the interface, but it would have been hard to @@ -102,10 +102,10 @@ Proof. left. destruct b; split; simpl; order'. Qed. -(** This caracterisation that uses only basic operations and +(** This characterisation that uses only basic operations and power was initially taken as specification for testbit. We describe [a] as having a low part and a high part, with - the corresponding bit in the middle. This caracterisation + the corresponding bit in the middle. This characterisation is moderatly complex to implement, but also moderately usable... *) diff --git a/theories/Numbers/Integer/Abstract/ZDivEucl.v b/theories/Numbers/Integer/Abstract/ZDivEucl.v index d7f25a66..5a7bd9ab 100644 --- a/theories/Numbers/Integer/Abstract/ZDivEucl.v +++ b/theories/Numbers/Integer/Abstract/ZDivEucl.v @@ -13,7 +13,7 @@ Require Import ZAxioms ZMulOrder ZSgnAbs NZDiv. (** * Euclidean Division for integers, Euclid convention We use here the "usual" formulation of the Euclid Theorem - [forall a b, b<>0 -> exists b q, a = b*q+r /\ 0 < r < |b| ] + [forall a b, b<>0 -> exists r q, a = b*q+r /\ 0 <= r < |b| ] The outcome of the modulo function is hence always positive. This corresponds to convention "E" in the following paper: diff --git a/theories/Numbers/Natural/Abstract/NBits.v b/theories/Numbers/Natural/Abstract/NBits.v index e1391f59..90663de3 100644 --- a/theories/Numbers/Natural/Abstract/NBits.v +++ b/theories/Numbers/Natural/Abstract/NBits.v @@ -78,7 +78,7 @@ Proof. apply testbit_even_succ, le_0_l. Qed. -(** Alternative caracterisations of [testbit] *) +(** Alternative characterisations of [testbit] *) (** This concise equation could have been taken as specification for testbit in the interface, but it would have been hard to @@ -99,10 +99,10 @@ Proof. destruct b; order'. Qed. -(** This caracterisation that uses only basic operations and +(** This characterisation that uses only basic operations and power was initially taken as specification for testbit. We describe [a] as having a low part and a high part, with - the corresponding bit in the middle. This caracterisation + the corresponding bit in the middle. This characterisation is moderatly complex to implement, but also moderately usable... *) diff --git a/theories/PArith/BinPos.v b/theories/PArith/BinPos.v index 000d895e..01ecdd71 100644 --- a/theories/PArith/BinPos.v +++ b/theories/PArith/BinPos.v @@ -1871,6 +1871,8 @@ Bind Scope positive_scope with Pos.t positive. (** Exportation of notations *) +Numeral Notation positive Pos.of_int Pos.to_uint : positive_scope. + Infix "+" := Pos.add : positive_scope. Infix "-" := Pos.sub : positive_scope. Infix "*" := Pos.mul : positive_scope. @@ -1905,12 +1907,12 @@ Notation IsNul := Pos.IsNul (only parsing). Notation IsPos := Pos.IsPos (only parsing). Notation IsNeg := Pos.IsNeg (only parsing). -Notation Psucc := Pos.succ (compat "8.6"). +Notation Psucc := Pos.succ (compat "8.7"). Notation Pplus := Pos.add (only parsing). Notation Pplus_carry := Pos.add_carry (only parsing). -Notation Ppred := Pos.pred (compat "8.6"). -Notation Piter_op := Pos.iter_op (compat "8.6"). -Notation Piter_op_succ := Pos.iter_op_succ (compat "8.6"). +Notation Ppred := Pos.pred (compat "8.7"). +Notation Piter_op := Pos.iter_op (compat "8.7"). +Notation Piter_op_succ := Pos.iter_op_succ (compat "8.7"). Notation Pmult_nat := (Pos.iter_op plus) (only parsing). Notation nat_of_P := Pos.to_nat (only parsing). Notation P_of_succ_nat := Pos.of_succ_nat (only parsing). @@ -1920,29 +1922,29 @@ Notation positive_mask_rect := Pos.mask_rect (only parsing). Notation positive_mask_ind := Pos.mask_ind (only parsing). Notation positive_mask_rec := Pos.mask_rec (only parsing). Notation Pdouble_plus_one_mask := Pos.succ_double_mask (only parsing). -Notation Pdouble_mask := Pos.double_mask (compat "8.6"). +Notation Pdouble_mask := Pos.double_mask (compat "8.7"). Notation Pdouble_minus_two := Pos.double_pred_mask (only parsing). Notation Pminus_mask := Pos.sub_mask (only parsing). Notation Pminus_mask_carry := Pos.sub_mask_carry (only parsing). Notation Pminus := Pos.sub (only parsing). Notation Pmult := Pos.mul (only parsing). Notation iter_pos := @Pos.iter (only parsing). -Notation Ppow := Pos.pow (compat "8.6"). -Notation Pdiv2 := Pos.div2 (compat "8.6"). -Notation Pdiv2_up := Pos.div2_up (compat "8.6"). +Notation Ppow := Pos.pow (compat "8.7"). +Notation Pdiv2 := Pos.div2 (compat "8.7"). +Notation Pdiv2_up := Pos.div2_up (compat "8.7"). Notation Psize := Pos.size_nat (only parsing). Notation Psize_pos := Pos.size (only parsing). Notation Pcompare x y m := (Pos.compare_cont m x y) (only parsing). -Notation Plt := Pos.lt (compat "8.6"). -Notation Pgt := Pos.gt (compat "8.6"). -Notation Ple := Pos.le (compat "8.6"). -Notation Pge := Pos.ge (compat "8.6"). -Notation Pmin := Pos.min (compat "8.6"). -Notation Pmax := Pos.max (compat "8.6"). -Notation Peqb := Pos.eqb (compat "8.6"). +Notation Plt := Pos.lt (compat "8.7"). +Notation Pgt := Pos.gt (compat "8.7"). +Notation Ple := Pos.le (compat "8.7"). +Notation Pge := Pos.ge (compat "8.7"). +Notation Pmin := Pos.min (compat "8.7"). +Notation Pmax := Pos.max (compat "8.7"). +Notation Peqb := Pos.eqb (compat "8.7"). Notation positive_eq_dec := Pos.eq_dec (only parsing). Notation xI_succ_xO := Pos.xI_succ_xO (only parsing). -Notation Psucc_discr := Pos.succ_discr (compat "8.6"). +Notation Psucc_discr := Pos.succ_discr (compat "8.7"). Notation Psucc_o_double_minus_one_eq_xO := Pos.succ_pred_double (only parsing). Notation Pdouble_minus_one_o_succ_eq_xI := @@ -1951,9 +1953,9 @@ Notation xO_succ_permute := Pos.double_succ (only parsing). Notation double_moins_un_xO_discr := Pos.pred_double_xO_discr (only parsing). Notation Psucc_not_one := Pos.succ_not_1 (only parsing). -Notation Ppred_succ := Pos.pred_succ (compat "8.6"). +Notation Ppred_succ := Pos.pred_succ (compat "8.7"). Notation Psucc_pred := Pos.succ_pred_or (only parsing). -Notation Psucc_inj := Pos.succ_inj (compat "8.6"). +Notation Psucc_inj := Pos.succ_inj (compat "8.7"). Notation Pplus_carry_spec := Pos.add_carry_spec (only parsing). Notation Pplus_comm := Pos.add_comm (only parsing). Notation Pplus_succ_permute_r := Pos.add_succ_r (only parsing). @@ -2000,17 +2002,17 @@ Notation Pmult_xO_discr := Pos.mul_xO_discr (only parsing). Notation Pmult_reg_r := Pos.mul_reg_r (only parsing). Notation Pmult_reg_l := Pos.mul_reg_l (only parsing). Notation Pmult_1_inversion_l := Pos.mul_eq_1_l (only parsing). -Notation Psquare_xO := Pos.square_xO (compat "8.6"). -Notation Psquare_xI := Pos.square_xI (compat "8.6"). +Notation Psquare_xO := Pos.square_xO (compat "8.7"). +Notation Psquare_xI := Pos.square_xI (compat "8.7"). Notation iter_pos_swap_gen := Pos.iter_swap_gen (only parsing). Notation iter_pos_swap := Pos.iter_swap (only parsing). Notation iter_pos_succ := Pos.iter_succ (only parsing). Notation iter_pos_plus := Pos.iter_add (only parsing). Notation iter_pos_invariant := Pos.iter_invariant (only parsing). -Notation Ppow_1_r := Pos.pow_1_r (compat "8.6"). -Notation Ppow_succ_r := Pos.pow_succ_r (compat "8.6"). -Notation Peqb_refl := Pos.eqb_refl (compat "8.6"). -Notation Peqb_eq := Pos.eqb_eq (compat "8.6"). +Notation Ppow_1_r := Pos.pow_1_r (compat "8.7"). +Notation Ppow_succ_r := Pos.pow_succ_r (compat "8.7"). +Notation Peqb_refl := Pos.eqb_refl (compat "8.7"). +Notation Peqb_eq := Pos.eqb_eq (compat "8.7"). Notation Pcompare_refl_id := Pos.compare_cont_refl (only parsing). Notation Pcompare_eq_iff := Pos.compare_eq_iff (only parsing). Notation Pcompare_Gt_Lt := Pos.compare_cont_Gt_Lt (only parsing). @@ -2020,23 +2022,23 @@ Notation Pcompare_Lt_Gt := Pos.compare_cont_Lt_Gt (only parsing). Notation Pcompare_antisym := Pos.compare_cont_antisym (only parsing). Notation ZC1 := Pos.gt_lt (only parsing). Notation ZC2 := Pos.lt_gt (only parsing). -Notation Pcompare_spec := Pos.compare_spec (compat "8.6"). +Notation Pcompare_spec := Pos.compare_spec (compat "8.7"). Notation Pcompare_p_Sp := Pos.lt_succ_diag_r (only parsing). -Notation Pcompare_succ_succ := Pos.compare_succ_succ (compat "8.6"). +Notation Pcompare_succ_succ := Pos.compare_succ_succ (compat "8.7"). Notation Pcompare_1 := Pos.nlt_1_r (only parsing). Notation Plt_1 := Pos.nlt_1_r (only parsing). -Notation Plt_1_succ := Pos.lt_1_succ (compat "8.6"). -Notation Plt_lt_succ := Pos.lt_lt_succ (compat "8.6"). -Notation Plt_irrefl := Pos.lt_irrefl (compat "8.6"). -Notation Plt_trans := Pos.lt_trans (compat "8.6"). -Notation Plt_ind := Pos.lt_ind (compat "8.6"). -Notation Ple_lteq := Pos.le_lteq (compat "8.6"). -Notation Ple_refl := Pos.le_refl (compat "8.6"). -Notation Ple_lt_trans := Pos.le_lt_trans (compat "8.6"). -Notation Plt_le_trans := Pos.lt_le_trans (compat "8.6"). -Notation Ple_trans := Pos.le_trans (compat "8.6"). -Notation Plt_succ_r := Pos.lt_succ_r (compat "8.6"). -Notation Ple_succ_l := Pos.le_succ_l (compat "8.6"). +Notation Plt_1_succ := Pos.lt_1_succ (compat "8.7"). +Notation Plt_lt_succ := Pos.lt_lt_succ (compat "8.7"). +Notation Plt_irrefl := Pos.lt_irrefl (compat "8.7"). +Notation Plt_trans := Pos.lt_trans (compat "8.7"). +Notation Plt_ind := Pos.lt_ind (compat "8.7"). +Notation Ple_lteq := Pos.le_lteq (compat "8.7"). +Notation Ple_refl := Pos.le_refl (compat "8.7"). +Notation Ple_lt_trans := Pos.le_lt_trans (compat "8.7"). +Notation Plt_le_trans := Pos.lt_le_trans (compat "8.7"). +Notation Ple_trans := Pos.le_trans (compat "8.7"). +Notation Plt_succ_r := Pos.lt_succ_r (compat "8.7"). +Notation Ple_succ_l := Pos.le_succ_l (compat "8.7"). Notation Pplus_compare_mono_l := Pos.add_compare_mono_l (only parsing). Notation Pplus_compare_mono_r := Pos.add_compare_mono_r (only parsing). Notation Pplus_lt_mono_l := Pos.add_lt_mono_l (only parsing). @@ -2055,8 +2057,8 @@ Notation Pmult_le_mono_r := Pos.mul_le_mono_r (only parsing). Notation Pmult_le_mono := Pos.mul_le_mono (only parsing). Notation Plt_plus_r := Pos.lt_add_r (only parsing). Notation Plt_not_plus_l := Pos.lt_not_add_l (only parsing). -Notation Ppow_gt_1 := Pos.pow_gt_1 (compat "8.6"). -Notation Ppred_mask := Pos.pred_mask (compat "8.6"). +Notation Ppow_gt_1 := Pos.pow_gt_1 (compat "8.7"). +Notation Ppred_mask := Pos.pred_mask (compat "8.7"). Notation Pminus_mask_succ_r := Pos.sub_mask_succ_r (only parsing). Notation Pminus_mask_carry_spec := Pos.sub_mask_carry_spec (only parsing). Notation Pminus_succ_r := Pos.sub_succ_r (only parsing). diff --git a/theories/PArith/BinPosDef.v b/theories/PArith/BinPosDef.v index 07031474..7f307335 100644 --- a/theories/PArith/BinPosDef.v +++ b/theories/PArith/BinPosDef.v @@ -26,6 +26,8 @@ Require Export BinNums. for the number 6 (which is 110 in binary notation). *) +Local Notation "1" := xH. + Notation "p ~ 1" := (xI p) (at level 7, left associativity, format "p '~' '1'") : positive_scope. Notation "p ~ 0" := (xO p) @@ -325,14 +327,14 @@ Definition sqrtrem_step (f g:positive->positive) p := let r' := g (f r) in if s' <=? r' then (s~1, sub_mask r' s') else (s~0, IsPos r') - | (s,_) => (s~0, sub_mask (g (f 1)) 4) + | (s,_) => (s~0, sub_mask (g (f 1)) 1~0~0) end. Fixpoint sqrtrem p : positive * mask := match p with | 1 => (1,IsNul) - | 2 => (1,IsPos 1) - | 3 => (1,IsPos 2) + | 1~0 => (1,IsPos 1) + | 1~1 => (1,IsPos 1~0) | p~0~0 => sqrtrem_step xO xO (sqrtrem p) | p~0~1 => sqrtrem_step xO xI (sqrtrem p) | p~1~0 => sqrtrem_step xI xO (sqrtrem p) @@ -614,4 +616,9 @@ Definition to_uint p := Decimal.rev (to_little_uint p). Definition to_int n := Decimal.Pos (to_uint n). +Numeral Notation positive of_int to_uint : positive_scope. + End Pos. + +(** Re-export the notation for those who just [Import BinPosDef] *) +Numeral Notation positive Pos.of_int Pos.to_uint : positive_scope. diff --git a/theories/Program/Tactics.v b/theories/Program/Tactics.v index bc838818..edbae653 100644 --- a/theories/Program/Tactics.v +++ b/theories/Program/Tactics.v @@ -326,7 +326,7 @@ Ltac program_solve_wf := Create HintDb program discriminated. -Ltac program_simpl := program_simplify ; try typeclasses eauto with program ; try program_solve_wf. +Ltac program_simpl := program_simplify ; try typeclasses eauto 10 with program ; try program_solve_wf. Obligation Tactic := program_simpl. diff --git a/theories/Reals/Machin.v b/theories/Reals/Machin.v index cdf98cbd..8f7e07ac 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 Fourier. +Require Import Lra. Require Import Rbase. Require Import Rtrigo1. Require Import Ranalysis_reg. @@ -67,7 +67,7 @@ assert (atan x <= PI/4). assert (atan y < PI/4). rewrite <- atan_1; apply atan_increasing. assumption. -rewrite Ropp_div; split; fourier. +rewrite Ropp_div; split; lra. Qed. (* A simple formula, reasonably efficient. *) @@ -77,8 +77,8 @@ assert (utility : 0 < PI/2) by (apply PI2_RGT_0). rewrite <- atan_1. rewrite (atan_sub_correct 1 (/2)). apply f_equal, f_equal; unfold atan_sub; field. - apply Rgt_not_eq; fourier. - apply tech; try split; try fourier. + apply Rgt_not_eq; lra. + apply tech; try split; try lra. apply atan_bound. Qed. @@ -86,7 +86,7 @@ Lemma Machin_4_5_239 : PI/4 = 4 * atan (/5) - atan(/239). Proof. rewrite <- atan_1. rewrite (atan_sub_correct 1 (/5)); - [ | apply Rgt_not_eq; fourier | apply tech; try split; fourier | + [ | apply Rgt_not_eq; lra | apply tech; try split; lra | apply atan_bound ]. replace (4 * atan (/5) - atan (/239)) with (atan (/5) + (atan (/5) + (atan (/5) + (atan (/5) + - @@ -95,17 +95,17 @@ apply f_equal. replace (atan_sub 1 (/5)) with (2/3) by (unfold atan_sub; field). rewrite (atan_sub_correct (2/3) (/5)); - [apply f_equal | apply Rgt_not_eq; fourier | apply tech; try split; fourier | + [apply f_equal | apply Rgt_not_eq; lra | apply tech; try split; lra | apply atan_bound ]. replace (atan_sub (2/3) (/5)) with (7/17) by (unfold atan_sub; field). rewrite (atan_sub_correct (7/17) (/5)); - [apply f_equal | apply Rgt_not_eq; fourier | apply tech; try split; fourier | + [apply f_equal | apply Rgt_not_eq; lra | apply tech; try split; lra | apply atan_bound ]. replace (atan_sub (7/17) (/5)) with (9/46) by (unfold atan_sub; field). rewrite (atan_sub_correct (9/46) (/5)); - [apply f_equal | apply Rgt_not_eq; fourier | apply tech; try split; fourier | + [apply f_equal | apply Rgt_not_eq; lra | apply tech; try split; lra | apply atan_bound ]. rewrite <- atan_opp; apply f_equal. unfold atan_sub; field. @@ -115,7 +115,7 @@ Lemma Machin_2_3_7 : PI/4 = 2 * atan(/3) + (atan (/7)). Proof. rewrite <- atan_1. rewrite (atan_sub_correct 1 (/3)); - [ | apply Rgt_not_eq; fourier | apply tech; try split; fourier | + [ | apply Rgt_not_eq; lra | apply tech; try split; lra | apply atan_bound ]. replace (2 * atan (/3) + atan (/7)) with (atan (/3) + (atan (/3) + atan (/7))) by ring. @@ -123,7 +123,7 @@ apply f_equal. replace (atan_sub 1 (/3)) with (/2) by (unfold atan_sub; field). rewrite (atan_sub_correct (/2) (/3)); - [apply f_equal | apply Rgt_not_eq; fourier | apply tech; try split; fourier | + [apply f_equal | apply Rgt_not_eq; lra | apply tech; try split; lra | apply atan_bound ]. apply f_equal; unfold atan_sub; field. Qed. @@ -138,19 +138,19 @@ Lemma PI_2_3_7_ineq : sum_f_R0 (tg_alt PI_2_3_7_tg) (S (2 * N)) <= PI / 4 <= sum_f_R0 (tg_alt PI_2_3_7_tg) (2 * N). Proof. -assert (dec3 : 0 <= /3 <= 1) by (split; fourier). -assert (dec7 : 0 <= /7 <= 1) by (split; fourier). +assert (dec3 : 0 <= /3 <= 1) by (split; lra). +assert (dec7 : 0 <= /7 <= 1) by (split; lra). assert (decr : Un_decreasing PI_2_3_7_tg). apply Ratan_seq_decreasing in dec3. apply Ratan_seq_decreasing in dec7. intros n; apply Rplus_le_compat. - apply Rmult_le_compat_l; [ fourier | exact (dec3 n)]. + apply Rmult_le_compat_l; [ lra | exact (dec3 n)]. exact (dec7 n). assert (cv : Un_cv PI_2_3_7_tg 0). apply Ratan_seq_converging in dec3. apply Ratan_seq_converging in dec7. intros eps ep. - assert (ep' : 0 < eps /3) by fourier. + assert (ep' : 0 < eps /3) by lra. destruct (dec3 _ ep') as [N1 Pn1]; destruct (dec7 _ ep') as [N2 Pn2]. exists (N1 + N2)%nat; intros n Nn. unfold PI_2_3_7_tg. @@ -161,14 +161,14 @@ assert (cv : Un_cv PI_2_3_7_tg 0). apply Rplus_lt_compat. unfold R_dist, Rminus, Rdiv. rewrite <- (Rmult_0_r 2), <- Ropp_mult_distr_r_reverse. - rewrite <- Rmult_plus_distr_l, Rabs_mult, (Rabs_pos_eq 2);[|fourier]. - rewrite Rmult_assoc; apply Rmult_lt_compat_l;[fourier | ]. + 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. rewrite Machin_2_3_7. -rewrite !atan_eq_ps_atan; try (split; fourier). +rewrite !atan_eq_ps_atan; try (split; lra). unfold ps_atan; destruct (in_int (/3)); destruct (in_int (/7)); - try match goal with id : ~ _ |- _ => case id; split; fourier end. + try match goal with id : ~ _ |- _ => case id; split; lra end. destruct (ps_atan_exists_1 (/3)) as [v3 Pv3]. destruct (ps_atan_exists_1 (/7)) as [v7 Pv7]. assert (main : Un_cv (sum_f_R0 (tg_alt PI_2_3_7_tg)) (2 * v3 + v7)). diff --git a/theories/Reals/PSeries_reg.v b/theories/Reals/PSeries_reg.v index 61d1b5af..146d6910 100644 --- a/theories/Reals/PSeries_reg.v +++ b/theories/Reals/PSeries_reg.v @@ -15,7 +15,7 @@ Require Import Ranalysis1. Require Import MVT. Require Import Max. Require Import Even. -Require Import Fourier. +Require Import Lra. Local Open Scope R_scope. (* Boule is French for Ball *) @@ -431,7 +431,7 @@ assert (ctrho : forall n z, Boule c d z -> continuity_pt (rho_ n) z). intros y dyz; unfold rho_; destruct (Req_EM_T y x) as [xy | xny]. rewrite xy in dyz. destruct (Rle_dec delta (Rabs (z - x))). - rewrite Rmin_left, R_dist_sym in dyz; unfold R_dist in dyz; fourier. + rewrite Rmin_left, R_dist_sym in dyz; unfold R_dist in dyz; lra. rewrite Rmin_right, R_dist_sym in dyz; unfold R_dist in dyz; [case (Rlt_irrefl _ dyz) |apply Rlt_le, Rnot_le_gt; assumption]. reflexivity. @@ -449,7 +449,7 @@ assert (ctrho : forall n z, Boule c d z -> continuity_pt (rho_ n) z). assert (CVU rho_ rho c d ). intros eps ep. assert (ep8 : 0 < eps/8). - fourier. + lra. destruct (cvu _ ep8) as [N Pn1]. assert (cauchy1 : forall n p, (N <= n)%nat -> (N <= p)%nat -> forall z, Boule c d z -> Rabs (f' n z - f' p z) < eps/4). @@ -537,7 +537,7 @@ assert (CVU rho_ rho c d ). simpl; unfold R_dist. unfold Rminus; rewrite (Rplus_comm y), Rplus_assoc, Rplus_opp_r, Rplus_0_r. rewrite Rabs_pos_eq;[ |apply Rlt_le; assumption ]. - apply Rlt_le_trans with (Rmin (Rmin d' d2) delta);[fourier | ]. + apply Rlt_le_trans with (Rmin (Rmin d' d2) delta);[lra | ]. apply Rle_trans with (Rmin d' d2); apply Rmin_l. apply Rle_trans with (1 := R_dist_tri _ _ (rho_ p (y + Rmin (Rmin d' d2) delta/2))). apply Rplus_le_compat. @@ -548,33 +548,32 @@ assert (CVU rho_ rho c d ). replace (rho_ p (y + Rmin (Rmin d' d2) delta / 2)) with ((f p (y + Rmin (Rmin d' d2) delta / 2) - f p x)/ ((y + Rmin (Rmin d' d2) delta / 2) - x)). - apply step_2; auto; try fourier. + apply step_2; auto; try lra. assert (0 < pos delta) by (apply cond_pos). apply Boule_convex with y (y + delta/2). assumption. destruct (Pdelta (y + delta/2)); auto. - rewrite xy; unfold Boule; rewrite Rabs_pos_eq; try fourier; auto. - split; try fourier. + rewrite xy; unfold Boule; rewrite Rabs_pos_eq; try lra; auto. + split; try lra. apply Rplus_le_compat_l, Rmult_le_compat_r;[ | apply Rmin_r]. now apply Rlt_le, Rinv_0_lt_compat, Rlt_0_2. - apply Rminus_not_eq_right; rewrite xy; apply Rgt_not_eq; fourier. unfold rho_. destruct (Req_EM_T (y + Rmin (Rmin d' d2) delta/2) x) as [ymx | ymnx]. - case (RIneq.Rle_not_lt _ _ (Req_le _ _ ymx)); fourier. + case (RIneq.Rle_not_lt _ _ (Req_le _ _ ymx)); lra. reflexivity. unfold rho_. destruct (Req_EM_T (y + Rmin (Rmin d' d2) delta / 2) x) as [ymx | ymnx]. - case (RIneq.Rle_not_lt _ _ (Req_le _ _ ymx)); fourier. + case (RIneq.Rle_not_lt _ _ (Req_le _ _ ymx)); lra. reflexivity. - apply Rlt_le, Pd2; split;[split;[exact I | apply Rlt_not_eq; fourier] | ]. + apply Rlt_le, Pd2; split;[split;[exact I | apply Rlt_not_eq; lra] | ]. simpl; unfold R_dist. unfold Rminus; rewrite (Rplus_comm y), Rplus_assoc, Rplus_opp_r, Rplus_0_r. - rewrite Rabs_pos_eq;[ | fourier]. - apply Rlt_le_trans with (Rmin (Rmin d' d2) delta); [fourier |]. + rewrite Rabs_pos_eq;[ | lra]. + apply Rlt_le_trans with (Rmin (Rmin d' d2) delta); [lra |]. apply Rle_trans with (Rmin d' d2). solve[apply Rmin_l]. solve[apply Rmin_r]. - apply Rlt_le, Rlt_le_trans with (eps/4);[ | fourier]. + apply Rlt_le, Rlt_le_trans with (eps/4);[ | lra]. unfold rho_; destruct (Req_EM_T y x); solve[auto]. assert (unif_ac' : forall p, (N <= p)%nat -> forall y, Boule c d y -> Rabs (rho y - rho_ p y) < eps). @@ -589,7 +588,7 @@ assert (CVU rho_ rho c d ). intros eps' ep'; simpl; exists 0%nat; intros; rewrite R_dist_eq; assumption. intros p pN y b_y. replace eps with (eps/2 + eps/2) by field. - assert (ep2 : 0 < eps/2) by fourier. + assert (ep2 : 0 < eps/2) by lra. destruct (cvrho y b_y _ ep2) as [N2 Pn2]. apply Rle_lt_trans with (1 := R_dist_tri _ _ (rho_ (max N N2) y)). apply Rplus_lt_le_compat. diff --git a/theories/Reals/R_sqrt.v b/theories/Reals/R_sqrt.v index d4035fad..6991923b 100644 --- a/theories/Reals/R_sqrt.v +++ b/theories/Reals/R_sqrt.v @@ -155,6 +155,22 @@ Proof. | apply (sqrt_positivity x (Rlt_le 0 x H1)) ]. Qed. +Lemma Rlt_mult_inv_pos : forall x y:R, 0 < x -> 0 < y -> 0 < x * / y. +intros x y H H0; try assumption. +replace 0 with (x * 0). +apply Rmult_lt_compat_l; auto with real. +ring. +Qed. + +Lemma Rle_mult_inv_pos : forall x y:R, 0 <= x -> 0 < y -> 0 <= x * / y. +intros x y H H0; try assumption. +case H; intros. +red; left. +apply Rlt_mult_inv_pos; auto with real. +rewrite <- H1. +red; right; ring. +Qed. + Lemma sqrt_div_alt : forall x y : R, 0 < y -> sqrt (x / y) = sqrt x / sqrt y. Proof. @@ -176,14 +192,14 @@ Proof. clearbody Hx'. clear Hx. apply Rsqr_inj. apply sqrt_pos. - apply Fourier_util.Rle_mult_inv_pos. + apply Rle_mult_inv_pos. apply Rsqrt_positivity. now apply sqrt_lt_R0. rewrite Rsqr_div, 2!Rsqr_sqrt. unfold Rsqr. now rewrite Rsqrt_Rsqrt. now apply Rlt_le. - now apply Fourier_util.Rle_mult_inv_pos. + now apply Rle_mult_inv_pos. apply Rgt_not_eq. now apply sqrt_lt_R0. Qed. diff --git a/theories/Reals/Ranalysis5.v b/theories/Reals/Ranalysis5.v index afb78e1c..e66130b3 100644 --- a/theories/Reals/Ranalysis5.v +++ b/theories/Reals/Ranalysis5.v @@ -12,7 +12,7 @@ Require Import Rbase. Require Import Ranalysis_reg. Require Import Rfunctions. Require Import Rseries. -Require Import Fourier. +Require Import Lra. Require Import RiemannInt. Require Import SeqProp. Require Import Max. @@ -56,7 +56,7 @@ Proof. } rewrite f_eq_g in Htemp by easy. unfold id in Htemp. - fourier. + lra. Qed. Lemma derivable_pt_id_interv : forall (lb ub x:R), @@ -99,7 +99,7 @@ assert (forall x l, lb < x < ub -> (derivable_pt_abs f x l <-> derivable_pt_abs apply Req_le ; apply Rabs_right ; apply Rgt_ge ; assumption. split. assert (Sublemma : forall x y z, -z < y - x -> x < y + z). - intros ; fourier. + intros ; lra. apply Sublemma. apply Sublemma2. rewrite Rabs_Ropp. apply Rlt_le_trans with (r2:=a-lb) ; [| apply RRle_abs] ; @@ -108,7 +108,7 @@ assert (forall x l, lb < x < ub -> (derivable_pt_abs f x l <-> derivable_pt_abs apply Rlt_le_trans with (r2:=Rmin (ub - a) (a - lb)) ; [| apply Rmin_r] ; apply Rlt_le_trans with (r2:=Rmin delta (Rmin (ub - a) (a - lb))) ; [| apply Rmin_r] ; assumption. assert (Sublemma : forall x y z, y < z - x -> x + y < z). - intros ; fourier. + intros ; lra. apply Sublemma. apply Sublemma2. apply Rlt_le_trans with (r2:=ub-a) ; [| apply RRle_abs] ; @@ -137,7 +137,7 @@ assert (forall x l, lb < x < ub -> (derivable_pt_abs f x l <-> derivable_pt_abs apply Req_le ; apply Rabs_right ; apply Rgt_ge ; assumption. split. assert (Sublemma : forall x y z, -z < y - x -> x < y + z). - intros ; fourier. + intros ; lra. apply Sublemma. apply Sublemma2. rewrite Rabs_Ropp. apply Rlt_le_trans with (r2:=a-lb) ; [| apply RRle_abs] ; @@ -146,7 +146,7 @@ assert (forall x l, lb < x < ub -> (derivable_pt_abs f x l <-> derivable_pt_abs apply Rlt_le_trans with (r2:=Rmin (ub - a) (a - lb)) ; [| apply Rmin_r] ; apply Rlt_le_trans with (r2:=Rmin delta (Rmin (ub - a) (a - lb))) ; [| apply Rmin_r] ; assumption. assert (Sublemma : forall x y z, y < z - x -> x + y < z). - intros ; fourier. + intros ; lra. apply Sublemma. apply Sublemma2. apply Rlt_le_trans with (r2:=ub-a) ; [| apply RRle_abs] ; @@ -415,7 +415,7 @@ Ltac case_le H := let h' := fresh in match t with ?x <= ?y => case (total_order_T x y); [intros h'; case h'; clear h' | - intros h'; clear -H h'; elimtype False; fourier ] end. + intros h'; clear -H h'; elimtype False; lra ] end. (* end hide *) @@ -539,37 +539,37 @@ intros f g lb ub lb_lt_ub f_incr_interv f_eq_g f_cont_interv b b_encad. assert (x1_encad : lb <= x1 <= ub). split. apply RmaxLess2. apply Rlt_le. rewrite Hx1. rewrite Sublemma. - split. apply Rlt_trans with (r2:=x) ; fourier. + split. apply Rlt_trans with (r2:=x) ; lra. assumption. assert (x2_encad : lb <= x2 <= ub). split. apply Rlt_le ; rewrite Hx2 ; apply Rgt_lt ; rewrite Sublemma2. - split. apply Rgt_trans with (r2:=x) ; fourier. + split. apply Rgt_trans with (r2:=x) ; lra. assumption. apply Rmin_r. assert (x_lt_x2 : x < x2). rewrite Hx2. apply Rgt_lt. rewrite Sublemma2. - split ; fourier. + split ; lra. assert (x1_lt_x : x1 < x). rewrite Hx1. rewrite Sublemma. - split ; fourier. + split ; lra. exists (Rmin (f x - f x1) (f x2 - f x)). - split. apply Rmin_pos ; apply Rgt_minus. apply f_incr_interv ; [apply RmaxLess2 | | ] ; fourier. + split. apply Rmin_pos ; apply Rgt_minus. apply f_incr_interv ; [apply RmaxLess2 | | ] ; lra. apply f_incr_interv ; intuition. intros y Temp. destruct Temp as (_,y_cond). rewrite <- f_x_b in y_cond. assert (Temp : forall x y d1 d2, d1 > 0 -> d2 > 0 -> Rabs (y - x) < Rmin d1 d2 -> x - d1 <= y <= x + d2). intros. - split. assert (H10 : forall x y z, x - y <= z -> x - z <= y). intuition. fourier. + split. assert (H10 : forall x y z, x - y <= z -> x - z <= y). intuition. lra. apply H10. apply Rle_trans with (r2:=Rabs (y0 - x0)). replace (Rabs (y0 - x0)) with (Rabs (x0 - y0)). apply RRle_abs. rewrite <- Rabs_Ropp. unfold Rminus ; rewrite Ropp_plus_distr. rewrite Ropp_involutive. intuition. apply Rle_trans with (r2:= Rmin d1 d2). apply Rlt_le ; assumption. apply Rmin_l. - assert (H10 : forall x y z, x - y <= z -> x <= y + z). intuition. fourier. + assert (H10 : forall x y z, x - y <= z -> x <= y + z). intuition. lra. apply H10. apply Rle_trans with (r2:=Rabs (y0 - x0)). apply RRle_abs. apply Rle_trans with (r2:= Rmin d1 d2). apply Rlt_le ; assumption. apply Rmin_r. @@ -602,12 +602,12 @@ intros f g lb ub lb_lt_ub f_incr_interv f_eq_g f_cont_interv b b_encad. assert (x1_neq_x' : x1 <> x'). intro Hfalse. rewrite Hfalse, f_x'_y in y_cond. assert (Hf : Rabs (y - f x) < f x - y). - apply Rlt_le_trans with (r2:=Rmin (f x - y) (f x2 - f x)). fourier. + apply Rlt_le_trans with (r2:=Rmin (f x - y) (f x2 - f x)). lra. apply Rmin_l. assert(Hfin : f x - y < f x - y). apply Rle_lt_trans with (r2:=Rabs (y - f x)). replace (Rabs (y - f x)) with (Rabs (f x - y)). apply RRle_abs. - rewrite <- Rabs_Ropp. replace (- (f x - y)) with (y - f x) by field ; reflexivity. fourier. + rewrite <- Rabs_Ropp. replace (- (f x - y)) with (y - f x) by field ; reflexivity. lra. apply (Rlt_irrefl (f x - y)) ; assumption. split ; intuition. assert (x'_lb : x - eps < x'). @@ -619,17 +619,17 @@ intros f g lb ub lb_lt_ub f_incr_interv f_eq_g f_cont_interv b b_encad. assert (x1_neq_x' : x' <> x2). intro Hfalse. rewrite <- Hfalse, f_x'_y in y_cond. assert (Hf : Rabs (y - f x) < y - f x). - apply Rlt_le_trans with (r2:=Rmin (f x - f x1) (y - f x)). fourier. + apply Rlt_le_trans with (r2:=Rmin (f x - f x1) (y - f x)). lra. apply Rmin_r. assert(Hfin : y - f x < y - f x). - apply Rle_lt_trans with (r2:=Rabs (y - f x)). apply RRle_abs. fourier. + apply Rle_lt_trans with (r2:=Rabs (y - f x)). apply RRle_abs. lra. apply (Rlt_irrefl (y - f x)) ; assumption. split ; intuition. assert (x'_ub : x' < x + eps). apply Sublemma3. split. intuition. apply Rlt_not_eq. apply Rlt_le_trans with (r2:=x2) ; [ |rewrite Hx2 ; apply Rmin_l] ; intuition. - apply Rabs_def1 ; fourier. + apply Rabs_def1 ; lra. assumption. split. apply Rle_trans with (r2:=x1) ; intuition. apply Rle_trans with (r2:=x2) ; intuition. @@ -742,7 +742,7 @@ intros f g lb ub x Prf g_cont_pur lb_lt_ub x_encad Prg_incr f_eq_g df_neq. assert (lb <= x + h <= ub). split. assert (Sublemma : forall x y z, -z <= y - x -> x <= y + z). - intros ; fourier. + intros ; lra. apply Sublemma. apply Rlt_le ; apply Sublemma2. rewrite Rabs_Ropp. apply Rlt_le_trans with (r2:=x-lb) ; [| apply RRle_abs] ; @@ -751,7 +751,7 @@ intros f g lb ub x Prf g_cont_pur lb_lt_ub x_encad Prg_incr f_eq_g df_neq. apply Rlt_le_trans with (r2:=delta''). assumption. intuition. apply Rmin_r. apply Rgt_minus. intuition. assert (Sublemma : forall x y z, y <= z - x -> x + y <= z). - intros ; fourier. + intros ; lra. apply Sublemma. apply Rlt_le ; apply Sublemma2. apply Rlt_le_trans with (r2:=ub-x) ; [| apply RRle_abs] ; @@ -767,7 +767,7 @@ intros f g lb ub x Prf g_cont_pur lb_lt_ub x_encad Prg_incr f_eq_g df_neq. assumption. split ; [|intuition]. assert (Sublemma : forall x y z, - z <= y - x -> x <= y + z). - intros ; fourier. + intros ; lra. apply Sublemma ; apply Rlt_le ; apply Sublemma2. rewrite Rabs_Ropp. apply Rlt_le_trans with (r2:=x-lb) ; [| apply RRle_abs] ; apply Rlt_le_trans with (r2:=Rmin (x - lb) (ub - x)) ; [| apply Rmin_l] ; @@ -1031,7 +1031,7 @@ Lemma derivable_pt_lim_CVU : forall (fn fn':nat -> R -> R) (f g:R->R) derivable_pt_lim f x (g x). Proof. intros fn fn' f g x c' r xinb Dfn_eq_fn' fn_CV_f fn'_CVU_g g_cont eps eps_pos. -assert (eps_8_pos : 0 < eps / 8) by fourier. +assert (eps_8_pos : 0 < eps / 8) by lra. elim (g_cont x xinb _ eps_8_pos) ; clear g_cont ; intros delta1 (delta1_pos, g_cont). destruct (Ball_in_inter _ _ _ _ _ xinb @@ -1041,11 +1041,11 @@ exists delta; intros h hpos hinbdelta. assert (eps'_pos : 0 < (Rabs h) * eps / 4). unfold Rdiv ; rewrite Rmult_assoc ; apply Rmult_lt_0_compat. apply Rabs_pos_lt ; assumption. -fourier. +lra. destruct (fn_CV_f x xinb ((Rabs h) * eps / 4) eps'_pos) as [N2 fnx_CV_fx]. assert (xhinbxdelta : Boule x delta (x + h)). clear -hinbdelta; apply Rabs_def2 in hinbdelta; unfold Boule; simpl. - destruct hinbdelta; apply Rabs_def1; fourier. + destruct hinbdelta; apply Rabs_def1; lra. assert (t : Boule c' r (x + h)). apply Pdelta in xhinbxdelta; tauto. destruct (fn_CV_f (x+h) t ((Rabs h) * eps / 4) eps'_pos) as [N1 fnxh_CV_fxh]. @@ -1064,17 +1064,17 @@ assert (Main : Rabs ((f (x+h) - fn N (x+h)) - (f x - fn N x) + (fn N (x+h) - fn exists (fn' N c) ; apply Dfn_eq_fn'. assert (t : Boule x delta c). apply Rabs_def2 in xhinbxdelta; destruct xhinbxdelta; destruct c_encad. - apply Rabs_def2 in xinb; apply Rabs_def1; fourier. + apply Rabs_def2 in xinb; apply Rabs_def1; lra. apply Pdelta in t; tauto. assert (pr2 : forall c : R, x + h < c < x -> derivable_pt id c). solve[intros; apply derivable_id]. - assert (xh_x : x+h < x) by fourier. + assert (xh_x : x+h < x) by lra. assert (pr3 : forall c : R, x + h <= c <= x -> continuity_pt (fn N) c). intros c c_encad ; apply derivable_continuous_pt. exists (fn' N c) ; apply Dfn_eq_fn' ; intuition. assert (t : Boule x delta c). apply Rabs_def2 in xhinbxdelta; destruct xhinbxdelta. - apply Rabs_def2 in xinb; apply Rabs_def1; fourier. + apply Rabs_def2 in xinb; apply Rabs_def1; lra. apply Pdelta in t; tauto. assert (pr4 : forall c : R, x + h <= c <= x -> continuity_pt id c). solve[intros; apply derivable_continuous ; apply derivable_id]. @@ -1117,7 +1117,7 @@ assert (Main : Rabs ((f (x+h) - fn N (x+h)) - (f x - fn N x) + (fn N (x+h) - fn assert (t : Boule x delta c). destruct P. apply Rabs_def2 in xhinbxdelta; destruct xhinbxdelta. - apply Rabs_def2 in xinb; apply Rabs_def1; fourier. + apply Rabs_def2 in xinb; apply Rabs_def1; lra. apply Pdelta in t; tauto. apply Rlt_trans with (Rabs h * eps / 4 + Rabs h * eps / 4 + Rabs h * (eps / 8) + Rabs h * (eps / 8)). @@ -1131,27 +1131,27 @@ 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). apply Rabs_def1. apply Rlt_trans with 0. - destruct P; fourier. + destruct P; lra. apply Rabs_pos_lt ; assumption. - rewrite <- Rabs_Ropp, Rabs_pos_eq, Ropp_involutive;[ | fourier]. - destruct P; fourier. + rewrite <- Rabs_Ropp, Rabs_pos_eq, Ropp_involutive;[ | lra]. + destruct P; lra. clear -Pdelta xhinbxdelta. apply Pdelta in xhinbxdelta; destruct xhinbxdelta as [_ P']. apply Rabs_def2 in P'; simpl in P'; destruct P'; - apply Rabs_def1; fourier. + apply Rabs_def1; lra. rewrite Rplus_assoc ; rewrite Rplus_assoc ; rewrite <- Rmult_plus_distr_l. replace (Rabs h * eps / 4 + (Rabs h * eps / 4 + Rabs h * (eps / 8 + eps / 8))) with (Rabs h * (eps / 4 + eps / 4 + eps / 8 + eps / 8)) by field. apply Rmult_lt_compat_l. apply Rabs_pos_lt ; assumption. - fourier. + lra. assert (H := pr1 c P) ; elim H ; clear H ; intros l Hl. assert (Temp : l = fn' N c). assert (bc'rc : Boule c' r c). assert (t : Boule x delta c). clear - xhinbxdelta P. destruct P; apply Rabs_def2 in xhinbxdelta; destruct xhinbxdelta. - apply Rabs_def1; fourier. + apply Rabs_def1; lra. apply Pdelta in t; tauto. assert (Hl' := Dfn_eq_fn' c N bc'rc). unfold derivable_pt_abs in Hl; clear -Hl Hl'. @@ -1175,17 +1175,17 @@ assert (Main : Rabs ((f (x+h) - fn N (x+h)) - (f x - fn N x) + (fn N (x+h) - fn exists (fn' N c) ; apply Dfn_eq_fn'. assert (t : Boule x delta c). apply Rabs_def2 in xhinbxdelta; destruct xhinbxdelta; destruct c_encad. - apply Rabs_def2 in xinb; apply Rabs_def1; fourier. + apply Rabs_def2 in xinb; apply Rabs_def1; lra. apply Pdelta in t; tauto. assert (pr2 : forall c : R, x < c < x + h -> derivable_pt id c). solve[intros; apply derivable_id]. - assert (xh_x : x < x + h) by fourier. + assert (xh_x : x < x + h) by lra. assert (pr3 : forall c : R, x <= c <= x + h -> continuity_pt (fn N) c). intros c c_encad ; apply derivable_continuous_pt. exists (fn' N c) ; apply Dfn_eq_fn' ; intuition. assert (t : Boule x delta c). apply Rabs_def2 in xhinbxdelta; destruct xhinbxdelta. - apply Rabs_def2 in xinb; apply Rabs_def1; fourier. + apply Rabs_def2 in xinb; apply Rabs_def1; lra. apply Pdelta in t; tauto. assert (pr4 : forall c : R, x <= c <= x + h -> continuity_pt id c). solve[intros; apply derivable_continuous ; apply derivable_id]. @@ -1223,7 +1223,7 @@ assert (Main : Rabs ((f (x+h) - fn N (x+h)) - (f x - fn N x) + (fn N (x+h) - fn assert (t : Boule x delta c). destruct P. apply Rabs_def2 in xhinbxdelta; destruct xhinbxdelta. - apply Rabs_def2 in xinb; apply Rabs_def1; fourier. + apply Rabs_def2 in xinb; apply Rabs_def1; lra. apply Pdelta in t; tauto. apply Rlt_trans with (Rabs h * eps / 4 + Rabs h * eps / 4 + Rabs h * (eps / 8) + Rabs h * (eps / 8)). @@ -1236,27 +1236,27 @@ assert (Main : Rabs ((f (x+h) - fn N (x+h)) - (f x - fn N x) + (fn N (x+h) - fn apply Rlt_not_eq ; exact (proj1 P). apply Rlt_trans with (Rabs h). apply Rabs_def1. - destruct P; rewrite Rabs_pos_eq;fourier. + destruct P; rewrite Rabs_pos_eq;lra. apply Rle_lt_trans with 0. - assert (t := Rabs_pos h); clear -t; fourier. - clear -P; destruct P; fourier. + assert (t := Rabs_pos h); clear -t; lra. + clear -P; destruct P; lra. clear -Pdelta xhinbxdelta. apply Pdelta in xhinbxdelta; destruct xhinbxdelta as [_ P']. apply Rabs_def2 in P'; simpl in P'; destruct P'; - apply Rabs_def1; fourier. + apply Rabs_def1; lra. rewrite Rplus_assoc ; rewrite Rplus_assoc ; rewrite <- Rmult_plus_distr_l. replace (Rabs h * eps / 4 + (Rabs h * eps / 4 + Rabs h * (eps / 8 + eps / 8))) with (Rabs h * (eps / 4 + eps / 4 + eps / 8 + eps / 8)) by field. apply Rmult_lt_compat_l. apply Rabs_pos_lt ; assumption. - fourier. + lra. assert (H := pr1 c P) ; elim H ; clear H ; intros l Hl. assert (Temp : l = fn' N c). assert (bc'rc : Boule c' r c). assert (t : Boule x delta c). clear - xhinbxdelta P. destruct P; apply Rabs_def2 in xhinbxdelta; destruct xhinbxdelta. - apply Rabs_def1; fourier. + apply Rabs_def1; lra. apply Pdelta in t; tauto. assert (Hl' := Dfn_eq_fn' c N bc'rc). unfold derivable_pt_abs in Hl; clear -Hl Hl'. diff --git a/theories/Reals/Ratan.v b/theories/Reals/Ratan.v index ce39d5ff..03e6ff61 100644 --- a/theories/Reals/Ratan.v +++ b/theories/Reals/Ratan.v @@ -8,7 +8,7 @@ (* * (see LICENSE file for the text of the license) *) (************************************************************************) -Require Import Fourier. +Require Import Lra. Require Import Rbase. Require Import PSeries_reg. Require Import Rtrigo1. @@ -32,7 +32,7 @@ intros x y; unfold Rdiv; rewrite <-Ropp_mult_distr_l_reverse; reflexivity. Qed. Definition pos_half_prf : 0 < /2. -Proof. fourier. Qed. +Proof. lra. Qed. Definition pos_half := mkposreal (/2) pos_half_prf. @@ -40,15 +40,15 @@ Lemma Boule_half_to_interval : forall x , Boule (/2) pos_half x -> 0 <= x <= 1. Proof. unfold Boule, pos_half; simpl. -intros x b; apply Rabs_def2 in b; destruct b; split; fourier. +intros x b; apply Rabs_def2 in b; destruct b; split; lra. Qed. Lemma Boule_lt : forall c r x, Boule c r x -> Rabs x < Rabs c + r. Proof. unfold Boule; intros c r x h. apply Rabs_def2 in h; destruct h; apply Rabs_def1; - (destruct (Rle_lt_dec 0 c);[rewrite Rabs_pos_eq; fourier | - rewrite <- Rabs_Ropp, Rabs_pos_eq; fourier]). + (destruct (Rle_lt_dec 0 c);[rewrite Rabs_pos_eq; lra | + rewrite <- Rabs_Ropp, Rabs_pos_eq; lra]). Qed. (* The following lemma does not belong here. *) @@ -117,53 +117,53 @@ intros [ | N] Npos n decr to0 cv nN. case (even_odd_cor n) as [p' [neven | nodd]]. rewrite neven. destruct (alternated_series_ineq _ _ p' decr to0 cv) as [D E]. - unfold R_dist; rewrite Rabs_pos_eq;[ | fourier]. + unfold R_dist; rewrite Rabs_pos_eq;[ | lra]. assert (dist : (p <= p')%nat) by omega. 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. match goal with _ : ?a <= l, _ : l <= ?b |- _ => replace (f (S (2 * p))) with (b - a) by - (rewrite tech5; unfold tg_alt; rewrite pow_1_odd; ring); fourier + (rewrite tech5; unfold tg_alt; rewrite pow_1_odd; ring); lra end. 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; - [ | fourier]. + [ | lra]. assert (dist : (p <= p')%nat) by omega. 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)]. unfold Rminus; rewrite tech5, Ropp_plus_distr, <- Rplus_assoc. - unfold tg_alt at 2; rewrite pow_1_odd; fourier. + unfold tg_alt at 2; rewrite pow_1_odd; lra. rewrite Nodd; destruct (alternated_series_ineq _ _ p decr to0 cv) as [B _]. destruct (alternated_series_ineq _ _ (S p) decr to0 cv) as [_ C]. assert (keep : (2 * S p = S (S ( 2 * p)))%nat) by ring. case (even_odd_cor n) as [p' [neven | nodd]]. rewrite neven; destruct (alternated_series_ineq _ _ p' decr to0 cv) as [D E]. - unfold R_dist; rewrite Rabs_pos_eq;[ | fourier]. + unfold R_dist; rewrite Rabs_pos_eq;[ | lra]. assert (dist : (S p < S p')%nat) by omega. 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. rewrite keep, tech5; unfold tg_alt at 2; rewrite <- keep, pow_1_even. - fourier. + lra. rewrite nodd; destruct (alternated_series_ineq _ _ p' decr to0 cv) as [D E]. - unfold R_dist; rewrite <- Rabs_Ropp, Rabs_pos_eq;[ | fourier]. + unfold R_dist; rewrite <- Rabs_Ropp, Rabs_pos_eq;[ | lra]. 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. 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; fourier). + assert (t : forall a b c, a <= b + 1 * c -> a - b <= c) by (intros; lra). solve[apply t]. clear WLOG; intros Hyp [ | n] decr to0 cv _. generalize (alternated_series_ineq f l 0 decr to0 cv). unfold R_dist, tg_alt; simpl; rewrite !Rmult_1_l, !Rmult_1_r. assert (f 1%nat <= f 0%nat) by apply decr. - intros [A B]; rewrite Rabs_pos_eq; fourier. + 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. @@ -180,7 +180,7 @@ Lemma Alt_CVU : forall (f : nat -> R -> R) g h c r, CVU (fun N x => sum_f_R0 (tg_alt (fun i => f i x)) N) g c r. Proof. intros f g h c r decr to0 to_g bound bound0 eps ep. -assert (ep' : 0 <eps/2) by fourier. +assert (ep' : 0 <eps/2) by lra. destruct (bound0 _ ep) as [N Pn]; exists N. intros n y nN dy. rewrite <- Rabs_Ropp, Ropp_minus_distr; apply Rle_lt_trans with (f n y). @@ -201,14 +201,14 @@ intros x; destruct (Rle_lt_dec 0 x). replace (x ^ 2) with (x * x) by field. apply Rmult_le_pos; assumption. replace (x ^ 2) with ((-x) * (-x)) by field. -apply Rmult_le_pos; fourier. +apply Rmult_le_pos; lra. Qed. Lemma pow2_abs : forall x, Rabs x ^ 2 = x ^ 2. Proof. intros x; destruct (Rle_lt_dec 0 x). rewrite Rabs_pos_eq;[field | assumption]. -rewrite <- Rabs_Ropp, Rabs_pos_eq;[field | fourier]. +rewrite <- Rabs_Ropp, Rabs_pos_eq;[field | lra]. Qed. (** * Properties of tangent *) @@ -307,18 +307,18 @@ destruct (MVT_cor1 cos (PI/2) x derivable_cos xgtpi2) as [c [Pc [cint1 cint2]]]. revert Pc; rewrite cos_PI2, Rminus_0_r. rewrite <- (pr_nu cos c (derivable_pt_cos c)), derive_pt_cos. -assert (0 < c < 2) by (split; assert (t := PI2_RGT_0); fourier). +assert (0 < c < 2) by (split; assert (t := PI2_RGT_0); lra). assert (0 < sin c) by now apply sin_pos_tech. intros Pc. case (Rlt_not_le _ _ cx). rewrite <- (Rplus_0_l (cos x)), Pc, Ropp_mult_distr_l_reverse. -apply Rle_minus, Rmult_le_pos;[apply Rlt_le; assumption | fourier ]. +apply Rle_minus, Rmult_le_pos;[apply Rlt_le; assumption | lra ]. Qed. Lemma PI2_3_2 : 3/2 < PI/2. Proof. -apply PI2_lower_bound;[split; fourier | ]. -destruct (pre_cos_bound (3/2) 1) as [t _]; [fourier | fourier | ]. +apply PI2_lower_bound;[split; lra | ]. +destruct (pre_cos_bound (3/2) 1) as [t _]; [lra | lra | ]. apply Rlt_le_trans with (2 := t); clear t. unfold cos_approx; simpl; unfold cos_term. rewrite !INR_IZR_INZ. @@ -330,7 +330,7 @@ apply Rdiv_lt_0_compat ; now apply IZR_lt. Qed. Lemma PI2_1 : 1 < PI/2. -Proof. assert (t := PI2_3_2); fourier. Qed. +Proof. assert (t := PI2_3_2); lra. Qed. Lemma tan_increasing : forall x y:R, @@ -347,7 +347,7 @@ intros x y Z_le_x x_lt_y y_le_1. derivable_pt tan x). intros ; apply derivable_pt_tan ; intuition. apply derive_increasing_interv with (a:=-PI/2) (b:=PI/2) (pr:=local_derivable_pt_tan) ; intuition. - fourier. + lra. assert (Temp := pr_nu tan t (derivable_pt_tan t t_encad) (local_derivable_pt_tan t t_encad)) ; rewrite <- Temp ; clear Temp. assert (Temp := derive_pt_tan t t_encad) ; rewrite Temp ; clear Temp. @@ -414,49 +414,49 @@ Qed. (** * Definition of arctangent as the reciprocal function of tangent and proof of this status *) Lemma tan_1_gt_1 : tan 1 > 1. Proof. -assert (0 < cos 1) by (apply cos_gt_0; assert (t:=PI2_1); fourier). +assert (0 < cos 1) by (apply cos_gt_0; assert (t:=PI2_1); lra). assert (t1 : cos 1 <= 1 - 1/2 + 1/24). - destruct (pre_cos_bound 1 0) as [_ t]; try fourier; revert t. + destruct (pre_cos_bound 1 0) as [_ t]; try lra; revert t. unfold cos_approx, cos_term; simpl; intros t; apply Rle_trans with (1:=t). clear t; apply Req_le; field. assert (t2 : 1 - 1/6 <= sin 1). - destruct (pre_sin_bound 1 0) as [t _]; try fourier; revert t. + destruct (pre_sin_bound 1 0) as [t _]; try lra; revert t. unfold sin_approx, sin_term; simpl; intros t; apply Rle_trans with (2:=t). clear t; apply Req_le; field. pattern 1 at 2; replace 1 with - (cos 1 / cos 1) by (field; apply Rgt_not_eq; fourier). + (cos 1 / cos 1) by (field; apply Rgt_not_eq; lra). apply Rlt_gt; apply (Rmult_lt_compat_r (/ cos 1) (cos 1) (sin 1)). apply Rinv_0_lt_compat; assumption. apply Rle_lt_trans with (1 := t1); apply Rlt_le_trans with (2 := t2). -fourier. +lra. Qed. Definition frame_tan y : {x | 0 < x < PI/2 /\ Rabs y < tan x}. Proof. destruct (total_order_T (Rabs y) 1) as [Hs|Hgt]. - assert (yle1 : Rabs y <= 1) by (destruct Hs; fourier). + assert (yle1 : Rabs y <= 1) by (destruct Hs; lra). clear Hs; exists 1; split;[split; [exact Rlt_0_1 | exact PI2_1] | ]. apply Rle_lt_trans with (1 := yle1); exact tan_1_gt_1. assert (0 < / (Rabs y + 1)). - apply Rinv_0_lt_compat; fourier. + apply Rinv_0_lt_compat; lra. set (u := /2 * / (Rabs y + 1)). assert (0 < u). - apply Rmult_lt_0_compat; [fourier | assumption]. + apply Rmult_lt_0_compat; [lra | assumption]. assert (vlt1 : / (Rabs y + 1) < 1). apply Rmult_lt_reg_r with (Rabs y + 1). - assert (t := Rabs_pos y); fourier. - rewrite Rinv_l; [rewrite Rmult_1_l | apply Rgt_not_eq]; fourier. + assert (t := Rabs_pos y); lra. + rewrite Rinv_l; [rewrite Rmult_1_l | apply Rgt_not_eq]; lra. assert (vlt2 : u < 1). apply Rlt_trans with (/ (Rabs y + 1)). rewrite double_var. - assert (t : forall x, 0 < x -> x < x + x) by (clear; intros; fourier). + assert (t : forall x, 0 < x -> x < x + x) by (clear; intros; lra). unfold u; rewrite Rmult_comm; apply t. unfold Rdiv; rewrite Rmult_comm; assumption. assumption. assert(int : 0 < PI / 2 - u < PI / 2). split. assert (t := PI2_1); apply Rlt_Rminus, Rlt_trans with (2 := t); assumption. - assert (dumb : forall x y, 0 < y -> x - y < x) by (clear; intros; fourier). + assert (dumb : forall x y, 0 < y -> x - y < x) by (clear; intros; lra). apply dumb; clear dumb; assumption. exists (PI/2 - u). assert (tmp : forall x y, 0 < x -> y < 1 -> x * y < x). @@ -473,7 +473,7 @@ split. assert (sin u < u). assert (t1 : 0 <= u) by (apply Rlt_le; assumption). assert (t2 : u <= 4) by - (apply Rle_trans with 1;[apply Rlt_le | fourier]; assumption). + (apply Rle_trans with 1;[apply Rlt_le | lra]; assumption). destruct (pre_sin_bound u 0 t1 t2) as [_ t]. apply Rle_lt_trans with (1 := t); clear t1 t2 t. unfold sin_approx; simpl; unfold sin_term; simpl ((-1) ^ 0); @@ -503,17 +503,17 @@ split. solve[apply Rinv_0_lt_compat, INR_fact_lt_0]. apply Rlt_trans with (2 := vlt2). simpl; unfold u; apply tmp; auto; rewrite Rmult_1_r; assumption. - apply Rlt_trans with (Rabs y + 1);[fourier | ]. + apply Rlt_trans with (Rabs y + 1);[lra | ]. pattern (Rabs y + 1) at 1; rewrite <- (Rinv_involutive (Rabs y + 1)); - [ | apply Rgt_not_eq; fourier]. + [ | apply Rgt_not_eq; lra]. rewrite <- Rinv_mult_distr. apply Rinv_lt_contravar. apply Rmult_lt_0_compat. - apply Rmult_lt_0_compat;[fourier | assumption]. + apply Rmult_lt_0_compat;[lra | assumption]. assumption. replace (/(Rabs y + 1)) with (2 * u). - fourier. - unfold u; field; apply Rgt_not_eq; clear -Hgt; fourier. + lra. + unfold u; field; apply Rgt_not_eq; clear -Hgt; lra. solve[discrR]. apply Rgt_not_eq; assumption. unfold tan. @@ -522,22 +522,22 @@ set (u' := PI / 2); unfold Rdiv; apply Rmult_lt_compat_r; unfold u'. rewrite cos_shift; assumption. assert (vlt3 : u < /4). replace (/4) with (/2 * /2) by field. - unfold u; apply Rmult_lt_compat_l;[fourier | ]. + unfold u; apply Rmult_lt_compat_l;[lra | ]. apply Rinv_lt_contravar. - apply Rmult_lt_0_compat; fourier. - fourier. -assert (1 < PI / 2 - u) by (assert (t := PI2_3_2); fourier). + apply Rmult_lt_0_compat; lra. + lra. +assert (1 < PI / 2 - u) by (assert (t := PI2_3_2); lra). apply Rlt_trans with (sin 1). - assert (t' : 1 <= 4) by fourier. + assert (t' : 1 <= 4) by lra. destruct (pre_sin_bound 1 0 (Rlt_le _ _ Rlt_0_1) t') as [t _]. apply Rlt_le_trans with (2 := t); clear t. - simpl plus; replace (sin_approx 1 1) with (5/6);[fourier | ]. + simpl plus; replace (sin_approx 1 1) with (5/6);[lra | ]. unfold sin_approx, sin_term; simpl; field. apply sin_increasing_1. - assert (t := PI2_1); fourier. + assert (t := PI2_1); lra. apply Rlt_le, PI2_1. - assert (t := PI2_1); fourier. - fourier. + assert (t := PI2_1); lra. + lra. assumption. Qed. @@ -547,7 +547,7 @@ intros x h; rewrite Ropp_div; apply Ropp_lt_contravar; assumption. Qed. Lemma pos_opp_lt : forall x, 0 < x -> -x < x. -Proof. intros; fourier. Qed. +Proof. intros; lra. Qed. Lemma tech_opp_tan : forall x y, -tan x < y -> tan (-x) < y. Proof. @@ -562,7 +562,7 @@ set (pr := (conj (tech_opp_tan _ _ (proj2 (Rabs_def2 _ _ Ptan_ub))) destruct (exists_atan_in_frame (-ub) ub y (pos_opp_lt _ ub0) (ub_opp _ ubpi2) ubpi2 pr) as [v [[vl vu] vq]]. exists v; clear pr. -split;[rewrite Ropp_div; split; fourier | assumption]. +split;[rewrite Ropp_div; split; lra | assumption]. Qed. Definition atan x := let (v, _) := pre_atan x in v. @@ -581,7 +581,7 @@ Lemma atan_opp : forall x, atan (- x) = - atan x. Proof. intros x; generalize (atan_bound (-x)); rewrite Ropp_div;intros [a b]. generalize (atan_bound x); rewrite Ropp_div; intros [c d]. -apply tan_is_inj; try rewrite Ropp_div; try split; try fourier. +apply tan_is_inj; try rewrite Ropp_div; try split; try lra. rewrite tan_neg, !atan_right_inv; reflexivity. Qed. @@ -604,23 +604,23 @@ assert (int_tan : forall y, tan (- ub) <= y -> y <= tan ub -> rewrite <- (atan_right_inv y); apply tan_increasing. destruct (atan_bound y); assumption. assumption. - fourier. - fourier. + lra. + lra. destruct (Rle_lt_dec (atan y) ub) as [h | abs]; auto. assert (tan ub < y). rewrite <- (atan_right_inv y); apply tan_increasing. - rewrite Ropp_div; fourier. + rewrite Ropp_div; lra. assumption. destruct (atan_bound y); assumption. - fourier. + lra. assert (incr : forall x y, -ub <= x -> x < y -> y <= ub -> tan x < tan y). intros y z l yz u; apply tan_increasing. - rewrite Ropp_div; fourier. + rewrite Ropp_div; lra. assumption. - fourier. + lra. assert (der : forall a, -ub <= a <= ub -> derivable_pt tan a). intros a [la ua]; apply derivable_pt_tan. - rewrite Ropp_div; split; fourier. + rewrite Ropp_div; split; lra. assert (df_neq : derive_pt tan (atan x) (derivable_pt_recip_interv_prelim1 tan atan (- ub) ub x lb_lt_ub xint inv_p int_tan incr der) <> 0). @@ -651,7 +651,7 @@ Qed. Lemma atan_0 : atan 0 = 0. Proof. apply tan_is_inj; try (apply atan_bound). - assert (t := PI_RGT_0); rewrite Ropp_div; split; fourier. + assert (t := PI_RGT_0); rewrite Ropp_div; split; lra. rewrite atan_right_inv, tan_0. reflexivity. Qed. @@ -659,7 +659,7 @@ Qed. Lemma atan_1 : atan 1 = PI/4. Proof. assert (ut := PI_RGT_0). -assert (-PI/2 < PI/4 < PI/2) by (rewrite Ropp_div; split; fourier). +assert (-PI/2 < PI/4 < PI/2) by (rewrite Ropp_div; split; lra). assert (t := atan_bound 1). apply tan_is_inj; auto. rewrite tan_PI4, atan_right_inv; reflexivity. @@ -688,23 +688,23 @@ assert (int_tan : forall y, tan (- ub) <= y -> y <= tan ub -> rewrite <- (atan_right_inv y); apply tan_increasing. destruct (atan_bound y); assumption. assumption. - fourier. - fourier. + lra. + lra. destruct (Rle_lt_dec (atan y) ub) as [h | abs]; auto. assert (tan ub < y). rewrite <- (atan_right_inv y); apply tan_increasing. - rewrite Ropp_div; fourier. + rewrite Ropp_div; lra. assumption. destruct (atan_bound y); assumption. - fourier. + lra. assert (incr : forall x y, -ub <= x -> x < y -> y <= ub -> tan x < tan y). intros y z l yz u; apply tan_increasing. - rewrite Ropp_div; fourier. + rewrite Ropp_div; lra. assumption. - fourier. + lra. assert (der : forall a, -ub <= a <= ub -> derivable_pt tan a). intros a [la ua]; apply derivable_pt_tan. - rewrite Ropp_div; split; fourier. + rewrite Ropp_div; split; lra. assert (df_neq : derive_pt tan (atan x) (derivable_pt_recip_interv_prelim1 tan atan (- ub) ub x lb_lt_ub xint inv_p int_tan incr der) <> 0). @@ -883,7 +883,7 @@ Proof. destruct (Rle_lt_dec 0 x). assert (pr : 0 <= x <= 1) by tauto. exact (ps_atan_exists_01 x pr). -assert (pr : 0 <= -x <= 1) by (destruct Hx; split; fourier). +assert (pr : 0 <= -x <= 1) by (destruct Hx; split; lra). destruct (ps_atan_exists_01 _ pr) as [v Pv]. exists (-v). apply (Un_cv_ext (fun n => (- 1) * sum_f_R0 (tg_alt (Ratan_seq (- x))) n)). @@ -898,8 +898,8 @@ Proof. destruct (Rle_lt_dec x 1). destruct (Rle_lt_dec (-1) x). left;split; auto. - right;intros [a1 a2]; fourier. -right;intros [a1 a2]; fourier. + right;intros [a1 a2]; lra. +right;intros [a1 a2]; lra. Qed. Definition ps_atan (x : R) : R := @@ -922,7 +922,7 @@ unfold ps_atan. unfold Rdiv; rewrite !Rmult_0_l, Rmult_0_r; reflexivity. intros eps ep; exists 0%nat; intros n _; unfold R_dist. rewrite Rminus_0_r, Rabs_pos_eq; auto with real. -case h2; split; fourier. +case h2; split; lra. Qed. Lemma ps_atan_exists_1_opp : @@ -948,9 +948,9 @@ destruct (in_int (- x)) as [inside | outside]. destruct (in_int x) as [ins' | outs']. generalize (ps_atan_exists_1_opp x inside ins'). intros h; exact h. - destruct inside; case outs'; split; fourier. + destruct inside; case outs'; split; lra. destruct (in_int x) as [ins' | outs']. - destruct outside; case ins'; split; fourier. + destruct outside; case ins'; split; lra. apply atan_opp. Qed. @@ -1057,7 +1057,7 @@ Proof. intros x n. assert (dif : - x ^ 2 <> 1). apply Rlt_not_eq; apply Rle_lt_trans with 0;[ | apply Rlt_0_1]. -assert (t := pow2_ge_0 x); fourier. +assert (t := pow2_ge_0 x); lra. replace (1 + x ^ 2) with (1 - - (x ^ 2)) by ring; rewrite <- (tech3 _ n dif). apply sum_eq; unfold tg_alt, Datan_seq; intros i _. rewrite pow_mult, <- Rpow_mult_distr. @@ -1073,7 +1073,7 @@ intros x y n n_lb x_encad ; assert (x_pos : x >= 0) by intuition. apply False_ind ; intuition. 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. fourier. + simpl ; apply Rmult_gt_0_lt_compat ; intuition. lra. rewrite x_pos ; rewrite pow_i. replace (y ^ (2*1)) with (y*y). apply Rmult_gt_0_compat ; assumption. simpl ; field. @@ -1084,7 +1084,7 @@ intros x y n n_lb x_encad ; assert (x_pos : x >= 0) by intuition. 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 ; fourier. + apply Rmult_gt_0_lt_compat ; intuition ; lra. rewrite x_pos. rewrite pow_i ; intuition. Qed. @@ -1141,7 +1141,7 @@ elim (pow_lt_1_zero _ x_ub2 _ eps'_pos) ; intros N HN ; exists N. intros n Hn. assert (H1 : - x^2 <> 1). apply Rlt_not_eq; apply Rle_lt_trans with (2 := Rlt_0_1). -assert (t := pow2_ge_0 x); fourier. +assert (t := pow2_ge_0 x); lra. rewrite Datan_sum_eq. unfold R_dist. assert (tool : forall a b, a / b - /b = (-1 + a) /b). @@ -1179,13 +1179,13 @@ apply (Alt_CVU (fun x n => Datan_seq n x) (Datan_seq (Rabs c + r)) c r). intros x inb; apply Datan_seq_decreasing; try (apply Boule_lt in inb; apply Rabs_def2 in inb; - destruct inb; fourier). + destruct inb; lra). intros x inb; apply Datan_seq_CV_0; try (apply Boule_lt in inb; apply Rabs_def2 in inb; - destruct inb; fourier). + destruct inb; lra). intros x inb; apply (Datan_lim x); try (apply Boule_lt in inb; apply Rabs_def2 in inb; - destruct inb; fourier). + destruct inb; lra). intros x [ | n] inb. solve[unfold Datan_seq; apply Rle_refl]. rewrite <- (Datan_seq_Rabs x); apply Rlt_le, Datan_seq_increasing. @@ -1193,7 +1193,7 @@ apply (Alt_CVU (fun x n => Datan_seq n x) apply Boule_lt in inb; intuition. solve[apply Rabs_pos]. apply Datan_seq_CV_0. - apply Rlt_trans with 0;[fourier | ]. + apply Rlt_trans with 0;[lra | ]. apply Rplus_le_lt_0_compat. solve[apply Rabs_pos]. destruct r; assumption. @@ -1226,7 +1226,7 @@ intros N x x_lb x_ub. apply Hdelta ; assumption. unfold id ; field ; assumption. intros eps eps_pos. - assert (eps_3_pos : (eps/3) > 0) by fourier. + assert (eps_3_pos : (eps/3) > 0) by lra. elim (IHN (eps/3) eps_3_pos) ; intros delta1 Hdelta1. assert (Main : derivable_pt_lim (fun x : R =>tg_alt (Ratan_seq x) (S N)) x ((tg_alt (Datan_seq x)) (S N))). clear -Tool ; intros eps' eps'_pos. @@ -1297,7 +1297,7 @@ intros N x x_lb x_ub. intuition ; apply Rlt_le_trans with (r2:=delta) ; intuition unfold delta, mydelta. apply Rmin_l. apply Rmin_r. - fourier. + lra. Qed. Lemma Ratan_CVU' : @@ -1310,7 +1310,7 @@ apply (Alt_CVU (fun i r => Ratan_seq r i) ps_atan PI_tg (/2) pos_half); now intros; apply Ratan_seq_converging, Boule_half_to_interval. intros x b; apply Boule_half_to_interval in b. unfold ps_atan; destruct (in_int x) as [inside | outside]; - [ | destruct b; case outside; split; fourier]. + [ | destruct b; case outside; split; lra]. destruct (ps_atan_exists_1 x inside) as [v Pv]. apply Un_cv_ext with (2 := Pv);[reflexivity]. intros x n b; apply Boule_half_to_interval in b. @@ -1330,7 +1330,7 @@ exists N; intros n x nN b_y. case (Rtotal_order 0 x) as [xgt0 | [x0 | x0]]. assert (Boule (/2) {| pos := / 2; cond_pos := pos_half_prf|} x). revert b_y; unfold Boule; simpl; intros b_y; apply Rabs_def2 in b_y. - destruct b_y; unfold Boule; simpl; apply Rabs_def1; fourier. + destruct b_y; unfold Boule; simpl; apply Rabs_def1; lra. apply Pn; assumption. rewrite <- x0, ps_atan0_0. rewrite <- (sum_eq (fun _ => 0)), sum_cte, Rmult_0_l, Rminus_0_r, Rabs_pos_eq. @@ -1343,7 +1343,7 @@ replace (ps_atan x - sum_f_R0 (tg_alt (Ratan_seq x)) n) with rewrite Rabs_Ropp. assert (Boule (/2) {| pos := / 2; cond_pos := pos_half_prf|} (-x)). revert b_y; unfold Boule; simpl; intros b_y; apply Rabs_def2 in b_y. - destruct b_y; unfold Boule; simpl; apply Rabs_def1; fourier. + destruct b_y; unfold Boule; simpl; apply Rabs_def1; lra. apply Pn; assumption. unfold Rminus; rewrite ps_atan_opp, Ropp_plus_distr, sum_Ratan_seq_opp. rewrite !Ropp_involutive; reflexivity. @@ -1372,7 +1372,7 @@ apply continuity_inv. apply continuity_plus. apply continuity_const ; unfold constant ; intuition. apply derivable_continuous ; apply derivable_pow. -intro x ; apply Rgt_not_eq ; apply Rge_gt_trans with (1+0) ; [|fourier] ; +intro x ; apply Rgt_not_eq ; apply Rge_gt_trans with (1+0) ; [|lra] ; apply Rplus_ge_compat_l. replace (x^2) with (x²). apply Rle_ge ; apply Rle_0_sqr. @@ -1393,11 +1393,11 @@ apply derivable_pt_lim_CVU with assumption. intros y N inb; apply Rabs_def2 in inb; destruct inb. apply Datan_is_datan. - fourier. - fourier. + lra. + lra. intros y inb; apply Rabs_def2 in inb; destruct inb. - assert (y_gt_0 : -1 < y) by fourier. - assert (y_lt_1 : y < 1) by fourier. + assert (y_gt_0 : -1 < y) by lra. + assert (y_lt_1 : y < 1) by lra. intros eps eps_pos ; elim (Ratan_is_ps_atan eps eps_pos). intros N HN ; exists N; intros n n_lb ; apply HN ; tauto. apply Datan_CVU_prelim. @@ -1406,8 +1406,8 @@ apply derivable_pt_lim_CVU with replace ((c + r - (c - r)) / 2) with (r :R) by field. assert (Rabs c < 1 - r). unfold Boule in Pcr1; destruct r; simpl in *; apply Rabs_def1; - apply Rabs_def2 in Pcr1; destruct Pcr1; fourier. - fourier. + apply Rabs_def2 in Pcr1; destruct Pcr1; lra. + lra. intros; apply Datan_continuity. Qed. @@ -1426,7 +1426,7 @@ Lemma ps_atan_continuity_pt_1 : forall eps : R, dist R_met (ps_atan x) (Alt_PI/4) < eps). Proof. intros eps eps_pos. -assert (eps_3_pos : eps / 3 > 0) by fourier. +assert (eps_3_pos : eps / 3 > 0) by lra. elim (Ratan_is_ps_atan (eps / 3) eps_3_pos) ; intros N1 HN1. unfold Alt_PI. destruct exist_PI as [v Pv]; replace ((4 * v)/4) with v by field. @@ -1461,10 +1461,10 @@ rewrite Rplus_assoc ; apply Rabs_triang. unfold D_x, no_cond ; split ; [ | apply Rgt_not_eq ] ; intuition. intuition. apply HN2; unfold N; omega. - fourier. + lra. rewrite <- Rabs_Ropp, Ropp_minus_distr; apply HN1. unfold N; omega. - fourier. + lra. assumption. field. ring. @@ -1486,11 +1486,11 @@ intros x x_encad Pratan Prmymeta. rewrite Hrew1. replace (Rsqr x) with (x ^ 2) by (unfold Rsqr; ring). unfold Rdiv; rewrite Rmult_1_l; reflexivity. - fourier. + lra. assumption. intros; reflexivity. - fourier. - assert (t := tan_1_gt_1); split;destruct x_encad; fourier. + lra. + assert (t := tan_1_gt_1); split;destruct x_encad; lra. intros; reflexivity. Qed. @@ -1503,46 +1503,46 @@ assert (pr1 : forall c : R, 0 < c < x -> derivable_pt (atan - ps_atan) c). apply derivable_pt_minus. exact (derivable_pt_atan c). apply derivable_pt_ps_atan. - destruct x_encad; destruct c_encad; split; fourier. + destruct x_encad; destruct c_encad; split; lra. assert (pr2 : forall c : R, 0 < c < x -> derivable_pt id c). - intros ; apply derivable_pt_id; fourier. + intros ; apply derivable_pt_id; lra. assert (delta_cont : forall c : R, 0 <= c <= x -> continuity_pt (atan - ps_atan) c). intros c [[c_encad1 | c_encad1 ] [c_encad2 | c_encad2]]; apply continuity_pt_minus. apply derivable_continuous_pt ; apply derivable_pt_atan. apply derivable_continuous_pt ; apply derivable_pt_ps_atan. - split; destruct x_encad; fourier. + split; destruct x_encad; lra. apply derivable_continuous_pt, derivable_pt_atan. apply derivable_continuous_pt, derivable_pt_ps_atan. - subst c; destruct x_encad; split; fourier. + subst c; destruct x_encad; split; lra. apply derivable_continuous_pt, derivable_pt_atan. apply derivable_continuous_pt, derivable_pt_ps_atan. - subst c; split; fourier. + subst c; split; lra. apply derivable_continuous_pt, derivable_pt_atan. apply derivable_continuous_pt, derivable_pt_ps_atan. - subst c; destruct x_encad; split; fourier. + subst c; destruct x_encad; split; lra. assert (id_cont : forall c : R, 0 <= c <= x -> continuity_pt id c). intros ; apply derivable_continuous ; apply derivable_id. -assert (x_lb : 0 < x) by (destruct x_encad; fourier). +assert (x_lb : 0 < x) by (destruct x_encad; lra). elim (MVT (atan - ps_atan)%F id 0 x pr1 pr2 x_lb delta_cont id_cont) ; intros d Temp ; elim Temp ; intros d_encad Main. clear - Main x_encad. assert (Temp : forall (pr: derivable_pt (atan - ps_atan) d), derive_pt (atan - ps_atan) d pr = 0). intro pr. assert (d_encad3 : -1 < d < 1). - destruct d_encad; destruct x_encad; split; fourier. + destruct d_encad; destruct x_encad; split; lra. pose (pr3 := derivable_pt_minus atan ps_atan d (derivable_pt_atan d) (derivable_pt_ps_atan d d_encad3)). rewrite <- pr_nu_var2_interv with (f:=(atan - ps_atan)%F) (g:=(atan - ps_atan)%F) (lb:=0) (ub:=x) (pr1:=pr3) (pr2:=pr). unfold pr3. rewrite derive_pt_minus. rewrite Datan_eq_DatanSeq_interv with (Prmymeta := derivable_pt_atan d). intuition. assumption. - destruct d_encad; fourier. + destruct d_encad; lra. assumption. reflexivity. assert (iatan0 : atan 0 = 0). apply tan_is_inj. apply atan_bound. - rewrite Ropp_div; assert (t := PI2_RGT_0); split; fourier. + rewrite Ropp_div; assert (t := PI2_RGT_0); split; lra. rewrite tan_0, atan_right_inv; reflexivity. generalize Main; rewrite Temp, Rmult_0_r. replace ((atan - ps_atan)%F x) with (atan x - ps_atan x) by intuition. @@ -1560,19 +1560,19 @@ Qed. Theorem Alt_PI_eq : Alt_PI = PI. Proof. apply Rmult_eq_reg_r with (/4); fold (Alt_PI/4); fold (PI/4); - [ | apply Rgt_not_eq; fourier]. + [ | apply Rgt_not_eq; lra]. assert (0 < PI/6) by (apply PI6_RGT_0). assert (t1:= PI2_1). assert (t2 := PI_4). assert (m := Alt_PI_RGT_0). -assert (-PI/2 < 1 < PI/2) by (rewrite Ropp_div; split; fourier). +assert (-PI/2 < 1 < PI/2) by (rewrite Ropp_div; split; lra). apply cond_eq; intros eps ep. change (R_dist (Alt_PI/4) (PI/4) < eps). assert (ca : continuity_pt atan 1). apply derivable_continuous_pt, derivable_pt_atan. assert (Xe : exists eps', exists eps'', eps' + eps'' <= eps /\ 0 < eps' /\ 0 < eps''). - exists (eps/2); exists (eps/2); repeat apply conj; fourier. + exists (eps/2); exists (eps/2); repeat apply conj; lra. destruct Xe as [eps' [eps'' [eps_ineq [ep' ep'']]]]. destruct (ps_atan_continuity_pt_1 _ ep') as [alpha [a0 Palpha]]. destruct (ca _ ep'') as [beta [b0 Pbeta]]. @@ -1585,14 +1585,14 @@ assert (Xa : exists a, 0 < a < 1 /\ R_dist a 1 < alpha /\ assert ((1 - alpha /2) <= Rmax (1 - alpha /2) (1 - beta /2)) by apply Rmax_l. assert ((1 - beta /2) <= Rmax (1 - alpha /2) (1 - beta /2)) by apply Rmax_r. assert (Rmax (1 - alpha /2) (1 - beta /2) < 1) - by (apply Rmax_lub_lt; fourier). - split;[split;[ | apply Rmax_lub_lt]; fourier | ]. + by (apply Rmax_lub_lt; lra). + split;[split;[ | apply Rmax_lub_lt]; lra | ]. assert (0 <= 1 - Rmax (/ 2) (Rmax (1 - alpha / 2) (1 - beta / 2))). assert (Rmax (/2) (Rmax (1 - alpha / 2) - (1 - beta /2)) <= 1) by (apply Rmax_lub; fourier). - fourier. + (1 - beta /2)) <= 1) by (apply Rmax_lub; lra). + lra. split; unfold R_dist; rewrite <-Rabs_Ropp, Ropp_minus_distr, - Rabs_pos_eq;fourier. + Rabs_pos_eq;lra. destruct Xa as [a [[Pa0 Pa1] [P1 P2]]]. apply Rle_lt_trans with (1 := R_dist_tri _ _ (ps_atan a)). apply Rlt_le_trans with (2 := eps_ineq). diff --git a/theories/Reals/Rbasic_fun.v b/theories/Reals/Rbasic_fun.v index aa886cee..59e01486 100644 --- a/theories/Reals/Rbasic_fun.v +++ b/theories/Reals/Rbasic_fun.v @@ -15,7 +15,7 @@ Require Import Rbase. Require Import R_Ifp. -Require Import Fourier. +Require Import Lra. Local Open Scope R_scope. Implicit Type r : R. @@ -357,7 +357,7 @@ Qed. Lemma Rle_abs : forall x:R, x <= Rabs x. Proof. - intro; unfold Rabs; case (Rcase_abs x); intros; fourier. + intro; unfold Rabs; case (Rcase_abs x); intros; lra. Qed. Definition RRle_abs := Rle_abs. diff --git a/theories/Reals/Rderiv.v b/theories/Reals/Rderiv.v index dfa5c710..aaf691ed 100644 --- a/theories/Reals/Rderiv.v +++ b/theories/Reals/Rderiv.v @@ -16,7 +16,7 @@ Require Import Rbase. Require Import Rfunctions. Require Import Rlimit. -Require Import Fourier. +Require Import Lra. Require Import Omega. Local Open Scope R_scope. @@ -77,7 +77,7 @@ Proof. elim (Rmin_Rgt (/ 2) x 0); intros a b; cut (0 < 2). intro; generalize (Rinv_0_lt_compat 2 H3); intro; fold (/ 2 > 0) in H4; apply (b (conj H4 H)). - fourier. + lra. intros; elim H3; clear H3; intros; generalize (let (H1, H2) := @@ -167,7 +167,7 @@ Proof. unfold Rabs; destruct (Rcase_abs 2) as [Hlt|Hge]; auto. cut (0 < 2). intro H7; elim (Rlt_asym 0 2 H7 Hlt). - fourier. + lra. apply Rabs_no_R0. discrR. Qed. diff --git a/theories/Reals/Reals.v b/theories/Reals/Reals.v index b249b519..3ef368bb 100644 --- a/theories/Reals/Reals.v +++ b/theories/Reals/Reals.v @@ -30,3 +30,4 @@ Require Export SeqSeries. Require Export Rtrigo. Require Export Ranalysis. Require Export Integration. +Require Import Fourier. diff --git a/theories/Reals/Rlimit.v b/theories/Reals/Rlimit.v index b14fcc4d..e3e995d2 100644 --- a/theories/Reals/Rlimit.v +++ b/theories/Reals/Rlimit.v @@ -15,7 +15,7 @@ Require Import Rbase. Require Import Rfunctions. -Require Import Fourier. +Require Import Lra. Local Open Scope R_scope. (*******************************) @@ -24,7 +24,7 @@ Local Open Scope R_scope. (*********) Lemma eps2_Rgt_R0 : forall eps:R, eps > 0 -> eps * / 2 > 0. Proof. - intros; fourier. + intros; lra. Qed. (*********) @@ -45,14 +45,14 @@ Qed. Lemma Rlt_eps2_eps : forall eps:R, eps > 0 -> eps * / 2 < eps. Proof. intros. - fourier. + lra. Qed. (*********) Lemma Rlt_eps4_eps : forall eps:R, eps > 0 -> eps * / (2 + 2) < eps. Proof. intros. - fourier. + lra. Qed. (*********) diff --git a/theories/Reals/Rpower.v b/theories/Reals/Rpower.v index c6fac951..d465523a 100644 --- a/theories/Reals/Rpower.v +++ b/theories/Reals/Rpower.v @@ -25,7 +25,7 @@ Require Import R_sqrt. Require Import Sqrt_reg. Require Import MVT. Require Import Ranalysis4. -Require Import Fourier. +Require Import Lra. Local Open Scope R_scope. Lemma P_Rmin : forall (P:R -> Prop) (x y:R), P x -> P y -> P (Rmin x y). @@ -714,7 +714,7 @@ Qed. Lemma Rlt_Rpower_l a b c: 0 < c -> 0 < a < b -> a ^R c < b ^R c. Proof. intros c0 [a0 ab]; apply exp_increasing. -now apply Rmult_lt_compat_l; auto; apply ln_increasing; fourier. +now apply Rmult_lt_compat_l; auto; apply ln_increasing; lra. Qed. Lemma Rle_Rpower_l a b c: 0 <= c -> 0 < a <= b -> a ^R c <= b ^R c. @@ -722,7 +722,7 @@ Proof. intros [c0 | c0]; [ | intros; rewrite <- c0, !Rpower_O; [apply Rle_refl | |] ]. intros [a0 [ab|ab]]. - now apply Rlt_le, Rlt_Rpower_l;[ | split]; fourier. + now apply Rlt_le, Rlt_Rpower_l;[ | split]; lra. rewrite ab; apply Rle_refl. apply Rlt_le_trans with a; tauto. tauto. @@ -754,10 +754,10 @@ assert (cmp : 0 < x + sqrt (x ^ 2 + 1)). replace (x ^ 2) with ((-x) ^ 2) by ring. assert (sqrt ((- x) ^ 2) < sqrt ((-x)^2+1)). apply sqrt_lt_1_alt. - split;[apply pow_le | ]; fourier. + split;[apply pow_le | ]; lra. pattern x at 1; replace x with (- (sqrt ((- x) ^ 2))). - assert (t:= sqrt_pos ((-x)^2)); fourier. - simpl; rewrite Rmult_1_r, sqrt_square, Ropp_involutive;[reflexivity | fourier]. + assert (t:= sqrt_pos ((-x)^2)); lra. + simpl; rewrite Rmult_1_r, sqrt_square, Ropp_involutive;[reflexivity | lra]. apply Rplus_lt_le_0_compat;[apply Rnot_le_gt; assumption | apply sqrt_pos]. rewrite exp_ln;[ | assumption]. rewrite exp_Ropp, exp_ln;[ | assumption]. @@ -770,7 +770,7 @@ apply Rmult_eq_reg_l with (2 * (x + sqrt (x ^ 2 + 1)));[ | apply Rgt_not_eq, Rmult_lt_0_compat;[apply Rlt_0_2 | assumption]]. assert (pow2_sqrt : forall x, 0 <= x -> sqrt x ^ 2 = x) by (intros; simpl; rewrite Rmult_1_r, sqrt_sqrt; auto). -field_simplify;[rewrite pow2_sqrt;[field | ] | apply Rgt_not_eq; fourier]. +field_simplify;[rewrite pow2_sqrt;[field | ] | apply Rgt_not_eq; lra]. apply Rplus_le_le_0_compat;[simpl; rewrite Rmult_1_r; apply (Rle_0_sqr x)|apply Rlt_le, Rlt_0_1]. Qed. @@ -784,12 +784,12 @@ assert (0 < x + sqrt (x ^ 2 + 1)). replace (x ^ 2) with ((-x) ^ 2) by ring. assert (sqrt ((- x) ^ 2) < sqrt ((-x)^2+1)). apply sqrt_lt_1_alt. - split;[apply pow_le|]; fourier. + split;[apply pow_le|]; lra. pattern x at 1; replace x with (- (sqrt ((- x) ^ 2))). - assert (t:= sqrt_pos ((-x)^2)); fourier. - simpl; rewrite Rmult_1_r, sqrt_square, Ropp_involutive; auto; fourier. + assert (t:= sqrt_pos ((-x)^2)); lra. + simpl; rewrite Rmult_1_r, sqrt_square, Ropp_involutive; auto; lra. assert (0 < x ^ 2 + 1). - apply Rplus_le_lt_0_compat;[simpl; rewrite Rmult_1_r; apply Rle_0_sqr|fourier]. + apply Rplus_le_lt_0_compat;[simpl; rewrite Rmult_1_r; apply Rle_0_sqr|lra]. replace (/sqrt (x ^ 2 + 1)) with (/(x + sqrt (x ^ 2 + 1)) * (1 + (/(2 * sqrt (x ^ 2 + 1)) * (INR 2 * x ^ 1 + 0)))). @@ -817,7 +817,7 @@ intros x y xy. case (Rle_dec (arcsinh y) (arcsinh x));[ | apply Rnot_le_lt ]. intros abs; case (Rlt_not_le _ _ xy). rewrite <- (sinh_arcsinh y), <- (sinh_arcsinh x). -destruct abs as [lt | q];[| rewrite q; fourier]. +destruct abs as [lt | q];[| rewrite q; lra]. apply Rlt_le, sinh_lt; assumption. Qed. diff --git a/theories/Reals/Rsqrt_def.v b/theories/Reals/Rsqrt_def.v index 6a3dd976..9b8dd1db 100644 --- a/theories/Reals/Rsqrt_def.v +++ b/theories/Reals/Rsqrt_def.v @@ -392,7 +392,7 @@ Definition cond_positivity (x:R) : bool := | right _ => false end. -(** Sequential caracterisation of continuity *) +(** Sequential characterisation of continuity *) Lemma continuity_seq : forall (f:R -> R) (Un:nat -> R) (l:R), continuity_pt f l -> Un_cv Un l -> Un_cv (fun i:nat => f (Un i)) (f l). diff --git a/theories/Reals/Rtrigo.v b/theories/Reals/Rtrigo.v index ffc0adf5..ddd8722e 100644 --- a/theories/Reals/Rtrigo.v +++ b/theories/Reals/Rtrigo.v @@ -18,7 +18,7 @@ Require Export Cos_rel. Require Export Cos_plus. Require Import ZArith_base. Require Import Zcomplements. -Require Import Fourier. +Require Import Lra. Require Import Ranalysis1. Require Import Rsqrt_def. Require Import PSeries_reg. diff --git a/theories/Reals/Rtrigo1.v b/theories/Reals/Rtrigo1.v index bf00f736..a75fd2dd 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. -Require Import Fourier. +Require Import Lra. Require Import Ranalysis1. Require Import Rsqrt_def. Require Import PSeries_reg. @@ -175,10 +175,10 @@ Qed. Lemma sin_gt_cos_7_8 : sin (7 / 8) > cos (7 / 8). Proof. -assert (lo1 : 0 <= 7/8) by fourier. -assert (up1 : 7/8 <= 4) by fourier. -assert (lo : -2 <= 7/8) by fourier. -assert (up : 7/8 <= 2) by fourier. +assert (lo1 : 0 <= 7/8) by lra. +assert (up1 : 7/8 <= 4) by lra. +assert (lo : -2 <= 7/8) by lra. +assert (up : 7/8 <= 2) by lra. destruct (pre_sin_bound _ 0 lo1 up1) as [lower _ ]. destruct (pre_cos_bound _ 0 lo up) as [_ upper]. apply Rle_lt_trans with (1 := upper). @@ -205,12 +205,12 @@ Definition PI_2_aux : {z | 7/8 <= z <= 7/4 /\ -cos z = 0}. assert (cc : continuity (fun r =>- cos r)). apply continuity_opp, continuity_cos. assert (cvp : 0 < cos (7/8)). - assert (int78 : -2 <= 7/8 <= 2) by (split; fourier). + assert (int78 : -2 <= 7/8 <= 2) by (split; lra). destruct int78 as [lower upper]. case (pre_cos_bound _ 0 lower upper). unfold cos_approx; simpl sum_f_R0; unfold cos_term. intros cl _; apply Rlt_le_trans with (2 := cl); simpl. - fourier. + lra. assert (cun : cos (7/4) < 0). replace (7/4) with (7/8 + 7/8) by field. rewrite cos_plus. @@ -218,7 +218,7 @@ assert (cun : cos (7/4) < 0). exact sin_gt_cos_7_8. apply Rlt_le; assumption. apply Rlt_le; apply Rlt_trans with (1 := cvp); exact sin_gt_cos_7_8. -apply IVT; auto; fourier. +apply IVT; auto; lra. Qed. Definition PI2 := proj1_sig PI_2_aux. @@ -270,7 +270,7 @@ Qed. Lemma sin_pos_tech : forall x, 0 < x < 2 -> 0 < sin x. intros x [int1 int2]. assert (lo : 0 <= x) by (apply Rlt_le; assumption). -assert (up : x <= 4) by (apply Rlt_le, Rlt_trans with (1:=int2); fourier). +assert (up : x <= 4) by (apply Rlt_le, Rlt_trans with (1:=int2); lra). destruct (pre_sin_bound _ 0 lo up) as [t _]; clear lo up. apply Rlt_le_trans with (2:= t); clear t. unfold sin_approx; simpl sum_f_R0; unfold sin_term; simpl. @@ -280,13 +280,13 @@ end. assert (t' : x ^ 2 <= 4). replace 4 with (2 ^ 2) by field. apply (pow_incr x 2); split; apply Rlt_le; assumption. -apply Rmult_lt_0_compat;[assumption | fourier ]. +apply Rmult_lt_0_compat;[assumption | lra ]. Qed. Lemma sin_PI2 : sin (PI / 2) = 1. replace (PI / 2) with PI2 by (unfold PI; field). assert (int' : 0 < PI2 < 2). - destruct pi2_int; split; fourier. + destruct pi2_int; split; lra. assert (lo2 := sin_pos_tech PI2 int'). assert (t2 : Rabs (sin PI2) = 1). rewrite <- Rabs_R1; apply Rsqr_eq_abs_0. @@ -295,10 +295,10 @@ revert t2; rewrite Rabs_pos_eq;[| apply Rlt_le]; tauto. Qed. Lemma PI_RGT_0 : PI > 0. -Proof. unfold PI; destruct pi2_int; fourier. Qed. +Proof. unfold PI; destruct pi2_int; lra. Qed. Lemma PI_4 : PI <= 4. -Proof. unfold PI; destruct pi2_int; fourier. Qed. +Proof. unfold PI; destruct pi2_int; lra. Qed. (**********) Lemma PI_neq0 : PI <> 0. @@ -344,13 +344,13 @@ Lemma cos_bound : forall (a : R) (n : nat), - PI / 2 <= a -> a <= PI / 2 -> Proof. intros a n lower upper; apply pre_cos_bound. apply Rle_trans with (2 := lower). - apply Rmult_le_reg_r with 2; [fourier |]. + apply Rmult_le_reg_r with 2; [lra |]. replace ((-PI/2) * 2) with (-PI) by field. - assert (t := PI_4); fourier. + assert (t := PI_4); lra. apply Rle_trans with (1 := upper). -apply Rmult_le_reg_r with 2; [fourier | ]. +apply Rmult_le_reg_r with 2; [lra | ]. replace ((PI/2) * 2) with PI by field. -generalize PI_4; intros; fourier. +generalize PI_4; intros; lra. Qed. (**********) Lemma neg_cos : forall x:R, cos (x + PI) = - cos x. @@ -749,19 +749,19 @@ Qed. Lemma _PI2_RLT_0 : - (PI / 2) < 0. Proof. assert (H := PI_RGT_0). - fourier. + lra. Qed. Lemma PI4_RLT_PI2 : PI / 4 < PI / 2. Proof. assert (H := PI_RGT_0). - fourier. + lra. Qed. Lemma PI2_Rlt_PI : PI / 2 < PI. Proof. assert (H := PI_RGT_0). - fourier. + lra. Qed. (***************************************************) diff --git a/theories/Reals/Rtrigo_calc.v b/theories/Reals/Rtrigo_calc.v index 7cbfc630..78797c87 100644 --- a/theories/Reals/Rtrigo_calc.v +++ b/theories/Reals/Rtrigo_calc.v @@ -205,7 +205,6 @@ Proof with trivial. rewrite cos2; unfold Rsqr; rewrite sin_PI6; rewrite sqrt_def... field. left ; prove_sup0. - discrR. Qed. Lemma tan_PI6 : tan (PI / 6) = 1 / sqrt 3. diff --git a/theories/Strings/Ascii.v b/theories/Strings/Ascii.v index 5154b75b..31a7fb8a 100644 --- a/theories/Strings/Ascii.v +++ b/theories/Strings/Ascii.v @@ -40,6 +40,40 @@ Proof. decide equality; apply bool_dec. Defined. +Local Open Scope lazy_bool_scope. + +Definition eqb (a b : ascii) : bool := + match a, b with + | Ascii a0 a1 a2 a3 a4 a5 a6 a7, + Ascii b0 b1 b2 b3 b4 b5 b6 b7 => + Bool.eqb a0 b0 &&& Bool.eqb a1 b1 &&& Bool.eqb a2 b2 &&& Bool.eqb a3 b3 + &&& Bool.eqb a4 b4 &&& Bool.eqb a5 b5 &&& Bool.eqb a6 b6 &&& Bool.eqb a7 b7 + end. + +Infix "=?" := eqb : char_scope. + +Lemma eqb_spec (a b : ascii) : reflect (a = b) (a =? b)%char. +Proof. + destruct a, b; simpl. + do 8 (case Bool.eqb_spec; [ intros -> | constructor; now intros [= ] ]). + now constructor. +Qed. + +Local Ltac t_eqb := + repeat first [ congruence + | progress subst + | apply conj + | match goal with + | [ |- context[eqb ?x ?y] ] => destruct (eqb_spec x y) + end + | intro ]. +Lemma eqb_refl x : (x =? x)%char = true. Proof. t_eqb. Qed. +Lemma eqb_sym x y : (x =? y)%char = (y =? x)%char. Proof. t_eqb. Qed. +Lemma eqb_eq n m : (n =? m)%char = true <-> n = m. Proof. t_eqb. Qed. +Lemma eqb_neq x y : (x =? y)%char = false <-> x <> y. Proof. t_eqb. Qed. +Lemma eqb_compat: Morphisms.Proper (Morphisms.respectful eq (Morphisms.respectful eq eq)) eqb. +Proof. t_eqb. Qed. + (** * Conversion between natural numbers modulo 256 and ascii characters *) (** Auxiliary function that turns a positive into an ascii by diff --git a/theories/Strings/BinaryString.v b/theories/Strings/BinaryString.v new file mode 100644 index 00000000..6df0a917 --- /dev/null +++ b/theories/Strings/BinaryString.v @@ -0,0 +1,147 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +Require Import Ascii String. +Require Import BinNums. +Import BinNatDef. +Import BinIntDef. +Import BinPosDef. + +Local Open Scope positive_scope. +Local Open Scope string_scope. + +Definition ascii_to_digit (ch : ascii) : option N + := (if ascii_dec ch "0" then Some 0 + else if ascii_dec ch "1" then Some 1 + else None)%N. + +Fixpoint pos_bin_app (p q:positive) : positive := + match q with + | q~0 => (pos_bin_app p q)~0 + | q~1 => (pos_bin_app p q)~1 + | 1 => p~1 + end. + +Module Raw. + Fixpoint of_pos (p : positive) (rest : string) : string + := match p with + | 1 => String "1" rest + | p'~0 => of_pos p' (String "0" rest) + | p'~1 => of_pos p' (String "1" rest) + end. + + Fixpoint to_N (s : string) (rest : N) + : N + := match s with + | "" => rest + | String ch s' + => to_N + s' + match ascii_to_digit ch with + | Some v => N.add v (N.double rest) + | None => N0 + end + end. + + Fixpoint to_N_of_pos (p : positive) (rest : string) (base : N) + : to_N (of_pos p rest) base + = to_N rest match base with + | N0 => N.pos p + | Npos v => Npos (pos_bin_app v p) + end. + Proof. + destruct p as [p|p|]; destruct base; try reflexivity; + cbn; rewrite to_N_of_pos; reflexivity. + Qed. +End Raw. + +Definition of_pos (p : positive) : string + := String "0" (String "b" (Raw.of_pos p "")). +Definition of_N (n : N) : string + := match n with + | N0 => "0b0" + | Npos p => of_pos p + end. +Definition of_Z (z : Z) : string + := match z with + | Zneg p => String "-" (of_pos p) + | Z0 => "0b0" + | Zpos p => of_pos p + end. +Definition of_nat (n : nat) : string + := of_N (N.of_nat n). + +Definition to_N (s : string) : N + := match s with + | String s0 (String sb s) + => if ascii_dec s0 "0" + then if ascii_dec sb "b" + then Raw.to_N s N0 + else N0 + else N0 + | _ => N0 + end. +Definition to_pos (s : string) : positive + := match to_N s with + | N0 => 1 + | Npos p => p + end. +Definition to_Z (s : string) : Z + := let '(is_neg, n) := match s with + | String s0 s' + => if ascii_dec s0 "-" + then (true, to_N s') + else (false, to_N s) + | EmptyString => (false, to_N s) + end in + match n with + | N0 => Z0 + | Npos p => if is_neg then Zneg p else Zpos p + end. +Definition to_nat (s : string) : nat + := N.to_nat (to_N s). + +Lemma to_N_of_N (n : N) + : to_N (of_N n) + = n. +Proof. + destruct n; [ reflexivity | apply Raw.to_N_of_pos ]. +Qed. + +Lemma Z_of_of_Z (z : Z) + : to_Z (of_Z z) + = z. +Proof. + cbv [of_Z to_Z]; destruct z as [|z|z]; cbn; + try reflexivity; + rewrite Raw.to_N_of_pos; cbn; reflexivity. +Qed. + +Lemma to_nat_of_nat (n : nat) + : to_nat (of_nat n) + = n. +Proof. + cbv [to_nat of_nat]; + rewrite to_N_of_N, Nnat.Nat2N.id; reflexivity. +Qed. + +Lemma to_pos_of_pos (p : positive) + : to_pos (of_pos p) + = p. +Proof. + cbv [of_pos to_pos to_N]; cbn; + rewrite Raw.to_N_of_pos; cbn; reflexivity. +Qed. + +Example of_pos_1 : of_pos 1 = "0b1" := eq_refl. +Example of_pos_2 : of_pos 2 = "0b10" := eq_refl. +Example of_pos_3 : of_pos 3 = "0b11" := eq_refl. +Example of_N_0 : of_N 0 = "0b0" := eq_refl. +Example of_Z_0 : of_Z 0 = "0b0" := eq_refl. +Example of_Z_m1 : of_Z (-1) = "-0b1" := eq_refl. +Example of_nat_0 : of_nat 0 = "0b0" := eq_refl. diff --git a/theories/Strings/HexString.v b/theories/Strings/HexString.v new file mode 100644 index 00000000..9ea93c90 --- /dev/null +++ b/theories/Strings/HexString.v @@ -0,0 +1,229 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +Require Import Ascii String. +Require Import BinNums. +Import BinNatDef. +Import BinIntDef. +Import BinPosDef. + +Local Open Scope positive_scope. +Local Open Scope string_scope. + +Local Notation "a || b" + := (if a then true else if b then true else false). +Definition ascii_to_digit (ch : ascii) : option N + := (if ascii_dec ch "0" then Some 0 + else if ascii_dec ch "1" then Some 1 + else if ascii_dec ch "2" then Some 2 + else if ascii_dec ch "3" then Some 3 + else if ascii_dec ch "4" then Some 4 + else if ascii_dec ch "5" then Some 5 + else if ascii_dec ch "6" then Some 6 + else if ascii_dec ch "7" then Some 7 + else if ascii_dec ch "8" then Some 8 + else if ascii_dec ch "9" then Some 9 + else if ascii_dec ch "a" || ascii_dec ch "A" then Some 10 + else if ascii_dec ch "b" || ascii_dec ch "B" then Some 11 + else if ascii_dec ch "c" || ascii_dec ch "C" then Some 12 + else if ascii_dec ch "d" || ascii_dec ch "D" then Some 13 + else if ascii_dec ch "e" || ascii_dec ch "E" then Some 14 + else if ascii_dec ch "f" || ascii_dec ch "F" then Some 15 + else None)%N. + +Fixpoint pos_hex_app (p q:positive) : positive := + match q with + | 1 => p~0~0~0~1 + | 2 => p~0~0~1~0 + | 3 => p~0~0~1~1 + | 4 => p~0~1~0~0 + | 5 => p~0~1~0~1 + | 6 => p~0~1~1~0 + | 7 => p~0~1~1~1 + | 8 => p~1~0~0~0 + | 9 => p~1~0~0~1 + | 10 => p~1~0~1~0 + | 11 => p~1~0~1~1 + | 12 => p~1~1~0~0 + | 13 => p~1~1~0~1 + | 14 => p~1~1~1~0 + | 15 => p~1~1~1~1 + | q~0~0~0~0 => (pos_hex_app p q)~0~0~0~0 + | q~0~0~0~1 => (pos_hex_app p q)~0~0~0~1 + | q~0~0~1~0 => (pos_hex_app p q)~0~0~1~0 + | q~0~0~1~1 => (pos_hex_app p q)~0~0~1~1 + | q~0~1~0~0 => (pos_hex_app p q)~0~1~0~0 + | q~0~1~0~1 => (pos_hex_app p q)~0~1~0~1 + | q~0~1~1~0 => (pos_hex_app p q)~0~1~1~0 + | q~0~1~1~1 => (pos_hex_app p q)~0~1~1~1 + | q~1~0~0~0 => (pos_hex_app p q)~1~0~0~0 + | q~1~0~0~1 => (pos_hex_app p q)~1~0~0~1 + | q~1~0~1~0 => (pos_hex_app p q)~1~0~1~0 + | q~1~0~1~1 => (pos_hex_app p q)~1~0~1~1 + | q~1~1~0~0 => (pos_hex_app p q)~1~1~0~0 + | q~1~1~0~1 => (pos_hex_app p q)~1~1~0~1 + | q~1~1~1~0 => (pos_hex_app p q)~1~1~1~0 + | q~1~1~1~1 => (pos_hex_app p q)~1~1~1~1 + end. + +Module Raw. + Fixpoint of_pos (p : positive) (rest : string) : string + := match p with + | 1 => String "1" rest + | 2 => String "2" rest + | 3 => String "3" rest + | 4 => String "4" rest + | 5 => String "5" rest + | 6 => String "6" rest + | 7 => String "7" rest + | 8 => String "8" rest + | 9 => String "9" rest + | 10 => String "a" rest + | 11 => String "b" rest + | 12 => String "c" rest + | 13 => String "d" rest + | 14 => String "e" rest + | 15 => String "f" rest + | p'~0~0~0~0 => of_pos p' (String "0" rest) + | p'~0~0~0~1 => of_pos p' (String "1" rest) + | p'~0~0~1~0 => of_pos p' (String "2" rest) + | p'~0~0~1~1 => of_pos p' (String "3" rest) + | p'~0~1~0~0 => of_pos p' (String "4" rest) + | p'~0~1~0~1 => of_pos p' (String "5" rest) + | p'~0~1~1~0 => of_pos p' (String "6" rest) + | p'~0~1~1~1 => of_pos p' (String "7" rest) + | p'~1~0~0~0 => of_pos p' (String "8" rest) + | p'~1~0~0~1 => of_pos p' (String "9" rest) + | p'~1~0~1~0 => of_pos p' (String "a" rest) + | p'~1~0~1~1 => of_pos p' (String "b" rest) + | p'~1~1~0~0 => of_pos p' (String "c" rest) + | p'~1~1~0~1 => of_pos p' (String "d" rest) + | p'~1~1~1~0 => of_pos p' (String "e" rest) + | p'~1~1~1~1 => of_pos p' (String "f" rest) + end. + + Fixpoint to_N (s : string) (rest : N) + : N + := match s with + | "" => rest + | String ch s' + => to_N + s' + match ascii_to_digit ch with + | Some v => N.add v (N.mul 16 rest) + | None => N0 + end + end. + + Fixpoint to_N_of_pos (p : positive) (rest : string) (base : N) + : to_N (of_pos p rest) base + = to_N rest match base with + | N0 => N.pos p + | Npos v => Npos (pos_hex_app v p) + end. + Proof. + do 4 try destruct p as [p|p|]; destruct base; try reflexivity; + cbn; rewrite to_N_of_pos; reflexivity. + Qed. +End Raw. + +Definition of_pos (p : positive) : string + := String "0" (String "x" (Raw.of_pos p "")). +Definition of_N (n : N) : string + := match n with + | N0 => "0x0" + | Npos p => of_pos p + end. +Definition of_Z (z : Z) : string + := match z with + | Zneg p => String "-" (of_pos p) + | Z0 => "0x0" + | Zpos p => of_pos p + end. +Definition of_nat (n : nat) : string + := of_N (N.of_nat n). + +Definition to_N (s : string) : N + := match s with + | String s0 (String so s) + => if ascii_dec s0 "0" + then if ascii_dec so "x" + then Raw.to_N s N0 + else N0 + else N0 + | _ => N0 + end. +Definition to_pos (s : string) : positive + := match to_N s with + | N0 => 1 + | Npos p => p + end. +Definition to_Z (s : string) : Z + := let '(is_neg, n) := match s with + | String s0 s' + => if ascii_dec s0 "-" + then (true, to_N s') + else (false, to_N s) + | EmptyString => (false, to_N s) + end in + match n with + | N0 => Z0 + | Npos p => if is_neg then Zneg p else Zpos p + end. +Definition to_nat (s : string) : nat + := N.to_nat (to_N s). + +Lemma to_N_of_N (n : N) + : to_N (of_N n) + = n. +Proof. + destruct n; [ reflexivity | apply Raw.to_N_of_pos ]. +Qed. + +Lemma to_Z_of_Z (z : Z) + : to_Z (of_Z z) + = z. +Proof. + cbv [of_Z to_Z]; destruct z as [|z|z]; cbn; + try reflexivity; + rewrite Raw.to_N_of_pos; cbn; reflexivity. +Qed. + +Lemma to_nat_of_nat (n : nat) + : to_nat (of_nat n) + = n. +Proof. + cbv [to_nat of_nat]; + rewrite to_N_of_N, Nnat.Nat2N.id; reflexivity. +Qed. + +Lemma to_pos_of_pos (p : positive) + : to_pos (of_pos p) + = p. +Proof. + cbv [of_pos to_pos to_N]; cbn; + rewrite Raw.to_N_of_pos; cbn; reflexivity. +Qed. + +Example of_pos_1 : of_pos 1 = "0x1" := eq_refl. +Example of_pos_2 : of_pos 2 = "0x2" := eq_refl. +Example of_pos_3 : of_pos 3 = "0x3" := eq_refl. +Example of_pos_7 : of_pos 7 = "0x7" := eq_refl. +Example of_pos_8 : of_pos 8 = "0x8" := eq_refl. +Example of_pos_9 : of_pos 9 = "0x9" := eq_refl. +Example of_pos_10 : of_pos 10 = "0xa" := eq_refl. +Example of_pos_11 : of_pos 11 = "0xb" := eq_refl. +Example of_pos_12 : of_pos 12 = "0xc" := eq_refl. +Example of_pos_13 : of_pos 13 = "0xd" := eq_refl. +Example of_pos_14 : of_pos 14 = "0xe" := eq_refl. +Example of_pos_15 : of_pos 15 = "0xf" := eq_refl. +Example of_pos_16 : of_pos 16 = "0x10" := eq_refl. +Example of_N_0 : of_N 0 = "0x0" := eq_refl. +Example of_Z_0 : of_Z 0 = "0x0" := eq_refl. +Example of_Z_m1 : of_Z (-1) = "-0x1" := eq_refl. +Example of_nat_0 : of_nat 0 = "0x0" := eq_refl. diff --git a/theories/Strings/OctalString.v b/theories/Strings/OctalString.v new file mode 100644 index 00000000..fe8cc9aa --- /dev/null +++ b/theories/Strings/OctalString.v @@ -0,0 +1,179 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +Require Import Ascii String. +Require Import BinNums. +Import BinNatDef. +Import BinIntDef. +Import BinPosDef. + +Local Open Scope positive_scope. +Local Open Scope string_scope. + +Definition ascii_to_digit (ch : ascii) : option N + := (if ascii_dec ch "0" then Some 0 + else if ascii_dec ch "1" then Some 1 + else if ascii_dec ch "2" then Some 2 + else if ascii_dec ch "3" then Some 3 + else if ascii_dec ch "4" then Some 4 + else if ascii_dec ch "5" then Some 5 + else if ascii_dec ch "6" then Some 6 + else if ascii_dec ch "7" then Some 7 + else None)%N. + +Fixpoint pos_oct_app (p q:positive) : positive := + match q with + | 1 => p~0~0~1 + | 2 => p~0~1~0 + | 3 => p~0~1~1 + | 4 => p~1~0~0 + | 5 => p~1~0~1 + | 6 => p~1~1~0 + | 7 => p~1~1~1 + | q~0~0~0 => (pos_oct_app p q)~0~0~0 + | q~0~0~1 => (pos_oct_app p q)~0~0~1 + | q~0~1~0 => (pos_oct_app p q)~0~1~0 + | q~0~1~1 => (pos_oct_app p q)~0~1~1 + | q~1~0~0 => (pos_oct_app p q)~1~0~0 + | q~1~0~1 => (pos_oct_app p q)~1~0~1 + | q~1~1~0 => (pos_oct_app p q)~1~1~0 + | q~1~1~1 => (pos_oct_app p q)~1~1~1 + end. + +Module Raw. + Fixpoint of_pos (p : positive) (rest : string) : string + := match p with + | 1 => String "1" rest + | 2 => String "2" rest + | 3 => String "3" rest + | 4 => String "4" rest + | 5 => String "5" rest + | 6 => String "6" rest + | 7 => String "7" rest + | p'~0~0~0 => of_pos p' (String "0" rest) + | p'~0~0~1 => of_pos p' (String "1" rest) + | p'~0~1~0 => of_pos p' (String "2" rest) + | p'~0~1~1 => of_pos p' (String "3" rest) + | p'~1~0~0 => of_pos p' (String "4" rest) + | p'~1~0~1 => of_pos p' (String "5" rest) + | p'~1~1~0 => of_pos p' (String "6" rest) + | p'~1~1~1 => of_pos p' (String "7" rest) + end. + + Fixpoint to_N (s : string) (rest : N) + : N + := match s with + | "" => rest + | String ch s' + => to_N + s' + match ascii_to_digit ch with + | Some v => N.add v (N.mul 8 rest) + | None => N0 + end + end. + + Fixpoint to_N_of_pos (p : positive) (rest : string) (base : N) + : to_N (of_pos p rest) base + = to_N rest match base with + | N0 => N.pos p + | Npos v => Npos (pos_oct_app v p) + end. + Proof. + do 3 try destruct p as [p|p|]; destruct base; try reflexivity; + cbn; rewrite to_N_of_pos; reflexivity. + Qed. +End Raw. + +Definition of_pos (p : positive) : string + := String "0" (String "o" (Raw.of_pos p "")). +Definition of_N (n : N) : string + := match n with + | N0 => "0o0" + | Npos p => of_pos p + end. +Definition of_Z (z : Z) : string + := match z with + | Zneg p => String "-" (of_pos p) + | Z0 => "0o0" + | Zpos p => of_pos p + end. +Definition of_nat (n : nat) : string + := of_N (N.of_nat n). + +Definition to_N (s : string) : N + := match s with + | String s0 (String so s) + => if ascii_dec s0 "0" + then if ascii_dec so "o" + then Raw.to_N s N0 + else N0 + else N0 + | _ => N0 + end. +Definition to_pos (s : string) : positive + := match to_N s with + | N0 => 1 + | Npos p => p + end. +Definition to_Z (s : string) : Z + := let '(is_neg, n) := match s with + | String s0 s' + => if ascii_dec s0 "-" + then (true, to_N s') + else (false, to_N s) + | EmptyString => (false, to_N s) + end in + match n with + | N0 => Z0 + | Npos p => if is_neg then Zneg p else Zpos p + end. +Definition to_nat (s : string) : nat + := N.to_nat (to_N s). + +Lemma to_N_of_N (n : N) + : to_N (of_N n) + = n. +Proof. + destruct n; [ reflexivity | apply Raw.to_N_of_pos ]. +Qed. + +Lemma to_Z_of_Z (z : Z) + : to_Z (of_Z z) + = z. +Proof. + cbv [of_Z to_Z]; destruct z as [|z|z]; cbn; + try reflexivity; + rewrite Raw.to_N_of_pos; cbn; reflexivity. +Qed. + +Lemma to_nat_of_nat (n : nat) + : to_nat (of_nat n) + = n. +Proof. + cbv [to_nat of_nat]; + rewrite to_N_of_N, Nnat.Nat2N.id; reflexivity. +Qed. + +Lemma to_pos_of_pos (p : positive) + : to_pos (of_pos p) + = p. +Proof. + cbv [of_pos to_pos to_N]; cbn; + rewrite Raw.to_N_of_pos; cbn; reflexivity. +Qed. + +Example of_pos_1 : of_pos 1 = "0o1" := eq_refl. +Example of_pos_2 : of_pos 2 = "0o2" := eq_refl. +Example of_pos_3 : of_pos 3 = "0o3" := eq_refl. +Example of_pos_7 : of_pos 7 = "0o7" := eq_refl. +Example of_pos_8 : of_pos 8 = "0o10" := eq_refl. +Example of_N_0 : of_N 0 = "0o0" := eq_refl. +Example of_Z_0 : of_Z 0 = "0o0" := eq_refl. +Example of_Z_m1 : of_Z (-1) = "-0o1" := eq_refl. +Example of_nat_0 : of_nat 0 = "0o0" := eq_refl. diff --git a/theories/Strings/String.v b/theories/Strings/String.v index 2be6618a..be9a10c6 100644 --- a/theories/Strings/String.v +++ b/theories/Strings/String.v @@ -14,6 +14,7 @@ Require Import Arith. Require Import Ascii. +Require Import Bool. Declare ML Module "string_syntax_plugin". (** *** Definition of strings *) @@ -35,6 +36,39 @@ Proof. decide equality; apply ascii_dec. Defined. +Local Open Scope lazy_bool_scope. + +Fixpoint eqb s1 s2 : bool := + match s1, s2 with + | EmptyString, EmptyString => true + | String c1 s1', String c2 s2' => Ascii.eqb c1 c2 &&& eqb s1' s2' + | _,_ => false + end. + +Infix "=?" := eqb : string_scope. + +Lemma eqb_spec s1 s2 : Bool.reflect (s1 = s2) (s1 =? s2)%string. +Proof. + revert s2. induction s1; destruct s2; try (constructor; easy); simpl. + case Ascii.eqb_spec; simpl; [intros -> | constructor; now intros [= ]]. + case IHs1; [intros ->; now constructor | constructor; now intros [= ]]. +Qed. + +Local Ltac t_eqb := + repeat first [ congruence + | progress subst + | apply conj + | match goal with + | [ |- context[eqb ?x ?y] ] => destruct (eqb_spec x y) + end + | intro ]. +Lemma eqb_refl x : (x =? x)%string = true. Proof. t_eqb. Qed. +Lemma eqb_sym x y : (x =? y)%string = (y =? x)%string. Proof. t_eqb. Qed. +Lemma eqb_eq n m : (n =? m)%string = true <-> n = m. Proof. t_eqb. Qed. +Lemma eqb_neq x y : (x =? y)%string = false <-> x <> y. Proof. t_eqb. Qed. +Lemma eqb_compat: Morphisms.Proper (Morphisms.respectful eq (Morphisms.respectful eq eq)) eqb. +Proof. t_eqb. Qed. + (** *** Concatenation of strings *) Reserved Notation "x ++ y" (right associativity, at level 60). diff --git a/theories/Structures/GenericMinMax.v b/theories/Structures/GenericMinMax.v index 05edc6cc..4d04667c 100644 --- a/theories/Structures/GenericMinMax.v +++ b/theories/Structures/GenericMinMax.v @@ -83,7 +83,7 @@ End GenericMinMax. Module MinMaxLogicalProperties (Import O:TotalOrder')(Import M:HasMinMax O). Module Import Private_Tac := !MakeOrderTac O O. -(** An alternative caracterisation of [max], equivalent to +(** An alternative characterisation of [max], equivalent to [max_l /\ max_r] *) Lemma max_spec n m : diff --git a/theories/Unicode/Utf8_core.v b/theories/Unicode/Utf8_core.v index 5a8931a8..d4cdb064 100644 --- a/theories/Unicode/Utf8_core.v +++ b/theories/Unicode/Utf8_core.v @@ -14,10 +14,10 @@ (* Logic *) Notation "∀ x .. y , P" := (forall x, .. (forall y, P) ..) (at level 200, x binder, y binder, right associativity, - format "'[ ' ∀ x .. y ']' , P") : type_scope. + format "'[ ' '[ ' ∀ x .. y ']' , '/' P ']'") : type_scope. Notation "∃ x .. y , P" := (exists x, .. (exists y, P) ..) (at level 200, x binder, y binder, right associativity, - format "'[ ' ∃ x .. y ']' , P") : type_scope. + format "'[ ' '[ ' ∃ x .. y ']' , '/' P ']'") : type_scope. Notation "x ∨ y" := (x \/ y) (at level 85, right associativity) : type_scope. Notation "x ∧ y" := (x /\ y) (at level 80, right associativity) : type_scope. @@ -31,4 +31,4 @@ Notation "x ≠ y" := (x <> y) (at level 70) : type_scope. (* Abstraction *) Notation "'λ' x .. y , t" := (fun x => .. (fun y => t) ..) (at level 200, x binder, y binder, right associativity, - format "'[ ' 'λ' x .. y ']' , t"). + format "'[ ' '[ ' 'λ' x .. y ']' , '/' t ']'"). diff --git a/theories/Vectors/VectorDef.v b/theories/Vectors/VectorDef.v index f6f3cafa..ba3e4110 100644 --- a/theories/Vectors/VectorDef.v +++ b/theories/Vectors/VectorDef.v @@ -312,5 +312,6 @@ Notation "h :: t" := (h :: t) (at level 60, right associativity) Notation "[ x ]" := (x :: []) : vector_scope. Notation "[ x ; y ; .. ; z ]" := (cons _ x _ (cons _ y _ .. (cons _ z _ (nil _)) ..)) : vector_scope. Notation "v [@ p ]" := (nth v p) (at level 1, format "v [@ p ]") : vector_scope. +Infix "++" := append : vector_scope. Open Scope vector_scope. End VectorNotations. diff --git a/theories/ZArith/BinInt.v b/theories/ZArith/BinInt.v index cf7397b5..12413453 100644 --- a/theories/ZArith/BinInt.v +++ b/theories/ZArith/BinInt.v @@ -1248,6 +1248,8 @@ Bind Scope Z_scope with Z.t Z. (** Re-export Notations *) +Numeral Notation Z Z.of_int Z.to_int : Z_scope. + Infix "+" := Z.add : Z_scope. Notation "- x" := (Z.opp x) : Z_scope. Infix "-" := Z.sub : Z_scope. @@ -1569,40 +1571,40 @@ End Z2Pos. Notation Zdouble_plus_one := Z.succ_double (only parsing). Notation Zdouble_minus_one := Z.pred_double (only parsing). -Notation Zdouble := Z.double (compat "8.6"). +Notation Zdouble := Z.double (compat "8.7"). Notation ZPminus := Z.pos_sub (only parsing). -Notation Zsucc' := Z.succ (compat "8.6"). -Notation Zpred' := Z.pred (compat "8.6"). -Notation Zplus' := Z.add (compat "8.6"). +Notation Zsucc' := Z.succ (compat "8.7"). +Notation Zpred' := Z.pred (compat "8.7"). +Notation Zplus' := Z.add (compat "8.7"). Notation Zplus := Z.add (only parsing). (* Slightly incompatible *) -Notation Zopp := Z.opp (compat "8.6"). -Notation Zsucc := Z.succ (compat "8.6"). -Notation Zpred := Z.pred (compat "8.6"). +Notation Zopp := Z.opp (compat "8.7"). +Notation Zsucc := Z.succ (compat "8.7"). +Notation Zpred := Z.pred (compat "8.7"). Notation Zminus := Z.sub (only parsing). Notation Zmult := Z.mul (only parsing). -Notation Zcompare := Z.compare (compat "8.6"). -Notation Zsgn := Z.sgn (compat "8.6"). -Notation Zle := Z.le (compat "8.6"). -Notation Zge := Z.ge (compat "8.6"). -Notation Zlt := Z.lt (compat "8.6"). -Notation Zgt := Z.gt (compat "8.6"). -Notation Zmax := Z.max (compat "8.6"). -Notation Zmin := Z.min (compat "8.6"). -Notation Zabs := Z.abs (compat "8.6"). -Notation Zabs_nat := Z.abs_nat (compat "8.6"). -Notation Zabs_N := Z.abs_N (compat "8.6"). +Notation Zcompare := Z.compare (compat "8.7"). +Notation Zsgn := Z.sgn (compat "8.7"). +Notation Zle := Z.le (compat "8.7"). +Notation Zge := Z.ge (compat "8.7"). +Notation Zlt := Z.lt (compat "8.7"). +Notation Zgt := Z.gt (compat "8.7"). +Notation Zmax := Z.max (compat "8.7"). +Notation Zmin := Z.min (compat "8.7"). +Notation Zabs := Z.abs (compat "8.7"). +Notation Zabs_nat := Z.abs_nat (compat "8.7"). +Notation Zabs_N := Z.abs_N (compat "8.7"). Notation Z_of_nat := Z.of_nat (only parsing). Notation Z_of_N := Z.of_N (only parsing). Notation Zind := Z.peano_ind (only parsing). -Notation Zopp_0 := Z.opp_0 (compat "8.6"). -Notation Zopp_involutive := Z.opp_involutive (compat "8.6"). -Notation Zopp_inj := Z.opp_inj (compat "8.6"). +Notation Zopp_0 := Z.opp_0 (compat "8.7"). +Notation Zopp_involutive := Z.opp_involutive (compat "8.7"). +Notation Zopp_inj := Z.opp_inj (compat "8.7"). Notation Zplus_0_l := Z.add_0_l (only parsing). Notation Zplus_0_r := Z.add_0_r (only parsing). Notation Zplus_comm := Z.add_comm (only parsing). Notation Zopp_plus_distr := Z.opp_add_distr (only parsing). -Notation Zopp_succ := Z.opp_succ (compat "8.6"). +Notation Zopp_succ := Z.opp_succ (compat "8.7"). Notation Zplus_opp_r := Z.add_opp_diag_r (only parsing). Notation Zplus_opp_l := Z.add_opp_diag_l (only parsing). Notation Zplus_assoc := Z.add_assoc (only parsing). @@ -1611,11 +1613,11 @@ Notation Zplus_reg_l := Z.add_reg_l (only parsing). Notation Zplus_succ_l := Z.add_succ_l (only parsing). Notation Zplus_succ_comm := Z.add_succ_comm (only parsing). Notation Zsucc_discr := Z.neq_succ_diag_r (only parsing). -Notation Zsucc_inj := Z.succ_inj (compat "8.6"). -Notation Zsucc'_inj := Z.succ_inj (compat "8.6"). -Notation Zsucc'_pred' := Z.succ_pred (compat "8.6"). -Notation Zpred'_succ' := Z.pred_succ (compat "8.6"). -Notation Zpred'_inj := Z.pred_inj (compat "8.6"). +Notation Zsucc_inj := Z.succ_inj (compat "8.7"). +Notation Zsucc'_inj := Z.succ_inj (compat "8.7"). +Notation Zsucc'_pred' := Z.succ_pred (compat "8.7"). +Notation Zpred'_succ' := Z.pred_succ (compat "8.7"). +Notation Zpred'_inj := Z.pred_inj (compat "8.7"). Notation Zsucc'_discr := Z.neq_succ_diag_r (only parsing). Notation Zminus_0_r := Z.sub_0_r (only parsing). Notation Zminus_diag := Z.sub_diag (only parsing). diff --git a/theories/ZArith/BinIntDef.v b/theories/ZArith/BinIntDef.v index db4de0b9..8cb62622 100644 --- a/theories/ZArith/BinIntDef.v +++ b/theories/ZArith/BinIntDef.v @@ -14,6 +14,10 @@ Require Import BinPos BinNat. Local Open Scope Z_scope. +Local Notation "0" := Z0. +Local Notation "1" := (Zpos 1). +Local Notation "2" := (Zpos 2). + (***********************************************************) (** * Binary Integers, Definitions of Operations *) (***********************************************************) @@ -53,7 +57,7 @@ Definition succ_double x := Definition pred_double x := match x with - | 0 => -1 + | 0 => neg 1 | neg p => neg p~1 | pos p => pos (Pos.pred_double p) end. @@ -104,7 +108,7 @@ Definition succ x := x + 1. (** ** Predecessor *) -Definition pred x := x + -1. +Definition pred x := x + neg 1. (** ** Subtraction *) @@ -171,7 +175,7 @@ Definition sgn z := match z with | 0 => 0 | pos p => 1 - | neg p => -1 + | neg p => neg 1 end. (** Boolean equality and comparisons *) @@ -635,4 +639,9 @@ Definition lxor a b := | neg a, neg b => of_N (N.lxor (Pos.pred_N a) (Pos.pred_N b)) end. +Numeral Notation Z of_int to_int : Z_scope. + End Z. + +(** Re-export the notation for those who just [Import BinIntDef] *) +Numeral Notation Z Z.of_int Z.to_int : Z_scope. diff --git a/theories/ZArith/ZArith_dec.v b/theories/ZArith/ZArith_dec.v index 9bcdb73a..6cadf30f 100644 --- a/theories/ZArith/ZArith_dec.v +++ b/theories/ZArith/ZArith_dec.v @@ -34,7 +34,7 @@ Lemma Zcompare_rec (P:Set) (n m:Z) : ((n ?= m) = Eq -> P) -> ((n ?= m) = Lt -> P) -> ((n ?= m) = Gt -> P) -> P. Proof. apply Zcompare_rect. Defined. -Notation Z_eq_dec := Z.eq_dec (compat "8.6"). +Notation Z_eq_dec := Z.eq_dec (compat "8.7"). Section decidability. diff --git a/theories/ZArith/Zabs.v b/theories/ZArith/Zabs.v index 0d8450e3..057eb499 100644 --- a/theories/ZArith/Zabs.v +++ b/theories/ZArith/Zabs.v @@ -29,17 +29,17 @@ Local Open Scope Z_scope. (**********************************************************************) (** * Properties of absolute value *) -Notation Zabs_eq := Z.abs_eq (compat "8.6"). +Notation Zabs_eq := Z.abs_eq (compat "8.7"). Notation Zabs_non_eq := Z.abs_neq (only parsing). Notation Zabs_Zopp := Z.abs_opp (only parsing). Notation Zabs_pos := Z.abs_nonneg (only parsing). -Notation Zabs_involutive := Z.abs_involutive (compat "8.6"). +Notation Zabs_involutive := Z.abs_involutive (compat "8.7"). Notation Zabs_eq_case := Z.abs_eq_cases (only parsing). -Notation Zabs_triangle := Z.abs_triangle (compat "8.6"). +Notation Zabs_triangle := Z.abs_triangle (compat "8.7"). Notation Zsgn_Zabs := Z.sgn_abs (only parsing). Notation Zabs_Zsgn := Z.abs_sgn (only parsing). Notation Zabs_Zmult := Z.abs_mul (only parsing). -Notation Zabs_square := Z.abs_square (compat "8.6"). +Notation Zabs_square := Z.abs_square (compat "8.7"). (** * Proving a property of the absolute value by cases *) diff --git a/theories/ZArith/Zcompare.v b/theories/ZArith/Zcompare.v index c8432e27..6ccb0153 100644 --- a/theories/ZArith/Zcompare.v +++ b/theories/ZArith/Zcompare.v @@ -183,15 +183,15 @@ Qed. (** Compatibility notations *) -Notation Zcompare_refl := Z.compare_refl (compat "8.6"). +Notation Zcompare_refl := Z.compare_refl (compat "8.7"). Notation Zcompare_Eq_eq := Z.compare_eq (only parsing). Notation Zcompare_Eq_iff_eq := Z.compare_eq_iff (only parsing). -Notation Zcompare_spec := Z.compare_spec (compat "8.6"). -Notation Zmin_l := Z.min_l (compat "8.6"). -Notation Zmin_r := Z.min_r (compat "8.6"). -Notation Zmax_l := Z.max_l (compat "8.6"). -Notation Zmax_r := Z.max_r (compat "8.6"). -Notation Zabs_eq := Z.abs_eq (compat "8.6"). +Notation Zcompare_spec := Z.compare_spec (compat "8.7"). +Notation Zmin_l := Z.min_l (compat "8.7"). +Notation Zmin_r := Z.min_r (compat "8.7"). +Notation Zmax_l := Z.max_l (compat "8.7"). +Notation Zmax_r := Z.max_r (compat "8.7"). +Notation Zabs_eq := Z.abs_eq (compat "8.7"). Notation Zabs_non_eq := Z.abs_neq (only parsing). Notation Zsgn_0 := Z.sgn_null (only parsing). Notation Zsgn_1 := Z.sgn_pos (only parsing). diff --git a/theories/ZArith/Zdiv.v b/theories/ZArith/Zdiv.v index 15d0e487..74614e11 100644 --- a/theories/ZArith/Zdiv.v +++ b/theories/ZArith/Zdiv.v @@ -21,11 +21,11 @@ Local Open Scope Z_scope. specifications and properties are in [BinInt]. *) Notation Zdiv_eucl_POS := Z.pos_div_eucl (only parsing). -Notation Zdiv_eucl := Z.div_eucl (compat "8.6"). -Notation Zdiv := Z.div (compat "8.6"). +Notation Zdiv_eucl := Z.div_eucl (compat "8.7"). +Notation Zdiv := Z.div (compat "8.7"). Notation Zmod := Z.modulo (only parsing). -Notation Zdiv_eucl_eq := Z.div_eucl_eq (compat "8.6"). +Notation Zdiv_eucl_eq := Z.div_eucl_eq (compat "8.7"). Notation Z_div_mod_eq_full := Z.div_mod (only parsing). Notation Zmod_POS_bound := Z.pos_div_eucl_bound (only parsing). Notation Zmod_pos_bound := Z.mod_pos_bound (only parsing). diff --git a/theories/ZArith/Zeven.v b/theories/ZArith/Zeven.v index 00a58b51..9e83bfc1 100644 --- a/theories/ZArith/Zeven.v +++ b/theories/ZArith/Zeven.v @@ -141,8 +141,8 @@ Notation Zodd_bool_pred := Z.odd_pred (only parsing). (** * Definition of [Z.quot2], [Z.div2] and properties wrt [Zeven] and [Zodd] *) -Notation Zdiv2 := Z.div2 (compat "8.6"). -Notation Zquot2 := Z.quot2 (compat "8.6"). +Notation Zdiv2 := Z.div2 (compat "8.7"). +Notation Zquot2 := Z.quot2 (compat "8.7"). (** Properties of [Z.div2] *) diff --git a/theories/ZArith/Zmax.v b/theories/ZArith/Zmax.v index 7f595fcf..26bd9e81 100644 --- a/theories/ZArith/Zmax.v +++ b/theories/ZArith/Zmax.v @@ -18,22 +18,22 @@ Local Open Scope Z_scope. (** Exact compatibility *) -Notation Zmax_case := Z.max_case (compat "8.6"). -Notation Zmax_case_strong := Z.max_case_strong (compat "8.6"). +Notation Zmax_case := Z.max_case (compat "8.7"). +Notation Zmax_case_strong := Z.max_case_strong (compat "8.7"). Notation Zmax_right := Z.max_r (only parsing). -Notation Zle_max_l := Z.le_max_l (compat "8.6"). -Notation Zle_max_r := Z.le_max_r (compat "8.6"). -Notation Zmax_lub := Z.max_lub (compat "8.6"). -Notation Zmax_lub_lt := Z.max_lub_lt (compat "8.6"). +Notation Zle_max_l := Z.le_max_l (compat "8.7"). +Notation Zle_max_r := Z.le_max_r (compat "8.7"). +Notation Zmax_lub := Z.max_lub (compat "8.7"). +Notation Zmax_lub_lt := Z.max_lub_lt (compat "8.7"). Notation Zle_max_compat_r := Z.max_le_compat_r (only parsing). Notation Zle_max_compat_l := Z.max_le_compat_l (only parsing). Notation Zmax_idempotent := Z.max_id (only parsing). Notation Zmax_n_n := Z.max_id (only parsing). -Notation Zmax_comm := Z.max_comm (compat "8.6"). -Notation Zmax_assoc := Z.max_assoc (compat "8.6"). +Notation Zmax_comm := Z.max_comm (compat "8.7"). +Notation Zmax_assoc := Z.max_assoc (compat "8.7"). Notation Zmax_irreducible_dec := Z.max_dec (only parsing). Notation Zmax_le_prime := Z.max_le (only parsing). -Notation Zsucc_max_distr := Z.succ_max_distr (compat "8.6"). +Notation Zsucc_max_distr := Z.succ_max_distr (compat "8.7"). Notation Zmax_SS := Z.succ_max_distr (only parsing). Notation Zplus_max_distr_l := Z.add_max_distr_l (only parsing). Notation Zplus_max_distr_r := Z.add_max_distr_r (only parsing). diff --git a/theories/ZArith/Zmin.v b/theories/ZArith/Zmin.v index 6bc72227..5509ee78 100644 --- a/theories/ZArith/Zmin.v +++ b/theories/ZArith/Zmin.v @@ -18,20 +18,20 @@ Local Open Scope Z_scope. (** Exact compatibility *) -Notation Zmin_case := Z.min_case (compat "8.6"). -Notation Zmin_case_strong := Z.min_case_strong (compat "8.6"). -Notation Zle_min_l := Z.le_min_l (compat "8.6"). -Notation Zle_min_r := Z.le_min_r (compat "8.6"). -Notation Zmin_glb := Z.min_glb (compat "8.6"). -Notation Zmin_glb_lt := Z.min_glb_lt (compat "8.6"). +Notation Zmin_case := Z.min_case (compat "8.7"). +Notation Zmin_case_strong := Z.min_case_strong (compat "8.7"). +Notation Zle_min_l := Z.le_min_l (compat "8.7"). +Notation Zle_min_r := Z.le_min_r (compat "8.7"). +Notation Zmin_glb := Z.min_glb (compat "8.7"). +Notation Zmin_glb_lt := Z.min_glb_lt (compat "8.7"). Notation Zle_min_compat_r := Z.min_le_compat_r (only parsing). Notation Zle_min_compat_l := Z.min_le_compat_l (only parsing). Notation Zmin_idempotent := Z.min_id (only parsing). Notation Zmin_n_n := Z.min_id (only parsing). -Notation Zmin_comm := Z.min_comm (compat "8.6"). -Notation Zmin_assoc := Z.min_assoc (compat "8.6"). +Notation Zmin_comm := Z.min_comm (compat "8.7"). +Notation Zmin_assoc := Z.min_assoc (compat "8.7"). Notation Zmin_irreducible_inf := Z.min_dec (only parsing). -Notation Zsucc_min_distr := Z.succ_min_distr (compat "8.6"). +Notation Zsucc_min_distr := Z.succ_min_distr (compat "8.7"). Notation Zmin_SS := Z.succ_min_distr (only parsing). Notation Zplus_min_distr_r := Z.add_min_distr_r (only parsing). Notation Zmin_plus := Z.add_min_distr_r (only parsing). diff --git a/theories/ZArith/Znumtheory.v b/theories/ZArith/Znumtheory.v index f5444c31..e6066d53 100644 --- a/theories/ZArith/Znumtheory.v +++ b/theories/ZArith/Znumtheory.v @@ -27,20 +27,20 @@ Open Scope Z_scope. - properties of the efficient [Z.gcd] function *) -Notation Zgcd := Z.gcd (compat "8.6"). -Notation Zggcd := Z.ggcd (compat "8.6"). -Notation Zggcd_gcd := Z.ggcd_gcd (compat "8.6"). -Notation Zggcd_correct_divisors := Z.ggcd_correct_divisors (compat "8.6"). -Notation Zgcd_divide_l := Z.gcd_divide_l (compat "8.6"). -Notation Zgcd_divide_r := Z.gcd_divide_r (compat "8.6"). -Notation Zgcd_greatest := Z.gcd_greatest (compat "8.6"). -Notation Zgcd_nonneg := Z.gcd_nonneg (compat "8.6"). -Notation Zggcd_opp := Z.ggcd_opp (compat "8.6"). +Notation Zgcd := Z.gcd (compat "8.7"). +Notation Zggcd := Z.ggcd (compat "8.7"). +Notation Zggcd_gcd := Z.ggcd_gcd (compat "8.7"). +Notation Zggcd_correct_divisors := Z.ggcd_correct_divisors (compat "8.7"). +Notation Zgcd_divide_l := Z.gcd_divide_l (compat "8.7"). +Notation Zgcd_divide_r := Z.gcd_divide_r (compat "8.7"). +Notation Zgcd_greatest := Z.gcd_greatest (compat "8.7"). +Notation Zgcd_nonneg := Z.gcd_nonneg (compat "8.7"). +Notation Zggcd_opp := Z.ggcd_opp (compat "8.7"). (** The former specialized inductive predicate [Z.divide] is now a generic existential predicate. *) -Notation Zdivide := Z.divide (compat "8.6"). +Notation Zdivide := Z.divide (compat "8.7"). (** Its former constructor is now a pseudo-constructor. *) @@ -48,7 +48,7 @@ Definition Zdivide_intro a b q (H:b=q*a) : Z.divide a b := ex_intro _ q H. (** Results concerning divisibility*) -Notation Zdivide_refl := Z.divide_refl (compat "8.6"). +Notation Zdivide_refl := Z.divide_refl (compat "8.7"). Notation Zone_divide := Z.divide_1_l (only parsing). Notation Zdivide_0 := Z.divide_0_r (only parsing). Notation Zmult_divide_compat_l := Z.mul_divide_mono_l (only parsing). @@ -97,8 +97,8 @@ Notation Zdivide_1 := Z.divide_1_r (only parsing). (** If [a] divides [b] and [b] divides [a] then [a] is [b] or [-b]. *) -Notation Zdivide_antisym := Z.divide_antisym (compat "8.6"). -Notation Zdivide_trans := Z.divide_trans (compat "8.6"). +Notation Zdivide_antisym := Z.divide_antisym (compat "8.7"). +Notation Zdivide_trans := Z.divide_trans (compat "8.7"). (** If [a] divides [b] and [b<>0] then [|a| <= |b|]. *) @@ -800,7 +800,7 @@ Proof. rewrite <- Zdivide_Zdiv_eq; auto. Qed. -Notation Zgcd_comm := Z.gcd_comm (compat "8.6"). +Notation Zgcd_comm := Z.gcd_comm (compat "8.7"). Lemma Zgcd_ass a b c : Z.gcd (Z.gcd a b) c = Z.gcd a (Z.gcd b c). Proof. diff --git a/theories/ZArith/Zorder.v b/theories/ZArith/Zorder.v index a1ec4b35..208e84ae 100644 --- a/theories/ZArith/Zorder.v +++ b/theories/ZArith/Zorder.v @@ -66,10 +66,10 @@ Qed. (** * Relating strict and large orders *) -Notation Zgt_lt := Z.gt_lt (compat "8.6"). -Notation Zlt_gt := Z.lt_gt (compat "8.6"). -Notation Zge_le := Z.ge_le (compat "8.6"). -Notation Zle_ge := Z.le_ge (compat "8.6"). +Notation Zgt_lt := Z.gt_lt (compat "8.7"). +Notation Zlt_gt := Z.lt_gt (compat "8.7"). +Notation Zge_le := Z.ge_le (compat "8.7"). +Notation Zle_ge := Z.le_ge (compat "8.7"). Notation Zgt_iff_lt := Z.gt_lt_iff (only parsing). Notation Zge_iff_le := Z.ge_le_iff (only parsing). @@ -123,7 +123,7 @@ Qed. (** Reflexivity *) -Notation Zle_refl := Z.le_refl (compat "8.6"). +Notation Zle_refl := Z.le_refl (compat "8.7"). Notation Zeq_le := Z.eq_le_incl (only parsing). Hint Resolve Z.le_refl: zarith. @@ -143,7 +143,7 @@ Qed. (** Irreflexivity *) -Notation Zlt_irrefl := Z.lt_irrefl (compat "8.6"). +Notation Zlt_irrefl := Z.lt_irrefl (compat "8.7"). Notation Zlt_not_eq := Z.lt_neq (only parsing). Lemma Zgt_irrefl n : ~ n > n. @@ -167,7 +167,7 @@ Notation Zle_or_lt := Z.le_gt_cases (only parsing). (** Transitivity of strict orders *) -Notation Zlt_trans := Z.lt_trans (compat "8.6"). +Notation Zlt_trans := Z.lt_trans (compat "8.7"). Lemma Zgt_trans n m p : n > m -> m > p -> n > p. Proof. @@ -176,8 +176,8 @@ Qed. (** Mixed transitivity *) -Notation Zlt_le_trans := Z.lt_le_trans (compat "8.6"). -Notation Zle_lt_trans := Z.le_lt_trans (compat "8.6"). +Notation Zlt_le_trans := Z.lt_le_trans (compat "8.7"). +Notation Zle_lt_trans := Z.le_lt_trans (compat "8.7"). Lemma Zle_gt_trans n m p : m <= n -> m > p -> n > p. Proof. @@ -191,7 +191,7 @@ Qed. (** Transitivity of large orders *) -Notation Zle_trans := Z.le_trans (compat "8.6"). +Notation Zle_trans := Z.le_trans (compat "8.7"). Lemma Zge_trans n m p : n >= m -> m >= p -> n >= p. Proof. @@ -257,8 +257,8 @@ Qed. (** Relating strict and large order using successor or predecessor *) -Notation Zlt_succ_r := Z.lt_succ_r (compat "8.6"). -Notation Zle_succ_l := Z.le_succ_l (compat "8.6"). +Notation Zlt_succ_r := Z.lt_succ_r (compat "8.7"). +Notation Zle_succ_l := Z.le_succ_l (compat "8.7"). Lemma Zgt_le_succ n m : m > n -> Z.succ n <= m. Proof. @@ -336,8 +336,8 @@ Qed. (** Special cases of ordered integers *) -Notation Zlt_0_1 := Z.lt_0_1 (compat "8.6"). -Notation Zle_0_1 := Z.le_0_1 (compat "8.6"). +Notation Zlt_0_1 := Z.lt_0_1 (compat "8.7"). +Notation Zle_0_1 := Z.le_0_1 (compat "8.7"). Lemma Zle_neg_pos : forall p q:positive, Zneg p <= Zpos q. Proof. diff --git a/theories/ZArith/Zpow_facts.v b/theories/ZArith/Zpow_facts.v index a9bc5bd0..881ead1c 100644 --- a/theories/ZArith/Zpow_facts.v +++ b/theories/ZArith/Zpow_facts.v @@ -233,7 +233,7 @@ Qed. (** * Z.square: a direct definition of [z^2] *) -Notation Psquare := Pos.square (compat "8.6"). -Notation Zsquare := Z.square (compat "8.6"). +Notation Psquare := Pos.square (compat "8.7"). +Notation Zsquare := Z.square (compat "8.7"). Notation Psquare_correct := Pos.square_spec (only parsing). Notation Zsquare_correct := Z.square_spec (only parsing). diff --git a/theories/ZArith/Zquot.v b/theories/ZArith/Zquot.v index e93ebb1a..264109dc 100644 --- a/theories/ZArith/Zquot.v +++ b/theories/ZArith/Zquot.v @@ -8,7 +8,7 @@ (* * (see LICENSE file for the text of the license) *) (************************************************************************) -Require Import Nnat ZArith_base ROmega ZArithRing Zdiv Morphisms. +Require Import Nnat ZArith_base Lia ZArithRing Zdiv Morphisms. Local Open Scope Z_scope. @@ -37,17 +37,17 @@ Notation Ndiv_Zquot := N2Z.inj_quot (only parsing). Notation Nmod_Zrem := N2Z.inj_rem (only parsing). Notation Z_quot_rem_eq := Z.quot_rem' (only parsing). Notation Zrem_lt := Z.rem_bound_abs (only parsing). -Notation Zquot_unique := Z.quot_unique (compat "8.6"). -Notation Zrem_unique := Z.rem_unique (compat "8.6"). -Notation Zrem_1_r := Z.rem_1_r (compat "8.6"). -Notation Zquot_1_r := Z.quot_1_r (compat "8.6"). -Notation Zrem_1_l := Z.rem_1_l (compat "8.6"). -Notation Zquot_1_l := Z.quot_1_l (compat "8.6"). -Notation Z_quot_same := Z.quot_same (compat "8.6"). +Notation Zquot_unique := Z.quot_unique (compat "8.7"). +Notation Zrem_unique := Z.rem_unique (compat "8.7"). +Notation Zrem_1_r := Z.rem_1_r (compat "8.7"). +Notation Zquot_1_r := Z.quot_1_r (compat "8.7"). +Notation Zrem_1_l := Z.rem_1_l (compat "8.7"). +Notation Zquot_1_l := Z.quot_1_l (compat "8.7"). +Notation Z_quot_same := Z.quot_same (compat "8.7"). Notation Z_quot_mult := Z.quot_mul (only parsing). -Notation Zquot_small := Z.quot_small (compat "8.6"). -Notation Zrem_small := Z.rem_small (compat "8.6"). -Notation Zquot2_quot := Zquot2_quot (compat "8.6"). +Notation Zquot_small := Z.quot_small (compat "8.7"). +Notation Zrem_small := Z.rem_small (compat "8.7"). +Notation Zquot2_quot := Zquot2_quot (compat "8.7"). (** Particular values taken for [a÷0] and [(Z.rem a 0)]. We avise to not rely on these arbitrary values. *) @@ -129,33 +129,33 @@ Qed. Theorem Zrem_lt_pos a b : 0<=a -> b<>0 -> 0 <= Z.rem a b < Z.abs b. Proof. intros; generalize (Z.rem_nonneg a b) (Z.rem_bound_abs a b); - romega with *. + lia. Qed. Theorem Zrem_lt_neg a b : a<=0 -> b<>0 -> -Z.abs b < Z.rem a b <= 0. Proof. intros; generalize (Z.rem_nonpos a b) (Z.rem_bound_abs a b); - romega with *. + lia. Qed. Theorem Zrem_lt_pos_pos a b : 0<=a -> 0<b -> 0 <= Z.rem a b < b. Proof. - intros; generalize (Zrem_lt_pos a b); romega with *. + intros; generalize (Zrem_lt_pos a b); lia. Qed. Theorem Zrem_lt_pos_neg a b : 0<=a -> b<0 -> 0 <= Z.rem a b < -b. Proof. - intros; generalize (Zrem_lt_pos a b); romega with *. + intros; generalize (Zrem_lt_pos a b); lia. Qed. Theorem Zrem_lt_neg_pos a b : a<=0 -> 0<b -> -b < Z.rem a b <= 0. Proof. - intros; generalize (Zrem_lt_neg a b); romega with *. + intros; generalize (Zrem_lt_neg a b); lia. Qed. Theorem Zrem_lt_neg_neg a b : a<=0 -> b<0 -> b < Z.rem a b <= 0. Proof. - intros; generalize (Zrem_lt_neg a b); romega with *. + intros; generalize (Zrem_lt_neg a b); lia. Qed. @@ -171,12 +171,12 @@ Lemma Remainder_equiv : forall a b r, Remainder a b r <-> Remainder_alt a b r. Proof. unfold Remainder, Remainder_alt; intuition. - - romega with *. - - romega with *. - - rewrite <-(Z.mul_opp_opp). apply Z.mul_nonneg_nonneg; romega. + - lia. + - lia. + - rewrite <-(Z.mul_opp_opp). apply Z.mul_nonneg_nonneg; lia. - assert (0 <= Z.sgn r * Z.sgn a). { rewrite <-Z.sgn_mul, Z.sgn_nonneg; auto. } - destruct r; simpl Z.sgn in *; romega with *. + destruct r; simpl Z.sgn in *; lia. Qed. Theorem Zquot_mod_unique_full a b q r : @@ -185,7 +185,7 @@ Proof. destruct 1 as [(H,H0)|(H,H0)]; intros. apply Zdiv_mod_unique with b; auto. apply Zrem_lt_pos; auto. - romega with *. + lia. rewrite <- H1; apply Z.quot_rem'. rewrite <- (Z.opp_involutive a). @@ -193,7 +193,7 @@ Proof. generalize (Zdiv_mod_unique b (-q) (-a÷b) (-r) (Z.rem (-a) b)). generalize (Zrem_lt_pos (-a) b). rewrite <-Z.quot_rem', Z.mul_opp_r, <-Z.opp_add_distr, <-H1. - romega with *. + lia. Qed. Theorem Zquot_unique_full a b q r : |