diff options
Diffstat (limited to 'src/Experiments/GenericFieldPow.v')
| -rw-r--r-- | src/Experiments/GenericFieldPow.v | 94 |
1 files changed, 51 insertions, 43 deletions
diff --git a/src/Experiments/GenericFieldPow.v b/src/Experiments/GenericFieldPow.v index 76d9cfa4f..033ed9363 100644 --- a/src/Experiments/GenericFieldPow.v +++ b/src/Experiments/GenericFieldPow.v @@ -66,7 +66,7 @@ Module F. Global Instance Proper_div : Proper (_==_ ==> _==_ ==> _==_) div. - Proof. + Proof using Type*. unfold div; repeat intro. repeat match goal with | [H: _ == _ |- _ ] => rewrite H; clear H @@ -74,7 +74,7 @@ Module F. Qed. Global Instance Proper_pow_pos : Proper (_==_==>eq==>_==_) pow_pos. - Proof. + Proof using Rr. cut (forall n (y x : F), x == y -> pow_pos x n == pow_pos y n); [repeat intro; subst; eauto|]. induction n; simpl; intros; trivial; @@ -82,7 +82,7 @@ Module F. Qed. Global Instance Propper_powZ : Proper (_==_==>eq==>_==_) powZ. - Proof. + Proof using Type*. repeat intro; subst; unfold powZ. match goal with |- context[match ?x with _ => _ end] => destruct x end; repeat (eapply Proper_pow_pos || f_equiv; trivial). @@ -90,13 +90,13 @@ Module F. Import Coq.setoid_ring.Field_theory Coq.setoid_ring.Field_tac. Lemma field_theory_for_tactic : field_theory 0 1 _+_ _*_ _-_ -_ _/_ inv _==_. - Proof. + Proof using Type*. split; repeat constructor; repeat intro; gen_rewrite; try cring; eauto using field_one_neq_zero, field_inv_def. Qed. Import Coq.setoid_ring.Ring_theory Coq.setoid_ring.NArithRing. Lemma power_theory_for_tactic : power_theory 1 _*_ _==_ NtoZ power. - Proof. constructor; destruct n; reflexivity. Qed. + Proof using Rr. constructor; destruct n; reflexivity. Qed. Create HintDb field_nonzero discriminated. Hint Resolve field_one_neq_zero : field_nonzero. @@ -107,10 +107,12 @@ Module F. power_tac power_theory_for_tactic [field_power_isconst]). Lemma div_mul_idemp_l : forall a b, (a==0 -> False) -> a*b/a == b. - Proof. intros. field. Qed. + Proof using Type*. intros. field. Qed. Context {eq_dec:forall x y : F, {x==y}+{x==y->False}}. Lemma mul_zero_why : forall a b, a*b == 0 -> a == 0 \/ b == 0. + Proof using Type*. + intros; destruct (eq_dec a 0); intuition. assert (a * b / a == 0) by (match goal with [H: _ == _ |- _ ] => rewrite H; field end). @@ -119,7 +121,7 @@ Module F. Import Coq.nsatz.Nsatz. Global Instance Integral_domain_Field : Integral_domain (R:=F). - Proof. + Proof using Type*. constructor; intros; eauto using mul_zero_why, field_one_neq_zero. Qed. @@ -150,12 +152,12 @@ Module F. Hint Extern 5 (_ == _) => field_nsatz : field. Hint Extern 5 (_ <-> _) => split. - Lemma mul_inv_l : forall x, not (x == 0) -> inv x * x == 1. Proof. auto with field. Qed. + Lemma mul_inv_l : forall x, not (x == 0) -> inv x * x == 1. Proof using Type*. auto with field. Qed. - Lemma mul_inv_r : forall x, not (x == 0) -> x * inv x == 1. Proof. auto with field. Qed. + Lemma mul_inv_r : forall x, not (x == 0) -> x * inv x == 1. Proof using Type*. auto with field. Qed. Lemma mul_cancel_r' (x y z:F) : not (z == 0) -> x * z == y * z -> x == y. - Proof. + Proof using Type*. intros. assert (x * z * inv z == y * z * inv z) by (match goal with [H: _ == _ |- _ ] => rewrite H; auto with field end). @@ -165,28 +167,28 @@ Module F. Qed. Lemma mul_cancel_r (x y z:F) : not (z == 0) -> (x * z == y * z <-> x == y). - Proof. intros;split;intros Heq; try eapply mul_cancel_r' in Heq; eauto with field. Qed. + Proof using Type*. intros;split;intros Heq; try eapply mul_cancel_r' in Heq; eauto with field. Qed. Lemma mul_cancel_l (x y z:F) : not (z == 0) -> (z * x == z * y <-> x == y). - Proof. intros;split;intros; try eapply mul_cancel_r; eauto with field. Qed. + Proof using Type*. intros;split;intros; try eapply mul_cancel_r; eauto with field. Qed. Lemma mul_cancel_r_eq : forall x z:F, not(z==0) -> (x*z == z <-> x == 1). - Proof. + Proof using Type*. intros;split;intros Heq; [|nsatz]. pose proof ring_mul_1_l z as Hz; rewrite <- Hz in Heq at 2; rewrite mul_cancel_r in Heq; eauto. Qed. Lemma mul_cancel_l_eq : forall x z:F, not(z==0) -> (z*x == z <-> x == 1). - Proof. intros;split;intros Heq; try eapply mul_cancel_r_eq; eauto with field. Qed. + Proof using Type*. intros;split;intros Heq; try eapply mul_cancel_r_eq; eauto with field. Qed. - Lemma inv_unique (a:F) : forall x y, x * a == 1 -> y * a == 1 -> x == y. Proof. auto with field. Qed. + Lemma inv_unique (a:F) : forall x y, x * a == 1 -> y * a == 1 -> x == y. Proof using Type*. auto with field. Qed. Lemma mul_nonzero_nonzero (a b:F) : not (a == 0) -> not (b == 0) -> not (a*b == 0). - Proof. intros; intro Hab. destruct (mul_zero_why _ _ Hab); auto. Qed. + Proof using Type*. intros; intro Hab. destruct (mul_zero_why _ _ Hab); auto. Qed. Hint Resolve mul_nonzero_nonzero : field_nonzero. Lemma inv_nonzero (x:F) : not(x == 0) -> not(inv x==0). - Proof. + Proof using H. intros Hx Hi. assert (Hc:not (inv x*x==0)) by (rewrite field_inv_def; eauto with field_nonzero); contradict Hc. ring [Hi]. @@ -194,32 +196,32 @@ Module F. Hint Resolve inv_nonzero : field_nonzero. Lemma div_nonzero (x y:F) : not(x==0) -> not(y==0) -> not(x/y==0). - Proof. + Proof using Type*. unfold division, div_notation, div; auto with field_nonzero. Qed. Hint Resolve div_nonzero : field_nonzero. Lemma pow_pos_nonzero (x:F) p : not(x==0) -> not(Ncring.pow_pos x p == 0). - Proof. + Proof using Type*. intros; induction p using Pos.peano_ind; try assumption; []. rewrite Ncring.pow_pos_succ; eauto using mul_nonzero_nonzero. Qed. Hint Resolve pow_pos_nonzero : field_nonzero. - Lemma sub_diag_iff (x y:F) : x - y == 0 <-> x == y. Proof. auto with field. Qed. + Lemma sub_diag_iff (x y:F) : x - y == 0 <-> x == y. Proof using Type*. auto with field. Qed. - Lemma mul_same (x:F) : x*x == x^2%Z. Proof. auto with field. Qed. + Lemma mul_same (x:F) : x*x == x^2%Z. Proof using Type*. auto with field. Qed. Lemma inv_mul (x y:F) : not(x==0) -> not (y==0) -> inv (x*y) == inv x * inv y. - Proof. intros;field;intuition. Qed. + Proof using H. intros;field;intuition. Qed. - Lemma pow_0_r (x:F) : x^0 == 1. Proof. auto with field. Qed. - Lemma pow_1_r : forall x:F, x^1%Z == x. Proof. auto with field. Qed. - Lemma pow_2_r : forall x:F, x^2%Z == x*x. Proof. auto with field. Qed. - Lemma pow_3_r : forall x:F, x^3%Z == x*x*x. Proof. auto with field. Qed. + Lemma pow_0_r (x:F) : x^0 == 1. Proof using Type*. auto with field. Qed. + Lemma pow_1_r : forall x:F, x^1%Z == x. Proof using Type*. auto with field. Qed. + Lemma pow_2_r : forall x:F, x^2%Z == x*x. Proof using Type*. auto with field. Qed. + Lemma pow_3_r : forall x:F, x^3%Z == x*x*x. Proof using Type*. auto with field. Qed. Lemma pow_succ_r (x:F) (n:Z) : not (x==0)\/(n>=0)%Z -> x^(n+1) == x * x^n. - Proof. + Proof using Type*. intros Hnz; unfold power, powZ, power_field, powZ; destruct n eqn:HSn. - simpl; ring. - setoid_rewrite <-Pos2Z.inj_succ; rewrite Ncring.pow_pos_succ; ring. @@ -234,7 +236,7 @@ Module F. Qed. Lemma pow_pred_r (x:F) (n:Z) : not (x==0) -> x^(n-1) == x^n/x. - Proof. + Proof using Type*. intros; unfold power, powZ, power_field, powZ; destruct n eqn:HSn. - simpl. rewrite unfold_div; field. - destruct (Z.pos p - 1) eqn:Hn. @@ -251,7 +253,7 @@ Module F. || setoid_rewrite pow_pred_r). Lemma pow_mul (x y:F) : forall (n:Z), not(x==0)/\not(y==0)\/(n>=0)%Z -> (x * y)^n == x^n * y^n. - Proof. + Proof using Type*. match goal with |- forall n, @?P n => eapply (Z.order_induction'_0 P) end. { repeat intro. subst. reflexivity. } - intros; cbv [power power_field powZ]; ring. @@ -262,6 +264,8 @@ Module F. Qed. Lemma pow_nonzero (x:F) : forall (n:Z), not(x==0) -> not(x^n==0). + Proof using Type*. + match goal with |- forall n, @?P n => eapply (Z.order_induction'_0 P) end; intros; pow_peano; eauto with field_nonzero. { repeat intro. subst. reflexivity. } @@ -269,6 +273,8 @@ Module F. Hint Resolve pow_nonzero : field_nonzero. Lemma pow_inv (x:F) : forall (n:Z), not(x==0) -> inv x^n == inv (x^n). + Proof using Type*. + match goal with |- forall n, @?P n => eapply (Z.order_induction'_0 P) end. { repeat intro. subst. reflexivity. } - intros; cbv [power power_field powZ]. field; eauto with field_nonzero. @@ -279,56 +285,58 @@ Module F. Qed. Lemma pow_0_l : forall n, (n>0)%Z -> (0:F)^n==0. + Proof using Type*. + match goal with |- forall n, @?P n => eapply (Z.order_induction'_0 P) end; intros; try omega. { repeat intro. subst. reflexivity. } setoid_rewrite pow_succ_r; [auto with field|right;omega]. Qed. Lemma pow_div (x y:F) (n:Z) : not (y==0) -> not(x==0)\/(n >= 0)%Z -> (x/y)^n == x^n/y^n. - Proof. + Proof using Type*. intros Hy Hxn. unfold division, div_notation, div. rewrite pow_mul, pow_inv; try field; destruct Hxn; auto with field_nonzero. Qed. Hint Extern 3 (_ >= _)%Z => omega : field_nonzero. Lemma issquare_mul (x y z:F) : not (y == 0) -> x^2%Z == z * y^2%Z -> (x/y)^2%Z == z. - Proof. intros. rewrite pow_div by (auto with field_nonzero); auto with field. Qed. + Proof using Type*. intros. rewrite pow_div by (auto with field_nonzero); auto with field. Qed. Lemma issquare_mul_sub (x y z:F) : 0 == z*y^2%Z - x^2%Z -> (x/y)^2%Z == z \/ x == 0. - Proof. destruct (eq_dec y 0); [right|left]; auto using issquare_mul with field. Qed. + Proof using Type*. destruct (eq_dec y 0); [right|left]; auto using issquare_mul with field. Qed. Lemma div_mul : forall x y z : F, not(y==0) -> (z == (x / y) <-> z * y == x). - Proof. auto with field. Qed. + Proof using H. auto with field. Qed. Lemma div_1_r : forall x : F, x/1 == x. - Proof. eauto with field field_nonzero. Qed. + Proof using Type*. eauto with field field_nonzero. Qed. Lemma div_1_l : forall x : F, not(x==0) -> 1/x == inv x. - Proof. auto with field. Qed. + Proof using Type*. auto with field. Qed. Lemma div_opp_l : forall x y, not (y==0) -> (-_ x) / y == -_ (x / y). - Proof. auto with field. Qed. + Proof using Type*. auto with field. Qed. Lemma div_opp_r : forall x y, not (y==0) -> x / (-_ y) == -_ (x / y). - Proof. auto with field. Qed. + Proof using Type*. auto with field. Qed. Lemma eq_opp_zero : forall x : F, (~ 1 + 1 == (0:F)) -> (x == -_ x <-> x == 0). - Proof. auto with field. Qed. + Proof using Type*. auto with field. Qed. Lemma add_cancel_l : forall x y z:F, z+x == z+y <-> x == y. - Proof. auto with field. Qed. + Proof using Type*. auto with field. Qed. Lemma add_cancel_r : forall x y z:F, x+z == y+z <-> x == y. - Proof. auto with field. Qed. + Proof using Type*. auto with field. Qed. Lemma add_cancel_r_eq : forall x z:F, x+z == z <-> x == 0. - Proof. auto with field. Qed. + Proof using Type*. auto with field. Qed. Lemma add_cancel_l_eq : forall x z:F, z+x == z <-> x == 0. - Proof. auto with field. Qed. + Proof using Type*. auto with field. Qed. Lemma sqrt_solutions : forall x y:F, y ^ 2%Z == x ^ 2%Z -> y == x \/ y == -_ x. - Proof. + Proof using Type*. intros ? ? squares_eq. remember (y - x) as z eqn:Heqz. assert (y == x + z) as Heqy by (subst; ring); rewrite Heqy in *; clear Heqy Heqz. |