diff options
Diffstat (limited to 'theories')
| -rw-r--r-- | theories/Array/PArray.v | 19 | ||||
| -rw-r--r-- | theories/Init/Tactics.v | 9 | ||||
| -rw-r--r-- | theories/Reals/RIneq.v | 60 | ||||
| -rw-r--r-- | theories/extraction/ExtrOCamlPArray.v | 1 | ||||
| -rw-r--r-- | theories/micromega/Zify.v | 15 | ||||
| -rw-r--r-- | theories/micromega/ZifyInt63.v | 178 | ||||
| -rw-r--r-- | theories/omega/PreOmega.v | 2 | ||||
| -rw-r--r-- | theories/ssr/ssrbool.v | 13 |
8 files changed, 237 insertions, 60 deletions
diff --git a/theories/Array/PArray.v b/theories/Array/PArray.v index 3511ba0918..e91a5bf9ad 100644 --- a/theories/Array/PArray.v +++ b/theories/Array/PArray.v @@ -22,12 +22,6 @@ Arguments length {_} _. Primitive copy : forall A, array A -> array A := #array_copy. Arguments copy {_} _. -(* [reroot t] produces an array that is extensionaly equal to [t], but whose - history has been squashed. Useful when performing multiple accesses in an old - copy of an array that has been updated. *) -Primitive reroot : forall A, array A -> array A := #array_reroot. -Arguments reroot {_} _. - Module Export PArrayNotations. Declare Scope array_scope. @@ -64,9 +58,6 @@ Axiom length_set : forall A t i (a:A), Axiom get_copy : forall A (t:array A) i, (copy t).[i] = t.[i]. Axiom length_copy : forall A (t:array A), length (copy t) = length t. -Axiom get_reroot : forall A (t:array A) i, (reroot t).[i] = t.[i]. -Axiom length_reroot : forall A (t:array A), length (reroot t) = length t. - Axiom array_ext : forall A (t1 t2:array A), length t1 = length t2 -> (forall i, i <? length t1 = true -> t1.[i] = t2.[i]) -> @@ -94,16 +85,6 @@ Proof. rewrite !get_out_of_bounds in get_make; assumption. Qed. -Lemma default_reroot A (t:array A) : default (reroot t) = default t. -Proof. - assert (irr_lt : length t <? length t = false). - destruct (Int63.ltbP (length t) (length t)); try reflexivity. - exfalso; eapply BinInt.Z.lt_irrefl; eassumption. - assert (get_reroot := get_reroot A t (length t)). - rewrite !get_out_of_bounds in get_reroot; try assumption. - rewrite length_reroot; assumption. -Qed. - Lemma get_set_same_default A (t : array A) (i : int) : t.[i <- default t].[i] = default t. Proof. diff --git a/theories/Init/Tactics.v b/theories/Init/Tactics.v index e1db68aea9..35bab1021e 100644 --- a/theories/Init/Tactics.v +++ b/theories/Init/Tactics.v @@ -245,13 +245,16 @@ Tactic Notation "clear" "dependent" hyp(h) := Tactic Notation "revert" "dependent" hyp(h) := generalize dependent h. -(** Provide an error message for dependent induction that reports an import is -required to use it. Importing Coq.Program.Equality will shadow this notation -with the actual [dependent induction] tactic. *) +(** Provide an error message for dependent induction/dependent destruction that + reports an import is required to use it. Importing Coq.Program.Equality will + shadow this notation with the actual tactics. *) Tactic Notation "dependent" "induction" ident(H) := fail "To use dependent induction, first [Require Import Coq.Program.Equality.]". +Tactic Notation "dependent" "destruction" ident(H) := + fail "To use dependent destruction, first [Require Import Coq.Program.Equality.]". + (** *** [inversion_sigma] *) (** The built-in [inversion] will frequently leave equalities of dependent pairs. When the first type in the pair is an hProp or diff --git a/theories/Reals/RIneq.v b/theories/Reals/RIneq.v index 4fa8b3216a..993b7b3ec4 100644 --- a/theories/Reals/RIneq.v +++ b/theories/Reals/RIneq.v @@ -459,12 +459,12 @@ Lemma Rplus_eq_0_l : forall r1 r2, 0 <= r1 -> 0 <= r2 -> r1 + r2 = 0 -> r1 = 0. Proof. intros a b H [H0| H0] H1; auto with real. - absurd (0 < a + b). - rewrite H1; auto with real. - apply Rle_lt_trans with (a + 0). - rewrite Rplus_0_r; assumption. - auto using Rplus_lt_compat_l with real. - rewrite <- H0, Rplus_0_r in H1; assumption. + - absurd (0 < a + b). + + rewrite H1; auto with real. + + apply Rle_lt_trans with (a + 0). + * rewrite Rplus_0_r; assumption. + * auto using Rplus_lt_compat_l with real. + - rewrite <- H0, Rplus_0_r in H1; assumption. Qed. Lemma Rplus_eq_R0 : @@ -1529,7 +1529,7 @@ Qed. Lemma Rinv_1_lt_contravar : forall r1 r2, 1 <= r1 -> r1 < r2 -> / r2 < / r1. Proof. - intros x y H' H'0. + intros x y H' H'0. cut (0 < x); [ intros Lt0 | apply Rlt_le_trans with (r2 := 1) ]; auto with real. apply Rmult_lt_reg_l with (r := x); auto with real. @@ -1753,11 +1753,11 @@ Qed. Lemma INR_IPR : forall p, INR (Pos.to_nat p) = IPR p. Proof. assert (H: forall p, 2 * INR (Pos.to_nat p) = IPR_2 p). - induction p as [p|p|] ; simpl IPR_2. + { induction p as [p|p|] ; simpl IPR_2. rewrite Pos2Nat.inj_xI, S_INR, mult_INR, <- IHp. now rewrite (Rplus_comm (2 * _)). now rewrite Pos2Nat.inj_xO, mult_INR, <- IHp. - apply Rmult_1_r. + apply Rmult_1_r. } intros [p|p|] ; unfold IPR. rewrite Pos2Nat.inj_xI, S_INR, mult_INR, <- H. apply Rplus_comm. @@ -1830,12 +1830,12 @@ Qed. Lemma pow_IZR : forall z n, pow (IZR z) n = IZR (Z.pow z (Z.of_nat n)). Proof. - intros z [|n];simpl;trivial. - rewrite Zpower_pos_nat. - rewrite SuccNat2Pos.id_succ. unfold Zpower_nat;simpl. - rewrite mult_IZR. - induction n;simpl;trivial. - rewrite mult_IZR;ring[IHn]. + intros z [|n];simpl;trivial. + rewrite Zpower_pos_nat. + rewrite SuccNat2Pos.id_succ. unfold Zpower_nat;simpl. + rewrite mult_IZR. + induction n;simpl;trivial. + rewrite mult_IZR;ring[IHn]. Qed. (**********) @@ -2043,7 +2043,7 @@ Proof. Qed. Lemma Ropp_div : forall x y, -x/y = - (x / y). -intros x y; unfold Rdiv; ring. + intros x y; unfold Rdiv; ring. Qed. Lemma Ropp_div_den : forall x y : R, y<>0 -> x / - y = - (x / y). @@ -2068,22 +2068,22 @@ Lemma R_rm : ring_morph 0%R 1%R Rplus Rmult Rminus Ropp eq 0%Z 1%Z Zplus Zmult Zminus Z.opp Zeq_bool IZR. Proof. -constructor ; try easy. -exact plus_IZR. -exact minus_IZR. -exact mult_IZR. -exact opp_IZR. -intros x y H. -apply f_equal. -now apply Zeq_bool_eq. + constructor ; try easy. + - exact plus_IZR. + - exact minus_IZR. + - exact mult_IZR. + - exact opp_IZR. + - intros x y H. + apply f_equal. + now apply Zeq_bool_eq. Qed. Lemma Zeq_bool_IZR x y : IZR x = IZR y -> Zeq_bool x y = true. Proof. -intros H. -apply Zeq_is_eq_bool. -now apply eq_IZR. + intros H. + apply Zeq_is_eq_bool. + now apply eq_IZR. Qed. Add Field RField : Rfield @@ -2127,15 +2127,15 @@ Qed. Lemma Rdiv_lt_0_compat : forall a b, 0 < a -> 0 < b -> 0 < a/b. Proof. -intros; apply Rmult_lt_0_compat;[|apply Rinv_0_lt_compat]; assumption. + intros; apply Rmult_lt_0_compat;[|apply Rinv_0_lt_compat]; assumption. Qed. Lemma Rdiv_plus_distr : forall a b c, (a + b)/c = a/c + b/c. -intros a b c; apply Rmult_plus_distr_r. + intros a b c; apply Rmult_plus_distr_r. Qed. Lemma Rdiv_minus_distr : forall a b c, (a - b)/c = a/c - b/c. -intros a b c; unfold Rminus, Rdiv; rewrite Rmult_plus_distr_r; ring. + intros a b c; unfold Rminus, Rdiv; rewrite Rmult_plus_distr_r; ring. Qed. (* A test for equality function. *) diff --git a/theories/extraction/ExtrOCamlPArray.v b/theories/extraction/ExtrOCamlPArray.v index 67646bdb53..56d40c1d16 100644 --- a/theories/extraction/ExtrOCamlPArray.v +++ b/theories/extraction/ExtrOCamlPArray.v @@ -23,4 +23,3 @@ Extract Constant PArray.default => "Parray.default". Extract Constant PArray.set => "Parray.set". Extract Constant PArray.length => "Parray.length". Extract Constant PArray.copy => "Parray.copy". -Extract Constant PArray.reroot => "Parray.reroot". diff --git a/theories/micromega/Zify.v b/theories/micromega/Zify.v index 183fd6a914..01cc9ad810 100644 --- a/theories/micromega/Zify.v +++ b/theories/micromega/Zify.v @@ -16,11 +16,22 @@ Ltac zify_pre_hook := idtac. Ltac zify_post_hook := idtac. -Ltac iter_specs := zify_iter_specs. +Ltac zify_convert_to_euclidean_division_equations_flag := constr:(false). + +(** [zify_internal_to_euclidean_division_equations] is bound in [PreOmega] *) +Ltac zify_internal_to_euclidean_division_equations := idtac. + +Ltac zify_to_euclidean_division_equations := + lazymatch zify_convert_to_euclidean_division_equations_flag with + | true => zify_internal_to_euclidean_division_equations + | false => idtac + end. + Ltac zify := intros; zify_pre_hook ; zify_elim_let ; zify_op ; (zify_iter_specs) ; - zify_saturate ; zify_post_hook. + zify_saturate ; + zify_to_euclidean_division_equations ; zify_post_hook. diff --git a/theories/micromega/ZifyInt63.v b/theories/micromega/ZifyInt63.v new file mode 100644 index 0000000000..27845898aa --- /dev/null +++ b/theories/micromega/ZifyInt63.v @@ -0,0 +1,178 @@ +Require Import ZArith. +Require Import Int63. +Require Import ZifyBool. +Import ZifyClasses. + +Lemma to_Z_bounded : forall x, (0 <= to_Z x < 9223372036854775808)%Z. +Proof. apply to_Z_bounded. Qed. + +Instance Inj_int_Z : InjTyp int Z := + mkinj _ _ to_Z (fun x => 0 <= x < 9223372036854775808)%Z to_Z_bounded. +Add Zify InjTyp Inj_int_Z. + +Instance Op_max_int : CstOp max_int := + { TCst := 9223372036854775807 ; TCstInj := eq_refl }. +Add Zify CstOp Op_max_int. + +Instance Op_digits : CstOp digits := + { TCst := 63 ; TCstInj := eq_refl }. +Add Zify CstOp Op_digits. + +Instance Op_size : CstOp size := + { TCst := 63 ; TCstInj := eq_refl }. +Add Zify CstOp Op_size. + +Instance Op_wB : CstOp wB := + { TCst := 2^63 ; TCstInj := eq_refl }. +Add Zify CstOp Op_wB. + +Lemma ltb_lt : forall n m, + (n <? m)%int63 = (φ (n)%int63 <? φ (m)%int63)%Z. +Proof. + intros. apply Bool.eq_true_iff_eq. + rewrite ltb_spec. rewrite <- Z.ltb_lt. + apply iff_refl. +Qed. + +Instance Op_ltb : BinOp ltb := + {| TBOp := Z.ltb; TBOpInj := ltb_lt |}. +Add Zify BinOp Op_ltb. + +Lemma leb_le : forall n m, + (n <=? m)%int63 = (φ (n)%int63 <=? φ (m)%int63)%Z. +Proof. + intros. apply Bool.eq_true_iff_eq. + rewrite leb_spec. rewrite <- Z.leb_le. + apply iff_refl. +Qed. + +Instance Op_leb : BinOp leb := + {| TBOp := Z.leb; TBOpInj := leb_le |}. +Add Zify BinOp Op_leb. + +Lemma eqb_eq : forall n m, + (n =? m)%int63 = (φ (n)%int63 =? φ (m)%int63)%Z. +Proof. + intros. apply Bool.eq_true_iff_eq. + rewrite eqb_spec. rewrite Z.eqb_eq. + split ; intro H. + now subst; reflexivity. + now apply to_Z_inj in H. +Qed. + +Instance Op_eqb : BinOp eqb := + {| TBOp := Z.eqb; TBOpInj := eqb_eq |}. +Add Zify BinOp Op_eqb. + +Lemma eq_int_inj : forall n m : int, n = m <-> (φ n = φ m)%int63. +Proof. + split; intro H. + rewrite H ; reflexivity. + apply to_Z_inj; auto. +Qed. + +Instance Op_eq : BinRel (@eq int) := + {| TR := @eq Z; TRInj := eq_int_inj |}. +Add Zify BinRel Op_eq. + +Instance Op_add : BinOp add := + {| TBOp := fun x y => (x + y) mod 9223372036854775808%Z; TBOpInj := add_spec |}%Z. +Add Zify BinOp Op_add. + +Instance Op_sub : BinOp sub := + {| TBOp := fun x y => (x - y) mod 9223372036854775808%Z; TBOpInj := sub_spec |}%Z. +Add Zify BinOp Op_sub. + +Instance Op_opp : UnOp Int63.opp := + {| TUOp := (fun x => (- x) mod 9223372036854775808)%Z; TUOpInj := (sub_spec 0) |}%Z. +Add Zify UnOp Op_opp. + +Instance Op_oppcarry : UnOp oppcarry := + {| TUOp := (fun x => 2^63 - x - 1)%Z; TUOpInj := oppcarry_spec |}%Z. +Add Zify UnOp Op_oppcarry. + +Instance Op_succ : UnOp succ := + {| TUOp := (fun x => (x + 1) mod 2^63)%Z; TUOpInj := succ_spec |}%Z. +Add Zify UnOp Op_succ. + +Instance Op_pred : UnOp Int63.pred := + {| TUOp := (fun x => (x - 1) mod 2^63)%Z; TUOpInj := pred_spec |}%Z. +Add Zify UnOp Op_pred. + +Instance Op_mul : BinOp mul := + {| TBOp := fun x y => (x * y) mod 9223372036854775808%Z; TBOpInj := mul_spec |}%Z. +Add Zify BinOp Op_mul. + +Instance Op_gcd : BinOp gcd:= + {| TBOp := (fun x y => Zgcd_alt.Zgcdn (2 * 63)%nat y x) ; TBOpInj := to_Z_gcd |}. +Add Zify BinOp Op_gcd. + +Instance Op_mod : BinOp Int63.mod := + {| TBOp := Z.modulo ; TBOpInj := mod_spec |}. +Add Zify BinOp Op_mod. + +Instance Op_subcarry : BinOp subcarry := + {| TBOp := (fun x y => (x - y - 1) mod 2^63)%Z ; TBOpInj := subcarry_spec |}. +Add Zify BinOp Op_subcarry. + +Instance Op_addcarry : BinOp addcarry := + {| TBOp := (fun x y => (x + y + 1) mod 2^63)%Z ; TBOpInj := addcarry_spec |}. +Add Zify BinOp Op_addcarry. + +Instance Op_lsr : BinOp lsr := + {| TBOp := (fun x y => x / 2^ y)%Z ; TBOpInj := lsr_spec |}. +Add Zify BinOp Op_lsr. + +Instance Op_lsl : BinOp lsl := + {| TBOp := (fun x y => (x * 2^ y) mod 2^ 63)%Z ; TBOpInj := lsl_spec |}. +Add Zify BinOp Op_lsl. + +Instance Op_lor : BinOp Int63.lor := + {| TBOp := Z.lor ; TBOpInj := lor_spec' |}. +Add Zify BinOp Op_lor. + +Instance Op_land : BinOp Int63.land := + {| TBOp := Z.land ; TBOpInj := land_spec' |}. +Add Zify BinOp Op_land. + +Instance Op_lxor : BinOp Int63.lxor := + {| TBOp := Z.lxor ; TBOpInj := lxor_spec' |}. +Add Zify BinOp Op_lxor. + +Instance Op_div : BinOp div := + {| TBOp := Z.div ; TBOpInj := div_spec |}. +Add Zify BinOp Op_div. + +Instance Op_bit : BinOp bit := + {| TBOp := Z.testbit ; TBOpInj := bitE |}. +Add Zify BinOp Op_bit. + +Instance Op_of_Z : UnOp of_Z := + { TUOp := (fun x => x mod 9223372036854775808)%Z; TUOpInj := of_Z_spec }. +Add Zify UnOp Op_of_Z. + +Instance Op_to_Z : UnOp to_Z := + { TUOp := fun x => x ; TUOpInj := fun x : int => eq_refl }. +Add Zify UnOp Op_to_Z. + +Instance Op_is_zero : UnOp is_zero := + { TUOp := (Z.eqb 0) ; TUOpInj := is_zeroE }. +Add Zify UnOp Op_is_zero. + +Lemma is_evenE : forall x, + is_even x = Z.even φ (x)%int63. +Proof. + intros. + generalize (is_even_spec x). + rewrite Z_evenE. + destruct (is_even x). + symmetry. apply Z.eqb_eq. auto. + symmetry. apply Z.eqb_neq. congruence. +Qed. + +Instance Op_is_even : UnOp is_even := + { TUOp := Z.even ; TUOpInj := is_evenE }. +Add Zify UnOp Op_is_even. + + +Ltac Zify.zify_convert_to_euclidean_division_equations_flag ::= constr:(true). diff --git a/theories/omega/PreOmega.v b/theories/omega/PreOmega.v index 506a4108ee..70f25e7243 100644 --- a/theories/omega/PreOmega.v +++ b/theories/omega/PreOmega.v @@ -573,4 +573,6 @@ Ltac zify_N := repeat zify_N_rel; repeat zify_N_op; unfold Z_of_N' in *. Require Import ZifyClasses ZifyInst. Require Zify. +Ltac Zify.zify_internal_to_euclidean_division_equations ::= Z.to_euclidean_division_equations. + Ltac zify := Zify.zify. diff --git a/theories/ssr/ssrbool.v b/theories/ssr/ssrbool.v index f35da63fd6..e8a036bbb0 100644 --- a/theories/ssr/ssrbool.v +++ b/theories/ssr/ssrbool.v @@ -1401,8 +1401,8 @@ Definition mem T (pT : predType T) : pT -> mem_pred T := let: PredType toP := pT in fun A => Mem [eta toP A]. Arguments mem {T pT} A : rename, simpl never. -Notation "x \in A" := (in_mem x (mem A)) : bool_scope. -Notation "x \in A" := (in_mem x (mem A)) : bool_scope. +Notation "x \in A" := (in_mem x (mem A)) (only parsing) : bool_scope. +Notation "x \in A" := (in_mem x (mem A)) (only printing) : bool_scope. Notation "x \notin A" := (~~ (x \in A)) : bool_scope. Notation "A =i B" := (eq_mem (mem A) (mem B)) : type_scope. Notation "{ 'subset' A <= B }" := (sub_mem (mem A) (mem B)) : type_scope. @@ -1573,9 +1573,12 @@ Arguments has_quality n {T}. Lemma qualifE n T p x : (x \in @Qualifier n T p) = p x. Proof. by []. Qed. -Notation "x \is A" := (x \in has_quality 0 A) : bool_scope. -Notation "x \is 'a' A" := (x \in has_quality 1 A) : bool_scope. -Notation "x \is 'an' A" := (x \in has_quality 2 A) : bool_scope. +Notation "x \is A" := (x \in has_quality 0 A) (only parsing) : bool_scope. +Notation "x \is A" := (x \in has_quality 0 A) (only printing) : bool_scope. +Notation "x \is 'a' A" := (x \in has_quality 1 A) (only parsing) : bool_scope. +Notation "x \is 'a' A" := (x \in has_quality 1 A) (only printing) : bool_scope. +Notation "x \is 'an' A" := (x \in has_quality 2 A) (only parsing) : bool_scope. +Notation "x \is 'an' A" := (x \in has_quality 2 A) (only printing) : bool_scope. Notation "x \isn't A" := (x \notin has_quality 0 A) : bool_scope. Notation "x \isn't 'a' A" := (x \notin has_quality 1 A) : bool_scope. Notation "x \isn't 'an' A" := (x \notin has_quality 2 A) : bool_scope. |