diff options
Diffstat (limited to 'theories/Numbers/Rational')
| -rw-r--r-- | theories/Numbers/Rational/BigQ/BigQ.v | 14 | ||||
| -rw-r--r-- | theories/Numbers/Rational/BigQ/QMake.v | 37 | ||||
| -rw-r--r-- | theories/Numbers/Rational/SpecViaQ/QSig.v | 10 |
3 files changed, 33 insertions, 28 deletions
diff --git a/theories/Numbers/Rational/BigQ/BigQ.v b/theories/Numbers/Rational/BigQ/BigQ.v index fe38ea4f..850afe53 100644 --- a/theories/Numbers/Rational/BigQ/BigQ.v +++ b/theories/Numbers/Rational/BigQ/BigQ.v @@ -104,18 +104,18 @@ Ltac isBigQcst t := | BigQ.Qz ?t => isBigZcst t | BigQ.Qq ?n ?d => match isBigZcst n with | true => isBigNcst d - | false => constr:false + | false => constr:(false) end - | BigQ.zero => constr:true - | BigQ.one => constr:true - | BigQ.minus_one => constr:true - | _ => constr:false + | BigQ.zero => constr:(true) + | BigQ.one => constr:(true) + | BigQ.minus_one => constr:(true) + | _ => constr:(false) end. Ltac BigQcst t := match isBigQcst t with - | true => constr:t - | false => constr:NotConstant + | true => constr:(t) + | false => constr:(NotConstant) end. Add Field BigQfield : BigQfieldth diff --git a/theories/Numbers/Rational/BigQ/QMake.v b/theories/Numbers/Rational/BigQ/QMake.v index 4ac36425..b9fed9d5 100644 --- a/theories/Numbers/Rational/BigQ/QMake.v +++ b/theories/Numbers/Rational/BigQ/QMake.v @@ -1050,13 +1050,13 @@ Module Make (NN:NType)(ZZ:ZType)(Import NZ:NType_ZType NN ZZ) <: QType. Theorem spec_of_Qc: forall q, [[of_Qc q]] = q. Proof. intros; apply Qc_decomp; simpl; intros. - rewrite strong_spec_of_Qc; auto. + rewrite strong_spec_of_Qc. apply canon. Qed. Theorem spec_oppc: forall q, [[opp q]] = -[[q]]. Proof. intros q; unfold Qcopp, to_Qc, Q2Qc. - apply Qc_decomp; intros _ _; unfold this. + apply Qc_decomp; unfold this. apply Qred_complete. rewrite spec_opp, <- Qred_opp, Qred_correct. apply Qeq_refl. @@ -1085,10 +1085,10 @@ Module Make (NN:NType)(ZZ:ZType)(Import NZ:NType_ZType NN ZZ) <: QType. unfold to_Qc. transitivity (Q2Qc ([x] + [y])). unfold Q2Qc. - apply Qc_decomp; intros _ _; unfold this. + apply Qc_decomp; unfold this. apply Qred_complete; apply spec_add; auto. unfold Qcplus, Q2Qc. - apply Qc_decomp; intros _ _; unfold this. + apply Qc_decomp; unfold this. apply Qred_complete. apply Qplus_comp; apply Qeq_sym; apply Qred_correct. Qed. @@ -1099,10 +1099,10 @@ Module Make (NN:NType)(ZZ:ZType)(Import NZ:NType_ZType NN ZZ) <: QType. unfold to_Qc. transitivity (Q2Qc ([x] + [y])). unfold Q2Qc. - apply Qc_decomp; intros _ _; unfold this. + apply Qc_decomp; unfold this. apply Qred_complete; apply spec_add_norm; auto. unfold Qcplus, Q2Qc. - apply Qc_decomp; intros _ _; unfold this. + apply Qc_decomp; unfold this. apply Qred_complete. apply Qplus_comp; apply Qeq_sym; apply Qred_correct. Qed. @@ -1147,10 +1147,10 @@ Module Make (NN:NType)(ZZ:ZType)(Import NZ:NType_ZType NN ZZ) <: QType. unfold to_Qc. transitivity (Q2Qc ([x] * [y])). unfold Q2Qc. - apply Qc_decomp; intros _ _; unfold this. + apply Qc_decomp; unfold this. apply Qred_complete; apply spec_mul; auto. unfold Qcmult, Q2Qc. - apply Qc_decomp; intros _ _; unfold this. + apply Qc_decomp; unfold this. apply Qred_complete. apply Qmult_comp; apply Qeq_sym; apply Qred_correct. Qed. @@ -1161,10 +1161,10 @@ Module Make (NN:NType)(ZZ:ZType)(Import NZ:NType_ZType NN ZZ) <: QType. unfold to_Qc. transitivity (Q2Qc ([x] * [y])). unfold Q2Qc. - apply Qc_decomp; intros _ _; unfold this. + apply Qc_decomp; unfold this. apply Qred_complete; apply spec_mul_norm; auto. unfold Qcmult, Q2Qc. - apply Qc_decomp; intros _ _; unfold this. + apply Qc_decomp; unfold this. apply Qred_complete. apply Qmult_comp; apply Qeq_sym; apply Qred_correct. Qed. @@ -1185,10 +1185,10 @@ Module Make (NN:NType)(ZZ:ZType)(Import NZ:NType_ZType NN ZZ) <: QType. unfold to_Qc. transitivity (Q2Qc (/[x])). unfold Q2Qc. - apply Qc_decomp; intros _ _; unfold this. + apply Qc_decomp; unfold this. apply Qred_complete; apply spec_inv; auto. unfold Qcinv, Q2Qc. - apply Qc_decomp; intros _ _; unfold this. + apply Qc_decomp; unfold this. apply Qred_complete. apply Qinv_comp; apply Qeq_sym; apply Qred_correct. Qed. @@ -1199,10 +1199,10 @@ Module Make (NN:NType)(ZZ:ZType)(Import NZ:NType_ZType NN ZZ) <: QType. unfold to_Qc. transitivity (Q2Qc (/[x])). unfold Q2Qc. - apply Qc_decomp; intros _ _; unfold this. + apply Qc_decomp; unfold this. apply Qred_complete; apply spec_inv_norm; auto. unfold Qcinv, Q2Qc. - apply Qc_decomp; intros _ _; unfold this. + apply Qc_decomp; unfold this. apply Qred_complete. apply Qinv_comp; apply Qeq_sym; apply Qred_correct. Qed. @@ -1247,13 +1247,13 @@ Module Make (NN:NType)(ZZ:ZType)(Import NZ:NType_ZType NN ZZ) <: QType. unfold to_Qc. transitivity (Q2Qc ([x]^2)). unfold Q2Qc. - apply Qc_decomp; intros _ _; unfold this. + apply Qc_decomp; unfold this. apply Qred_complete; apply spec_square; auto. simpl Qcpower. replace (Q2Qc [x] * 1) with (Q2Qc [x]); try ring. simpl. unfold Qcmult, Q2Qc. - apply Qc_decomp; intros _ _; unfold this. + apply Qc_decomp; unfold this. apply Qred_complete. apply Qmult_comp; apply Qeq_sym; apply Qred_correct. Qed. @@ -1264,14 +1264,14 @@ Module Make (NN:NType)(ZZ:ZType)(Import NZ:NType_ZType NN ZZ) <: QType. unfold to_Qc. transitivity (Q2Qc ([x]^Zpos p)). unfold Q2Qc. - apply Qc_decomp; intros _ _; unfold this. + apply Qc_decomp; unfold this. apply Qred_complete; apply spec_power_pos; auto. induction p using Pos.peano_ind. simpl; ring. rewrite Pos2Nat.inj_succ; simpl Qcpower. rewrite <- IHp; clear IHp. unfold Qcmult, Q2Qc. - apply Qc_decomp; intros _ _; unfold this. + apply Qc_decomp; unfold this. apply Qred_complete. setoid_replace ([x] ^ ' Pos.succ p)%Q with ([x] * [x] ^ ' p)%Q. apply Qmult_comp; apply Qeq_sym; apply Qred_correct. @@ -1281,4 +1281,3 @@ Module Make (NN:NType)(ZZ:ZType)(Import NZ:NType_ZType NN ZZ) <: QType. Qed. End Make. - diff --git a/theories/Numbers/Rational/SpecViaQ/QSig.v b/theories/Numbers/Rational/SpecViaQ/QSig.v index a40d9405..8e20fd06 100644 --- a/theories/Numbers/Rational/SpecViaQ/QSig.v +++ b/theories/Numbers/Rational/SpecViaQ/QSig.v @@ -115,7 +115,10 @@ Ltac solve_wd2 := intros x x' Hx y y' Hy; qify; now rewrite Hx, Hy. Local Obligation Tactic := solve_wd2 || solve_wd1. Instance : Measure to_Q. -Instance eq_equiv : Equivalence eq := {}. +Instance eq_equiv : Equivalence eq. +Proof. + change eq with (RelCompFun Qeq to_Q); apply _. +Defined. Program Instance lt_wd : Proper (eq==>eq==>iff) lt. Program Instance le_wd : Proper (eq==>eq==>iff) le. @@ -141,7 +144,10 @@ Proof. intros. qify. destruct (Qcompare_spec [x] [y]); auto. Qed. (** Let's implement [TotalOrder] *) Definition lt_compat := lt_wd. -Instance lt_strorder : StrictOrder lt := {}. +Instance lt_strorder : StrictOrder lt. +Proof. + change lt with (RelCompFun Qlt to_Q); apply _. +Qed. Lemma le_lteq : forall x y, x<=y <-> x<y \/ x==y. Proof. intros. qify. apply Qle_lteq. Qed. |