diff options
Diffstat (limited to 'theories/Numbers')
-rw-r--r-- | theories/Numbers/BigNumPrelude.v | 4 | ||||
-rw-r--r-- | theories/Numbers/Cyclic/Int31/Ring31.v | 20 | ||||
-rw-r--r-- | theories/Numbers/Cyclic/ZModulo/ZModulo.v | 6 | ||||
-rw-r--r-- | theories/Numbers/Integer/Abstract/ZDivEucl.v | 14 | ||||
-rw-r--r-- | theories/Numbers/Integer/BigZ/BigZ.v | 24 | ||||
-rw-r--r-- | theories/Numbers/Integer/BigZ/ZMake.v | 12 | ||||
-rw-r--r-- | theories/Numbers/NatInt/NZGcd.v | 2 | ||||
-rw-r--r-- | theories/Numbers/Natural/BigN/BigN.v | 26 | ||||
-rw-r--r-- | theories/Numbers/Natural/BigN/NMake.v | 2 | ||||
-rw-r--r-- | theories/Numbers/Natural/BigN/NMake_gen.ml | 2 | ||||
-rw-r--r-- | theories/Numbers/Natural/Peano/NPeano.v | 84 | ||||
-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 |
14 files changed, 172 insertions, 85 deletions
diff --git a/theories/Numbers/BigNumPrelude.v b/theories/Numbers/BigNumPrelude.v index 45a7527c..bd893087 100644 --- a/theories/Numbers/BigNumPrelude.v +++ b/theories/Numbers/BigNumPrelude.v @@ -10,7 +10,7 @@ (** * BigNumPrelude *) -(** Auxillary functions & theorems used for arbitrary precision efficient +(** Auxiliary functions & theorems used for arbitrary precision efficient numbers. *) @@ -22,7 +22,7 @@ Require Export Zpow_facts. Declare ML Module "numbers_syntax_plugin". (* *** Nota Bene *** - All results that were general enough has been moved in ZArith. + All results that were general enough have been moved in ZArith. Only remain here specialized lemmas and compatibility elements. (P.L. 5/11/2007). *) diff --git a/theories/Numbers/Cyclic/Int31/Ring31.v b/theories/Numbers/Cyclic/Int31/Ring31.v index 215b8bd5..d160f5f1 100644 --- a/theories/Numbers/Cyclic/Int31/Ring31.v +++ b/theories/Numbers/Cyclic/Int31/Ring31.v @@ -19,13 +19,13 @@ Local Open Scope list_scope. Ltac isInt31cst_lst l := match l with - | nil => constr:true + | nil => constr:(true) | ?t::?l => match t with | D1 => isInt31cst_lst l | D0 => isInt31cst_lst l - | _ => constr:false + | _ => constr:(false) end - | _ => constr:false + | _ => constr:(false) end. Ltac isInt31cst t := @@ -38,17 +38,17 @@ Ltac isInt31cst t := ::i11::i12::i13::i14::i15::i16::i17::i18::i19::i20 ::i21::i22::i23::i24::i25::i26::i27::i28::i29::i30::nil) in isInt31cst_lst l - | Int31.On => constr:true - | Int31.In => constr:true - | Int31.Tn => constr:true - | Int31.Twon => constr:true - | _ => constr:false + | Int31.On => constr:(true) + | Int31.In => constr:(true) + | Int31.Tn => constr:(true) + | Int31.Twon => constr:(true) + | _ => constr:(false) end. Ltac Int31cst t := match isInt31cst t with - | true => constr:t - | false => constr:NotConstant + | true => constr:(t) + | false => constr:(NotConstant) end. (** The generic ring structure inferred from the Cyclic structure *) diff --git a/theories/Numbers/Cyclic/ZModulo/ZModulo.v b/theories/Numbers/Cyclic/ZModulo/ZModulo.v index c115a831..04fc5a8d 100644 --- a/theories/Numbers/Cyclic/ZModulo/ZModulo.v +++ b/theories/Numbers/Cyclic/ZModulo/ZModulo.v @@ -369,7 +369,7 @@ Section ZModulo. assert (Z.div_eucl ([|x|]*[|y|]) wB = (([|x|]*[|y|])/wB,([|x|]*[|y|]) mod wB)). unfold Z.modulo, Z.div; destruct Z.div_eucl; auto. generalize (Z_div_mod ([|x|]*[|y|]) wB wB_pos); destruct Z.div_eucl as (h,l). - destruct 1; injection H; clear H; intros. + destruct 1; injection H as ? ?. rewrite H0. assert ([|l|] = l). apply Zmod_small; auto. @@ -411,7 +411,7 @@ Section ZModulo. unfold Z.modulo, Z.div; destruct Z.div_eucl; auto. generalize (Z_div_mod [|a|] [|b|] H0). destruct Z.div_eucl as (q,r); destruct 1; intros. - injection H1; clear H1; intros. + injection H1 as ? ?. assert ([|r|]=r). apply Zmod_small; generalize (Z_mod_lt b wB wB_pos); fold [|b|]; auto with zarith. @@ -522,7 +522,7 @@ Section ZModulo. unfold Z.modulo, Z.div; destruct Z.div_eucl; auto. generalize (Z_div_mod a [|b|] H3). destruct Z.div_eucl as (q,r); destruct 1; intros. - injection H4; clear H4; intros. + injection H4 as ? ?. assert ([|r|]=r). apply Zmod_small; generalize (Z_mod_lt b wB wB_pos); fold [|b|]; auto with zarith. diff --git a/theories/Numbers/Integer/Abstract/ZDivEucl.v b/theories/Numbers/Integer/Abstract/ZDivEucl.v index 278e1bcf..c2fa69e5 100644 --- a/theories/Numbers/Integer/Abstract/ZDivEucl.v +++ b/theories/Numbers/Integer/Abstract/ZDivEucl.v @@ -30,18 +30,23 @@ Require Import ZAxioms ZMulOrder ZSgnAbs NZDiv. We just ignore them here. *) -Module Type EuclidSpec (Import A : ZAxiomsSig')(Import B : DivMod' A). - Axiom mod_always_pos : forall a b, b ~= 0 -> 0 <= a mod b < abs b. +Module Type EuclidSpec (Import A : ZAxiomsSig')(Import B : DivMod A). + Axiom mod_always_pos : forall a b, b ~= 0 -> 0 <= B.modulo a b < abs b. End EuclidSpec. Module Type ZEuclid (Z:ZAxiomsSig) := NZDiv.NZDiv Z <+ EuclidSpec Z. -Module Type ZEuclid' (Z:ZAxiomsSig) := NZDiv.NZDiv' Z <+ EuclidSpec Z. Module ZEuclidProp (Import A : ZAxiomsSig') (Import B : ZMulOrderProp A) (Import C : ZSgnAbsProp A B) - (Import D : ZEuclid' A). + (Import D : ZEuclid A). + + (** We put notations in a scope, to avoid warnings about + redefinitions of notations *) + Infix "/" := D.div : euclid. + Infix "mod" := D.modulo : euclid. + Local Open Scope euclid. Module Import Private_NZDiv := Nop <+ NZDivProp A D B. @@ -615,4 +620,3 @@ intros (c,Hc). rewrite Hc. now apply mod_mul. Qed. End ZEuclidProp. - diff --git a/theories/Numbers/Integer/BigZ/BigZ.v b/theories/Numbers/Integer/BigZ/BigZ.v index ec495d09..7c76011f 100644 --- a/theories/Numbers/Integer/BigZ/BigZ.v +++ b/theories/Numbers/Integer/BigZ/BigZ.v @@ -138,7 +138,7 @@ intros NEQ. generalize (BigZ.spec_div_eucl a b). generalize (Z_div_mod_full [a] [b] NEQ). destruct BigZ.div_eucl as (q,r), Z.div_eucl as (q',r'). -intros (EQ,_). injection 1. intros EQr EQq. +intros (EQ,_). injection 1 as EQr EQq. BigZ.zify. rewrite EQr, EQq; auto. Qed. @@ -148,26 +148,26 @@ Ltac isBigZcst t := match t with | BigZ.Pos ?t => isBigNcst t | BigZ.Neg ?t => isBigNcst t - | BigZ.zero => constr:true - | BigZ.one => constr:true - | BigZ.two => constr:true - | BigZ.minus_one => constr:true - | _ => constr:false + | BigZ.zero => constr:(true) + | BigZ.one => constr:(true) + | BigZ.two => constr:(true) + | BigZ.minus_one => constr:(true) + | _ => constr:(false) end. Ltac BigZcst t := match isBigZcst t with - | true => constr:t - | false => constr:NotConstant + | true => constr:(t) + | false => constr:(NotConstant) end. Ltac BigZ_to_N t := match t with | BigZ.Pos ?t => BigN_to_N t - | BigZ.zero => constr:0%N - | BigZ.one => constr:1%N - | BigZ.two => constr:2%N - | _ => constr:NotConstant + | BigZ.zero => constr:(0%N) + | BigZ.one => constr:(1%N) + | BigZ.two => constr:(2%N) + | _ => constr:(NotConstant) end. (** Registration for the "ring" tactic *) diff --git a/theories/Numbers/Integer/BigZ/ZMake.v b/theories/Numbers/Integer/BigZ/ZMake.v index 8673b8a5..fec6e068 100644 --- a/theories/Numbers/Integer/BigZ/ZMake.v +++ b/theories/Numbers/Integer/BigZ/ZMake.v @@ -147,7 +147,7 @@ Module Make (NN:NType) <: ZType. Proof. apply Bool.eq_iff_eq_true. rewrite Z.leb_le. unfold Z.le, leb. rewrite spec_compare. - destruct Z.compare; split; try easy. now destruct 1. + now destruct Z.compare; split. Qed. Definition min n m := match compare n m with Gt => m | _ => n end. @@ -427,13 +427,13 @@ Module Make (NN:NType) <: ZType. (* Pos Neg *) generalize (NN.spec_div_eucl x y); destruct (NN.div_eucl x y) as (q,r). break_nonneg x px EQx; break_nonneg y py EQy; - try (injection 1; intros Hr Hq; rewrite NN.spec_eqb, NN.spec_0, Hr; + try (injection 1 as Hq Hr; rewrite NN.spec_eqb, NN.spec_0, Hr; simpl; rewrite Hq, NN.spec_0; auto). change (- Zpos py) with (Zneg py). assert (GT : Zpos py > 0) by (compute; auto). generalize (Z_div_mod (Zpos px) (Zpos py) GT). unfold Z.div_eucl. destruct (Z.pos_div_eucl px (Zpos py)) as (q',r'). - intros (EQ,MOD). injection 1. intros Hr' Hq'. + intros (EQ,MOD). injection 1 as Hq' Hr'. rewrite NN.spec_eqb, NN.spec_0, Hr'. break_nonneg r pr EQr. subst; simpl. rewrite NN.spec_0; auto. @@ -442,13 +442,13 @@ Module Make (NN:NType) <: ZType. (* Neg Pos *) generalize (NN.spec_div_eucl x y); destruct (NN.div_eucl x y) as (q,r). break_nonneg x px EQx; break_nonneg y py EQy; - try (injection 1; intros Hr Hq; rewrite NN.spec_eqb, NN.spec_0, Hr; + try (injection 1 as Hq Hr; rewrite NN.spec_eqb, NN.spec_0, Hr; simpl; rewrite Hq, NN.spec_0; auto). change (- Zpos px) with (Zneg px). assert (GT : Zpos py > 0) by (compute; auto). generalize (Z_div_mod (Zpos px) (Zpos py) GT). unfold Z.div_eucl. destruct (Z.pos_div_eucl px (Zpos py)) as (q',r'). - intros (EQ,MOD). injection 1. intros Hr' Hq'. + intros (EQ,MOD). injection 1 as Hq' Hr'. rewrite NN.spec_eqb, NN.spec_0, Hr'. break_nonneg r pr EQr. subst; simpl. rewrite NN.spec_0; auto. @@ -457,7 +457,7 @@ Module Make (NN:NType) <: ZType. (* Neg Neg *) generalize (NN.spec_div_eucl x y); destruct (NN.div_eucl x y) as (q,r). break_nonneg x px EQx; break_nonneg y py EQy; - try (injection 1; intros Hr Hq; rewrite Hr, Hq; auto). + try (injection 1 as -> ->; auto). simpl. intros <-; auto. Qed. diff --git a/theories/Numbers/NatInt/NZGcd.v b/theories/Numbers/NatInt/NZGcd.v index 1d367294..44088f8c 100644 --- a/theories/Numbers/NatInt/NZGcd.v +++ b/theories/Numbers/NatInt/NZGcd.v @@ -60,8 +60,6 @@ Proof. intros n. exists 0. now nzsimpl. Qed. -Hint Rewrite divide_1_l divide_0_r : nz. - Lemma divide_0_l : forall n, (0 | n) -> n==0. Proof. intros n (m,Hm). revert Hm. now nzsimpl. diff --git a/theories/Numbers/Natural/BigN/BigN.v b/theories/Numbers/Natural/BigN/BigN.v index 29a1145e..e8ff516f 100644 --- a/theories/Numbers/Natural/BigN/BigN.v +++ b/theories/Numbers/Natural/BigN/BigN.v @@ -110,7 +110,7 @@ intros NEQ. generalize (BigN.spec_div_eucl a b). generalize (Z_div_mod_full [a] [b] NEQ). destruct BigN.div_eucl as (q,r), Z.div_eucl as (q',r'). -intros (EQ,_). injection 1. intros EQr EQq. +intros (EQ,_). injection 1 as EQr EQq. BigN.zify. rewrite EQr, EQq; auto. Qed. @@ -119,10 +119,10 @@ Qed. Ltac isStaticWordCst t := match t with - | W0 => constr:true + | W0 => constr:(true) | WW ?t1 ?t2 => match isStaticWordCst t1 with - | false => constr:false + | false => constr:(false) | true => isStaticWordCst t2 end | _ => isInt31cst t @@ -139,30 +139,30 @@ Ltac isBigNcst t := | BigN.N6 ?t => isStaticWordCst t | BigN.Nn ?n ?t => match isnatcst n with | true => isStaticWordCst t - | false => constr:false + | false => constr:(false) end - | BigN.zero => constr:true - | BigN.one => constr:true - | BigN.two => constr:true - | _ => constr:false + | BigN.zero => constr:(true) + | BigN.one => constr:(true) + | BigN.two => constr:(true) + | _ => constr:(false) end. Ltac BigNcst t := match isBigNcst t with - | true => constr:t - | false => constr:NotConstant + | true => constr:(t) + | false => constr:(NotConstant) end. Ltac BigN_to_N t := match isBigNcst t with | true => eval vm_compute in (BigN.to_N t) - | false => constr:NotConstant + | false => constr:(NotConstant) end. Ltac Ncst t := match isNcst t with - | true => constr:t - | false => constr:NotConstant + | true => constr:(t) + | false => constr:(NotConstant) end. (** Registration for the "ring" tactic *) diff --git a/theories/Numbers/Natural/BigN/NMake.v b/theories/Numbers/Natural/BigN/NMake.v index 98949736..1425041a 100644 --- a/theories/Numbers/Natural/BigN/NMake.v +++ b/theories/Numbers/Natural/BigN/NMake.v @@ -338,7 +338,7 @@ Module Make (W0:CyclicType) <: NType. Proof. apply eq_iff_eq_true. rewrite Z.leb_le. unfold Z.le, leb. rewrite spec_compare. - destruct Z.compare; split; try easy. now destruct 1. + now destruct Z.compare; split. Qed. Definition min (n m : t) : t := match compare n m with Gt => m | _ => n end. diff --git a/theories/Numbers/Natural/BigN/NMake_gen.ml b/theories/Numbers/Natural/BigN/NMake_gen.ml index 601fa108..5177fae6 100644 --- a/theories/Numbers/Natural/BigN/NMake_gen.ml +++ b/theories/Numbers/Natural/BigN/NMake_gen.ml @@ -147,7 +147,7 @@ pr pr " Local Notation Size := (SizePlus O)."; pr ""; - pr " Tactic Notation \"do_size\" tactic(t) := do %i t." (size+1); + pr " Tactic Notation (at level 3) \"do_size\" tactic3(t) := do %i t." (size+1); pr ""; pr " Definition dom_t n := match n with"; diff --git a/theories/Numbers/Natural/Peano/NPeano.v b/theories/Numbers/Natural/Peano/NPeano.v index 58b1b018..d0168bd9 100644 --- a/theories/Numbers/Natural/Peano/NPeano.v +++ b/theories/Numbers/Natural/Peano/NPeano.v @@ -8,8 +8,88 @@ (* Evgeny Makarov, INRIA, 2007 *) (************************************************************************) -Require Import PeanoNat NAxioms. +Require Import PeanoNat Even NAxioms. -(** * [PeanoNat.Nat] already implements [NAxiomSig] *) +(** This file is DEPRECATED ! Use [PeanoNat] (or [Arith]) instead. *) + +(** [PeanoNat.Nat] already implements [NAxiomSig] *) Module Nat <: NAxiomsSig := Nat. + +(** Compat notations for stuff that used to be at the beginning of NPeano. *) + +Notation leb := Nat.leb (compat "8.4"). +Notation ltb := Nat.ltb (compat "8.4"). +Notation leb_le := Nat.leb_le (compat "8.4"). +Notation ltb_lt := Nat.ltb_lt (compat "8.4"). +Notation pow := Nat.pow (compat "8.4"). +Notation pow_0_r := Nat.pow_0_r (compat "8.4"). +Notation pow_succ_r := Nat.pow_succ_r (compat "8.4"). +Notation square := Nat.square (compat "8.4"). +Notation square_spec := Nat.square_spec (compat "8.4"). +Notation Even := Nat.Even (compat "8.4"). +Notation Odd := Nat.Odd (compat "8.4"). +Notation even := Nat.even (compat "8.4"). +Notation odd := Nat.odd (compat "8.4"). +Notation even_spec := Nat.even_spec (compat "8.4"). +Notation odd_spec := Nat.odd_spec (compat "8.4"). + +Lemma Even_equiv n : Even n <-> Even.even n. +Proof. symmetry. apply Even.even_equiv. Qed. +Lemma Odd_equiv n : Odd n <-> Even.odd n. +Proof. symmetry. apply Even.odd_equiv. Qed. + +Notation divmod := Nat.divmod (compat "8.4"). +Notation div := Nat.div (compat "8.4"). +Notation modulo := Nat.modulo (compat "8.4"). +Notation divmod_spec := Nat.divmod_spec (compat "8.4"). +Notation div_mod := Nat.div_mod (compat "8.4"). +Notation mod_bound_pos := Nat.mod_bound_pos (compat "8.4"). +Notation sqrt_iter := Nat.sqrt_iter (compat "8.4"). +Notation sqrt := Nat.sqrt (compat "8.4"). +Notation sqrt_iter_spec := Nat.sqrt_iter_spec (compat "8.4"). +Notation sqrt_spec := Nat.sqrt_spec (compat "8.4"). +Notation log2_iter := Nat.log2_iter (compat "8.4"). +Notation log2 := Nat.log2 (compat "8.4"). +Notation log2_iter_spec := Nat.log2_iter_spec (compat "8.4"). +Notation log2_spec := Nat.log2_spec (compat "8.4"). +Notation log2_nonpos := Nat.log2_nonpos (compat "8.4"). +Notation gcd := Nat.gcd (compat "8.4"). +Notation divide := Nat.divide (compat "8.4"). +Notation gcd_divide := Nat.gcd_divide (compat "8.4"). +Notation gcd_divide_l := Nat.gcd_divide_l (compat "8.4"). +Notation gcd_divide_r := Nat.gcd_divide_r (compat "8.4"). +Notation gcd_greatest := Nat.gcd_greatest (compat "8.4"). +Notation testbit := Nat.testbit (compat "8.4"). +Notation shiftl := Nat.shiftl (compat "8.4"). +Notation shiftr := Nat.shiftr (compat "8.4"). +Notation bitwise := Nat.bitwise (compat "8.4"). +Notation land := Nat.land (compat "8.4"). +Notation lor := Nat.lor (compat "8.4"). +Notation ldiff := Nat.ldiff (compat "8.4"). +Notation lxor := Nat.lxor (compat "8.4"). +Notation double_twice := Nat.double_twice (compat "8.4"). +Notation testbit_0_l := Nat.testbit_0_l (compat "8.4"). +Notation testbit_odd_0 := Nat.testbit_odd_0 (compat "8.4"). +Notation testbit_even_0 := Nat.testbit_even_0 (compat "8.4"). +Notation testbit_odd_succ := Nat.testbit_odd_succ (compat "8.4"). +Notation testbit_even_succ := Nat.testbit_even_succ (compat "8.4"). +Notation shiftr_spec := Nat.shiftr_spec (compat "8.4"). +Notation shiftl_spec_high := Nat.shiftl_spec_high (compat "8.4"). +Notation shiftl_spec_low := Nat.shiftl_spec_low (compat "8.4"). +Notation div2_bitwise := Nat.div2_bitwise (compat "8.4"). +Notation odd_bitwise := Nat.odd_bitwise (compat "8.4"). +Notation div2_decr := Nat.div2_decr (compat "8.4"). +Notation testbit_bitwise_1 := Nat.testbit_bitwise_1 (compat "8.4"). +Notation testbit_bitwise_2 := Nat.testbit_bitwise_2 (compat "8.4"). +Notation land_spec := Nat.land_spec (compat "8.4"). +Notation ldiff_spec := Nat.ldiff_spec (compat "8.4"). +Notation lor_spec := Nat.lor_spec (compat "8.4"). +Notation lxor_spec := Nat.lxor_spec (compat "8.4"). + +Infix "<=?" := Nat.leb (at level 70) : nat_scope. +Infix "<?" := Nat.ltb (at level 70) : nat_scope. +Infix "^" := Nat.pow : nat_scope. +Infix "/" := Nat.div : nat_scope. +Infix "mod" := Nat.modulo (at level 40, no associativity) : nat_scope. +Notation "( x | y )" := (Nat.divide x y) (at level 0) : nat_scope. 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. |