diff options
Diffstat (limited to 'theories')
36 files changed, 579 insertions, 145 deletions
diff --git a/theories/FSets/FSetDecide.v b/theories/FSets/FSetDecide.v index d597c0404a..5fe2cade3b 100644 --- a/theories/FSets/FSetDecide.v +++ b/theories/FSets/FSetDecide.v @@ -489,7 +489,7 @@ the above form: variables. We are going to use them with [autorewrite]. *) - Hint Rewrite + Global Hint Rewrite F.empty_iff F.singleton_iff F.add_iff F.remove_iff F.union_iff F.inter_iff F.diff_iff : set_simpl. @@ -499,7 +499,7 @@ the above form: now split. Qed. - Hint Rewrite eq_refl_iff : set_eq_simpl. + Global Hint Rewrite eq_refl_iff : set_eq_simpl. (** ** Decidability of FSet Propositions *) diff --git a/theories/Lists/List.v b/theories/Lists/List.v index 115c7cb365..d6277b3bb5 100644 --- a/theories/Lists/List.v +++ b/theories/Lists/List.v @@ -3327,7 +3327,7 @@ Ltac invlist f := (** * Exporting hints and tactics *) -Hint Rewrite +Global Hint Rewrite rev_involutive (* rev (rev l) = l *) rev_unit (* rev (l ++ a :: nil) = a :: rev l *) map_nth (* nth n (map f l) (f d) = f (nth n l d) *) diff --git a/theories/MSets/MSetDecide.v b/theories/MSets/MSetDecide.v index aa0c419f0e..579e5e9630 100644 --- a/theories/MSets/MSetDecide.v +++ b/theories/MSets/MSetDecide.v @@ -489,7 +489,7 @@ the above form: variables. We are going to use them with [autorewrite]. *) - Hint Rewrite + Global Hint Rewrite F.empty_iff F.singleton_iff F.add_iff F.remove_iff F.union_iff F.inter_iff F.diff_iff : set_simpl. @@ -499,7 +499,7 @@ the above form: now split. Qed. - Hint Rewrite eq_refl_iff : set_eq_simpl. + Global Hint Rewrite eq_refl_iff : set_eq_simpl. (** ** Decidability of MSet Propositions *) diff --git a/theories/MSets/MSetRBT.v b/theories/MSets/MSetRBT.v index f80929e320..2d210e24a6 100644 --- a/theories/MSets/MSetRBT.v +++ b/theories/MSets/MSetRBT.v @@ -651,7 +651,7 @@ Proof. destruct (rbal'_match l x r); ok. Qed. -Hint Rewrite In_node_iff In_leaf_iff +Global Hint Rewrite In_node_iff In_leaf_iff makeRed_spec makeBlack_spec lbal_spec rbal_spec rbal'_spec : rb. Ltac descolor := destruct_all Color.t. @@ -670,7 +670,7 @@ Proof. - descolor; autorew; rewrite IHl; intuition_in. - descolor; autorew; rewrite IHr; intuition_in. Qed. -Hint Rewrite ins_spec : rb. +Global Hint Rewrite ins_spec : rb. Instance ins_ok s x `{Ok s} : Ok (ins x s). Proof. @@ -685,7 +685,7 @@ Proof. unfold add. now autorew. Qed. -Hint Rewrite add_spec' : rb. +Global Hint Rewrite add_spec' : rb. Lemma add_spec s x y `{Ok s} : InT y (add x s) <-> X.eq y x \/ InT y s. @@ -754,7 +754,7 @@ Proof. * ok. apply lbal_ok; ok. Qed. -Hint Rewrite lbalS_spec rbalS_spec : rb. +Global Hint Rewrite lbalS_spec rbalS_spec : rb. (** ** Append for deletion *) @@ -807,7 +807,7 @@ Proof. [intros a y b | intros t Ht]; autorew; tauto. Qed. -Hint Rewrite append_spec : rb. +Global Hint Rewrite append_spec : rb. Lemma append_ok : forall x l r `{Ok l, Ok r}, lt_tree x l -> gt_tree x r -> Ok (append l r). @@ -861,7 +861,7 @@ induct s x. rewrite ?IHr by trivial; intuition_in; order. Qed. -Hint Rewrite del_spec : rb. +Global Hint Rewrite del_spec : rb. Instance del_ok s x `{Ok s} : Ok (del x s). Proof. @@ -882,7 +882,7 @@ Proof. unfold remove. now autorew. Qed. -Hint Rewrite remove_spec : rb. +Global Hint Rewrite remove_spec : rb. Instance remove_ok s x `{Ok s} : Ok (remove x s). Proof. diff --git a/theories/NArith/Nnat.v b/theories/NArith/Nnat.v index 48df5fe884..420c17c9a4 100644 --- a/theories/NArith/Nnat.v +++ b/theories/NArith/Nnat.v @@ -127,7 +127,7 @@ Qed. End N2Nat. -Hint Rewrite N2Nat.inj_double N2Nat.inj_succ_double +Global Hint Rewrite N2Nat.inj_double N2Nat.inj_succ_double N2Nat.inj_succ N2Nat.inj_add N2Nat.inj_mul N2Nat.inj_sub N2Nat.inj_pred N2Nat.inj_div2 N2Nat.inj_max N2Nat.inj_min N2Nat.id @@ -147,7 +147,7 @@ Proof. induction n; simpl; trivial. apply SuccNat2Pos.id_succ. Qed. -Hint Rewrite id : Nnat. +Global Hint Rewrite id : Nnat. Ltac nat2N := apply N2Nat.inj; now autorewrite with Nnat. (** [N.of_nat] is hence injective *) @@ -206,7 +206,7 @@ Proof. now rewrite N2Nat.inj_iter, !id. Qed. End Nat2N. -Hint Rewrite Nat2N.id : Nnat. +Global Hint Rewrite Nat2N.id : Nnat. (** Compatibility notations *) diff --git a/theories/Numbers/Cyclic/Abstract/CyclicAxioms.v b/theories/Numbers/Cyclic/Abstract/CyclicAxioms.v index e3e8f532b3..374af6de63 100644 --- a/theories/Numbers/Cyclic/Abstract/CyclicAxioms.v +++ b/theories/Numbers/Cyclic/Abstract/CyclicAxioms.v @@ -348,7 +348,7 @@ Local Notation "- x" := (ZnZ.opp x). Local Infix "*" := ZnZ.mul. Local Notation wB := (base ZnZ.digits). -Hint Rewrite ZnZ.spec_0 ZnZ.spec_1 ZnZ.spec_add ZnZ.spec_mul +Global Hint Rewrite ZnZ.spec_0 ZnZ.spec_1 ZnZ.spec_add ZnZ.spec_mul ZnZ.spec_opp ZnZ.spec_sub : cyclic. diff --git a/theories/Numbers/Cyclic/Abstract/NZCyclic.v b/theories/Numbers/Cyclic/Abstract/NZCyclic.v index 7c5b43096a..f74a78e876 100644 --- a/theories/Numbers/Cyclic/Abstract/NZCyclic.v +++ b/theories/Numbers/Cyclic/Abstract/NZCyclic.v @@ -51,7 +51,7 @@ Local Infix "+" := add. Local Infix "-" := sub. Local Infix "*" := mul. -Hint Rewrite ZnZ.spec_0 ZnZ.spec_1 ZnZ.spec_succ ZnZ.spec_pred +Global Hint Rewrite ZnZ.spec_0 ZnZ.spec_1 ZnZ.spec_succ ZnZ.spec_pred ZnZ.spec_add ZnZ.spec_mul ZnZ.spec_sub : cyclic. Ltac zify := unfold eq, zero, one, two, succ, pred, add, sub, mul in *; diff --git a/theories/Numbers/Cyclic/Int63/Int63.v b/theories/Numbers/Cyclic/Int63/Int63.v index f324bbf52b..a3ebe67325 100644 --- a/theories/Numbers/Cyclic/Int63/Int63.v +++ b/theories/Numbers/Cyclic/Int63/Int63.v @@ -205,6 +205,7 @@ Qed. Corollary to_Z_bounded : forall x, (0 <= φ x < wB)%Z. Proof. apply to_Z_rec_bounded. Qed. + (* =================================================== *) Local Open Scope Z_scope. (* General arithmetic results *) @@ -954,6 +955,7 @@ Proof. intros _ HH; generalize (HH H1); discriminate. clear H. generalize (ltb_spec j i); case Int63.ltb; intros H2; unfold bit; simpl. + change 62%int63 with (digits - 1)%int63. assert (F2: (φ j < φ i)%Z) by (case H2; auto); clear H2. replace (is_zero (((x << i) >> j) << (digits - 1))) with true; auto. case (to_Z_bounded j); intros H1j H2j. @@ -1903,6 +1905,22 @@ Qed. Lemma lxor0_r i : i lxor 0 = i. Proof. rewrite lxorC; exact (lxor0 i). Qed. +Lemma opp_to_Z_opp (x : int) : + φ x mod wB <> 0 -> + (- φ (- x)) mod wB = (φ x) mod wB. +Proof. + intros neqx0. + rewrite opp_spec. + rewrite (Z_mod_nz_opp_full (φ x%int63)) by assumption. + rewrite (Z.mod_small (φ x%int63)) by apply to_Z_bounded. + rewrite <- Z.add_opp_l. + rewrite Z.opp_add_distr, Z.opp_involutive. + replace (- wB) with (-1 * wB) by easy. + rewrite Z_mod_plus by easy. + now rewrite Z.mod_small by apply to_Z_bounded. +Qed. + + Module Export Int63Notations. Local Open Scope int63_scope. #[deprecated(since="8.13",note="use infix mod instead")] diff --git a/theories/Numbers/Cyclic/Int63/PrimInt63.v b/theories/Numbers/Cyclic/Int63/PrimInt63.v index 64c1b862c7..98127ef0ac 100644 --- a/theories/Numbers/Cyclic/Int63/PrimInt63.v +++ b/theories/Numbers/Cyclic/Int63/PrimInt63.v @@ -17,11 +17,21 @@ Register comparison as kernel.ind_cmp. Primitive int := #int63_type. Register int as num.int63.type. +Variant pos_neg_int63 := Pos (d:int) | Neg (d:int). +Register pos_neg_int63 as num.int63.pos_neg_int63. Declare Scope int63_scope. Definition id_int : int -> int := fun x => x. -Declare ML Module "int63_syntax_plugin". - -Module Export Int63NotationsInternalA. +Record int_wrapper := wrap_int {int_wrap : int}. +Register wrap_int as num.int63.wrap_int. +Definition printer (x : int_wrapper) : pos_neg_int63 := Pos (int_wrap x). +Definition parser (x : pos_neg_int63) : option int := + match x with + | Pos p => Some p + | Neg _ => None + end. +Number Notation int parser printer : int63_scope. + +Module Import Int63NotationsInternalA. Delimit Scope int63_scope with int63. Bind Scope int63_scope with int. End Int63NotationsInternalA. @@ -37,6 +47,9 @@ Primitive lor := #int63_lor. Primitive lxor := #int63_lxor. + +Primitive asr := #int63_asr. + (* Arithmetic modulo operations *) Primitive add := #int63_add. @@ -50,6 +63,10 @@ Primitive div := #int63_div. Primitive mod := #int63_mod. +Primitive divs := #int63_divs. + +Primitive mods := #int63_mods. + (* Comparisons *) Primitive eqb := #int63_eq. @@ -57,6 +74,10 @@ Primitive ltb := #int63_lt. Primitive leb := #int63_le. +Primitive ltsb := #int63_lts. + +Primitive lesb := #int63_les. + (** Exact arithmetic operations *) Primitive addc := #int63_addc. @@ -76,7 +97,13 @@ Primitive addmuldiv := #int63_addmuldiv. (** Comparison *) Primitive compare := #int63_compare. +Primitive compares := #int63_compares. + (** Exotic operations *) Primitive head0 := #int63_head0. Primitive tail0 := #int63_tail0. + +Module Export PrimInt63Notations. + Export Int63NotationsInternalA. +End PrimInt63Notations. diff --git a/theories/Numbers/Cyclic/Int63/Sint63.v b/theories/Numbers/Cyclic/Int63/Sint63.v new file mode 100644 index 0000000000..c0239ae3db --- /dev/null +++ b/theories/Numbers/Cyclic/Int63/Sint63.v @@ -0,0 +1,407 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) +(* \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) *) +(************************************************************************) + +Require Import ZArith. +Import Znumtheory. +Require Export Int63. +Require Import Lia. + +Declare Scope sint63_scope. +Definition printer (x : int_wrapper) : pos_neg_int63 := + if (int_wrap x <? 4611686018427387904)%int63 then (* 2^62 *) + Pos (int_wrap x) + else + Neg ((int_wrap x) lxor max_int + 1)%int63. +Definition parser (x : pos_neg_int63) : option int := + match x with + | Pos p => if (p <? 4611686018427387904)%int63 then Some p else None + | Neg n => if (n <=? 4611686018427387904)%int63 + then Some ((n - 1) lxor max_int)%int63 else None + end. +Number Notation int parser printer : sint63_scope. + + +Module Import Sint63NotationsInternalA. +Delimit Scope sint63_scope with sint63. +Bind Scope sint63_scope with int. +End Sint63NotationsInternalA. + + +Module Import Sint63NotationsInternalB. +Infix "<<" := Int63.lsl (at level 30, no associativity) : sint63_scope. +(* TODO do we want >> to be asr or lsr? And is there a notation for the other one? *) +Infix ">>" := asr (at level 30, no associativity) : sint63_scope. +Infix "land" := Int63.land (at level 40, left associativity) : sint63_scope. +Infix "lor" := Int63.lor (at level 40, left associativity) : sint63_scope. +Infix "lxor" := Int63.lxor (at level 40, left associativity) : sint63_scope. +Infix "+" := Int63.add : sint63_scope. +Infix "-" := Int63.sub : sint63_scope. +Infix "*" := Int63.mul : sint63_scope. +Infix "/" := divs : sint63_scope. +Infix "mod" := mods (at level 40, no associativity) : sint63_scope. +Infix "=?" := Int63.eqb (at level 70, no associativity) : sint63_scope. +Infix "<?" := ltsb (at level 70, no associativity) : sint63_scope. +Infix "<=?" := lesb (at level 70, no associativity) : sint63_scope. +Infix "≤?" := lesb (at level 70, no associativity) : sint63_scope. +Notation "- x" := (opp x) : sint63_scope. +Notation "n ?= m" := (compares n m) (at level 70, no associativity) : sint63_scope. +End Sint63NotationsInternalB. + +Definition min_int := Eval vm_compute in (lsl 1 62). +Definition max_int := Eval vm_compute in (min_int - 1)%sint63. + +(** Translation to and from Z *) +Definition to_Z (i:int) := + if (i <? min_int)%int63 then + φ i%int63 + else + (- φ (- i)%int63)%Z. + +Lemma to_Z_0 : to_Z 0 = 0. +Proof. easy. Qed. + +Lemma to_Z_min : to_Z min_int = - (wB / 2). +Proof. easy. Qed. + +Lemma to_Z_max : to_Z max_int = wB / 2 - 1. +Proof. easy. Qed. + +Lemma to_Z_bounded : forall x, (to_Z min_int <= to_Z x <= to_Z max_int)%Z. +Proof. + intros x; unfold to_Z. + case ltbP; [> lia | intros _]. + case (ltbP max_int); [> intros _ | now intros H; exfalso; apply H]. + rewrite opp_spec. + rewrite Z_mod_nz_opp_full by easy. + rewrite Z.mod_small by apply Int63.to_Z_bounded. + case ltbP. + - intros ltxmin; split. + + now transitivity 0%Z; [>| now apply Int63.to_Z_bounded]. + + replace (φ min_int%int63) with (φ max_int%int63 + 1)%Z in ltxmin. + * lia. + * now compute. + - rewrite Z.nlt_ge; intros leminx. + rewrite opp_spec. + rewrite Z_mod_nz_opp_full. + + rewrite Z.mod_small by apply Int63.to_Z_bounded. + split. + * rewrite <- Z.opp_le_mono. + now rewrite <- Z.sub_le_mono_l. + * transitivity 0%Z; [>| now apply Int63.to_Z_bounded]. + rewrite Z.opp_nonpos_nonneg. + apply Zle_minus_le_0. + apply Z.lt_le_incl. + now apply Int63.to_Z_bounded. + + rewrite Z.mod_small by apply Int63.to_Z_bounded. + now intros eqx0; rewrite eqx0 in leminx. +Qed. + +Lemma of_to_Z : forall x, of_Z (to_Z x) = x. +Proof. + unfold to_Z, of_Z. + intros x. + generalize (Int63.to_Z_bounded x). + case ltbP. + - intros ltxmin [leq0x _]. + generalize (Int63.of_to_Z x). + destruct (φ x%int63). + + now intros <-. + + now intros <-; unfold Int63.of_Z. + + now intros _. + - intros nltxmin leq0xltwB. + rewrite (opp_spec x). + rewrite Z_mod_nz_opp_full. + + rewrite Zmod_small by easy. + destruct (wB - φ x%int63) eqn: iswbmx. + * lia. + * simpl. + apply to_Z_inj. + rewrite opp_spec. + generalize (of_Z_spec (Z.pos p)). + simpl Int63.of_Z; intros ->. + rewrite <- iswbmx. + rewrite <- Z.sub_0_l. + rewrite <- (Zmod_0_l wB). + rewrite <- Zminus_mod. + replace (0 - _) with (φ x%int63 - wB) by ring. + rewrite <- Zminus_mod_idemp_r. + rewrite Z_mod_same_full. + rewrite Z.sub_0_r. + now rewrite Z.mod_small. + * lia. + + rewrite Z.mod_small by easy. + intros eqx0; revert nltxmin; rewrite eqx0. + now compute. +Qed. + +Lemma to_Z_inj (x y : int) : to_Z x = to_Z y -> x = y. +Proof. exact (fun e => can_inj of_to_Z e). Qed. + +Lemma to_Z_mod_Int63to_Z (x : int) : to_Z x mod wB = φ x%int63. +Proof. + unfold to_Z. + case ltbP; [> now rewrite Z.mod_small by now apply Int63.to_Z_bounded |]. + rewrite Z.nlt_ge; intros gexmin. + rewrite opp_to_Z_opp; rewrite Z.mod_small by now apply Int63.to_Z_bounded. + - easy. + - now intros neqx0; rewrite neqx0 in gexmin. +Qed. + + +(** Centered modulo *) +Definition cmod (x d : Z) : Z := + (x + d / 2) mod d - (d / 2). + +Lemma cmod_mod (x d : Z) : + cmod (x mod d) d = cmod x d. +Proof. + now unfold cmod; rewrite Zplus_mod_idemp_l. +Qed. + +Lemma cmod_small (x d : Z) : + - (d / 2) <= x < d / 2 -> cmod x d = x. +Proof. + intros bound. + unfold cmod. + rewrite Zmod_small; [> lia |]. + split; [> lia |]. + rewrite Z.lt_add_lt_sub_r. + apply (Z.lt_le_trans _ (d / 2)); [> easy |]. + now rewrite <- Z.le_add_le_sub_r, Z.add_diag, Z.mul_div_le. +Qed. + +Lemma to_Z_cmodwB (x : int) : + to_Z x = cmod (φ x%int63) wB. +Proof. + unfold to_Z, cmod. + case ltbP; change φ (min_int)%int63 with (wB / 2). + - intros ltxmin. + rewrite Z.mod_small; [> lia |]. + split. + + now apply Z.add_nonneg_nonneg; try apply Int63.to_Z_bounded. + + change wB with (wB / 2 + wB / 2) at 2; lia. + - rewrite Z.nlt_ge; intros gexmin. + rewrite Int63.opp_spec. + rewrite Z_mod_nz_opp_full. + + rewrite Z.mod_small by apply Int63.to_Z_bounded. + rewrite <- (Z_mod_plus_full _ (-1)). + change (-1 * wB) with (- (wB / 2) - wB / 2). + rewrite <- Z.add_assoc, Zplus_minus. + rewrite Z.mod_small. + * change wB with (wB / 2 + wB / 2) at 1; lia. + * split; [> lia |]. + apply Z.lt_sub_lt_add_r. + transitivity wB; [>| easy]. + now apply Int63.to_Z_bounded. + + rewrite Z.mod_small by now apply Int63.to_Z_bounded. + now intros not0; rewrite not0 in gexmin. +Qed. + +Lemma of_Z_spec (z : Z) : to_Z (of_Z z) = cmod z wB. +Proof. now rewrite to_Z_cmodwB, Int63.of_Z_spec, cmod_mod. Qed. + +Lemma of_Z_cmod (z : Z) : of_Z (cmod z wB) = of_Z z. +Proof. now rewrite <- of_Z_spec, of_to_Z. Qed. + +Lemma is_int (z : Z) : + to_Z min_int <= z <= to_Z max_int -> + z = to_Z (of_Z z). +Proof. + rewrite to_Z_min, to_Z_max. + intros bound; rewrite of_Z_spec, cmod_small; lia. +Qed. + +(** Specification of operations that differ on signed and unsigned ints *) + +Axiom asr_spec : forall x p, to_Z (x >> p) = (to_Z x) / 2 ^ (to_Z p). + +Axiom div_spec : forall x y, + to_Z x <> to_Z min_int \/ to_Z y <> (-1)%Z -> + to_Z (x / y) = Z.quot (to_Z x) (to_Z y). + +Axiom mod_spec : forall x y, to_Z (x mod y) = Z.rem (to_Z x) (to_Z y). + +Axiom ltb_spec : forall x y, (x <? y)%sint63 = true <-> to_Z x < to_Z y. + +Axiom leb_spec : forall x y, (x <=? y)%sint63 = true <-> to_Z x <= to_Z y. + +Axiom compare_spec : forall x y, (x ?= y)%sint63 = (to_Z x ?= to_Z y). + +(** Specification of operations that coincide on signed and unsigned ints *) + +Lemma add_spec (x y : int) : + to_Z (x + y)%sint63 = cmod (to_Z x + to_Z y) wB. +Proof. + rewrite to_Z_cmodwB, Int63.add_spec. + rewrite <- 2!to_Z_mod_Int63to_Z, <- Z.add_mod by easy. + now rewrite cmod_mod. +Qed. + +Lemma sub_spec (x y : int) : + to_Z (x - y)%sint63 = cmod (to_Z x - to_Z y) wB. +Proof. + rewrite to_Z_cmodwB, Int63.sub_spec. + rewrite <- 2!to_Z_mod_Int63to_Z, <- Zminus_mod by easy. + now rewrite cmod_mod. +Qed. + +Lemma mul_spec (x y : int) : + to_Z (x * y)%sint63 = cmod (to_Z x * to_Z y) wB. +Proof. + rewrite to_Z_cmodwB, Int63.mul_spec. + rewrite <- 2!to_Z_mod_Int63to_Z, <- Zmult_mod by easy. + now rewrite cmod_mod. +Qed. + +Lemma succ_spec (x : int) : + to_Z (succ x)%sint63 = cmod (to_Z x + 1) wB. +Proof. now unfold succ; rewrite add_spec. Qed. + +Lemma pred_spec (x : int) : + to_Z (pred x)%sint63 = cmod (to_Z x - 1) wB. +Proof. now unfold pred; rewrite sub_spec. Qed. + +Lemma opp_spec (x : int) : + to_Z (- x)%sint63 = cmod (- to_Z x) wB. +Proof. + rewrite to_Z_cmodwB, Int63.opp_spec. + rewrite <- Z.sub_0_l, <- to_Z_mod_Int63to_Z, Zminus_mod_idemp_r. + now rewrite cmod_mod. +Qed. + +(** Behaviour when there is no under or overflow *) + +Lemma add_bounded (x y : int) : + to_Z min_int <= to_Z x + to_Z y <= to_Z max_int -> + to_Z (x + y) = to_Z x + to_Z y. +Proof. + rewrite to_Z_min, to_Z_max; intros bound. + now rewrite add_spec, cmod_small; [>| lia]. +Qed. + +Lemma sub_bounded (x y : int) : + to_Z min_int <= to_Z x - to_Z y <= to_Z max_int -> + to_Z (x - y) = to_Z x - to_Z y. +Proof. + rewrite to_Z_min, to_Z_max; intros bound. + now rewrite sub_spec, cmod_small; [>| lia]. +Qed. + +Lemma mul_bounded (x y : int) : + to_Z min_int <= to_Z x * to_Z y <= to_Z max_int -> + to_Z (x * y) = to_Z x * to_Z y. +Proof. + rewrite to_Z_min, to_Z_max; intros bound. + now rewrite mul_spec, cmod_small; [>| lia]. +Qed. + +Lemma succ_bounded (x : int) : + to_Z min_int <= to_Z x + 1 <= to_Z max_int -> + to_Z (succ x) = to_Z x + 1. +Proof. + rewrite to_Z_min, to_Z_max; intros bound. + now rewrite succ_spec, cmod_small; [>| lia]. +Qed. + +Lemma pred_bounded (x : int) : + to_Z min_int <= to_Z x - 1 <= to_Z max_int -> + to_Z (pred x) = to_Z x - 1. +Proof. + rewrite to_Z_min, to_Z_max; intros bound. + now rewrite pred_spec, cmod_small; [>| lia]. +Qed. + +Lemma opp_bounded (x : int) : + to_Z min_int <= - to_Z x <= to_Z max_int -> + to_Z (- x) = - to_Z x. +Proof. + rewrite to_Z_min, to_Z_max; intros bound. + now rewrite opp_spec, cmod_small; [>| lia]. +Qed. + +(** Relationship with of_Z *) + +Lemma add_of_Z (x y : int) : + (x + y)%sint63 = of_Z (to_Z x + to_Z y). +Proof. now rewrite <- of_Z_cmod, <- add_spec, of_to_Z. Qed. + +Lemma sub_of_Z (x y : int) : + (x - y)%sint63 = of_Z (to_Z x - to_Z y). +Proof. now rewrite <- of_Z_cmod, <- sub_spec, of_to_Z. Qed. + +Lemma mul_of_Z (x y : int) : + (x * y)%sint63 = of_Z (to_Z x * to_Z y). +Proof. now rewrite <- of_Z_cmod, <- mul_spec, of_to_Z. Qed. + +Lemma succ_of_Z (x : int) : + (succ x)%sint63 = of_Z (to_Z x + 1). +Proof. now rewrite <- of_Z_cmod, <- succ_spec, of_to_Z. Qed. + +Lemma pred_of_Z (x : int) : + (pred x)%sint63 = of_Z (to_Z x - 1). +Proof. now rewrite <- of_Z_cmod, <- pred_spec, of_to_Z. Qed. + +Lemma opp_of_Z (x : int) : + (- x)%sint63 = of_Z (- to_Z x). +Proof. now rewrite <- of_Z_cmod, <- opp_spec, of_to_Z. Qed. + +(** Comparison *) +Import Bool. + +Lemma eqbP x y : reflect (to_Z x = to_Z y) (x =? y)%sint63. +Proof. + apply iff_reflect; rewrite Int63.eqb_spec. + now split; [> apply to_Z_inj | apply f_equal]. +Qed. + +Lemma ltbP x y : reflect (to_Z x < to_Z y) (x <? y)%sint63. +Proof. now apply iff_reflect; symmetry; apply ltb_spec. Qed. + +Lemma lebP x y : reflect (to_Z x <= to_Z y) (x ≤? y)%sint63. +Proof. now apply iff_reflect; symmetry; apply leb_spec. Qed. + +(** ASR *) +Lemma asr_0 (i : int) : (0 >> i)%sint63 = 0%sint63. +Proof. now apply to_Z_inj; rewrite asr_spec. Qed. + +Lemma asr_0_r (i : int) : (i >> 0)%sint63 = i. +Proof. now apply to_Z_inj; rewrite asr_spec, Zdiv_1_r. Qed. + +Lemma asr_neg_r (i n : int) : to_Z n < 0 -> (i >> n)%sint63 = 0%sint63. +Proof. + intros ltn0. + apply to_Z_inj. + rewrite asr_spec, Z.pow_neg_r by assumption. + now rewrite Zdiv_0_r. +Qed. + +Lemma asr_1 (n : int) : (1 >> n)%sint63 = (n =? 0)%sint63. +Proof. + apply to_Z_inj; rewrite asr_spec. + case eqbP; [> now intros -> | intros neqn0]. + case (lebP 0 n). + - intros le0n. + apply Z.div_1_l; apply Z.pow_gt_1; [> easy |]. + rewrite to_Z_0 in *; lia. + - rewrite Z.nle_gt; intros ltn0. + now rewrite Z.pow_neg_r. +Qed. + +Notation asr := asr (only parsing). +Notation div := divs (only parsing). +Notation rem := mods (only parsing). +Notation ltb := ltsb (only parsing). +Notation leb := lesb (only parsing). +Notation compare := compares (only parsing). + +Module Export Sint63Notations. + Export Sint63NotationsInternalA. + Export Sint63NotationsInternalB. +End Sint63Notations. diff --git a/theories/Numbers/HexadecimalNat.v b/theories/Numbers/HexadecimalNat.v index 94a14b90bd..696e89bd8e 100644 --- a/theories/Numbers/HexadecimalNat.v +++ b/theories/Numbers/HexadecimalNat.v @@ -230,7 +230,7 @@ Proof. simpl_of_lu; rewrite ?Nat.add_succ_l, Nat.add_0_l, ?to_lu_succ, to_of_lu_sixteenfold by assumption; - unfold lnorm; simpl; now destruct nztail. + unfold lnorm; cbn; now destruct nztail. Qed. (** Second bijection result *) diff --git a/theories/Numbers/Integer/Abstract/ZAdd.v b/theories/Numbers/Integer/Abstract/ZAdd.v index 0c097b6773..9d9244eefb 100644 --- a/theories/Numbers/Integer/Abstract/ZAdd.v +++ b/theories/Numbers/Integer/Abstract/ZAdd.v @@ -18,7 +18,7 @@ Include ZBaseProp Z. (** Theorems that are either not valid on N or have different proofs on N and Z *) -Hint Rewrite opp_0 : nz. +Global Hint Rewrite opp_0 : nz. Theorem add_pred_l n m : P n + m == P (n + m). Proof. diff --git a/theories/Numbers/Integer/Abstract/ZBits.v b/theories/Numbers/Integer/Abstract/ZBits.v index 4d2361689d..832931e5ef 100644 --- a/theories/Numbers/Integer/Abstract/ZBits.v +++ b/theories/Numbers/Integer/Abstract/ZBits.v @@ -26,7 +26,7 @@ Include BoolEqualityFacts A. Ltac order_nz := try apply pow_nonzero; order'. Ltac order_pos' := try apply abs_nonneg; order_pos. -Hint Rewrite div_0_l mod_0_l div_1_r mod_1_r : nz. +Global Hint Rewrite div_0_l mod_0_l div_1_r mod_1_r : nz. (** Some properties of power and division *) @@ -566,7 +566,7 @@ Tactic Notation "bitwise" "as" simple_intropattern(m) simple_intropattern(Hm) Ltac bitwise := bitwise as ?m ?Hm. -Hint Rewrite lxor_spec lor_spec land_spec ldiff_spec bits_0 : bitwise. +Global Hint Rewrite lxor_spec lor_spec land_spec ldiff_spec bits_0 : bitwise. (** The streams of bits that correspond to a numbers are exactly the ones which are stationary after some point. *) diff --git a/theories/Numbers/NatInt/NZAdd.v b/theories/Numbers/NatInt/NZAdd.v index 66cbba9e08..2ad8dfcedb 100644 --- a/theories/Numbers/NatInt/NZAdd.v +++ b/theories/Numbers/NatInt/NZAdd.v @@ -14,9 +14,9 @@ Require Import NZAxioms NZBase. Module Type NZAddProp (Import NZ : NZAxiomsSig')(Import NZBase : NZBaseProp NZ). -Hint Rewrite +Global Hint Rewrite pred_succ add_0_l add_succ_l mul_0_l mul_succ_l sub_0_r sub_succ_r : nz. -Hint Rewrite one_succ two_succ : nz'. +Global Hint Rewrite one_succ two_succ : nz'. Ltac nzsimpl := autorewrite with nz. Ltac nzsimpl' := autorewrite with nz nz'. @@ -39,7 +39,7 @@ Proof. intros n m. now rewrite add_succ_r, add_succ_l. Qed. -Hint Rewrite add_0_r add_succ_r : nz. +Global Hint Rewrite add_0_r add_succ_r : nz. Theorem add_comm : forall n m, n + m == m + n. Proof. @@ -58,7 +58,7 @@ Proof. intro n; now nzsimpl'. Qed. -Hint Rewrite add_1_l add_1_r : nz. +Global Hint Rewrite add_1_l add_1_r : nz. Theorem add_assoc : forall n m p, n + (m + p) == (n + m) + p. Proof. @@ -104,6 +104,6 @@ Proof. intro n; now nzsimpl'. Qed. -Hint Rewrite sub_1_r : nz. +Global Hint Rewrite sub_1_r : nz. End NZAddProp. diff --git a/theories/Numbers/NatInt/NZMul.v b/theories/Numbers/NatInt/NZMul.v index 3d6465191d..14728eaf40 100644 --- a/theories/Numbers/NatInt/NZMul.v +++ b/theories/Numbers/NatInt/NZMul.v @@ -28,7 +28,7 @@ Proof. now rewrite add_cancel_r. Qed. -Hint Rewrite mul_0_r mul_succ_r : nz. +Global Hint Rewrite mul_0_r mul_succ_r : nz. Theorem mul_comm : forall n m, n * m == m * n. Proof. @@ -69,7 +69,7 @@ Proof. intro n. now nzsimpl'. Qed. -Hint Rewrite mul_1_l mul_1_r : nz. +Global Hint Rewrite mul_1_l mul_1_r : nz. Theorem mul_shuffle0 : forall n m p, n*m*p == n*p*m. Proof. diff --git a/theories/Numbers/NatInt/NZPow.v b/theories/Numbers/NatInt/NZPow.v index 3b2a496229..00edcd641f 100644 --- a/theories/Numbers/NatInt/NZPow.v +++ b/theories/Numbers/NatInt/NZPow.v @@ -45,7 +45,7 @@ Module Type NZPowProp (Import B : NZPow' A) (Import C : NZMulOrderProp A). -Hint Rewrite pow_0_r pow_succ_r : nz. +Global Hint Rewrite pow_0_r pow_succ_r : nz. (** Power and basic constants *) @@ -76,14 +76,14 @@ Proof. - now nzsimpl. Qed. -Hint Rewrite pow_1_r pow_1_l : nz. +Global Hint Rewrite pow_1_r pow_1_l : nz. Lemma pow_2_r : forall a, a^2 == a*a. Proof. intros. rewrite two_succ. nzsimpl; order'. Qed. -Hint Rewrite pow_2_r : nz. +Global Hint Rewrite pow_2_r : nz. (** Power and nullity *) diff --git a/theories/Numbers/Natural/Abstract/NBits.v b/theories/Numbers/Natural/Abstract/NBits.v index 313b9adfd1..427a18d4ae 100644 --- a/theories/Numbers/Natural/Abstract/NBits.v +++ b/theories/Numbers/Natural/Abstract/NBits.v @@ -23,7 +23,7 @@ Module Type NBitsProp Include BoolEqualityFacts A. Ltac order_nz := try apply pow_nonzero; order'. -Hint Rewrite div_0_l mod_0_l div_1_r mod_1_r : nz. +Global Hint Rewrite div_0_l mod_0_l div_1_r mod_1_r : nz. (** Some properties of power and division *) @@ -368,7 +368,7 @@ Proof. split. apply bits_inj. intros EQ; now rewrite EQ. Qed. -Hint Rewrite lxor_spec lor_spec land_spec ldiff_spec bits_0 : bitwise. +Global Hint Rewrite lxor_spec lor_spec land_spec ldiff_spec bits_0 : bitwise. Tactic Notation "bitwise" "as" simple_intropattern(m) := apply bits_inj; intros m; autorewrite with bitwise. diff --git a/theories/PArith/BinPos.v b/theories/PArith/BinPos.v index e97f2dc748..7d50bdacad 100644 --- a/theories/PArith/BinPos.v +++ b/theories/PArith/BinPos.v @@ -876,7 +876,7 @@ Lemma compare_xO_xI p q : (p~0 ?= q~1) = switch_Eq Lt (p ?= q). Proof. exact (compare_cont_spec p q Lt). Qed. -Hint Rewrite compare_xO_xO compare_xI_xI compare_xI_xO compare_xO_xI : compare. +Global Hint Rewrite compare_xO_xO compare_xI_xI compare_xI_xO compare_xO_xI : compare. Ltac simpl_compare := autorewrite with compare. Ltac simpl_compare_in H := autorewrite with compare in H. diff --git a/theories/Program/Combinators.v b/theories/Program/Combinators.v index 8813131d7b..18e55aefc6 100644 --- a/theories/Program/Combinators.v +++ b/theories/Program/Combinators.v @@ -40,8 +40,8 @@ Proof. reflexivity. Qed. -Hint Rewrite @compose_id_left @compose_id_right : core. -Hint Rewrite <- @compose_assoc : core. +Global Hint Rewrite @compose_id_left @compose_id_right : core. +Global Hint Rewrite <- @compose_assoc : core. (** [flip] is involutive. *) diff --git a/theories/Program/Equality.v b/theories/Program/Equality.v index 25af2d5ffb..090322054e 100644 --- a/theories/Program/Equality.v +++ b/theories/Program/Equality.v @@ -162,7 +162,7 @@ Ltac pi_eq_proofs := repeat pi_eq_proof. Ltac clear_eq_proofs := abstract_eq_proofs ; pi_eq_proofs. -Hint Rewrite <- eq_rect_eq : refl_id. +Global Hint Rewrite <- eq_rect_eq : refl_id. (** The [refl_id] database should be populated with lemmas of the form [coerce_* t eq_refl = t]. *) @@ -178,7 +178,7 @@ Lemma inj_pairT2_refl A (x : A) (P : A -> Type) (p : P x) : Eqdep.EqdepTheory.inj_pairT2 A P x p p eq_refl = eq_refl. Proof. apply UIP_refl. Qed. -Hint Rewrite @JMeq_eq_refl @UIP_refl_refl @inj_pairT2_refl : refl_id. +Global Hint Rewrite @JMeq_eq_refl @UIP_refl_refl @inj_pairT2_refl : refl_id. Ltac rewrite_refl_id := autorewrite with refl_id. diff --git a/theories/Program/Tactics.v b/theories/Program/Tactics.v index fce69437d7..d852ad24fe 100644 --- a/theories/Program/Tactics.v +++ b/theories/Program/Tactics.v @@ -319,7 +319,3 @@ Create HintDb program discriminated. Ltac program_simpl := program_simplify ; try typeclasses eauto 10 with program ; try program_solve_wf. Obligation Tactic := program_simpl. - -Definition obligation (A : Type) {a : A} := a. - -Register obligation as program.tactics.obligation. diff --git a/theories/QArith/Qreals.v b/theories/QArith/Qreals.v index 5a23a20811..620ed6b5b7 100644 --- a/theories/QArith/Qreals.v +++ b/theories/QArith/Qreals.v @@ -180,4 +180,4 @@ intros; rewrite Q2R_mult. rewrite Q2R_inv; auto. Qed. -Hint Rewrite Q2R_plus Q2R_mult Q2R_opp Q2R_minus Q2R_inv Q2R_div : q2r_simpl. +Global Hint Rewrite Q2R_plus Q2R_mult Q2R_opp Q2R_minus Q2R_inv Q2R_div : q2r_simpl. diff --git a/theories/Reals/Abstract/ConstructiveReals.v b/theories/Reals/Abstract/ConstructiveReals.v index 60fad8795a..5a599587d0 100644 --- a/theories/Reals/Abstract/ConstructiveReals.v +++ b/theories/Reals/Abstract/ConstructiveReals.v @@ -285,14 +285,14 @@ Lemma CRlt_trans : forall {R : ConstructiveReals} (x y z : CRcarrier R), Proof. intros. apply (CRlt_le_trans _ y _ H). apply CRlt_asym. exact H0. -Defined. +Qed. Lemma CRlt_trans_flip : forall {R : ConstructiveReals} (x y z : CRcarrier R), y < z -> x < y -> x < z. Proof. intros. apply (CRlt_le_trans _ y). exact H0. apply CRlt_asym. exact H. -Defined. +Qed. Lemma CReq_refl : forall {R : ConstructiveReals} (x : CRcarrier R), x == x. diff --git a/theories/Reals/Abstract/ConstructiveRealsMorphisms.v b/theories/Reals/Abstract/ConstructiveRealsMorphisms.v index 53b5aca38c..6ed5845440 100644 --- a/theories/Reals/Abstract/ConstructiveRealsMorphisms.v +++ b/theories/Reals/Abstract/ConstructiveRealsMorphisms.v @@ -232,7 +232,7 @@ Proof. apply CRplus_lt_compat_l. apply (CRle_lt_trans _ (CR_of_Q R 0)). apply CRle_refl. apply CR_of_Q_lt. exact H. -Defined. +Qed. Lemma CRplus_neg_rat_lt : forall {R : ConstructiveReals} (x : CRcarrier R) (q : Q), Qlt q 0 -> CRlt R (CRplus R x (CR_of_Q R q)) x. diff --git a/theories/Reals/Alembert.v b/theories/Reals/Alembert.v index 069a1292cd..9a00408de3 100644 --- a/theories/Reals/Alembert.v +++ b/theories/Reals/Alembert.v @@ -112,7 +112,7 @@ Proof. pattern (sum_f_R0 An n) at 1; rewrite <- Rplus_0_r; apply Rplus_le_compat_l; left; apply H | apply H1 ]. -Defined. +Qed. Lemma Alembert_C2 : forall An:nat -> R, @@ -330,7 +330,7 @@ Proof. rewrite <- Rabs_Ropp; apply RRle_abs. rewrite double; pattern (Rabs (An n)) at 1; rewrite <- Rplus_0_r; apply Rplus_lt_compat_l; apply Rabs_pos_lt; apply H. -Defined. +Qed. Lemma AlembertC3_step1 : forall (An:nat -> R) (x:R), @@ -374,7 +374,7 @@ Proof. [ assumption | apply Rinv_0_lt_compat; apply Rabs_pos_lt; assumption ]. intro; unfold Bn; apply prod_neq_R0; [ apply H0 | apply pow_nonzero; assumption ]. -Defined. +Qed. Lemma AlembertC3_step2 : forall (An:nat -> R) (x:R), x = 0 -> { l:R | Pser An x l }. @@ -405,7 +405,7 @@ Proof. cut (x <> 0). intro; apply AlembertC3_step1; assumption. red; intro; rewrite H1 in Hgt; elim (Rlt_irrefl _ Hgt). -Defined. +Qed. Lemma Alembert_C4 : forall (An:nat -> R) (k:R), diff --git a/theories/Reals/Cauchy/ConstructiveCauchyReals.v b/theories/Reals/Cauchy/ConstructiveCauchyReals.v index 8a11c155ce..4fb3846abc 100644 --- a/theories/Reals/Cauchy/ConstructiveCauchyReals.v +++ b/theories/Reals/Cauchy/ConstructiveCauchyReals.v @@ -320,7 +320,6 @@ Proof. - contradiction. - exact Hxltz. Qed. -(* Todo: this was Defined. Why *) Lemma CReal_lt_le_trans : forall x y z : CReal, x < y -> y <= z -> x < z. @@ -330,7 +329,6 @@ Proof. - exact Hxltz. - contradiction. Qed. -(* Todo: this was Defined. Why *) Lemma CReal_le_trans : forall x y z : CReal, x <= y -> y <= z -> x <= z. @@ -347,7 +345,6 @@ Proof. apply (CReal_lt_le_trans _ y _ Hxlty). apply CRealLt_asym; exact Hyltz. Qed. -(* Todo: this was Defined. Why *) Lemma CRealEq_trans : forall x y z : CReal, CRealEq x y -> CRealEq y z -> CRealEq x z. diff --git a/theories/Reals/Cauchy/ConstructiveCauchyRealsMult.v b/theories/Reals/Cauchy/ConstructiveCauchyRealsMult.v index a180e13444..bc45868244 100644 --- a/theories/Reals/Cauchy/ConstructiveCauchyRealsMult.v +++ b/theories/Reals/Cauchy/ConstructiveCauchyRealsMult.v @@ -733,13 +733,11 @@ Definition CReal_inv_pos (x : CReal) (Hxpos : 0 < x) : CReal := bound := CReal_inv_pos_bound x Hxpos |}. -(* ToDo: make this more obviously computing *) - Definition CReal_neg_lt_pos : forall x : CReal, x < 0 -> 0 < -x. Proof. intros x [n nmaj]. exists n. - apply (Qlt_le_trans _ _ _ nmaj). destruct x. simpl. - unfold Qminus. rewrite Qplus_0_l, Qplus_0_r. apply Qle_refl. + simpl in *. unfold CReal_opp_seq, Qminus. + abstract now rewrite Qplus_0_r, <- (Qplus_0_l (- seq x n)). Defined. Definition CReal_inv (x : CReal) (xnz : x # 0) : CReal diff --git a/theories/Reals/Cauchy/ConstructiveRcomplete.v b/theories/Reals/Cauchy/ConstructiveRcomplete.v index 70d2861d17..c2b60e6478 100644 --- a/theories/Reals/Cauchy/ConstructiveRcomplete.v +++ b/theories/Reals/Cauchy/ConstructiveRcomplete.v @@ -75,7 +75,7 @@ Proof. rewrite inject_Q_plus, (opp_inject_Q 2). ring_simplify. exact H. rewrite Qinv_plus_distr. reflexivity. -Defined. +Qed. (* ToDo: Move to ConstructiveCauchyAbs.v *) Lemma Qabs_Rabs : forall q : Q, @@ -688,21 +688,7 @@ Proof. exact (a i j H0 H1). exists l. intros p. destruct (cv p). exists x. exact c. -Defined. - -(* ToDO: Belongs into sumbool.v *) -Section connectives. - - Variables A B : Prop. - - Hypothesis H1 : {A} + {~A}. - Hypothesis H2 : {B} + {~B}. - - Definition sumbool_or_not_or : {A \/ B} + {~(A \/ B)}. - case H1; case H2; tauto. - Defined. - -End connectives. +Qed. Lemma Qnot_le_iff_lt: forall x y : Q, ~ (x <= y)%Q <-> (y < x)%Q. @@ -740,13 +726,11 @@ Proof. clear maj. right. exists n. apply H0. - clear H0 H. intro n. - apply sumbool_or_not_or. - + destruct (Qlt_le_dec (2 * 2 ^ n)%Q (seq b n - seq a n)%Q). - * left; assumption. - * right; apply Qle_not_lt; assumption. - + destruct (Qlt_le_dec (2 * 2 ^ n)%Q (seq d n - seq c n)%Q). - * left; assumption. - * right; apply Qle_not_lt; assumption. + destruct (Qlt_le_dec (2 * 2 ^ n)%Q (seq b n - seq a n)%Q) as [H1|H1]. + + now left; left. + + destruct (Qlt_le_dec (2 * 2 ^ n)%Q (seq d n - seq c n)%Q) as [H2|H2]. + * now left; right. + * now right; intros [H3|H3]; apply Qle_not_lt with (2 := H3). Qed. Definition CRealConstructive : ConstructiveReals diff --git a/theories/Reals/ClassicalDedekindReals.v b/theories/Reals/ClassicalDedekindReals.v index 500838ed26..0736b09761 100644 --- a/theories/Reals/ClassicalDedekindReals.v +++ b/theories/Reals/ClassicalDedekindReals.v @@ -233,17 +233,12 @@ Qed. (** *** Conversion from CReal to DReal *) -Definition DRealAbstr : CReal -> DReal. +Lemma DRealAbstr_aux : + forall x H, + isLowerCut (fun q : Q => + if sig_forall_dec (fun n : nat => seq x (- Z.of_nat n) <= q + 2 ^ (- Z.of_nat n)) (H q) + then true else false). Proof. - intro x. - assert (forall (q : Q) (n : nat), - {(fun n0 : nat => (seq x (-Z.of_nat n0) <= q + (2^-Z.of_nat n0))%Q) n} + - {~ (fun n0 : nat => (seq x (-Z.of_nat n0) <= q + (2^-Z.of_nat n0))%Q) n}). - { intros. destruct (Qlt_le_dec (q + (2^-Z.of_nat n)) (seq x (-Z.of_nat n))). - right. apply (Qlt_not_le _ _ q0). left. exact q0. } - - exists (fun q:Q => if sig_forall_dec (fun n:nat => Qle (seq x (-Z.of_nat n)) (q + (2^-Z.of_nat n))) (H q) - then true else false). repeat split. - intros. destruct (sig_forall_dec (fun n : nat => (seq x (-Z.of_nat n) <= q + (2^-Z.of_nat n))%Q) @@ -303,6 +298,20 @@ Proof. apply (Qmult_le_l _ _ 2) in q0. field_simplify in q0. apply (Qplus_le_l _ _ (-seq x (-Z.of_nat n))) in q0. ring_simplify in q0. contradiction. reflexivity. +Qed. + +Definition DRealAbstr : CReal -> DReal. +Proof. + intro x. + assert (forall (q : Q) (n : nat), + {(fun n0 : nat => (seq x (-Z.of_nat n0) <= q + (2^-Z.of_nat n0))%Q) n} + + {~ (fun n0 : nat => (seq x (-Z.of_nat n0) <= q + (2^-Z.of_nat n0))%Q) n}). + { intros. destruct (Qlt_le_dec (q + (2^-Z.of_nat n)) (seq x (-Z.of_nat n))). + right. apply (Qlt_not_le _ _ q0). left. exact q0. } + + exists (fun q:Q => if sig_forall_dec (fun n:nat => Qle (seq x (-Z.of_nat n)) (q + (2^-Z.of_nat n))) (H q) + then true else false). + apply DRealAbstr_aux. Defined. (** *** Conversion from DReal to CReal *) diff --git a/theories/Reals/NewtonInt.v b/theories/Reals/NewtonInt.v index 6692119738..6107775003 100644 --- a/theories/Reals/NewtonInt.v +++ b/theories/Reals/NewtonInt.v @@ -170,7 +170,7 @@ Proof. reg. exists H5; symmetry ; reg; rewrite <- H3; rewrite <- H4; reflexivity. assumption. -Defined. +Qed. (**********) Lemma antiderivative_P1 : diff --git a/theories/Reals/Rtrigo_def.v b/theories/Reals/Rtrigo_def.v index 7f5a859c81..2004f40f00 100644 --- a/theories/Reals/Rtrigo_def.v +++ b/theories/Reals/Rtrigo_def.v @@ -41,9 +41,13 @@ Proof. red; intro; rewrite H0 in H; elim (lt_irrefl _ H). Qed. -Lemma exist_exp0 : { l:R | exp_in 0 l }. +(* Value of [exp 0] *) +Lemma exp_0 : exp 0 = 1. Proof. - exists 1. + cut (exp_in 0 1). + cut (exp_in 0 (exp 0)). + apply uniqueness_sum. + exact (proj2_sig (exist_exp 0)). unfold exp_in; unfold infinite_sum; intros. exists 0%nat. intros; replace (sum_f_R0 (fun i:nat => / INR (fact i) * 0 ^ i) n) with 1. @@ -56,18 +60,6 @@ Proof. simpl. ring. unfold ge; apply le_O_n. -Defined. - -(* Value of [exp 0] *) -Lemma exp_0 : exp 0 = 1. -Proof. - cut (exp_in 0 (exp 0)). - cut (exp_in 0 1). - unfold exp_in; intros; eapply uniqueness_sum. - apply H0. - apply H. - exact (proj2_sig exist_exp0). - exact (proj2_sig (exist_exp 0)). Qed. (*****************************************) @@ -384,9 +376,14 @@ Proof. intros; ring. Qed. -Lemma exist_cos0 : { l:R | cos_in 0 l }. +(* Value of [cos 0] *) +Lemma cos_0 : cos 0 = 1. Proof. - exists 1. + cut (cos_in 0 1). + cut (cos_in 0 (cos 0)). + apply uniqueness_sum. + rewrite <- Rsqr_0 at 1. + exact (proj2_sig (exist_cos (Rsqr 0))). unfold cos_in; unfold infinite_sum; intros; exists 0%nat. intros. unfold R_dist. @@ -400,17 +397,4 @@ Proof. rewrite Rplus_0_r. apply Hrecn; unfold ge; apply le_O_n. simpl; ring. -Defined. - -(* Value of [cos 0] *) -Lemma cos_0 : cos 0 = 1. -Proof. - cut (cos_in 0 (cos 0)). - cut (cos_in 0 1). - unfold cos_in; intros; eapply uniqueness_sum. - apply H0. - apply H. - exact (proj2_sig exist_cos0). - assert (H := proj2_sig (exist_cos (Rsqr 0))); unfold cos; - pattern 0 at 1; replace 0 with (Rsqr 0); [ exact H | apply Rsqr_0 ]. Qed. diff --git a/theories/Strings/Ascii.v b/theories/Strings/Ascii.v index 06b02ab211..37d30a282c 100644 --- a/theories/Strings/Ascii.v +++ b/theories/Strings/Ascii.v @@ -173,6 +173,14 @@ Proof. apply N_ascii_bounded. Qed. +Definition ltb (a b : ascii) : bool := + (N_of_ascii a <? N_of_ascii b)%N. + +Definition leb (a b : ascii) : bool := + (N_of_ascii a <=? N_of_ascii b)%N. + +Infix "<?" := ltb : char_scope. +Infix "<=?" := leb : char_scope. (** * Concrete syntax *) diff --git a/theories/Structures/OrdersFacts.v b/theories/Structures/OrdersFacts.v index 4ac54d280a..c3e67b9d5a 100644 --- a/theories/Structures/OrdersFacts.v +++ b/theories/Structures/OrdersFacts.v @@ -53,7 +53,7 @@ Module Type CompareFacts (Import O:DecStrOrder'). rewrite compare_gt_iff; intuition. Qed. - Hint Rewrite compare_eq_iff compare_lt_iff compare_gt_iff : order. + Global Hint Rewrite compare_eq_iff compare_lt_iff compare_gt_iff : order. Instance compare_compat : Proper (eq==>eq==>Logic.eq) compare. Proof. diff --git a/theories/ZArith/Int.v b/theories/ZArith/Int.v index abf7f681b0..c709149109 100644 --- a/theories/ZArith/Int.v +++ b/theories/ZArith/Int.v @@ -146,7 +146,7 @@ Module MoreInt (Import I:Int). (** A magic (but costly) tactic that goes from [int] back to the [Z] friendly world ... *) - Hint Rewrite -> + Global Hint Rewrite -> i2z_0 i2z_1 i2z_2 i2z_3 i2z_add i2z_opp i2z_sub i2z_mul i2z_max i2z_eqb i2z_ltb i2z_leb : i2z. diff --git a/theories/dune b/theories/dune index 18e000cfe1..1cd3d8c119 100644 --- a/theories/dune +++ b/theories/dune @@ -1,6 +1,6 @@ (coq.theory (name Coq) - (package coq) + (package coq-stdlib) (synopsis "Coq's Standard Library") (flags -q) ; (mode native) @@ -8,30 +8,29 @@ ; (per_file ; (Init/*.v -> -boot)) (libraries - coq.plugins.ltac - coq.plugins.tauto + coq-core.plugins.ltac + coq-core.plugins.tauto - coq.plugins.cc - coq.plugins.firstorder + coq-core.plugins.cc + coq-core.plugins.firstorder - coq.plugins.number_string_notation - coq.plugins.int63_syntax - coq.plugins.float_syntax + coq-core.plugins.number_string_notation + coq-core.plugins.float_syntax - coq.plugins.btauto - coq.plugins.rtauto + coq-core.plugins.btauto + coq-core.plugins.rtauto - coq.plugins.ring - coq.plugins.nsatz - coq.plugins.omega + coq-core.plugins.ring + coq-core.plugins.nsatz + coq-core.plugins.omega - coq.plugins.zify - coq.plugins.micromega + coq-core.plugins.zify + coq-core.plugins.micromega - coq.plugins.funind + coq-core.plugins.funind - coq.plugins.ssreflect - coq.plugins.ssrsearch - coq.plugins.derive)) + coq-core.plugins.ssreflect + coq-core.plugins.ssrsearch + coq-core.plugins.derive)) (include_subdirs qualified) diff --git a/theories/extraction/ExtrOCamlInt63.v b/theories/extraction/ExtrOCamlInt63.v index 7f7b4af98d..1949a1a9d8 100644 --- a/theories/extraction/ExtrOCamlInt63.v +++ b/theories/extraction/ExtrOCamlInt63.v @@ -10,7 +10,7 @@ (** Extraction to OCaml of native 63-bit machine integers. *) -From Coq Require Int63 Extraction. +From Coq Require Int63 Sint63 Extraction. (** Basic data types used by some primitive operators. *) @@ -26,6 +26,7 @@ Extraction Inline Int63.int. Extract Constant Int63.lsl => "Uint63.l_sl". Extract Constant Int63.lsr => "Uint63.l_sr". +Extract Constant Sint63.asr => "Uint63.a_sr". Extract Constant Int63.land => "Uint63.l_and". Extract Constant Int63.lor => "Uint63.l_or". Extract Constant Int63.lxor => "Uint63.l_xor". @@ -36,10 +37,15 @@ Extract Constant Int63.mul => "Uint63.mul". Extract Constant Int63.mulc => "Uint63.mulc". Extract Constant Int63.div => "Uint63.div". Extract Constant Int63.mod => "Uint63.rem". +Extract Constant Sint63.div => "Uint63.divs". +Extract Constant Sint63.rem => "Uint63.rems". + Extract Constant Int63.eqb => "Uint63.equal". Extract Constant Int63.ltb => "Uint63.lt". Extract Constant Int63.leb => "Uint63.le". +Extract Constant Sint63.ltb => "Uint63.lts". +Extract Constant Sint63.leb => "Uint63.les". Extract Constant Int63.addc => "Uint63.addc". Extract Constant Int63.addcarryc => "Uint63.addcarryc". @@ -51,6 +57,7 @@ Extract Constant Int63.diveucl_21 => "Uint63.div21". Extract Constant Int63.addmuldiv => "Uint63.addmuldiv". Extract Constant Int63.compare => "Uint63.compare". +Extract Constant Sint63.compare => "Uint63.compares". Extract Constant Int63.head0 => "Uint63.head0". Extract Constant Int63.tail0 => "Uint63.tail0". |