diff options
| -rw-r--r-- | theories/Numbers/Integer/BigZ/BigZ.v | 96 | ||||
| -rw-r--r-- | theories/Numbers/Integer/BigZ/ZMake.v | 13 | ||||
| -rw-r--r-- | theories/Numbers/Integer/SpecViaZ/ZSig.v | 2 | ||||
| -rw-r--r-- | theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.v | 2 | ||||
| -rw-r--r-- | theories/Numbers/Natural/BigN/BigN.v | 140 | ||||
| -rw-r--r-- | theories/Numbers/Natural/BigN/NMake_gen.ml | 14 | ||||
| -rw-r--r-- | theories/Numbers/Natural/SpecViaZ/NSig.v | 2 | ||||
| -rw-r--r-- | theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v | 4 | ||||
| -rw-r--r-- | theories/Numbers/Rational/BigQ/BigQ.v | 166 | ||||
| -rw-r--r-- | theories/Numbers/Rational/SpecViaQ/QSig.v | 154 |
10 files changed, 459 insertions, 134 deletions
diff --git a/theories/Numbers/Integer/BigZ/BigZ.v b/theories/Numbers/Integer/BigZ/BigZ.v index 73cc5c21b..aa62ae76b 100644 --- a/theories/Numbers/Integer/BigZ/BigZ.v +++ b/theories/Numbers/Integer/BigZ/BigZ.v @@ -63,24 +63,31 @@ Arguments Scope BigZ.min [bigZ_scope bigZ_scope]. Arguments Scope BigZ.max [bigZ_scope bigZ_scope]. Arguments Scope BigZ.eq_bool [bigZ_scope bigZ_scope]. Arguments Scope BigZ.power_pos [bigZ_scope positive_scope]. +Arguments Scope BigZ.power [bigZ_scope N_scope]. Arguments Scope BigZ.sqrt [bigZ_scope]. Arguments Scope BigZ.div_eucl [bigZ_scope bigZ_scope]. Arguments Scope BigZ.modulo [bigZ_scope bigZ_scope]. Arguments Scope BigZ.gcd [bigZ_scope bigZ_scope]. Local Notation "0" := BigZ.zero : bigZ_scope. +Local Notation "1" := BigZ.one : bigZ_scope. Infix "+" := BigZ.add : bigZ_scope. Infix "-" := BigZ.sub : bigZ_scope. Notation "- x" := (BigZ.opp x) : bigZ_scope. Infix "*" := BigZ.mul : bigZ_scope. Infix "/" := BigZ.div : bigZ_scope. -Infix "^" := BigZ.power_pos : bigZ_scope. +Infix "^" := BigZ.power : bigZ_scope. Infix "?=" := BigZ.compare : bigZ_scope. Infix "==" := BigZ.eq (at level 70, no associativity) : bigZ_scope. +Notation "x != y" := (~x==y)%bigZ (at level 70, no associativity) : bigZ_scope. Infix "<" := BigZ.lt : bigZ_scope. Infix "<=" := BigZ.le : bigZ_scope. Notation "x > y" := (BigZ.lt y x)(only parsing) : bigZ_scope. Notation "x >= y" := (BigZ.le y x)(only parsing) : bigZ_scope. +Notation "x < y < z" := (x<y /\ y<z)%bigZ : bigZ_scope. +Notation "x < y <= z" := (x<y /\ y<=z)%bigZ : bigZ_scope. +Notation "x <= y < z" := (x<=y /\ y<z)%bigZ : bigZ_scope. +Notation "x <= y <= z" := (x<=y /\ y<=z)%bigZ : bigZ_scope. Notation "[ i ]" := (BigZ.to_Z i) : bigZ_scope. Infix "mod" := BigZ.modulo (at level 40, no associativity) : bigN_scope. @@ -118,31 +125,94 @@ Qed. (** [BigZ] is a ring *) Lemma BigZring : - ring_theory BigZ.zero BigZ.one BigZ.add BigZ.mul BigZ.sub BigZ.opp BigZ.eq. + ring_theory 0 1 BigZ.add BigZ.mul BigZ.sub BigZ.opp BigZ.eq. Proof. constructor. -exact BigZ.add_0_l. -exact BigZ.add_comm. -exact BigZ.add_assoc. -exact BigZ.mul_1_l. -exact BigZ.mul_comm. -exact BigZ.mul_assoc. +exact BigZ.add_0_l. exact BigZ.add_comm. exact BigZ.add_assoc. +exact BigZ.mul_1_l. exact BigZ.mul_comm. exact BigZ.mul_assoc. exact BigZ.mul_add_distr_r. symmetry. apply BigZ.add_opp_r. exact BigZ.add_opp_diag_r. Qed. -Add Ring BigZr : BigZring. +Lemma BigZeqb_correct : forall x y, BigZ.eq_bool x y = true -> x==y. +Proof. now apply BigZ.eqb_eq. Qed. -(** [BigZ] benefits from an "order" tactic *) +Lemma BigZpower : power_theory 1 BigZ.mul BigZ.eq (@id N) BigZ.power. +Proof. +constructor. +intros. red. rewrite BigZ.spec_power. unfold id. +destruct Zpower_theory as [EQ]. rewrite EQ. +destruct n; simpl. reflexivity. +induction p; simpl; intros; BigZ.zify; rewrite ?IHp; auto. +Qed. + +Lemma BigZdiv : div_theory BigZ.eq BigZ.add BigZ.mul (@id _) + (fun a b => if BigZ.eq_bool b 0 then (0,a) else BigZ.div_eucl a b). +Proof. +constructor. unfold id. intros a b. +BigZ.zify. +generalize (Zeq_bool_if [b] 0); destruct (Zeq_bool [b] 0). +BigZ.zify. auto with zarith. +intros NEQ. +generalize (BigZ.spec_div_eucl a b). +generalize (Z_div_mod_full [a] [b] NEQ). +destruct BigZ.div_eucl as (q,r), Zdiv_eucl as (q',r'). +intros (EQ,_). injection 1. intros EQr EQq. +BigZ.zify. rewrite EQr, EQq; auto. +Qed. + +(** Detection of constants *) + +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.minus_one => constr:true + | _ => constr:false + end. + +Ltac BigZcst t := + match isBigZcst t with + | true => constr:t + | false => constr:NotConstant + end. + +(** Registration for the "ring" tactic *) + +Add Ring BigZr : BigZring + (decidable BigZeqb_correct, + constants [BigZcst], + power_tac BigZpower [Ncst], + div BigZdiv). + +Section TestRing. +Let test : forall x y, 1 + x*y + x^2 + 1 == 1*1 + 1 + y*x + 1*x*x. +Proof. +intros. ring_simplify. reflexivity. +Qed. +Let test' : forall x y, 1 + x*y + x^2 - 1*1 - y*x + 1*(-x)*x == 0. +Proof. +intros. ring_simplify. reflexivity. +Qed. +End TestRing. + +(** [BigZ] also benefits from an "order" tactic *) Ltac bigZ_order := BigZ.order. -Section Test. +Section TestOrder. Let test : forall x y : bigZ, x<=y -> y<=x -> x==y. Proof. bigZ_order. Qed. -End Test. +End TestOrder. + +(** We can use at least a bit of (r)omega by translating to [Z]. *) -(** Todo: tactic translating from [BigZ] to [Z] + omega *) +Section TestOmega. +Let test : forall x y : bigZ, x<=y -> y<=x -> x==y. +Proof. intros x y. BigZ.zify. omega. Qed. +End TestOmega. (** Todo: micromega *) diff --git a/theories/Numbers/Integer/BigZ/ZMake.v b/theories/Numbers/Integer/BigZ/ZMake.v index 05c7ee32f..3196f11ea 100644 --- a/theories/Numbers/Integer/BigZ/ZMake.v +++ b/theories/Numbers/Integer/BigZ/ZMake.v @@ -302,6 +302,19 @@ Module Make (N:NType) <: ZType. rewrite F0; ring. Qed. + Definition power x n := + match n with + | N0 => one + | Npos p => power_pos x p + end. + + Theorem spec_power: forall x n, to_Z (power x n) = to_Z x ^ Z_of_N n. + Proof. + destruct n; simpl. rewrite N.spec_1; reflexivity. + apply spec_power_pos. + Qed. + + Definition sqrt x := match x with | Pos nx => Pos (N.sqrt nx) diff --git a/theories/Numbers/Integer/SpecViaZ/ZSig.v b/theories/Numbers/Integer/SpecViaZ/ZSig.v index a9945e848..ffa91706f 100644 --- a/theories/Numbers/Integer/SpecViaZ/ZSig.v +++ b/theories/Numbers/Integer/SpecViaZ/ZSig.v @@ -49,6 +49,7 @@ Module Type ZType. Parameter mul : t -> t -> t. Parameter square : t -> t. Parameter power_pos : t -> positive -> t. + Parameter power : t -> N -> t. Parameter sqrt : t -> t. Parameter div_eucl : t -> t -> t * t. Parameter div : t -> t -> t. @@ -72,6 +73,7 @@ Module Type ZType. Parameter spec_mul: forall x y, [mul x y] = [x] * [y]. Parameter spec_square: forall x, [square x] = [x] * [x]. Parameter spec_power_pos: forall x n, [power_pos x n] = [x] ^ Zpos n. + Parameter spec_power: forall x n, [power x n] = [x] ^ Z_of_N n. Parameter spec_sqrt: forall x, 0 <= [x] -> [sqrt x] ^ 2 <= [x] < ([sqrt x] + 1) ^ 2. Parameter spec_div_eucl: forall x y, diff --git a/theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.v b/theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.v index 3d53707eb..bcecb6a8a 100644 --- a/theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.v +++ b/theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.v @@ -255,5 +255,5 @@ Qed. End ZTypeIsZAxioms. Module ZType_ZAxioms (Z : ZType) - <: ZAxiomsSig <: ZDivSig <: HasCompare Z <: HasEqBool Z + <: ZAxiomsSig <: ZDivSig <: HasCompare Z <: HasEqBool Z <: HasMinMax Z := Z <+ ZTypeIsZAxioms. diff --git a/theories/Numbers/Natural/BigN/BigN.v b/theories/Numbers/Natural/BigN/BigN.v index 64d2e58e6..9a4d7a9b0 100644 --- a/theories/Numbers/Natural/BigN/BigN.v +++ b/theories/Numbers/Natural/BigN/BigN.v @@ -59,23 +59,30 @@ Arguments Scope BigN.min [bigN_scope bigN_scope]. Arguments Scope BigN.max [bigN_scope bigN_scope]. Arguments Scope BigN.eq_bool [bigN_scope bigN_scope]. Arguments Scope BigN.power_pos [bigN_scope positive_scope]. +Arguments Scope BigN.power [bigN_scope N_scope]. Arguments Scope BigN.sqrt [bigN_scope]. Arguments Scope BigN.div_eucl [bigN_scope bigN_scope]. Arguments Scope BigN.modulo [bigN_scope bigN_scope]. Arguments Scope BigN.gcd [bigN_scope bigN_scope]. Local Notation "0" := BigN.zero : bigN_scope. (* temporary notation *) +Local Notation "1" := BigN.one : bigN_scope. (* temporary notation *) Infix "+" := BigN.add : bigN_scope. Infix "-" := BigN.sub : bigN_scope. Infix "*" := BigN.mul : bigN_scope. Infix "/" := BigN.div : bigN_scope. -Infix "^" := BigN.power_pos : bigN_scope. +Infix "^" := BigN.power : bigN_scope. Infix "?=" := BigN.compare : bigN_scope. Infix "==" := BigN.eq (at level 70, no associativity) : bigN_scope. +Notation "x != y" := (~x==y)%bigN (at level 70, no associativity) : bigN_scope. Infix "<" := BigN.lt : bigN_scope. Infix "<=" := BigN.le : bigN_scope. Notation "x > y" := (BigN.lt y x)(only parsing) : bigN_scope. Notation "x >= y" := (BigN.le y x)(only parsing) : bigN_scope. +Notation "x < y < z" := (x<y /\ y<z)%bigN : bigN_scope. +Notation "x < y <= z" := (x<y /\ y<=z)%bigN : bigN_scope. +Notation "x <= y < z" := (x<=y /\ y<z)%bigN : bigN_scope. +Notation "x <= y <= z" := (x<=y /\ y<=z)%bigN : bigN_scope. Notation "[ i ]" := (BigN.to_Z i) : bigN_scope. Infix "mod" := BigN.modulo (at level 40, no associativity) : bigN_scope. @@ -92,23 +99,130 @@ Qed. (** [BigN] is a semi-ring *) -Lemma BigNring : - semi_ring_theory BigN.zero BigN.one BigN.add BigN.mul BigN.eq. +Lemma BigNring : semi_ring_theory 0 1 BigN.add BigN.mul BigN.eq. Proof. constructor. -exact BigN.add_0_l. -exact BigN.add_comm. -exact BigN.add_assoc. -exact BigN.mul_1_l. -exact BigN.mul_0_l. -exact BigN.mul_comm. -exact BigN.mul_assoc. -exact BigN.mul_add_distr_r. +exact BigN.add_0_l. exact BigN.add_comm. exact BigN.add_assoc. +exact BigN.mul_1_l. exact BigN.mul_0_l. exact BigN.mul_comm. +exact BigN.mul_assoc. exact BigN.mul_add_distr_r. Qed. -Add Ring BigNr : BigNring. +Lemma BigNeqb_correct : forall x y, BigN.eq_bool x y = true -> x==y. +Proof. now apply BigN.eqb_eq. Qed. -(** We benefit from an "order" tactic *) +Lemma BigNpower : power_theory 1 BigN.mul BigN.eq (@id N) BigN.power. +Proof. +constructor. +intros. red. rewrite BigN.spec_power. unfold id. +destruct Zpower_theory as [EQ]. rewrite EQ. +destruct n; simpl. reflexivity. +induction p; simpl; intros; BigN.zify; rewrite ?IHp; auto. +Qed. + +Lemma BigNdiv : div_theory BigN.eq BigN.add BigN.mul (@id _) + (fun a b => if BigN.eq_bool b 0 then (0,a) else BigN.div_eucl a b). +Proof. +constructor. unfold id. intros a b. +BigN.zify. +generalize (Zeq_bool_if [b] 0); destruct (Zeq_bool [b] 0). +BigN.zify. auto with zarith. +intros NEQ. +generalize (BigN.spec_div_eucl a b). +generalize (Z_div_mod_full [a] [b] NEQ). +destruct BigN.div_eucl as (q,r), Zdiv_eucl as (q',r'). +intros (EQ,_). injection 1. intros EQr EQq. +BigN.zify. rewrite EQr, EQq; auto. +Qed. + + +(** Detection of constants *) + +Local Open Scope list_scope. + +Ltac isInt31cst_lst l := + match l with + | nil => constr:true + | ?t::?l => match t with + | D1 => isInt31cst_lst l + | D0 => isInt31cst_lst l + | _ => constr:false + end + | _ => constr:false + end. + +Ltac isInt31cst t := + match t with + | I31 ?i0 ?i1 ?i2 ?i3 ?i4 ?i5 ?i6 ?i7 ?i8 ?i9 ?i10 + ?i11 ?i12 ?i13 ?i14 ?i15 ?i16 ?i17 ?i18 ?i19 ?i20 + ?i21 ?i22 ?i23 ?i24 ?i25 ?i26 ?i27 ?i28 ?i29 ?i30 => + let l := + constr:(i0::i1::i2::i3::i4::i5::i6::i7::i8::i9::i10 + ::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 + end. + +Ltac isStaticWordCst t := + match t with + | W0 => constr:true + | WW ?t1 ?t2 => + match isStaticWordCst t1 with + | false => constr:false + | true => isStaticWordCst t2 + end + | _ => isInt31cst t + end. + +Ltac isBigNcst t := + match t with + | BigN.N0 ?t => isStaticWordCst t + | BigN.N1 ?t => isStaticWordCst t + | BigN.N2 ?t => isStaticWordCst t + | BigN.N3 ?t => isStaticWordCst t + | BigN.N4 ?t => isStaticWordCst t + | BigN.N5 ?t => isStaticWordCst t + | BigN.N6 ?t => isStaticWordCst t + | BigN.Nn ?n ?t => match isnatcst n with + | true => isStaticWordCst t + | false => constr:false + end + | BigN.zero => constr:true + | BigN.one => constr:true + | _ => constr:false + end. + +Ltac BigNcst t := + match isBigNcst t with + | true => constr:t + | false => constr:NotConstant + end. + +Ltac Ncst t := + match isNcst t with + | true => constr:t + | false => constr:NotConstant + end. + +(** Registration for the "ring" tactic *) + +Add Ring BigNr : BigNring + (decidable BigNeqb_correct, + constants [BigNcst], + power_tac BigNpower [Ncst], + div BigNdiv). + +Section TestRing. +Let test : forall x y, 1 + x*y + x^2 + 1 == 1*1 + 1 + y*x + 1*x*x. +intros. ring_simplify. reflexivity. +Qed. +End TestRing. + +(** We benefit also from an "order" tactic *) Ltac bigN_order := BigN.order. diff --git a/theories/Numbers/Natural/BigN/NMake_gen.ml b/theories/Numbers/Natural/BigN/NMake_gen.ml index 6257e8e63..8240604c2 100644 --- a/theories/Numbers/Natural/BigN/NMake_gen.ml +++ b/theories/Numbers/Natural/BigN/NMake_gen.ml @@ -1780,6 +1780,20 @@ let _ = pp " intros; rewrite Zpower_1_r; auto."; pp " Qed."; pp ""; + + pr " Definition power x (n:N) := match n with"; + pr " | BinNat.N0 => one"; + pr " | BinNat.Npos p => power_pos x p"; + pr " end."; + pr ""; + + pr " Theorem spec_power: forall x n, [power x n] = [x] ^ Z_of_N n."; + pa " Admitted."; + pp " Proof."; + pp " destruct n; simpl. apply (spec_1 w0_spec)."; + pp " apply spec_power_pos."; + pp " Qed."; + pr ""; pr ""; pr " (***************************************************************)"; diff --git a/theories/Numbers/Natural/SpecViaZ/NSig.v b/theories/Numbers/Natural/SpecViaZ/NSig.v index 586e4992e..116927766 100644 --- a/theories/Numbers/Natural/SpecViaZ/NSig.v +++ b/theories/Numbers/Natural/SpecViaZ/NSig.v @@ -49,6 +49,7 @@ Module Type NType. Parameter mul : t -> t -> t. Parameter square : t -> t. Parameter power_pos : t -> positive -> t. + Parameter power : t -> N -> t. Parameter sqrt : t -> t. Parameter div_eucl : t -> t -> t * t. Parameter div : t -> t -> t. @@ -68,6 +69,7 @@ Module Type NType. Parameter spec_mul: forall x y, [mul x y] = [x] * [y]. Parameter spec_square: forall x, [square x] = [x] * [x]. Parameter spec_power_pos: forall x n, [power_pos x n] = [x] ^ Zpos n. + Parameter spec_power: forall x n, [power x n] = [x] ^ Z_of_N n. Parameter spec_sqrt: forall x, [sqrt x] ^ 2 <= [x] < ([sqrt x] + 1) ^ 2. Parameter spec_div_eucl: forall x y, let (q,r) := div_eucl x y in ([q], [r]) = Zdiv_eucl [x] [y]. diff --git a/theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v b/theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v index 9e3674a23..49a60916a 100644 --- a/theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v +++ b/theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v @@ -17,7 +17,7 @@ Module NTypeIsNAxioms (Import N : NType'). Hint Rewrite spec_0 spec_succ spec_add spec_mul spec_pred spec_sub spec_div spec_modulo spec_gcd spec_compare spec_eq_bool - spec_max spec_min + spec_max spec_min spec_power_pos spec_power : nsimpl. Ltac nsimpl := autorewrite with nsimpl. Ltac ncongruence := unfold eq; repeat red; intros; nsimpl; congruence. @@ -252,5 +252,5 @@ Qed. End NTypeIsNAxioms. Module NType_NAxioms (N : NType) - <: NAxiomsSig <: NDivSig <: HasCompare N <: HasEqBool N + <: NAxiomsSig <: NDivSig <: HasCompare N <: HasEqBool N <: HasMinMax N := N <+ NTypeIsNAxioms. diff --git a/theories/Numbers/Rational/BigQ/BigQ.v b/theories/Numbers/Rational/BigQ/BigQ.v index 15abaaa42..0bc71166d 100644 --- a/theories/Numbers/Rational/BigQ/BigQ.v +++ b/theories/Numbers/Rational/BigQ/BigQ.v @@ -11,7 +11,7 @@ (** Initial authors: Benjamin Gregoire, Laurent Thery, INRIA, 2007 *) Require Export BigZ. -Require Import Field Qfield QSig QMake. +Require Import Field Qfield QSig QMake Orders GenericMinMax. (** We choose for BigQ an implemention with multiple representation of 0: 0, 1/0, 2/0 etc. @@ -35,7 +35,9 @@ End BigN_BigZ. (** This allows to build [BigQ] out of [BigN] and [BigQ] via [QMake] *) -Module BigQ <: QSig.QType := QMake.Make BigN BigZ BigN_BigZ. +Module BigQ <: QType <: OrderedTypeFull <: TotalOrder := + QMake.Make BigN BigZ BigN_BigZ <+ !QProperties <+ HasEqBool2Dec + <+ !MinMaxLogicalProperties <+ !MinMaxDecProperties. (** Notations about [BigQ] *) @@ -76,6 +78,8 @@ Arguments Scope BigQ.power_norm [bigQ_scope bigQ_scope]. (** As in QArith, we use [#] to denote fractions *) Notation "p # q" := (BigQ.Qq p q) (at level 55, no associativity) : bigQ_scope. +Local Notation "0" := BigQ.zero : bigQ_scope. +Local Notation "1" := BigQ.one : bigQ_scope. Infix "+" := BigQ.add : bigQ_scope. Infix "-" := BigQ.sub : bigQ_scope. Notation "- x" := (BigQ.opp x) : bigQ_scope. @@ -84,146 +88,102 @@ Infix "/" := BigQ.div : bigQ_scope. Infix "^" := BigQ.power : bigQ_scope. Infix "?=" := BigQ.compare : bigQ_scope. Infix "==" := BigQ.eq : bigQ_scope. +Notation "x != y" := (~x==y)%bigQ (at level 70, no associativity) : bigQ_scope. Infix "<" := BigQ.lt : bigQ_scope. Infix "<=" := BigQ.le : bigQ_scope. Notation "x > y" := (BigQ.lt y x)(only parsing) : bigQ_scope. Notation "x >= y" := (BigQ.le y x)(only parsing) : bigQ_scope. +Notation "x < y < z" := (x<y /\ y<z)%bigQ : bigQ_scope. +Notation "x < y <= z" := (x<y /\ y<=z)%bigQ : bigQ_scope. +Notation "x <= y < z" := (x<=y /\ y<z)%bigQ : bigQ_scope. +Notation "x <= y <= z" := (x<=y /\ y<=z)%bigQ : bigQ_scope. Notation "[ q ]" := (BigQ.to_Q q) : bigQ_scope. Local Open Scope bigQ_scope. -(** [BigQ] is a setoid *) - -Instance BigQeq_rel : Equivalence BigQ.eq. -Proof. unfold BigQ.eq. split; red; eauto with qarith. Qed. - -Instance BigQadd_wd : Proper (BigQ.eq==>BigQ.eq==>BigQ.eq) BigQ.add. -Proof. - do 3 red. unfold BigQ.eq; intros. - rewrite !BigQ.spec_add, H, H0. reflexivity. -Qed. - -Instance BigQopp_wd : Proper (BigQ.eq==>BigQ.eq) BigQ.opp. -Proof. - do 2 red. unfold BigQ.eq; intros. - rewrite !BigQ.spec_opp, H; reflexivity. -Qed. - -Instance BigQsub_wd : Proper (BigQ.eq==>BigQ.eq==>BigQ.eq) BigQ.sub. -Proof. - do 3 red. unfold BigQ.eq; intros. - rewrite !BigQ.spec_sub, H, H0; reflexivity. -Qed. - -Instance BigQmul_wd : Proper (BigQ.eq==>BigQ.eq==>BigQ.eq) BigQ.mul. -Proof. - do 3 red. unfold BigQ.eq; intros. - rewrite !BigQ.spec_mul, H, H0; reflexivity. -Qed. - -Instance BigQinv_wd : Proper (BigQ.eq==>BigQ.eq) BigQ.inv. -Proof. - do 2 red; unfold BigQ.eq; intros. - rewrite !BigQ.spec_inv, H; reflexivity. -Qed. - -Instance BigQdiv_wd : Proper (BigQ.eq==>BigQ.eq==>BigQ.eq) BigQ.div. -Proof. - do 3 red; unfold BigQ.eq; intros. - rewrite !BigQ.spec_div, H, H0; reflexivity. -Qed. - -(* TODO : fix this. For the moment it's useless (horribly slow) -Hint Rewrite - BigQ.spec_0 BigQ.spec_1 BigQ.spec_m1 BigQ.spec_compare - BigQ.spec_red BigQ.spec_add BigQ.spec_sub BigQ.spec_opp - BigQ.spec_mul BigQ.spec_inv BigQ.spec_div BigQ.spec_power_pos - BigQ.spec_square : bigq. *) - - (** [BigQ] is a field *) Lemma BigQfieldth : - field_theory BigQ.zero BigQ.one BigQ.add BigQ.mul BigQ.sub BigQ.opp BigQ.div BigQ.inv BigQ.eq. + field_theory 0 1 BigQ.add BigQ.mul BigQ.sub BigQ.opp + BigQ.div BigQ.inv BigQ.eq. Proof. constructor. -constructor; intros; red. -rewrite BigQ.spec_add, BigQ.spec_0; ring. -rewrite ! BigQ.spec_add; ring. -rewrite ! BigQ.spec_add; ring. -rewrite BigQ.spec_mul, BigQ.spec_1; ring. -rewrite ! BigQ.spec_mul; ring. -rewrite ! BigQ.spec_mul; ring. -rewrite BigQ.spec_add, ! BigQ.spec_mul, BigQ.spec_add; ring. -unfold BigQ.sub; apply Qeq_refl. -rewrite BigQ.spec_add, BigQ.spec_0, BigQ.spec_opp; ring. -compute; discriminate. -intros; red. -unfold BigQ.div; apply Qeq_refl. -intros; red. -rewrite BigQ.spec_mul, BigQ.spec_inv, BigQ.spec_1; field. -rewrite <- BigQ.spec_0; auto. -Qed. - -Lemma BigQpowerth : - power_theory BigQ.one BigQ.mul BigQ.eq Z_of_N BigQ.power. -Proof. constructor. -intros; red. -rewrite BigQ.spec_power. -replace ([r] ^ Z_of_N n)%Q with (pow_N 1 Qmult [r] n)%Q. -destruct n. -simpl; compute; auto. -induction p; simpl; auto; try rewrite !BigQ.spec_mul, !IHp; apply Qeq_refl. -destruct n; reflexivity. +exact BigQ.add_0_l. exact BigQ.add_comm. exact BigQ.add_assoc. +exact BigQ.mul_1_l. exact BigQ.mul_comm. exact BigQ.mul_assoc. +exact BigQ.mul_add_distr_r. exact BigQ.sub_add_opp. +exact BigQ.add_opp_diag_r. exact BigQ.neq_1_0. +exact BigQ.div_mul_inv. exact BigQ.mul_inv_diag_l. Qed. -Lemma BigQ_eq_bool_iff : - forall x y, BigQ.eq_bool x y = true <-> x==y. +Lemma BigQpowerth : + power_theory 1 BigQ.mul BigQ.eq Z_of_N BigQ.power. Proof. -intros. rewrite BigQ.spec_eq_bool. apply Qeq_bool_iff. +constructor. intros. BigQ.qify. +replace ([r] ^ Z_of_N n)%Q with (pow_N 1 Qmult [r] n)%Q by (now destruct n). +destruct n. reflexivity. +induction p; simpl; auto; rewrite ?BigQ.spec_mul, ?IHp; reflexivity. Qed. -Lemma BigQ_eq_bool_correct : - forall x y, BigQ.eq_bool x y = true -> x==y. -Proof. now apply BigQ_eq_bool_iff. Qed. - -Lemma BigQ_eq_bool_complete : - forall x y, x==y -> BigQ.eq_bool x y = true. -Proof. now apply BigQ_eq_bool_iff. Qed. - -(* TODO : improve later the detection of constants ... *) +Ltac isBigQcst t := + match t with + | BigQ.Qz ?t => isBigZcst t + | BigQ.Qq ?n ?d => match isBigZcst n with + | true => isBigNcst d + | false => constr:false + end + | BigQ.zero => constr:true + | BigQ.one => constr:true + | BigQ.minus_one => constr:true + | _ => constr:false + end. Ltac BigQcst t := - match t with - | BigQ.zero => BigQ.zero - | BigQ.one => BigQ.one - | BigQ.minus_one => BigQ.minus_one - | _ => NotConstant + match isBigQcst t with + | true => constr:t + | false => constr:NotConstant end. Add Field BigQfield : BigQfieldth - (decidable BigQ_eq_bool_correct, - completeness BigQ_eq_bool_complete, + (decidable BigQ.eqb_correct, + completeness BigQ.eqb_complete, constants [BigQcst], power_tac BigQpowerth [Qpow_tac]). -Section Examples. +Section TestField. Let ex1 : forall x y z, (x+y)*z == (x*z)+(y*z). intros. ring. Qed. -Let ex8 : forall x, x ^ 1 == x. +Let ex8 : forall x, x ^ 2 == x*x. intro. ring. Qed. -Let ex10 : forall x y, ~(y==BigQ.zero) -> (x/y)*y == x. +Let ex10 : forall x y, y!=0 -> (x/y)*y == x. intros. field. auto. Qed. -End Examples.
\ No newline at end of file +End TestField. + +(** [BigQ] can also benefit from an "order" tactic *) + +Module BigQ_Order := !OrdersTac.MakeOrderTac BigQ. +Ltac bigQ_order := BigQ_Order.order. + +Section TestOrder. +Let test : forall x y : bigQ, x<=y -> y<=x -> x==y. +Proof. bigQ_order. Qed. +End TestOrder. + +(** We can also reason by switching to QArith thanks to tactic + BigQ.qify. *) + +Section TestQify. +Let test : forall x : bigQ, 0+x == 1*x. +Proof. intro x. BigQ.qify. ring. Qed. +End TestQify. diff --git a/theories/Numbers/Rational/SpecViaQ/QSig.v b/theories/Numbers/Rational/SpecViaQ/QSig.v index 1959f4ad6..10d0189a3 100644 --- a/theories/Numbers/Rational/SpecViaQ/QSig.v +++ b/theories/Numbers/Rational/SpecViaQ/QSig.v @@ -8,7 +8,7 @@ (*i $Id$ i*) -Require Import QArith Qpower Qminmax. +Require Import QArith Qpower Qminmax Orders RelationPairs GenericMinMax. Open Scope Q_scope. @@ -23,7 +23,7 @@ Module Type QType. Parameter t : Type. Parameter to_Q : t -> Q. - Notation "[ x ]" := (to_Q x). + Local Notation "[ x ]" := (to_Q x). Definition eq x y := [x] == [y]. Definition lt x y := [x] < [y]. @@ -73,3 +73,153 @@ End QType. that expect reduced arguments and return reduced results. *) (** TODO : also speak of specifications via Qcanon ... *) + +Module Type QType_Notation (Import Q : QType). + Notation "[ x ]" := (to_Q x). + Infix "==" := eq (at level 70). + Notation "x != y" := (~x==y) (at level 70). + Infix "<=" := le. + Infix "<" := lt. + Notation "0" := zero. + Notation "1" := one. + Infix "+" := add. + Infix "-" := sub. + Infix "*" := mul. + Notation "- x" := (opp x). + Infix "/" := div. + Notation "/ x" := (inv x). + Infix "^" := power. +End QType_Notation. + +Module Type QType' := QType <+ QType_Notation. + + +Module QProperties (Import Q : QType'). + +(** Conversion to Q *) + +Hint Rewrite + spec_red spec_compare spec_eq_bool spec_min spec_max + spec_add spec_sub spec_opp spec_mul spec_square spec_inv spec_div + spec_power : qsimpl. +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 *. + +(** NB: do not add [spec_0] in the autorewrite database. Otherwise, + after instanciation in BigQ, this lemma become convertible to 0=0, + and autorewrite loops. Idem for [spec_1] and [spec_m1] *) + +(** Morphisms *) + +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. + +Instance : Measure to_Q. +Instance eq_equiv : Equivalence eq. + +Program Instance lt_wd : Proper (eq==>eq==>iff) lt. +Program Instance le_wd : Proper (eq==>eq==>iff) le. +Program Instance red_wd : Proper (eq==>eq) red. +Program Instance compare_wd : Proper (eq==>eq==>Logic.eq) compare. +Program Instance eq_bool_wd : Proper (eq==>eq==>Logic.eq) eq_bool. +Program Instance min_wd : Proper (eq==>eq==>eq) min. +Program Instance max_wd : Proper (eq==>eq==>eq) max. +Program Instance add_wd : Proper (eq==>eq==>eq) add. +Program Instance sub_wd : Proper (eq==>eq==>eq) sub. +Program Instance opp_wd : Proper (eq==>eq) opp. +Program Instance mul_wd : Proper (eq==>eq==>eq) mul. +Program Instance square_wd : Proper (eq==>eq) square. +Program Instance inv_wd : Proper (eq==>eq) inv. +Program Instance div_wd : Proper (eq==>eq==>eq) div. +Program Instance power_wd : Proper (eq==>Logic.eq==>eq) power. + +(** Let's implement [HasCompare] *) + +Lemma compare_spec : forall x y, CompSpec eq lt x y (compare x y). +Proof. intros. qify. destruct (Qcompare_spec [x] [y]); auto. Qed. + +(** Let's implement [TotalOrder] *) + +Definition lt_compat := lt_wd. +Instance lt_strorder : StrictOrder lt. + +Lemma le_lteq : forall x y, x<=y <-> x<y \/ x==y. +Proof. intros. qify. apply Qle_lteq. Qed. + +Lemma lt_total : forall x y, x<y \/ x==y \/ y<x. +Proof. intros. destruct (compare_spec x y); auto. Qed. + +(** Let's implement [HasEqBool] *) + +Definition eqb := eq_bool. + +Lemma eqb_eq : forall x y, eq_bool x y = true <-> x == y. +Proof. intros. qify. apply Qeq_bool_iff. Qed. + +Lemma eqb_correct : forall x y, eq_bool x y = true -> x == y. +Proof. now apply eqb_eq. Qed. + +Lemma eqb_complete : forall x y, x == y -> eq_bool x y = true. +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. + +Lemma max_r : forall x y, x<=y -> max x y == y. +Proof. intros x y. qify. 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. + +Lemma min_r : forall x y, y<=x -> min x y == y. +Proof. intros x y. qify. 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. + +Lemma add_comm : forall x y, x+y == y+x. +Proof. intros. qify. apply Qplus_comm. Qed. + +Lemma add_assoc : forall x y z, x+(y+z) == x+y+z. +Proof. intros. qify. apply Qplus_assoc. Qed. + +Lemma mul_1_l : forall x, 1*x == x. +Proof. intros. qify. apply Qmult_1_l. Qed. + +Lemma mul_comm : forall x y, x*y == y*x. +Proof. intros. qify. apply Qmult_comm. Qed. + +Lemma mul_assoc : forall x y z, x*(y*z) == x*y*z. +Proof. intros. qify. 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. + +Lemma sub_add_opp : forall x y, x-y == x+(-y). +Proof. intros. qify. now unfold Qminus. Qed. + +Lemma add_opp_diag_r : forall x, x+(-x) == 0. +Proof. intros. qify. apply Qplus_opp_r. Qed. + +(** Q is a field *) + +Lemma neq_1_0 : 1!=0. +Proof. intros. qify. apply Q_apart_0_1. Qed. + +Lemma div_mul_inv : forall x y, x/y == x*(/y). +Proof. intros. qify. 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. + +End QProperties. + +Module QTypeExt (Q : QType) + <: QType <: TotalOrder <: HasCompare Q <: HasMinMax Q <: HasEqBool Q + := Q <+ QProperties.
\ No newline at end of file |