diff --git a/BigN/BigN.v b/BigN/BigN.v index fff3d4b..e141d08 100644 --- a/BigN/BigN.v +++ b/BigN/BigN.v @@ -97,7 +97,7 @@ constructor. intros. red. rewrite BigN.spec_pow, BigN.spec_of_N. rewrite Zpower_theory.(rpow_pow_N). destruct n; simpl. reflexivity. -induction p; simpl; intros; BigN.zify; rewrite ?IHp; auto. +induction p; simpl; intros; BigN.zify_strat; rewrite ?IHp; auto. Qed. Lemma BigNdiv : div_theory BigN.eq BigN.add BigN.mul (@id _) @@ -106,13 +106,13 @@ Proof. constructor. unfold id. intros a b. BigN.zify. case Z.eqb_spec. -BigN.zify. auto with zarith. +BigN.zify_strat. auto with zarith. intros NEQ. generalize (BigN.spec_div_eucl a b). generalize (Z_div_mod_full (BigN.to_Z a) (BigN.to_Z b) NEQ). destruct BigN.div_eucl as (q,r), Z.div_eucl as (q',r'). intros (EQ,_). injection 1 as EQr EQq. -BigN.zify. rewrite EQr, EQq; auto. +BigN.zify_strat. rewrite EQr, EQq; auto. Qed. @@ -193,5 +193,5 @@ End TestOrder. Section TestLia. Let test : forall x y : bigN, x<=y -> y<=x -> x==y. -Proof. intros x y. BigN.zify. lia. Defined. +Proof. intros x y. BigN.zify_strat. lia. Defined. End TestLia. diff --git a/BigQ/BigQ.v b/BigQ/BigQ.v index 145ae72..70d39b1 100644 --- a/BigQ/BigQ.v +++ b/BigQ/BigQ.v @@ -105,7 +105,7 @@ Declare Equivalent Keys pow_N pow_pos. Lemma BigQpowerth : power_theory 1 BigQ.mul BigQ.eq Z.of_N BigQ.power. Proof. -constructor. intros. BigQ.qify. +constructor. intros. BigQ.qify_strat. replace (BigQ.to_Q r ^ Z.of_N n)%Q with (pow_N 1 Qmult (BigQ.to_Q r) n)%Q by (now destruct n). destruct n. reflexivity. induction p; simpl; auto; rewrite ?BigQ.spec_mul, ?IHp; reflexivity. @@ -178,5 +178,5 @@ End TestOrder. Section TestQify. Let test : forall x : bigQ, 0+x == 1*x. -Proof. intro x. BigQ.qify. ring. Defined. +Proof. intro x. BigQ.qify_strat. ring. Defined. End TestQify. diff --git a/BigQ/QMake.v b/BigQ/QMake.v index a6f4787..4523081 100644 --- a/BigQ/QMake.v +++ b/BigQ/QMake.v @@ -94,8 +94,14 @@ Module Make (NN:NType)(ZZ:ZType)(Import NZ:NType_ZType NN ZZ) <: QType. spec_Z_of_N spec_Zabs_N : nz. + Ltac nzsimpl_strat := try rewrite_strat (repeat (topdown (hints nz))). Ltac nzsimpl := autorewrite with nz in *. + Ltac qsimpl_strat := try red; unfold to_Q; simpl; intros; + destr_eqb; simpl; nzsimpl_strat; intros; + rewrite ?Z2Pos.id by auto; + auto. + Ltac qsimpl := try red; unfold to_Q; simpl; intros; destr_eqb; simpl; nzsimpl; intros; rewrite ?Z2Pos.id by auto; @@ -120,17 +126,17 @@ Module Make (NN:NType)(ZZ:ZType)(Import NZ:NType_ZType NN ZZ) <: QType. Lemma spec_0: [zero] == 0. Proof. - simpl. nzsimpl. reflexivity. + simpl. nzsimpl_strat. reflexivity. Qed. Lemma spec_1: [one] == 1. Proof. - simpl. nzsimpl. reflexivity. + simpl. nzsimpl_strat. reflexivity. Qed. Lemma spec_m1: [minus_one] == -(1). Proof. - simpl. nzsimpl. reflexivity. + simpl. nzsimpl_strat. reflexivity. Qed. Definition compare (x y: t) := @@ -155,7 +161,7 @@ Module Make (NN:NType)(ZZ:ZType)(Import NZ:NType_ZType NN ZZ) <: QType. Theorem spec_compare: forall q1 q2, (compare q1 q2) = ([q1] ?= [q2]). Proof. intros [z1 | x1 y1] [z2 | x2 y2]; - unfold Qcompare, compare; qsimpl. + unfold Qcompare, compare; qsimpl_strat. Qed. Definition lt n m := [n] < [m]. @@ -198,11 +204,11 @@ Module Make (NN:NType)(ZZ:ZType)(Import NZ:NType_ZType NN ZZ) <: QType. Theorem strong_spec_check_int : forall n d, [check_int n d] = [Qq n d]. Proof. intros; unfold check_int. - nzsimpl. + nzsimpl_strat. destr_zcompare. - simpl. rewrite <- H; qsimpl. congruence. + simpl. rewrite <- H; qsimpl_strat. congruence. reflexivity. - qsimpl. lia. + qsimpl_strat. lia. Qed. (** Normalisation function *) @@ -220,19 +226,19 @@ Module Make (NN:NType)(ZZ:ZType)(Import NZ:NType_ZType NN ZZ) <: QType. intros p q; unfold norm. assert (Hp := NN.spec_pos (Zabs_N p)). assert (Hq := NN.spec_pos q). - nzsimpl. + nzsimpl_strat. destr_zcompare. (* Eq *) rewrite strong_spec_check_int; reflexivity. (* Lt *) rewrite strong_spec_check_int. - qsimpl. + qsimpl_strat. generalize (Zgcd_div_pos (ZZ.to_Z p) (NN.to_Z q)). lia. replace (NN.to_Z q) with 0%Z in * by (symmetry; assumption). rewrite Zdiv_0_l in *; auto with zarith. apply Z.gcd_div_swap; lia. (* Gt *) - qsimpl. + qsimpl_strat. assert (H' : Z.gcd (ZZ.to_Z p) (NN.to_Z q) = 0%Z). generalize (Z.gcd_nonneg (ZZ.to_Z p) (NN.to_Z q)); lia. symmetry; apply (Z.gcd_eq_0_l _ _ H'); auto. @@ -247,12 +253,12 @@ Module Make (NN:NType)(ZZ:ZType)(Import NZ:NType_ZType NN ZZ) <: QType. unfold norm. assert (Hp := NN.spec_pos (Zabs_N p)). assert (Hq := NN.spec_pos q). - nzsimpl. + nzsimpl_strat. destr_zcompare; rewrite ?strong_spec_check_int. (* Eq *) - qsimpl. + qsimpl_strat. (* Lt *) - qsimpl. + qsimpl_strat. destruct (Z_lt_le_dec 0 (NN.to_Z q)). apply Z.gcd_div_gcd; auto with zarith. replace (NN.to_Z q) with 0%Z in * by lia. @@ -311,7 +317,7 @@ Module Make (NN:NType)(ZZ:ZType)(Import NZ:NType_ZType NN ZZ) <: QType. Theorem spec_add : forall x y, [add x y] == [x] + [y]. Proof. - intros [x | nx dx] [y | ny dy]; unfold Qplus; qsimpl. + intros [x | nx dx] [y | ny dy]; unfold Qplus; qsimpl_strat. 1-2, 4, 6: lia. rewrite Pos.mul_1_r, Z2Pos.id; auto. rewrite Pos.mul_1_r, Z2Pos.id; auto. @@ -357,7 +363,7 @@ Module Make (NN:NType)(ZZ:ZType)(Import NZ:NType_ZType NN ZZ) <: QType. [ | rewrite spec_add, spec_add_norm; apply Qeq_refl ]. rewrite <- strong_spec_red. destruct x as [zx|nx dx]; destruct y as [zy|ny dy]; - simpl; destr_eqb; nzsimpl; simpl; auto. + simpl; destr_eqb; nzsimpl_strat; simpl; auto. Qed. Definition opp (x: t): t := @@ -428,12 +434,12 @@ Module Make (NN:NType)(ZZ:ZType)(Import NZ:NType_ZType NN ZZ) <: QType. Theorem spec_mul : forall x y, [mul x y] == [x] * [y]. Proof. - intros [x | nx dx] [y | ny dy]; unfold Qmult; simpl; qsimpl. + intros [x | nx dx] [y | ny dy]; unfold Qmult; simpl; qsimpl_strat. rewrite Pos.mul_1_r, Z2Pos.id; auto. rewrite Z.mul_eq_0 in *; intuition lia. nsubst; auto with zarith. nsubst; auto with zarith. - nsubst; nzsimpl; auto with zarith. + nsubst; nzsimpl_strat; auto with zarith. rewrite Pos2Z.inj_mul, 2 Z2Pos.id; auto. Qed. @@ -443,7 +449,7 @@ Module Make (NN:NType)(ZZ:ZType)(Import NZ:NType_ZType NN ZZ) <: QType. Lemma spec_norm_denum : forall n d, [norm_denum n d] == [Qq n d]. Proof. - unfold norm_denum; intros; simpl; qsimpl. + unfold norm_denum; intros; simpl; qsimpl_strat. congruence. nsubst; auto with zarith. Qed. @@ -462,8 +468,8 @@ Module Make (NN:NType)(ZZ:ZType)(Import NZ:NType_ZType NN ZZ) <: QType. intros. unfold irred; nzsimpl; simpl. destr_zcompare. - exists 1%Z; nzsimpl; auto. - exists 0%Z; nzsimpl. + exists 1%Z; nzsimpl_strat; auto. + exists 0%Z; nzsimpl_strat. assert (Z.gcd (ZZ.to_Z n) (NN.to_Z d) = 0%Z). generalize (Z.gcd_nonneg (ZZ.to_Z n) (NN.to_Z d)); lia. clear H. @@ -473,9 +479,9 @@ Module Make (NN:NType)(ZZ:ZType)(Import NZ:NType_ZType NN ZZ) <: QType. exists (Z.gcd (ZZ.to_Z n) (NN.to_Z d)). simpl. split. - nzsimpl. + nzsimpl_strat. rewrite Z.mul_comm; symmetry; apply Zdivide_Zdiv_eq; auto using Z.gcd_divide_l with zarith. - nzsimpl. + nzsimpl_strat. rewrite Z.mul_comm; symmetry; apply Zdivide_Zdiv_eq; auto using Z.gcd_divide_r with zarith. Qed. @@ -485,13 +491,13 @@ Module Make (NN:NType)(ZZ:ZType)(Import NZ:NType_ZType NN ZZ) <: QType. intros. unfold irred. split. - nzsimpl; intros. + nzsimpl_strat; intros. destr_zcompare; auto. simpl. - nzsimpl. + nzsimpl_strat. rewrite H, Zdiv_0_l; auto. - nzsimpl; destr_zcompare; simpl; auto. - nzsimpl. + nzsimpl_strat; destr_zcompare; simpl; auto. + nzsimpl_strat. intros. generalize (NN.spec_pos d); intros. destruct (NN.to_Z d); auto. @@ -514,7 +520,7 @@ Module Make (NN:NType)(ZZ:ZType)(Import NZ:NType_ZType NN ZZ) <: QType. apply (Z.gcd_eq_0_r (ZZ.to_Z n)). generalize (Z.gcd_nonneg (ZZ.to_Z n) (NN.to_Z d)); lia. - nzsimpl. + nzsimpl_strat. apply Z.gcd_div_gcd. generalize (NN.spec_pos d); lia. generalize (Z.gcd_nonneg (ZZ.to_Z n) (NN.to_Z d)); lia. @@ -546,13 +552,13 @@ Module Make (NN:NType)(ZZ:ZType)(Import NZ:NType_ZType NN ZZ) <: QType. Lemma spec_mul_norm_Qz_Qq : forall z n d, [mul_norm_Qz_Qq z n d] == [Qq (ZZ.mul z n) d]. Proof. - intros z n d; unfold mul_norm_Qz_Qq; nzsimpl; rewrite Zcompare_gt. - destr_eqb; nzsimpl; intros Hz. - qsimpl; rewrite Hz; auto. + intros z n d; unfold mul_norm_Qz_Qq; nzsimpl_strat; rewrite Zcompare_gt. + destr_eqb; nzsimpl_strat; intros Hz. + qsimpl_strat; rewrite Hz; auto. destruct Z_le_gt_dec as [LE|GT]. - qsimpl. + qsimpl_strat. rewrite spec_norm_denum. - qsimpl. + qsimpl_strat. rewrite Zdiv_gcd_zero in GT; auto with zarith. nsubst. rewrite Zdiv_0_l in *; discriminate. rewrite <- Z.mul_assoc, (Z.mul_comm (ZZ.to_Z n)), Z.mul_assoc. @@ -565,32 +571,32 @@ Module Make (NN:NType)(ZZ:ZType)(Import NZ:NType_ZType NN ZZ) <: QType. Proof. unfold Reduced. rewrite 2 strong_spec_red, 2 Qred_iff. - simpl; nzsimpl. - destr_eqb; intros Hd H; simpl in *; nzsimpl. + simpl; nzsimpl_strat. + destr_eqb; intros Hd H; simpl in *; nzsimpl_strat. - unfold mul_norm_Qz_Qq; nzsimpl; rewrite Zcompare_gt. - destr_eqb; intros Hz; simpl; nzsimpl; simpl; auto. + unfold mul_norm_Qz_Qq; nzsimpl_strat; rewrite Zcompare_gt. + destr_eqb; intros Hz; simpl; nzsimpl_strat; simpl; auto. destruct Z_le_gt_dec. - simpl; nzsimpl. + simpl; nzsimpl_strat. destr_eqb; simpl; nzsimpl; auto with zarith. unfold norm_denum. destr_eqb; simpl; nzsimpl. rewrite Hd, Zdiv_0_l; discriminate. intros _. - destr_eqb; simpl; nzsimpl; auto. - nzsimpl; rewrite Hd, Zdiv_0_l; auto with zarith. + destr_eqb; simpl; nzsimpl_strat; auto. + nzsimpl_strat; rewrite Hd, Zdiv_0_l; auto with zarith. rewrite Z2Pos.id in H; auto. - unfold mul_norm_Qz_Qq; nzsimpl; rewrite Zcompare_gt. - destr_eqb; intros Hz; simpl; nzsimpl; simpl; auto. + unfold mul_norm_Qz_Qq; nzsimpl_strat; rewrite Zcompare_gt. + destr_eqb; intros Hz; simpl; nzsimpl_strat; simpl; auto. destruct Z_le_gt_dec as [H'|H']. simpl; nzsimpl. - destr_eqb; simpl; nzsimpl; auto. + destr_eqb; simpl; nzsimpl_strat; auto. intros. rewrite Z2Pos.id; auto. apply Zgcd_mult_rel_prime; auto. generalize (Z.gcd_eq_0_l (ZZ.to_Z z) (NN.to_Z d)) (Z.gcd_nonneg (ZZ.to_Z z) (NN.to_Z d)); lia. - destr_eqb; simpl; nzsimpl; auto. + destr_eqb; simpl; nzsimpl_strat; auto. unfold norm_denum. destr_eqb; nzsimpl; simpl; destr_eqb; simpl; auto. intros; nzsimpl. @@ -617,7 +623,7 @@ Module Make (NN:NType)(ZZ:ZType)(Import NZ:NType_ZType NN ZZ) <: QType. unfold mul_norm, mul; destruct x; destruct y. apply Qeq_refl. apply spec_mul_norm_Qz_Qq. - rewrite spec_mul_norm_Qz_Qq; qsimpl; ring. + rewrite spec_mul_norm_Qz_Qq; qsimpl_strat; ring. rename t0 into nx, t3 into dy, t2 into ny, t1 into dx. destruct (spec_irred nx dy) as (g & Hg). @@ -627,7 +633,7 @@ Module Make (NN:NType)(ZZ:ZType)(Import NZ:NType_ZType NN ZZ) <: QType. destruct irred as (n1,d1); destruct irred as (n2,d2). simpl @snd in *; destruct Hg as [Hg1 Hg2]; destruct Hg' as [Hg1' Hg2']. rewrite spec_norm_denum. - qsimpl. + qsimpl_strat. match goal with E : (_ * _ = 0)%Z |- _ => rewrite Z.mul_eq_0 in E; destruct E as [Eq|Eq] end. @@ -666,7 +672,7 @@ Module Make (NN:NType)(ZZ:ZType)(Import NZ:NType_ZType NN ZZ) <: QType. destruct irred as (n1,d1); destruct irred as (n2,d2). simpl @snd in *; destruct Hg as [Hg1 Hg2]; destruct Hg' as [Hg1' Hg2']. - unfold norm_denum; qsimpl. + unfold norm_denum; qsimpl_strat. assert (NEQ : NN.to_Z dy <> 0%Z) by (rewrite Hz; intros EQ; rewrite EQ in *; lia). @@ -678,7 +684,7 @@ Module Make (NN:NType)(ZZ:ZType)(Import NZ:NType_ZType NN ZZ) <: QType. revert H H0. rewrite 2 strong_spec_red, 2 Qred_iff; simpl. - destr_eqb; simpl; nzsimpl; try lia; intros. + destr_eqb; simpl; nzsimpl_strat; try lia; intros. rewrite Z2Pos.id in *; auto. apply Zgcd_mult_rel_prime; rewrite Z.gcd_comm; @@ -719,7 +725,7 @@ Module Make (NN:NType)(ZZ:ZType)(Import NZ:NType_ZType NN ZZ) <: QType. rewrite ZZ.spec_compare; destr_zcompare. (* 0 = z *) rewrite <- H. - simpl; nzsimpl; compute; auto. + simpl; nzsimpl_strat; compute; auto. (* 0 < z *) simpl. destr_eqb; nzsimpl; [ intros; rewrite Z.abs_eq in *; lia | intros _ ]. @@ -741,7 +747,7 @@ Module Make (NN:NType)(ZZ:ZType)(Import NZ:NType_ZType NN ZZ) <: QType. rewrite ZZ.spec_compare; destr_zcompare. (* 0 = n *) rewrite <- H. - simpl; nzsimpl. + simpl; nzsimpl_strat. destr_eqb; intros; compute; auto. (* 0 < n *) simpl. @@ -762,7 +768,7 @@ Module Make (NN:NType)(ZZ:ZType)(Import NZ:NType_ZType NN ZZ) <: QType. intros; rewrite Z.abs_neq in *; lia. nsubst; compute; auto. set (n':=ZZ.to_Z n) in *; clearbody n'. - red; simpl; nzsimpl. + red; simpl; nzsimpl_strat. rewrite Z.abs_neq by lia. rewrite Z2Pos.id by lia. unfold Qinv; simpl; destruct n'; simpl; auto; try discriminate. @@ -804,21 +810,21 @@ Module Make (NN:NType)(ZZ:ZType)(Import NZ:NType_ZType NN ZZ) <: QType. simpl. rewrite ZZ.spec_compare; destr_zcompare; auto with qarith. (* Qq n d *) - simpl; nzsimpl; destr_eqb. + simpl; nzsimpl_strat; destr_eqb. destr_zcompare; simpl; auto with qarith. - destr_eqb; nzsimpl; auto with qarith. + destr_eqb; nzsimpl_strat; auto with qarith. intros _ Hd; rewrite Hd; auto with qarith. - destr_eqb; nzsimpl; auto with qarith. + destr_eqb; nzsimpl_strat; auto with qarith. intros _ Hd; rewrite Hd; auto with qarith. (* 0 < n *) destr_zcompare; auto with qarith. - destr_zcompare; nzsimpl; simpl; auto with qarith; intros. - destr_eqb; nzsimpl; [ intros; rewrite Z.abs_eq in *; lia | intros _ ]. + destr_zcompare; nzsimpl_strat; simpl; auto with qarith; intros. + destr_eqb; nzsimpl_strat; [ intros; rewrite Z.abs_eq in *; lia | intros _ ]. rewrite H0; auto with qarith. lia. (* 0 > n *) - destr_zcompare; nzsimpl; simpl; auto with qarith. - destr_eqb; nzsimpl; [ intros; rewrite Z.abs_neq in *; lia | intros _ ]. + destr_zcompare; nzsimpl_strat; simpl; auto with qarith. + destr_eqb; nzsimpl_strat; [ intros; rewrite Z.abs_neq in *; lia | intros _ ]. rewrite H0; auto with qarith. lia. Qed. @@ -830,23 +836,23 @@ Module Make (NN:NType)(ZZ:ZType)(Import NZ:NType_ZType NN ZZ) <: QType. intros. destruct x as [ z | n d ]. (* Qz *) - simpl; nzsimpl. + simpl; nzsimpl_strat. rewrite strong_spec_red, Qred_iff. - destr_zcompare; simpl; nzsimpl; auto. - destr_eqb; nzsimpl; simpl; auto. - destr_eqb; nzsimpl; simpl; auto. + destr_zcompare; simpl; nzsimpl_strat; auto. + destr_eqb; nzsimpl_strat; simpl; auto. + destr_eqb; nzsimpl_strat; simpl; auto. (* Qq n d *) rewrite strong_spec_red, Qred_iff in H; revert H. - simpl; nzsimpl. - destr_eqb; nzsimpl; auto with qarith. - destr_zcompare; simpl; nzsimpl; auto; intros. + simpl; nzsimpl_strat. + destr_eqb; nzsimpl_strat; auto with qarith. + destr_zcompare; simpl; nzsimpl_strat; auto; intros. (* 0 < n *) - destr_zcompare; simpl; nzsimpl; auto. - destr_eqb; nzsimpl; simpl; auto. + destr_zcompare; simpl; nzsimpl_strat; auto. + destr_eqb; nzsimpl_strat; simpl; auto. rewrite Z.abs_eq; lia. intros _. - rewrite strong_spec_norm; simpl; nzsimpl. - destr_eqb; nzsimpl. + rewrite strong_spec_norm; simpl; nzsimpl_strat. + destr_eqb; nzsimpl_strat. rewrite Z.abs_eq; lia. intros _. rewrite Qred_iff. @@ -855,13 +861,13 @@ Module Make (NN:NType)(ZZ:ZType)(Import NZ:NType_ZType NN ZZ) <: QType. rewrite Z2Pos.id in *; auto. rewrite Z.gcd_comm; auto. (* 0 > n *) - destr_eqb; nzsimpl; simpl; auto; intros. - destr_zcompare; simpl; nzsimpl; auto. - destr_eqb; nzsimpl. + destr_eqb; nzsimpl_strat; simpl; auto; intros. + destr_zcompare; simpl; nzsimpl_strat; auto. + destr_eqb; nzsimpl_strat. rewrite Z.abs_neq; lia. intros _. - rewrite strong_spec_norm; simpl; nzsimpl. - destr_eqb; nzsimpl. + rewrite strong_spec_norm; simpl; nzsimpl_strat. + destr_eqb; nzsimpl_strat. rewrite Z.abs_neq; lia. intros _. rewrite Qred_iff. @@ -913,11 +919,11 @@ Module Make (NN:NType)(ZZ:ZType)(Import NZ:NType_ZType NN ZZ) <: QType. destruct x as [ z | n d ]. simpl; rewrite ZZ.spec_square; red; auto. simpl. - destr_eqb; nzsimpl; intros. + destr_eqb; nzsimpl_strat; intros. apply Qeq_refl. - rewrite NN.spec_square in *; nzsimpl. + rewrite NN.spec_square in *; nzsimpl_strat. rewrite Z.mul_eq_0 in *; lia. - rewrite NN.spec_square in *; nzsimpl; nsubst; lia. + rewrite NN.spec_square in *; nzsimpl_strat; nsubst; lia. rewrite ZZ.spec_square, NN.spec_square. red; simpl. rewrite Pos2Z.inj_mul; rewrite !Z2Pos.id; auto. @@ -941,7 +947,7 @@ Module Make (NN:NType)(ZZ:ZType)(Import NZ:NType_ZType NN ZZ) <: QType. (* Qq *) simpl. rewrite ZZ.spec_pow_pos. - destr_eqb; nzsimpl; intros. + destr_eqb; nzsimpl_strat; intros. - apply Qeq_sym; apply Qpower_positive_0. - rewrite NN.spec_pow_pos in *. assert (0 < NN.to_Z d ^ Zpos p)%Z by @@ -964,12 +970,12 @@ Module Make (NN:NType)(ZZ:ZType)(Import NZ:NType_ZType NN ZZ) <: QType. red; simpl; auto. red; simpl; intros. rewrite strong_spec_norm; simpl. - destr_eqb; nzsimpl; intros. + destr_eqb; nzsimpl_strat; intros. simpl; auto. rewrite Qred_iff. revert H. unfold Reduced; rewrite strong_spec_red, Qred_iff; simpl. - destr_eqb; nzsimpl; simpl; intros. + destr_eqb; nzsimpl_strat; simpl; intros. exfalso. rewrite NN.spec_pow_pos in *. nsubst. rewrite Z.pow_0_l' in *; [lia|discriminate]. @@ -988,7 +994,7 @@ Module Make (NN:NType)(ZZ:ZType)(Import NZ:NType_ZType NN ZZ) <: QType. Theorem spec_power : forall x z, [power x z] == [x]^z. Proof. destruct z. - simpl; nzsimpl; red; auto. + simpl; nzsimpl_strat; red; auto. apply spec_power_pos. simpl. rewrite spec_inv, spec_power_pos; apply Qeq_refl. @@ -1004,7 +1010,7 @@ Module Make (NN:NType)(ZZ:ZType)(Import NZ:NType_ZType NN ZZ) <: QType. Theorem spec_power_norm : forall x z, [power_norm x z] == [x]^z. Proof. destruct z. - simpl; nzsimpl; red; auto. + simpl; nzsimpl_strat; red; auto. apply spec_power_pos. simpl. rewrite spec_inv_norm, spec_power_pos; apply Qeq_refl. @@ -1017,7 +1023,7 @@ Module Make (NN:NType)(ZZ:ZType)(Import NZ:NType_ZType NN ZZ) <: QType. destruct z; simpl. intros _; unfold Reduced; rewrite strong_spec_red. unfold one. - simpl to_Q; nzsimpl; auto. + simpl to_Q; nzsimpl_strat; auto. intros; apply strong_spec_power_pos; auto. intros; apply strong_spec_inv_norm; apply strong_spec_power_pos; auto. Qed. diff --git a/BigZ/BigZ.v b/BigZ/BigZ.v index b8be51a..30441d4 100644 --- a/BigZ/BigZ.v +++ b/BigZ/BigZ.v @@ -127,7 +127,7 @@ constructor. intros. unfold BigZ.eq, BigZ_of_N. rewrite BigZ.spec_pow, BigZ.spec_of_Z. rewrite Zpower_theory.(rpow_pow_N). destruct n; simpl. reflexivity. -induction p; simpl; intros; BigZ.zify; rewrite ?IHp; auto. +induction p; simpl; intros; BigZ.zify_strat; rewrite ?IHp; auto. Qed. Lemma BigZdiv : div_theory BigZ.eq BigZ.add BigZ.mul (@id _) @@ -136,13 +136,13 @@ Proof. constructor. unfold id. intros a b. BigZ.zify. case Z.eqb_spec. -BigZ.zify. auto with zarith. +BigZ.zify_strat. auto with zarith. intros NEQ. generalize (BigZ.spec_div_eucl a b). generalize (Z_div_mod_full (BigZ.to_Z a) (BigZ.to_Z b) NEQ). destruct BigZ.div_eucl as (q,r), Z.div_eucl as (q',r'). intros (EQ,_). injection 1 as EQr EQq. -BigZ.zify. rewrite EQr, EQq; auto. +BigZ.zify_strat. rewrite EQr, EQq; auto. Qed. (** Detection of constants *) @@ -207,5 +207,5 @@ End TestOrder. Section TestLia. Let test : forall x y : bigZ, x<=y -> y<=x -> x==y. -Proof. intros x y. BigZ.zify. Lia.lia. Defined. +Proof. intros x y. BigZ.zify_strat. Lia.lia. Defined. End TestLia. diff --git a/CyclicDouble/DoubleSqrt.v b/CyclicDouble/DoubleSqrt.v index 1d7724b..b13c0cb 100644 --- a/CyclicDouble/DoubleSqrt.v +++ b/CyclicDouble/DoubleSqrt.v @@ -18,6 +18,7 @@ Require Import DoubleBase. Local Open Scope Z_scope. Ltac zarith := auto with zarith; fail. +Ltac rm10 := try (rewrite_strat (repeat (topdown (hints rm10)))). Section DoubleSqrt. Variable w : univ_of_cycles. @@ -445,7 +446,7 @@ intros x; case x; simpl ww_is_even. end. apply Z.pow_pos_nonneg; lia. } - unfold ww_digits; autorewrite with rm10. + unfold ww_digits; rm10. assert (tmp: forall p q r, p + (q - r) = p + q - r) by zarith; rewrite tmp; clear tmp. assert (tmp: forall p, p + p = 2 * p) by zarith; @@ -821,9 +822,9 @@ intros x; case x; simpl ww_is_even. assert (V1 := spec_ww_to_Z w_digits w_to_Z spec_to_Z (WW w4 w5)). enough (0 < [[WW w4 w5]]) by zarith. apply Z.lt_le_trans with (wB/ 2 * wB + 0). - autorewrite with rm10; apply Z.mul_pos_pos. + rm10; apply Z.mul_pos_pos. apply Z.mul_lt_mono_pos_r with 2. zarith. - autorewrite with rm10. + rm10. rewrite Z.mul_comm; rewrite wB_div_2. case (spec_to_Z w5);zarith. case (spec_to_Z w5);zarith. @@ -849,9 +850,9 @@ intros x; case x; simpl ww_is_even. rename V1 into VV1. assert (VV2: 0 < [[WW w4 w5]]). apply Z.lt_le_trans with (wB/ 2 * wB + 0). - autorewrite with rm10; apply Z.mul_pos_pos. + rm10; apply Z.mul_pos_pos. apply Z.mul_lt_mono_pos_r with 2. zarith. - autorewrite with rm10. + rm10. rewrite Z.mul_comm, wB_div_2. assert (VV3 := spec_to_Z w5);zarith. assert (VV3 := spec_to_Z w5);zarith. @@ -942,7 +943,7 @@ intros x; case x; simpl ww_is_even. end. assert (V := Zsquare_pos [|w5|]); rewrite Zsquare_mult in V; zarith. - autorewrite with rm10. + rm10. match goal with |- _ <= 2 * (?U * ?V + ?W) => apply Z.le_trans with (2 * U * V + 0) end. @@ -989,7 +990,7 @@ intros x; case x; simpl ww_is_even. end. assert (V1 := Zsquare_pos [|w5|]); rewrite Zsquare_mult in V1; zarith. - autorewrite with rm10. + rm10. match goal with |- _ <= 2 * (?U * ?V + ?W) => apply Z.le_trans with (2 * U * V + 0) end. @@ -1031,9 +1032,9 @@ intros x; case x; simpl ww_is_even. match goal with |- _ <= _ * ?X => apply Z.le_trans with (1 * X); [ | zarith ] end. - autorewrite with rm10. + rm10. rewrite <- wB_div_2; apply Z.mul_le_mono_nonneg_l; zarith. - * rewrite <- V3 in VV; generalize VV; autorewrite with rm10; + * rewrite <- V3 in VV; generalize VV; rm10; clear VV; intros VV. rewrite spec_ww_add_c by zarith. rewrite ww_add_mult_mult_2_plus_1. @@ -1108,7 +1109,7 @@ Qed. generalize (spec_ww_is_even (ww_head0 x)); case_eq (ww_is_even (ww_head0 x)). intros HH H1; rewrite HH; split; auto. intros H2. - generalize (spec_ww_head0 x H2); case (ww_head0 x); autorewrite with rm10. + generalize (spec_ww_head0 x H2); case (ww_head0 x); rm10. intros (H3, H4); split. 2: zarith. apply Z.le_trans with (2 := H3). apply Zdiv_le_compat_l; zarith. @@ -1170,7 +1171,7 @@ Qed. zarith. intros H1. rewrite spec_ww_compare. case Z.compare_spec; - simpl ww_to_Z; autorewrite with rm10. + simpl ww_to_Z; rm10. generalize H1; case x. intros HH; contradict HH; simpl ww_to_Z; zarith. intros w0 w1; simpl ww_to_Z; autorewrite with w_rewrite rm10. @@ -1178,12 +1179,12 @@ Qed. generalize (H4 H2); clear H4; rewrite H5; clear H5; autorewrite with rm10. intros (H4, H5). assert (V: wB/4 <= [|w0|]). { - apply beta_lex with 0 [|w1|] wB. 2-3: zarith. autorewrite with rm10. + apply beta_lex with 0 [|w1|] wB. 2-3: zarith. rm10. rewrite <- wwB_4_wB_4; auto. } generalize (@spec_w_sqrt2 w0 w1 V). case (w_sqrt2 w0 w1); intros w2 c. simpl ww_to_Z; simpl @fst. - case c; unfold interp_carry; autorewrite with rm10. + case c; unfold interp_carry; rm10. intros w3 (H6, H7); rewrite H6. assert (V1 := spec_to_Z w3). split. zarith. @@ -1235,7 +1236,7 @@ Qed. by (rewrite Z.mul_comm; zarith). intros H2. assert (V: wB/4 <= [|w0|]). { - apply beta_lex with 0 [|w1|] wB. 2: zarith. autorewrite with rm10. + apply beta_lex with 0 [|w1|] wB. 2: zarith. rm10. simpl ww_to_Z in H2; rewrite H2. rewrite <- wwB_4_wB_4 by zarith. rewrite Z.mul_comm; zarith. @@ -1260,7 +1261,7 @@ Qed. assert (Hv5: [[(ww_add_mul_div (ww_pred ww_zdigits) W0 (ww_head1 x))]] = [[ww_head1 x]]/2). rewrite spec_ww_add_mul_div. - simpl ww_to_Z; autorewrite with rm10. + simpl ww_to_Z; rm10. rewrite Hv3. ring_simplify (Zpos (xO w_digits) - (Zpos (xO w_digits) - 1)). rewrite Z.pow_1_r. @@ -1277,7 +1278,7 @@ Qed. rewrite spec_w_add_mul_div. rewrite spec_w_sub. rewrite spec_w_0. - simpl ww_to_Z; autorewrite with rm10. + simpl ww_to_Z; rm10. rewrite Hv6; rewrite spec_w_zdigits. rewrite (fun x y => Zmod_small (x - y)). ring_simplify (Zpos w_digits - (Zpos w_digits - [[ww_head1 x]] / 2)). @@ -1304,7 +1305,7 @@ Qed. enough (0 <= Y) by zarith end. case (Z_mod_lt [|w2|] (2 ^ ([[ww_head1 x]] / 2))); zarith. - case c; unfold interp_carry; autorewrite with rm10; + case c; unfold interp_carry; rm10; intros w3; assert (V3 := spec_to_Z w3);zarith. apply Z.mul_lt_mono_pos_r with (2 ^ [[ww_head1 x]]). zarith. rewrite H4. @@ -1326,7 +1327,7 @@ Qed. pattern [|w2|] at 1; rewrite (Z_div_mod_eq_full [|w2|] (2 ^ ([[ww_head1 x]]/2))) by zarith. rewrite <- Z.add_assoc; rewrite Z.mul_add_distr_l. - autorewrite with rm10; apply Z.add_le_mono_l. + rm10; apply Z.add_le_mono_l. case (Z_mod_lt [|w2|] (2 ^ ([[ww_head1 x]]/2))); zarith. split. zarith. apply Z.le_lt_trans with ([|w2|]). 2: zarith. @@ -1334,7 +1335,7 @@ Qed. pattern [|w2|] at 1; replace [|w2|] with ([|w2|] * 2 ^0). apply Z.mul_le_mono_nonneg_l. zarith. apply Zpower_le_monotone; zarith. - rewrite Z.pow_0_r; autorewrite with rm10; auto. + rewrite Z.pow_0_r; rm10; auto. split. rewrite Hv0 in Hv2; rewrite (Pos2Z.inj_xO w_digits) in Hv2; zarith. apply Z.le_lt_trans with (Zpos w_digits). zarith. diff --git a/SpecViaQ/QSig.v b/SpecViaQ/QSig.v index d994090..c42a7ee 100644 --- a/SpecViaQ/QSig.v +++ b/SpecViaQ/QSig.v @@ -105,6 +105,9 @@ Hint Rewrite Ltac qify := unfold eq, lt, le in *; autorewrite with qsimpl; try rewrite spec_0 in *; try rewrite spec_1 in *; try rewrite spec_m1 in *. +Ltac qify_strat := unfold eq, lt, le in *; try (rewrite_strat (repeat (topdown (hints qsimpl)))); + try rewrite spec_0 in *; try rewrite spec_1 in *; try rewrite spec_m1 in *. + (** NB: do not add [spec_0] in the autorewrite database. Otherwise, after instantiation in BigQ, this lemma become convertible to 0=0, and autorewrite loops. Idem for [spec_1] and [spec_m1] *) @@ -114,7 +117,10 @@ Ltac qify := unfold eq, lt, le in *; autorewrite with qsimpl; Ltac solve_wd1 := intros x x' Hx; qify; now rewrite Hx. Ltac solve_wd2 := intros x x' Hx y y' Hy; qify; now rewrite Hx, Hy. -Local Obligation Tactic := solve_wd2 || solve_wd1. +Ltac solve_wd1_strat := intros x x' Hx; qify_strat; now rewrite Hx. +Ltac solve_wd2_strat := intros x x' Hx y y' Hy; qify_strat; now rewrite Hx, Hy. + +Local Obligation Tactic := solve_wd2_strat || solve_wd1_strat. #[global] Instance : Measure to_Q := {}. @@ -158,7 +164,7 @@ Program Instance power_wd : Proper (eq==>Logic.eq==>eq) power. (** Let's implement [HasCompare] *) Lemma compare_spec : forall x y, CompareSpec (x==y) (x x x == y. -Proof. intros. qify. apply Qeq_bool_iff. Qed. +Proof. intros. qify_strat. apply Qeq_bool_iff. Qed. Lemma eqb_correct : forall x y, eq_bool x y = true -> x == y. Proof. now apply eqb_eq. Qed. @@ -191,56 +197,56 @@ Proof. now apply eqb_eq. Qed. (** Let's implement [HasMinMax] *) Lemma max_l : forall x y, y<=x -> max x y == x. -Proof. intros x y. qify. apply Qminmax.Q.max_l. Qed. +Proof. intros x y. qify_strat. apply Qminmax.Q.max_l. Qed. Lemma max_r : forall x y, x<=y -> max x y == y. -Proof. intros x y. qify. apply Qminmax.Q.max_r. Qed. +Proof. intros x y. qify_strat. apply Qminmax.Q.max_r. Qed. Lemma min_l : forall x y, x<=y -> min x y == x. -Proof. intros x y. qify. apply Qminmax.Q.min_l. Qed. +Proof. intros x y. qify_strat. apply Qminmax.Q.min_l. Qed. Lemma min_r : forall x y, y<=x -> min x y == y. -Proof. intros x y. qify. apply Qminmax.Q.min_r. Qed. +Proof. intros x y. qify_strat. apply Qminmax.Q.min_r. Qed. (** Q is a ring *) Lemma add_0_l : forall x, 0+x == x. -Proof. intros. qify. apply Qplus_0_l. Qed. +Proof. intros. qify_strat. apply Qplus_0_l. Qed. Lemma add_comm : forall x y, x+y == y+x. -Proof. intros. qify. apply Qplus_comm. Qed. +Proof. intros. qify_strat. apply Qplus_comm. Qed. Lemma add_assoc : forall x y z, x+(y+z) == x+y+z. -Proof. intros. qify. apply Qplus_assoc. Qed. +Proof. intros. qify_strat. apply Qplus_assoc. Qed. Lemma mul_1_l : forall x, 1*x == x. -Proof. intros. qify. apply Qmult_1_l. Qed. +Proof. intros. qify_strat. apply Qmult_1_l. Qed. Lemma mul_comm : forall x y, x*y == y*x. -Proof. intros. qify. apply Qmult_comm. Qed. +Proof. intros. qify_strat. apply Qmult_comm. Qed. Lemma mul_assoc : forall x y z, x*(y*z) == x*y*z. -Proof. intros. qify. apply Qmult_assoc. Qed. +Proof. intros. qify_strat. apply Qmult_assoc. Qed. Lemma mul_add_distr_r : forall x y z, (x+y)*z == x*z + y*z. -Proof. intros. qify. apply Qmult_plus_distr_l. Qed. +Proof. intros. qify_strat. apply Qmult_plus_distr_l. Qed. Lemma sub_add_opp : forall x y, x-y == x+(-y). -Proof. intros. qify. now unfold Qminus. Qed. +Proof. intros. qify_strat. now unfold Qminus. Qed. Lemma add_opp_diag_r : forall x, x+(-x) == 0. -Proof. intros. qify. apply Qplus_opp_r. Qed. +Proof. intros. qify_strat. apply Qplus_opp_r. Qed. (** Q is a field *) Lemma neq_1_0 : 1!=0. -Proof. intros. qify. apply Q_apart_0_1. Qed. +Proof. intros. qify_strat. apply Q_apart_0_1. Qed. Lemma div_mul_inv : forall x y, x/y == x*(/y). -Proof. intros. qify. now unfold Qdiv. Qed. +Proof. intros. qify_strat. now unfold Qdiv. Qed. Lemma mul_inv_diag_l : forall x, x!=0 -> /x * x == 1. -Proof. intros x. qify. rewrite Qmult_comm. apply Qmult_inv_r. Qed. +Proof. intros x. qify_strat. rewrite Qmult_comm. apply Qmult_inv_r. Qed. End QProperties. diff --git a/SpecViaZ/NSigNAxioms.v b/SpecViaZ/NSigNAxioms.v index 4d24b0b..e62d912 100644 --- a/SpecViaZ/NSigNAxioms.v +++ b/SpecViaZ/NSigNAxioms.v @@ -22,8 +22,10 @@ Hint Rewrite spec_land spec_lor spec_ldiff spec_lxor spec_div2 spec_of_N : nsimpl. Ltac nsimpl := autorewrite with nsimpl. +Ltac nsimpl_strat := try (rewrite_strat (repeat (topdown (hints nsimpl)))). Ltac ncongruence := unfold eq, to_N; repeat red; intros; nsimpl; congruence. Ltac zify := unfold eq, lt, le, to_N in *; nsimpl. +Ltac zify_strat := unfold eq, lt, le, to_N in *; nsimpl_strat. Ltac omega_pos n := generalize (spec_pos n); lia. Local Obligation Tactic := ncongruence. @@ -45,24 +47,24 @@ Program Instance mul_wd : Proper (eq==>eq==>eq) mul. Theorem pred_succ : forall n, pred (succ n) == n. Proof. -intros. zify. omega_pos n. +intros. zify_strat. omega_pos n. Qed. Theorem one_succ : 1 == succ 0. Proof. -now zify. +now zify_strat. Qed. Theorem two_succ : 2 == succ 1. Proof. -now zify. +now zify_strat. Qed. Definition N_of_Z z := of_N (Z.to_N z). Lemma spec_N_of_Z z : (0<=z)%Z -> [N_of_Z z] = z. Proof. - unfold N_of_Z. zify. apply Z2N.id. + unfold N_of_Z. zify_strat. apply Z2N.id. Qed. Section Induction. @@ -105,69 +107,69 @@ End Induction. Theorem add_0_l : forall n, 0 + n == n. Proof. -intros. zify. auto with zarith. +intros. zify_strat. auto with zarith. Qed. Theorem add_succ_l : forall n m, (succ n) + m == succ (n + m). Proof. -intros. zify. auto with zarith. +intros. zify_strat. auto with zarith. Qed. Theorem sub_0_r : forall n, n - 0 == n. Proof. -intros. zify. omega_pos n. +intros. zify_strat. omega_pos n. Qed. Theorem sub_succ_r : forall n m, n - (succ m) == pred (n - m). Proof. -intros. zify. lia. +intros. zify_strat. lia. Qed. Theorem mul_0_l : forall n, 0 * n == 0. Proof. -intros. zify. auto with zarith. +intros. zify_strat. auto with zarith. Qed. Theorem mul_succ_l : forall n m, (succ n) * m == n * m + m. Proof. -intros. zify. ring. +intros. zify_strat. ring. Qed. (** Order *) Lemma eqb_eq x y : eqb x y = true <-> x == y. Proof. - zify. apply Z.eqb_eq. + zify_strat. apply Z.eqb_eq. Qed. Lemma leb_le x y : leb x y = true <-> x <= y. Proof. - zify. apply Z.leb_le. + zify_strat. apply Z.leb_le. Qed. Lemma ltb_lt x y : ltb x y = true <-> x < y. Proof. - zify. apply Z.ltb_lt. + zify_strat. apply Z.ltb_lt. Qed. Lemma compare_eq_iff n m : compare n m = Eq <-> n == m. Proof. - intros. zify. apply Z.compare_eq_iff. + intros. zify_strat. apply Z.compare_eq_iff. Qed. Lemma compare_lt_iff n m : compare n m = Lt <-> n < m. Proof. - intros. zify. reflexivity. + intros. zify_strat. reflexivity. Qed. Lemma compare_le_iff n m : compare n m <> Gt <-> n <= m. Proof. - intros. zify. reflexivity. + intros. zify_strat. reflexivity. Qed. Lemma compare_antisym n m : compare m n = CompOpp (compare n m). Proof. - intros. zify. apply Z.compare_antisym. + intros. zify_strat. apply Z.compare_antisym. Qed. Include BoolOrderFacts NN NN NN [no inline]. @@ -175,25 +177,25 @@ Include BoolOrderFacts NN NN NN [no inline]. #[global] Instance compare_wd : Proper (eq ==> eq ==> Logic.eq) compare. Proof. -intros x x' Hx y y' Hy. zify. now rewrite Hx, Hy. +intros x x' Hx y y' Hy. zify_strat. now rewrite Hx, Hy. Qed. #[global] Instance eqb_wd : Proper (eq ==> eq ==> Logic.eq) eqb. Proof. -intros x x' Hx y y' Hy. zify. now rewrite Hx, Hy. +intros x x' Hx y y' Hy. zify_strat. now rewrite Hx, Hy. Qed. #[global] Instance ltb_wd : Proper (eq ==> eq ==> Logic.eq) ltb. Proof. -intros x x' Hx y y' Hy. zify. now rewrite Hx, Hy. +intros x x' Hx y y' Hy. zify_strat. now rewrite Hx, Hy. Qed. #[global] Instance leb_wd : Proper (eq ==> eq ==> Logic.eq) leb. Proof. -intros x x' Hx y y' Hy. zify. now rewrite Hx, Hy. +intros x x' Hx y y' Hy. zify_strat. now rewrite Hx, Hy. Qed. #[global] @@ -204,34 +206,34 @@ Qed. Theorem lt_succ_r : forall n m, n < succ m <-> n <= m. Proof. -intros. zify. lia. +intros. zify_strat. lia. Qed. Theorem min_l : forall n m, n <= m -> min n m == n. Proof. -now intros n m; zify; lia. +now intros n m; zify_strat; lia. Qed. Theorem min_r : forall n m, m <= n -> min n m == m. Proof. -now intros n m; zify; lia. +now intros n m; zify_strat; lia. Qed. Theorem max_l : forall n m, m <= n -> max n m == n. Proof. -now intros n m; zify; lia. +now intros n m; zify_strat; lia. Qed. Theorem max_r : forall n m, n <= m -> max n m == m. Proof. -now intros n m; zify; lia. +now intros n m; zify_strat; lia. Qed. (** Properties specific to natural numbers, not integers. *) Theorem pred_0 : pred 0 == 0. Proof. -zify. auto. +zify_strat. auto. Qed. (** Power *) @@ -241,40 +243,40 @@ Program Instance pow_wd : Proper (eq==>eq==>eq) pow. Lemma pow_0_r : forall a, a^0 == 1. Proof. - intros. now zify. + intros. now zify_strat. Qed. Lemma pow_succ_r : forall a b, 0<=b -> a^(succ b) == a * a^b. Proof. - intros a b. zify. intros. now Z.nzsimpl. + intros a b. zify_strat. intros. now Z.nzsimpl. Qed. Lemma pow_neg_r : forall a b, b<0 -> a^b == 0. Proof. - intros a b. zify. intro Hb. exfalso. omega_pos b. + intros a b. zify_strat. intro Hb. exfalso. omega_pos b. Qed. Lemma pow_pow_N : forall a b, a^b == pow_N a (to_N b). Proof. - intros. zify. f_equal. + intros. zify_strat. f_equal. now rewrite Z2N.id by apply spec_pos. Qed. Lemma pow_N_pow : forall a b, pow_N a b == a^(of_N b). Proof. - intros. now zify. + intros. now zify_strat. Qed. Lemma pow_pos_N : forall a p, pow_pos a p == pow_N a (Npos p). Proof. - intros. now zify. + intros. now zify_strat. Qed. (** Square *) Lemma square_spec n : square n == n * n. Proof. - now zify. + now zify_strat. Qed. (** Sqrt *) @@ -282,12 +284,12 @@ Qed. Lemma sqrt_spec : forall n, 0<=n -> (sqrt n)*(sqrt n) <= n /\ n < (succ (sqrt n))*(succ (sqrt n)). Proof. - intros n. zify. apply Z.sqrt_spec. + intros n. zify_strat. apply Z.sqrt_spec. Qed. Lemma sqrt_neg : forall n, n<0 -> sqrt n == 0. Proof. - intros n. zify. intro H. exfalso. omega_pos n. + intros n. zify_strat. intro H. exfalso. omega_pos n. Qed. (** Log2 *) @@ -295,13 +297,13 @@ Qed. Lemma log2_spec : forall n, 0 2^(log2 n) <= n /\ n < 2^(succ (log2 n)). Proof. - intros n. zify. change (Z.log2 [n]+1)%Z with (Z.succ (Z.log2 [n])). + intros n. zify_strat. change (Z.log2 [n]+1)%Z with (Z.succ (Z.log2 [n])). apply Z.log2_spec. Qed. Lemma log2_nonpos : forall n, n<=0 -> log2 n == 0. Proof. - intros n. zify. apply Z.log2_nonpos. + intros n. zify_strat. apply Z.log2_nonpos. Qed. (** Even / Odd *) @@ -311,18 +313,18 @@ Definition Odd n := exists m, n == 2*m+1. Lemma even_spec n : even n = true <-> Even n. Proof. - unfold Even. zify. rewrite Z.even_spec. + unfold Even. zify_strat. rewrite Z.even_spec. split; intros (m,Hm). - - exists (N_of_Z m). zify. rewrite spec_N_of_Z; trivial. omega_pos n. - - exists [m]. revert Hm; now zify. + - exists (N_of_Z m). zify_strat. rewrite spec_N_of_Z; trivial. omega_pos n. + - exists [m]. revert Hm; now zify_strat. Qed. Lemma odd_spec n : odd n = true <-> Odd n. Proof. - unfold Odd. zify. rewrite Z.odd_spec. + unfold Odd. zify_strat. rewrite Z.odd_spec. split; intros (m,Hm). - - exists (N_of_Z m). zify. rewrite spec_N_of_Z; trivial. omega_pos n. - - exists [m]. revert Hm; now zify. + - exists (N_of_Z m). zify_strat. rewrite spec_N_of_Z; trivial. omega_pos n. + - exists [m]. revert Hm; now zify_strat. Qed. (** Div / Mod *) @@ -334,13 +336,13 @@ Program Instance mod_wd : Proper (eq==>eq==>eq) modulo. Theorem div_mod : forall a b, ~b==0 -> a == b*(div a b) + (modulo a b). Proof. -intros a b. zify. intros. apply Z.div_mod; auto. +intros a b. zify_strat. intros. apply Z.div_mod; auto. Qed. Theorem mod_bound_pos : forall a b, 0<=a -> 0 0 <= modulo a b /\ modulo a b < b. Proof. -intros a b. zify. apply Z.mod_bound_pos. +intros a b. zify_strat. apply Z.mod_bound_pos. Qed. (** Gcd *) @@ -351,8 +353,8 @@ Local Notation "( x | y )" := (divide x y) (at level 0). Lemma spec_divide : forall n m, (n|m) <-> Z.divide [n] [m]. Proof. intros n m. split. - - intros (p,H). exists [p]. revert H; now zify. - - intros (z,H). exists (of_N (Z.abs_N z)). zify. + - intros (p,H). exists [p]. revert H; now zify_strat. + - intros (z,H). exists (of_N (Z.abs_N z)). zify_strat. rewrite N2Z.inj_abs_N. rewrite <- (Z.abs_eq [m]), <- (Z.abs_eq [n]) by apply spec_pos. now rewrite H, Z.abs_mul. @@ -360,22 +362,22 @@ Qed. Lemma gcd_divide_l : forall n m, (gcd n m | n). Proof. - intros n m. apply spec_divide. zify. apply Z.gcd_divide_l. + intros n m. apply spec_divide. zify_strat. apply Z.gcd_divide_l. Qed. Lemma gcd_divide_r : forall n m, (gcd n m | m). Proof. - intros n m. apply spec_divide. zify. apply Z.gcd_divide_r. + intros n m. apply spec_divide. zify_strat. apply Z.gcd_divide_r. Qed. Lemma gcd_greatest : forall n m p, (p|n) -> (p|m) -> (p|gcd n m). Proof. - intros n m p. rewrite !spec_divide. zify. apply Z.gcd_greatest. + intros n m p. rewrite !spec_divide. zify_strat. apply Z.gcd_greatest. Qed. Lemma gcd_nonneg : forall n m, 0 <= gcd n m. Proof. - intros. zify. apply Z.gcd_nonneg. + intros. zify_strat. apply Z.gcd_nonneg. Qed. (** Bitwise operations *) @@ -385,77 +387,77 @@ Program Instance testbit_wd : Proper (eq==>eq==>Logic.eq) testbit. Lemma testbit_odd_0 : forall a, testbit (2*a+1) 0 = true. Proof. - intros. zify. apply Z.testbit_odd_0. + intros. zify_strat. apply Z.testbit_odd_0. Qed. Lemma testbit_even_0 : forall a, testbit (2*a) 0 = false. Proof. - intros. zify. apply Z.testbit_even_0. + intros. zify_strat. apply Z.testbit_even_0. Qed. Lemma testbit_odd_succ : forall a n, 0<=n -> testbit (2*a+1) (succ n) = testbit a n. Proof. - intros a n. zify. apply Z.testbit_odd_succ. + intros a n. zify_strat. apply Z.testbit_odd_succ. Qed. Lemma testbit_even_succ : forall a n, 0<=n -> testbit (2*a) (succ n) = testbit a n. Proof. - intros a n. zify. apply Z.testbit_even_succ. + intros a n. zify_strat. apply Z.testbit_even_succ. Qed. Lemma testbit_neg_r : forall a n, n<0 -> testbit a n = false. Proof. - intros a n. zify. apply Z.testbit_neg_r. + intros a n. zify_strat. apply Z.testbit_neg_r. Qed. Lemma shiftr_spec : forall a n m, 0<=m -> testbit (shiftr a n) m = testbit a (m+n). Proof. - intros a n m. zify. apply Z.shiftr_spec. + intros a n m. zify_strat. apply Z.shiftr_spec. Qed. Lemma shiftl_spec_high : forall a n m, 0<=m -> n<=m -> testbit (shiftl a n) m = testbit a (m-n). Proof. - intros a n m. zify. intros Hn H. rewrite Z.max_r by auto with zarith. + intros a n m. zify_strat. intros Hn H. rewrite Z.max_r by auto with zarith. now apply Z.shiftl_spec_high. Qed. Lemma shiftl_spec_low : forall a n m, m testbit (shiftl a n) m = false. Proof. - intros a n m. zify. intros H. now apply Z.shiftl_spec_low. + intros a n m. zify_strat. intros H. now apply Z.shiftl_spec_low. Qed. Lemma land_spec : forall a b n, testbit (land a b) n = testbit a n && testbit b n. Proof. - intros a n m. zify. now apply Z.land_spec. + intros a n m. zify_strat. now apply Z.land_spec. Qed. Lemma lor_spec : forall a b n, testbit (lor a b) n = testbit a n || testbit b n. Proof. - intros a n m. zify. now apply Z.lor_spec. + intros a n m. zify_strat. now apply Z.lor_spec. Qed. Lemma ldiff_spec : forall a b n, testbit (ldiff a b) n = testbit a n && negb (testbit b n). Proof. - intros a n m. zify. now apply Z.ldiff_spec. + intros a n m. zify_strat. now apply Z.ldiff_spec. Qed. Lemma lxor_spec : forall a b n, testbit (lxor a b) n = xorb (testbit a n) (testbit b n). Proof. - intros a n m. zify. now apply Z.lxor_spec. + intros a n m. zify_strat. now apply Z.lxor_spec. Qed. Lemma div2_spec : forall a, div2 a == shiftr a 1. Proof. - intros a. zify. now apply Z.div2_spec. + intros a. zify_strat. now apply Z.div2_spec. Qed. (** Recursion *) @@ -491,10 +493,10 @@ Theorem recursion_succ : Proof. unfold eq, recursion; intros A Aeq a f EAaa f_wd n. replace (to_N (succ n)) with (N.succ (to_N n)) by - (zify; now rewrite <- Z2N.inj_succ by apply spec_pos). + (zify_strat; now rewrite <- Z2N.inj_succ by apply spec_pos). rewrite N.peano_rect_succ. apply f_wd; auto. -zify. now rewrite Z2N.id by apply spec_pos. +zify_strat. now rewrite Z2N.id by apply spec_pos. fold (recursion a f n). apply recursion_wd; auto. red; auto. Qed. diff --git a/SpecViaZ/ZSigZAxioms.v b/SpecViaZ/ZSigZAxioms.v index 97f50bd..4805fb0 100644 --- a/SpecViaZ/ZSigZAxioms.v +++ b/SpecViaZ/ZSigZAxioms.v @@ -24,7 +24,9 @@ Hint Rewrite : zsimpl. Ltac zsimpl := autorewrite with zsimpl. +Ltac zsimpl_strat := try (rewrite_strat (repeat (topdown (hints zsimpl)))). Ltac zcongruence := repeat red; intros; zsimpl; congruence. +Ltac zify_strat := unfold eq, lt, le in *; zsimpl_strat. Ltac zify := unfold eq, lt, le in *; zsimpl. #[global] @@ -46,17 +48,17 @@ Program Instance mul_wd : Proper (eq ==> eq ==> eq) mul. Theorem pred_succ : forall n, pred (succ n) == n. Proof. -intros. zify. auto with zarith. +intros. zify_strat. auto with zarith. Qed. Theorem one_succ : 1 == succ 0. Proof. -now zify. +now zify_strat. Qed. Theorem two_succ : 2 == succ 1. Proof. -now zify. +now zify_strat. Qed. Section Induction. @@ -72,7 +74,7 @@ Lemma B0 : B 0. Proof. unfold B; simpl. rewrite <- (A_wd 0); auto. -zify. auto. +zify_strat. auto. Qed. Lemma BS : forall z : Z, B z -> B (z + 1). @@ -80,7 +82,7 @@ Proof. intros z H. unfold B in *. apply -> AS in H. setoid_replace (of_Z (z + 1)) with (succ (of_Z z)); auto. -zify. auto. +zify_strat. auto. Qed. Lemma BP : forall z : Z, B z -> B (z - 1). @@ -88,7 +90,7 @@ Proof. intros z H. unfold B in *. rewrite AS. setoid_replace (succ (of_Z (z - 1))) with (of_Z z); auto. -zify. auto with zarith. +zify_strat. auto with zarith. Qed. Lemma B_holds : forall z : Z, B z. @@ -109,76 +111,76 @@ Theorem bi_induction : forall n, A n. Proof. intro n. setoid_replace n with (of_Z (to_Z n)). apply B_holds. -zify. auto. +zify_strat. auto. Qed. End Induction. Theorem add_0_l : forall n, 0 + n == n. Proof. -intros. zify. auto with zarith. +intros. zify_strat. auto with zarith. Qed. Theorem add_succ_l : forall n m, (succ n) + m == succ (n + m). Proof. -intros. zify. auto with zarith. +intros. zify_strat. auto with zarith. Qed. Theorem sub_0_r : forall n, n - 0 == n. Proof. -intros. zify. auto with zarith. +intros. zify_strat. auto with zarith. Qed. Theorem sub_succ_r : forall n m, n - (succ m) == pred (n - m). Proof. -intros. zify. auto with zarith. +intros. zify_strat. auto with zarith. Qed. Theorem mul_0_l : forall n, 0 * n == 0. Proof. -intros. zify. auto with zarith. +intros. zify_strat. auto with zarith. Qed. Theorem mul_succ_l : forall n m, (succ n) * m == n * m + m. Proof. -intros. zify. ring. +intros. zify_strat. ring. Qed. (** Order *) Lemma eqb_eq x y : eqb x y = true <-> x == y. Proof. - zify. apply Z.eqb_eq. + zify_strat. apply Z.eqb_eq. Qed. Lemma leb_le x y : leb x y = true <-> x <= y. Proof. - zify. apply Z.leb_le. + zify_strat. apply Z.leb_le. Qed. Lemma ltb_lt x y : ltb x y = true <-> x < y. Proof. - zify. apply Z.ltb_lt. + zify_strat. apply Z.ltb_lt. Qed. Lemma compare_eq_iff n m : compare n m = Eq <-> n == m. Proof. - intros. zify. apply Z.compare_eq_iff. + intros. zify_strat. apply Z.compare_eq_iff. Qed. Lemma compare_lt_iff n m : compare n m = Lt <-> n < m. Proof. - intros. zify. reflexivity. + intros. zify_strat. reflexivity. Qed. Lemma compare_le_iff n m : compare n m <> Gt <-> n <= m. Proof. - intros. zify. reflexivity. + intros. zify_strat. reflexivity. Qed. Lemma compare_antisym n m : compare m n = CompOpp (compare n m). Proof. - intros. zify. apply Z.compare_antisym. + intros. zify_strat. apply Z.compare_antisym. Qed. Include BoolOrderFacts ZZ ZZ ZZ [no inline]. @@ -186,25 +188,25 @@ Include BoolOrderFacts ZZ ZZ ZZ [no inline]. #[global] Instance compare_wd : Proper (eq ==> eq ==> Logic.eq) compare. Proof. -intros x x' Hx y y' Hy. zify. now rewrite Hx, Hy. +intros x x' Hx y y' Hy. zify_strat. now rewrite Hx, Hy. Qed. #[global] Instance eqb_wd : Proper (eq ==> eq ==> Logic.eq) eqb. Proof. -intros x x' Hx y y' Hy. zify. now rewrite Hx, Hy. +intros x x' Hx y y' Hy. zify_strat. now rewrite Hx, Hy. Qed. #[global] Instance ltb_wd : Proper (eq ==> eq ==> Logic.eq) ltb. Proof. -intros x x' Hx y y' Hy. zify. now rewrite Hx, Hy. +intros x x' Hx y y' Hy. zify_strat. now rewrite Hx, Hy. Qed. #[global] Instance leb_wd : Proper (eq ==> eq ==> Logic.eq) leb. Proof. -intros x x' Hx y y' Hy. zify. now rewrite Hx, Hy. +intros x x' Hx y y' Hy. zify_strat. now rewrite Hx, Hy. Qed. #[global] @@ -215,34 +217,34 @@ Qed. Theorem lt_succ_r : forall n m, n < (succ m) <-> n <= m. Proof. -intros. zify. lia. +intros. zify_strat. lia. Qed. Theorem min_l : forall n m, n <= m -> min n m == n. Proof. -now intros n m; zify; lia. +now intros n m; zify_strat; lia. Qed. Theorem min_r : forall n m, m <= n -> min n m == m. Proof. -now intros n m; zify; lia. +now intros n m; zify_strat; lia. Qed. Theorem max_l : forall n m, m <= n -> max n m == n. Proof. -now intros n m; zify; lia. +now intros n m; zify_strat; lia. Qed. Theorem max_r : forall n m, n <= m -> max n m == m. Proof. -now intros n m; zify; lia. +now intros n m; zify_strat; lia. Qed. (** Part specific to integers, not natural numbers *) Theorem succ_pred : forall n, succ (pred n) == n. Proof. -intros. zify. auto with zarith. +intros. zify_strat. auto with zarith. Qed. (** Opp *) @@ -252,39 +254,39 @@ Program Instance opp_wd : Proper (eq ==> eq) opp. Theorem opp_0 : - 0 == 0. Proof. -intros. zify. auto with zarith. +intros. zify_strat. auto with zarith. Qed. Theorem opp_succ : forall n, - (succ n) == pred (- n). Proof. -intros. zify. auto with zarith. +intros. zify_strat. auto with zarith. Qed. (** Abs / Sgn *) Theorem abs_eq : forall n, 0 <= n -> abs n == n. Proof. -now intros n; zify; lia. +now intros n; zify_strat; lia. Qed. Theorem abs_neq : forall n, n <= 0 -> abs n == -n. Proof. -now intros n; zify; lia. +now intros n; zify_strat; lia. Qed. Theorem sgn_null : forall n, n==0 -> sgn n == 0. Proof. -now intros n; zify; lia. +now intros n; zify_strat; lia. Qed. Theorem sgn_pos : forall n, 0 sgn n == 1. Proof. -now intros n; zify; lia. +now intros n; zify_strat; lia. Qed. Theorem sgn_neg : forall n, n<0 -> sgn n == opp 1. Proof. -now intros n; zify; lia. +now intros n; zify_strat; lia. Qed. (** Power *) @@ -294,23 +296,23 @@ Program Instance pow_wd : Proper (eq==>eq==>eq) pow. Lemma pow_0_r : forall a, a^0 == 1. Proof. - intros. now zify. + intros. now zify_strat. Qed. Lemma pow_succ_r : forall a b, 0<=b -> a^(succ b) == a * a^b. Proof. - intros a b. zify. intros. now rewrite Z.add_1_r, Z.pow_succ_r. + intros a b. zify_strat. intros. now rewrite Z.add_1_r, Z.pow_succ_r. Qed. Lemma pow_neg_r : forall a b, b<0 -> a^b == 0. Proof. - intros a b. zify. intros Hb. + intros a b. zify_strat. intros Hb. destruct [b]; reflexivity || discriminate. Qed. Lemma pow_pow_N : forall a b, 0<=b -> a^b == pow_N a (Z.to_N (to_Z b)). Proof. - intros a b. zify. intros Hb. now rewrite spec_pow_N, Z2N.id. + intros a b. zify_strat. intros Hb. now rewrite spec_pow_N, Z2N.id. Qed. Lemma pow_pos_N : forall a p, pow_pos a p == pow_N a (Npos p). @@ -322,7 +324,7 @@ Qed. Lemma square_spec n : square n == n * n. Proof. - now zify. + now zify_strat. Qed. (** Sqrt *) @@ -330,12 +332,12 @@ Qed. Lemma sqrt_spec : forall n, 0<=n -> (sqrt n)*(sqrt n) <= n /\ n < (succ (sqrt n))*(succ (sqrt n)). Proof. - intros n. zify. apply Z.sqrt_spec. + intros n. zify_strat. apply Z.sqrt_spec. Qed. Lemma sqrt_neg : forall n, n<0 -> sqrt n == 0. Proof. - intros n. zify. apply Z.sqrt_neg. + intros n. zify_strat. apply Z.sqrt_neg. Qed. (** Log2 *) @@ -343,12 +345,12 @@ Qed. Lemma log2_spec : forall n, 0 2^(log2 n) <= n /\ n < 2^(succ (log2 n)). Proof. - intros n. zify. apply Z.log2_spec. + intros n. zify_strat. apply Z.log2_spec. Qed. Lemma log2_nonpos : forall n, n<=0 -> log2 n == 0. Proof. - intros n. zify. apply Z.log2_nonpos. + intros n. zify_strat. apply Z.log2_nonpos. Qed. (** Even / Odd *) @@ -358,18 +360,18 @@ Definition Odd n := exists m, n == 2*m+1. Lemma even_spec n : even n = true <-> Even n. Proof. - unfold Even. zify. rewrite Z.even_spec. + unfold Even. zify_strat. rewrite Z.even_spec. split; intros (m,Hm). - - exists (of_Z m). now zify. - - exists [m]. revert Hm. now zify. + - exists (of_Z m). now zify_strat. + - exists [m]. revert Hm. now zify_strat. Qed. Lemma odd_spec n : odd n = true <-> Odd n. Proof. - unfold Odd. zify. rewrite Z.odd_spec. + unfold Odd. zify_strat. rewrite Z.odd_spec. split; intros (m,Hm). - - exists (of_Z m). now zify. - - exists [m]. revert Hm. now zify. + - exists (of_Z m). now zify_strat. + - exists [m]. revert Hm. now zify_strat. Qed. (** Div / Mod *) @@ -381,19 +383,19 @@ Program Instance mod_wd : Proper (eq==>eq==>eq) modulo. Theorem div_mod : forall a b, ~b==0 -> a == b*(div a b) + (modulo a b). Proof. -intros a b. zify. intros. apply Z.div_mod; auto. +intros a b. zify_strat. intros. apply Z.div_mod; auto. Qed. Theorem mod_pos_bound : forall a b, 0 < b -> 0 <= modulo a b /\ modulo a b < b. Proof. -intros a b. zify. intros. apply Z_mod_lt; auto with zarith. +intros a b. zify_strat. intros. apply Z_mod_lt; auto with zarith. Qed. Theorem mod_neg_bound : forall a b, b < 0 -> b < modulo a b /\ modulo a b <= 0. Proof. -intros a b. zify. intros. apply Z_mod_neg; auto with zarith. +intros a b. zify_strat. intros. apply Z_mod_neg; auto with zarith. Qed. Definition mod_bound_pos : @@ -409,23 +411,23 @@ Program Instance rem_wd : Proper (eq==>eq==>eq) rem. Theorem quot_rem : forall a b, ~b==0 -> a == b*(quot a b) + rem a b. Proof. -intros a b. zify. apply Z.quot_rem. +intros a b. zify_strat. apply Z.quot_rem. Qed. Theorem rem_bound_pos : forall a b, 0<=a -> 0 0 <= rem a b /\ rem a b < b. Proof. -intros a b. zify. apply Z.rem_bound_pos. +intros a b. zify_strat. apply Z.rem_bound_pos. Qed. Theorem rem_opp_l : forall a b, ~b==0 -> rem (-a) b == -(rem a b). Proof. -intros a b. zify. apply Z.rem_opp_l. +intros a b. zify_strat. apply Z.rem_opp_l. Qed. Theorem rem_opp_r : forall a b, ~b==0 -> rem a (-b) == rem a b. Proof. -intros a b. zify. apply Z.rem_opp_r. +intros a b. zify_strat. apply Z.rem_opp_r. Qed. (** Gcd *) @@ -436,28 +438,28 @@ Local Notation "( x | y )" := (divide x y) (at level 0). Lemma spec_divide : forall n m, (n|m) <-> Z.divide [n] [m]. Proof. intros n m. split. - - intros (p,H). exists [p]. revert H; now zify. - - intros (z,H). exists (of_Z z). now zify. + - intros (p,H). exists [p]. revert H; now zify_strat. + - intros (z,H). exists (of_Z z). now zify_strat. Qed. Lemma gcd_divide_l : forall n m, (gcd n m | n). Proof. - intros n m. apply spec_divide. zify. apply Z.gcd_divide_l. + intros n m. apply spec_divide. zify_strat. apply Z.gcd_divide_l. Qed. Lemma gcd_divide_r : forall n m, (gcd n m | m). Proof. - intros n m. apply spec_divide. zify. apply Z.gcd_divide_r. + intros n m. apply spec_divide. zify_strat. apply Z.gcd_divide_r. Qed. Lemma gcd_greatest : forall n m p, (p|n) -> (p|m) -> (p|gcd n m). Proof. - intros n m p. rewrite !spec_divide. zify. apply Z.gcd_greatest. + intros n m p. rewrite !spec_divide. zify_strat. apply Z.gcd_greatest. Qed. Lemma gcd_nonneg : forall n m, 0 <= gcd n m. Proof. - intros. zify. apply Z.gcd_nonneg. + intros. zify_strat. apply Z.gcd_nonneg. Qed. (** Bitwise operations *) @@ -467,77 +469,77 @@ Program Instance testbit_wd : Proper (eq==>eq==>Logic.eq) testbit. Lemma testbit_odd_0 : forall a, testbit (2*a+1) 0 = true. Proof. - intros. zify. apply Z.testbit_odd_0. + intros. zify_strat. apply Z.testbit_odd_0. Qed. Lemma testbit_even_0 : forall a, testbit (2*a) 0 = false. Proof. - intros. zify. apply Z.testbit_even_0. + intros. zify_strat. apply Z.testbit_even_0. Qed. Lemma testbit_odd_succ : forall a n, 0<=n -> testbit (2*a+1) (succ n) = testbit a n. Proof. - intros a n. zify. apply Z.testbit_odd_succ. + intros a n. zify_strat. apply Z.testbit_odd_succ. Qed. Lemma testbit_even_succ : forall a n, 0<=n -> testbit (2*a) (succ n) = testbit a n. Proof. - intros a n. zify. apply Z.testbit_even_succ. + intros a n. zify_strat. apply Z.testbit_even_succ. Qed. Lemma testbit_neg_r : forall a n, n<0 -> testbit a n = false. Proof. - intros a n. zify. apply Z.testbit_neg_r. + intros a n. zify_strat. apply Z.testbit_neg_r. Qed. Lemma shiftr_spec : forall a n m, 0<=m -> testbit (shiftr a n) m = testbit a (m+n). Proof. - intros a n m. zify. apply Z.shiftr_spec. + intros a n m. zify_strat. apply Z.shiftr_spec. Qed. Lemma shiftl_spec_high : forall a n m, 0<=m -> n<=m -> testbit (shiftl a n) m = testbit a (m-n). Proof. - intros a n m. zify. intros Hn H. + intros a n m. zify_strat. intros Hn H. now apply Z.shiftl_spec_high. Qed. Lemma shiftl_spec_low : forall a n m, m testbit (shiftl a n) m = false. Proof. - intros a n m. zify. intros H. now apply Z.shiftl_spec_low. + intros a n m. zify_strat. intros H. now apply Z.shiftl_spec_low. Qed. Lemma land_spec : forall a b n, testbit (land a b) n = testbit a n && testbit b n. Proof. - intros a n m. zify. now apply Z.land_spec. + intros a n m. zify_strat. now apply Z.land_spec. Qed. Lemma lor_spec : forall a b n, testbit (lor a b) n = testbit a n || testbit b n. Proof. - intros a n m. zify. now apply Z.lor_spec. + intros a n m. zify_strat. now apply Z.lor_spec. Qed. Lemma ldiff_spec : forall a b n, testbit (ldiff a b) n = testbit a n && negb (testbit b n). Proof. - intros a n m. zify. now apply Z.ldiff_spec. + intros a n m. zify_strat. now apply Z.ldiff_spec. Qed. Lemma lxor_spec : forall a b n, testbit (lxor a b) n = xorb (testbit a n) (testbit b n). Proof. - intros a n m. zify. now apply Z.lxor_spec. + intros a n m. zify_strat. now apply Z.lxor_spec. Qed. Lemma div2_spec : forall a, div2 a == shiftr a 1. Proof. - intros a. zify. now apply Z.div2_spec. + intros a. zify_strat. now apply Z.div2_spec. Qed. End ZTypeIsZAxioms.