aboutsummaryrefslogtreecommitdiff
path: root/plugins
diff options
context:
space:
mode:
Diffstat (limited to 'plugins')
-rw-r--r--plugins/micromega/EnvRing.v4
-rw-r--r--plugins/micromega/OrderedRing.v40
-rw-r--r--plugins/micromega/RingMicromega.v100
-rw-r--r--plugins/micromega/ZCoeff.v34
-rw-r--r--plugins/setoid_ring/Field_theory.v50
-rw-r--r--plugins/setoid_ring/InitialRing.v26
-rw-r--r--plugins/setoid_ring/Ring_polynom.v14
-rw-r--r--plugins/setoid_ring/Ring_theory.v14
8 files changed, 140 insertions, 142 deletions
diff --git a/plugins/micromega/EnvRing.v b/plugins/micromega/EnvRing.v
index eb84b1203d..36ed0210e3 100644
--- a/plugins/micromega/EnvRing.v
+++ b/plugins/micromega/EnvRing.v
@@ -594,7 +594,7 @@ Qed.
Lemma pow_pos_add x i j : x^(j + i) == x^i * x^j.
Proof.
rewrite Pos.add_comm.
- apply (pow_pos_add Rsth Reqe.(Rmul_ext) ARth.(ARmul_assoc)).
+ apply (pow_pos_add Rsth (Rmul_ext Reqe) (ARmul_assoc ARth)).
Qed.
Lemma ceqb_spec c c' : BoolSpec ([c] == [c']) True (c ?=! c').
@@ -1085,7 +1085,7 @@ Section POWER.
- simpl. rewrite IHpe1, IHpe2. now rewrite Pmul_ok.
- simpl. rewrite IHpe. Esimpl.
- simpl. rewrite Ppow_N_ok by reflexivity.
- rewrite pow_th.(rpow_pow_N). destruct n0; simpl; Esimpl.
+ rewrite (rpow_pow_N pow_th). destruct n0; simpl; Esimpl.
induction p;simpl; now rewrite ?IHp, ?IHpe, ?Pms_ok, ?Pmul_ok.
Qed.
diff --git a/plugins/micromega/OrderedRing.v b/plugins/micromega/OrderedRing.v
index 62505453f9..e0e2232be5 100644
--- a/plugins/micromega/OrderedRing.v
+++ b/plugins/micromega/OrderedRing.v
@@ -87,40 +87,40 @@ Notation "x < y" := (rlt x y).
Add Relation R req
- reflexivity proved by sor.(SORsetoid).(@Equivalence_Reflexive _ _)
- symmetry proved by sor.(SORsetoid).(@Equivalence_Symmetric _ _)
- transitivity proved by sor.(SORsetoid).(@Equivalence_Transitive _ _)
+ reflexivity proved by (@Equivalence_Reflexive _ _ (SORsetoid sor))
+ symmetry proved by (@Equivalence_Symmetric _ _ (SORsetoid sor))
+ transitivity proved by (@Equivalence_Transitive _ _ (SORsetoid sor))
as sor_setoid.
Add Morphism rplus with signature req ==> req ==> req as rplus_morph.
Proof.
-exact sor.(SORplus_wd).
+exact (SORplus_wd sor).
Qed.
Add Morphism rtimes with signature req ==> req ==> req as rtimes_morph.
Proof.
-exact sor.(SORtimes_wd).
+exact (SORtimes_wd sor).
Qed.
Add Morphism ropp with signature req ==> req as ropp_morph.
Proof.
-exact sor.(SORopp_wd).
+exact (SORopp_wd sor).
Qed.
Add Morphism rle with signature req ==> req ==> iff as rle_morph.
Proof.
-exact sor.(SORle_wd).
+exact (SORle_wd sor).
Qed.
Add Morphism rlt with signature req ==> req ==> iff as rlt_morph.
Proof.
-exact sor.(SORlt_wd).
+exact (SORlt_wd sor).
Qed.
-Add Ring SOR : sor.(SORrt).
+Add Ring SOR : (SORrt sor).
Add Morphism rminus with signature req ==> req ==> req as rminus_morph.
Proof.
intros x1 x2 H1 y1 y2 H2.
-rewrite (sor.(SORrt).(Rsub_def) x1 y1).
-rewrite (sor.(SORrt).(Rsub_def) x2 y2).
+rewrite ((Rsub_def (SORrt sor)) x1 y1).
+rewrite ((Rsub_def (SORrt sor)) x2 y2).
rewrite H1; now rewrite H2.
Qed.
@@ -180,22 +180,22 @@ Qed.
(* Relations *)
Theorem Rle_refl : forall n : R, n <= n.
-Proof sor.(SORle_refl).
+Proof (SORle_refl sor).
Theorem Rle_antisymm : forall n m : R, n <= m -> m <= n -> n == m.
-Proof sor.(SORle_antisymm).
+Proof (SORle_antisymm sor).
Theorem Rle_trans : forall n m p : R, n <= m -> m <= p -> n <= p.
-Proof sor.(SORle_trans).
+Proof (SORle_trans sor).
Theorem Rlt_trichotomy : forall n m : R, n < m \/ n == m \/ m < n.
-Proof sor.(SORlt_trichotomy).
+Proof (SORlt_trichotomy sor).
Theorem Rlt_le_neq : forall n m : R, n < m <-> n <= m /\ n ~= m.
-Proof sor.(SORlt_le_neq).
+Proof (SORlt_le_neq sor).
Theorem Rneq_0_1 : 0 ~= 1.
-Proof sor.(SORneq_0_1).
+Proof (SORneq_0_1 sor).
Theorem Req_em : forall n m : R, n == m \/ n ~= m.
Proof.
@@ -274,8 +274,8 @@ Qed.
Theorem Rplus_le_mono_l : forall n m p : R, n <= m <-> p + n <= p + m.
Proof.
intros n m p; split.
-apply sor.(SORplus_le_mono_l).
-intro H. apply (sor.(SORplus_le_mono_l) (p + n) (p + m) (- p)) in H.
+apply (SORplus_le_mono_l sor).
+intro H. apply ((SORplus_le_mono_l sor) (p + n) (p + m) (- p)) in H.
setoid_replace (- p + (p + n)) with n in H by ring.
setoid_replace (- p + (p + m)) with m in H by ring. assumption.
Qed.
@@ -375,7 +375,7 @@ Qed.
(* Times and order *)
Theorem Rtimes_pos_pos : forall n m : R, 0 < n -> 0 < m -> 0 < n * m.
-Proof sor.(SORtimes_pos_pos).
+Proof (SORtimes_pos_pos sor).
Theorem Rtimes_nonneg_nonneg : forall n m : R, 0 <= n -> 0 <= m -> 0 <= n * m.
Proof.
diff --git a/plugins/micromega/RingMicromega.v b/plugins/micromega/RingMicromega.v
index 782fab5e68..9504f4edf6 100644
--- a/plugins/micromega/RingMicromega.v
+++ b/plugins/micromega/RingMicromega.v
@@ -81,30 +81,30 @@ Record SORaddon := mk_SOR_addon {
Variable addon : SORaddon.
Add Relation R req
- reflexivity proved by sor.(SORsetoid).(@Equivalence_Reflexive _ _)
- symmetry proved by sor.(SORsetoid).(@Equivalence_Symmetric _ _)
- transitivity proved by sor.(SORsetoid).(@Equivalence_Transitive _ _)
+ reflexivity proved by (@Equivalence_Reflexive _ _ (SORsetoid sor))
+ symmetry proved by (@Equivalence_Symmetric _ _ (SORsetoid sor))
+ transitivity proved by (@Equivalence_Transitive _ _ (SORsetoid sor))
as micomega_sor_setoid.
Add Morphism rplus with signature req ==> req ==> req as rplus_morph.
Proof.
-exact sor.(SORplus_wd).
+exact (SORplus_wd sor).
Qed.
Add Morphism rtimes with signature req ==> req ==> req as rtimes_morph.
Proof.
-exact sor.(SORtimes_wd).
+exact (SORtimes_wd sor).
Qed.
Add Morphism ropp with signature req ==> req as ropp_morph.
Proof.
-exact sor.(SORopp_wd).
+exact (SORopp_wd sor).
Qed.
Add Morphism rle with signature req ==> req ==> iff as rle_morph.
Proof.
- exact sor.(SORle_wd).
+ exact (SORle_wd sor).
Qed.
Add Morphism rlt with signature req ==> req ==> iff as rlt_morph.
Proof.
- exact sor.(SORlt_wd).
+ exact (SORlt_wd sor).
Qed.
Add Morphism rminus with signature req ==> req ==> req as rminus_morph.
@@ -124,12 +124,12 @@ Ltac le_elim H := rewrite (Rle_lt_eq sor) in H; destruct H as [H | H].
Lemma cleb_sound : forall x y : C, x [<=] y = true -> [x] <= [y].
Proof.
- exact addon.(SORcleb_morph).
+ exact (SORcleb_morph addon).
Qed.
Lemma cneqb_sound : forall x y : C, x [~=] y = true -> [x] ~= [y].
Proof.
-intros x y H1. apply addon.(SORcneqb_morph). unfold cneqb, negb in H1.
+intros x y H1. apply (SORcneqb_morph addon). unfold cneqb, negb in H1.
destruct (ceqb x y); now try discriminate.
Qed.
@@ -325,9 +325,9 @@ Definition map_option2 (A B C : Type) (f : A -> B -> option C)
Arguments map_option2 [A B C] f o o'.
Definition Rops_wd := mk_reqe (*rplus rtimes ropp req*)
- sor.(SORplus_wd)
- sor.(SORtimes_wd)
- sor.(SORopp_wd).
+ (SORplus_wd sor)
+ (SORtimes_wd sor)
+ (SORopp_wd sor).
Definition pexpr_times_nformula (e: PolC) (f : NFormula) : option NFormula :=
let (ef,o) := f in
@@ -368,8 +368,8 @@ Proof.
destruct f.
intros. destruct o ; inversion H0 ; try discriminate.
simpl in *. unfold eval_pol in *.
- rewrite (Pmul_ok sor.(SORsetoid) Rops_wd
- (Rth_ARth (SORsetoid sor) Rops_wd sor.(SORrt)) addon.(SORrm)).
+ rewrite (Pmul_ok (SORsetoid sor) Rops_wd
+ (Rth_ARth (SORsetoid sor) Rops_wd (SORrt sor)) (SORrm addon)).
rewrite H. apply (Rtimes_0_r sor).
Qed.
@@ -385,8 +385,8 @@ Proof.
intros. inversion H2 ; simpl.
unfold eval_pol.
destruct o1; simpl;
- rewrite (Pmul_ok sor.(SORsetoid) Rops_wd
- (Rth_ARth (SORsetoid sor) Rops_wd sor.(SORrt)) addon.(SORrm));
+ rewrite (Pmul_ok (SORsetoid sor) Rops_wd
+ (Rth_ARth (SORsetoid sor) Rops_wd (SORrt sor)) (SORrm addon));
apply OpMult_sound with (3:= H);assumption.
Qed.
@@ -402,8 +402,8 @@ Proof.
intros. inversion H2 ; simpl.
unfold eval_pol.
destruct o1; simpl;
- rewrite (Padd_ok sor.(SORsetoid) Rops_wd
- (Rth_ARth (SORsetoid sor) Rops_wd sor.(SORrt)) addon.(SORrm));
+ rewrite (Padd_ok (SORsetoid sor) Rops_wd
+ (Rth_ARth (SORsetoid sor) Rops_wd (SORrt sor)) (SORrm addon));
apply OpAdd_sound with (3:= H);assumption.
Qed.
@@ -422,12 +422,12 @@ Proof.
(* index is out-of-bounds *)
inversion H0.
rewrite Heq. simpl.
- now apply addon.(SORrm).(morph0).
+ now apply (morph0 (SORrm addon)).
(* PsatzSquare *)
simpl. intros. inversion H0.
simpl. unfold eval_pol.
- rewrite (Psquare_ok sor.(SORsetoid) Rops_wd
- (Rth_ARth (SORsetoid sor) Rops_wd sor.(SORrt)) addon.(SORrm));
+ rewrite (Psquare_ok (SORsetoid sor) Rops_wd
+ (Rth_ARth (SORsetoid sor) Rops_wd (SORrt sor)) (SORrm addon));
now apply (Rtimes_square_nonneg sor).
(* PsatzMulC *)
simpl.
@@ -454,11 +454,11 @@ Proof.
simpl.
intro. case_eq (cO [<] c).
intros. inversion H1. simpl.
- rewrite <- addon.(SORrm).(morph0). now apply cltb_sound.
+ rewrite <- (morph0 (SORrm addon)). now apply cltb_sound.
discriminate.
(* PsatzZ *)
simpl. intros. inversion H0.
- simpl. apply addon.(SORrm).(morph0).
+ simpl. apply (morph0 (SORrm addon)).
Qed.
Fixpoint ge_bool (n m : nat) : bool :=
@@ -529,8 +529,8 @@ Proof.
inv H.
simpl.
unfold eval_pol.
- rewrite (Psquare_ok sor.(SORsetoid) Rops_wd
- (Rth_ARth (SORsetoid sor) Rops_wd sor.(SORrt)) addon.(SORrm));
+ rewrite (Psquare_ok (SORsetoid sor) Rops_wd
+ (Rth_ARth (SORsetoid sor) Rops_wd (SORrt sor)) (SORrm addon));
now apply (Rtimes_square_nonneg sor).
(* PsatzMulC *)
simpl in *.
@@ -570,12 +570,12 @@ Proof.
case_eq (cO [<] c).
intros. rewrite H1 in H. inv H.
unfold eval_nformula. simpl.
- rewrite <- addon.(SORrm).(morph0). now apply cltb_sound.
+ rewrite <- (morph0 (SORrm addon)). now apply cltb_sound.
intros. rewrite H1 in H. discriminate.
(* PsatzZ *)
simpl in *. inv H.
unfold eval_nformula. simpl.
- apply addon.(SORrm).(morph0).
+ apply (morph0 (SORrm addon)).
Qed.
@@ -592,19 +592,19 @@ Definition psubC := PsubC cminus.
Definition PsubC_ok : forall c P env, eval_pol env (psubC P c) == eval_pol env P - [c] :=
let Rops_wd := mk_reqe (*rplus rtimes ropp req*)
- sor.(SORplus_wd)
- sor.(SORtimes_wd)
- sor.(SORopp_wd) in
- PsubC_ok sor.(SORsetoid) Rops_wd (Rth_ARth (SORsetoid sor) Rops_wd sor.(SORrt))
- addon.(SORrm).
+ (SORplus_wd sor)
+ (SORtimes_wd sor)
+ (SORopp_wd sor) in
+ PsubC_ok (SORsetoid sor) Rops_wd (Rth_ARth (SORsetoid sor) Rops_wd (SORrt sor))
+ (SORrm addon).
Definition PaddC_ok : forall c P env, eval_pol env (paddC P c) == eval_pol env P + [c] :=
let Rops_wd := mk_reqe (*rplus rtimes ropp req*)
- sor.(SORplus_wd)
- sor.(SORtimes_wd)
- sor.(SORopp_wd) in
- PaddC_ok sor.(SORsetoid) Rops_wd (Rth_ARth (SORsetoid sor) Rops_wd sor.(SORrt))
- addon.(SORrm).
+ (SORplus_wd sor)
+ (SORtimes_wd sor)
+ (SORopp_wd sor) in
+ PaddC_ok (SORsetoid sor) Rops_wd (Rth_ARth (SORsetoid sor) Rops_wd (SORrt sor))
+ (SORrm addon).
(* Check that a formula f is inconsistent by normalizing and comparing the
@@ -631,9 +631,9 @@ intros p op H1 env. unfold check_inconsistent in H1.
destruct op; simpl ;
(*****)
destruct p ; simpl; try discriminate H1;
-try rewrite <- addon.(SORrm).(morph0); trivial.
+try rewrite <- (morph0 (SORrm addon)); trivial.
now apply cneqb_sound.
-apply addon.(SORrm).(morph_eq) in H1. congruence.
+apply (morph_eq (SORrm addon)) in H1. congruence.
apply cleb_sound in H1. now apply -> (Rle_ngt sor).
apply cltb_sound in H1. now apply -> (Rlt_nge sor).
Qed.
@@ -736,21 +736,21 @@ let (lhs, op, rhs) := f in
Lemma eval_pol_sub : forall env lhs rhs, eval_pol env (psub lhs rhs) == eval_pol env lhs - eval_pol env rhs.
Proof.
intros.
- apply (Psub_ok sor.(SORsetoid) Rops_wd
- (Rth_ARth (SORsetoid sor) Rops_wd sor.(SORrt)) addon.(SORrm)).
+ apply (Psub_ok (SORsetoid sor) Rops_wd
+ (Rth_ARth (SORsetoid sor) Rops_wd (SORrt sor)) (SORrm addon)).
Qed.
Lemma eval_pol_add : forall env lhs rhs, eval_pol env (padd lhs rhs) == eval_pol env lhs + eval_pol env rhs.
Proof.
intros.
- apply (Padd_ok sor.(SORsetoid) Rops_wd
- (Rth_ARth (SORsetoid sor) Rops_wd sor.(SORrt)) addon.(SORrm)).
+ apply (Padd_ok (SORsetoid sor) Rops_wd
+ (Rth_ARth (SORsetoid sor) Rops_wd (SORrt sor)) (SORrm addon)).
Qed.
Lemma eval_pol_norm : forall env lhs, eval_pexpr env lhs == eval_pol env (norm lhs).
Proof.
intros.
- apply (norm_aux_spec sor.(SORsetoid) Rops_wd (Rth_ARth (SORsetoid sor) Rops_wd sor.(SORrt)) addon.(SORrm) addon.(SORpower) ).
+ apply (norm_aux_spec (SORsetoid sor) Rops_wd (Rth_ARth (SORsetoid sor) Rops_wd (SORrt sor)) (SORrm addon) (SORpower addon) ).
Qed.
@@ -805,7 +805,7 @@ Definition cnf_normalise (t:Formula C) : cnf (NFormula) :=
List.map (fun x => x::nil) (xnormalise t).
-Add Ring SORRing : sor.(SORrt).
+Add Ring SORRing : (SORrt sor).
Lemma cnf_normalise_correct : forall env t, eval_cnf eval_nformula env (cnf_normalise t) -> eval_formula env t.
Proof.
@@ -816,7 +816,7 @@ Proof.
generalize (eval_pexpr env lhs);
generalize (eval_pexpr env rhs) ; intros z1 z2 ; intros.
(**)
- apply sor.(SORle_antisymm).
+ apply (SORle_antisymm sor).
rewrite (Rle_ngt sor). rewrite (Rlt_lt_minus sor). tauto.
rewrite (Rle_ngt sor). rewrite (Rlt_lt_minus sor). tauto.
now rewrite <- (Rminus_eq_0 sor).
@@ -855,7 +855,7 @@ Proof.
rewrite H1 ; ring.
(**)
apply H1.
- apply sor.(SORle_antisymm).
+ apply (SORle_antisymm sor).
rewrite (Rle_ngt sor). rewrite (Rlt_lt_minus sor). tauto.
rewrite (Rle_ngt sor). rewrite (Rlt_lt_minus sor). tauto.
(**)
@@ -912,7 +912,7 @@ Proof.
unfold Env.nth.
unfold jump at 2.
rewrite <- Pos.add_1_l.
- rewrite addon.(SORpower).(rpow_pow_N).
+ rewrite (rpow_pow_N (SORpower addon)).
unfold pow_N. ring.
Qed.
@@ -932,7 +932,7 @@ Proof.
unfold Env.tail.
rewrite xdenorm_correct.
change (Pos.succ xH) with 2%positive.
- rewrite addon.(SORpower).(rpow_pow_N).
+ rewrite (rpow_pow_N (SORpower addon)).
simpl. reflexivity.
Qed.
diff --git a/plugins/micromega/ZCoeff.v b/plugins/micromega/ZCoeff.v
index 137453a9ed..9ff6850fdf 100644
--- a/plugins/micromega/ZCoeff.v
+++ b/plugins/micromega/ZCoeff.v
@@ -43,48 +43,48 @@ Notation "x < y" := (rlt x y).
Lemma req_refl : forall x, req x x.
Proof.
- destruct sor.(SORsetoid) as (Equivalence_Reflexive,_,_).
+ destruct (SORsetoid sor) as (Equivalence_Reflexive,_,_).
apply Equivalence_Reflexive.
Qed.
Lemma req_sym : forall x y, req x y -> req y x.
Proof.
- destruct sor.(SORsetoid) as (_,Equivalence_Symmetric,_).
+ destruct (SORsetoid sor) as (_,Equivalence_Symmetric,_).
apply Equivalence_Symmetric.
Qed.
Lemma req_trans : forall x y z, req x y -> req y z -> req x z.
Proof.
- destruct sor.(SORsetoid) as (_,_,Equivalence_Transitive).
+ destruct (SORsetoid sor) as (_,_,Equivalence_Transitive).
apply Equivalence_Transitive.
Qed.
Add Relation R req
- reflexivity proved by sor.(SORsetoid).(@Equivalence_Reflexive _ _)
- symmetry proved by sor.(SORsetoid).(@Equivalence_Symmetric _ _)
- transitivity proved by sor.(SORsetoid).(@Equivalence_Transitive _ _)
+ reflexivity proved by (@Equivalence_Reflexive _ _ (SORsetoid sor))
+ symmetry proved by (@Equivalence_Symmetric _ _ (SORsetoid sor))
+ transitivity proved by (@Equivalence_Transitive _ _ (SORsetoid sor))
as sor_setoid.
Add Morphism rplus with signature req ==> req ==> req as rplus_morph.
Proof.
-exact sor.(SORplus_wd).
+exact (SORplus_wd sor).
Qed.
Add Morphism rtimes with signature req ==> req ==> req as rtimes_morph.
Proof.
-exact sor.(SORtimes_wd).
+exact (SORtimes_wd sor).
Qed.
Add Morphism ropp with signature req ==> req as ropp_morph.
Proof.
-exact sor.(SORopp_wd).
+exact (SORopp_wd sor).
Qed.
Add Morphism rle with signature req ==> req ==> iff as rle_morph.
Proof.
-exact sor.(SORle_wd).
+exact (SORle_wd sor).
Qed.
Add Morphism rlt with signature req ==> req ==> iff as rlt_morph.
Proof.
-exact sor.(SORlt_wd).
+exact (SORlt_wd sor).
Qed.
Add Morphism rminus with signature req ==> req ==> req as rminus_morph.
Proof.
@@ -115,7 +115,7 @@ Lemma Zring_morph :
0%Z 1%Z Z.add Z.mul Z.sub Z.opp
Zeq_bool gen_order_phi_Z.
Proof.
-exact (gen_phiZ_morph sor.(SORsetoid) ring_ops_wd sor.(SORrt)).
+exact (gen_phiZ_morph (SORsetoid sor) ring_ops_wd (SORrt sor)).
Qed.
Lemma phi_pos1_pos : forall x : positive, 0 < phi_pos1 x.
@@ -127,8 +127,8 @@ Qed.
Lemma phi_pos1_succ : forall x : positive, phi_pos1 (Pos.succ x) == 1 + phi_pos1 x.
Proof.
-exact (ARgen_phiPOS_Psucc sor.(SORsetoid) ring_ops_wd
- (Rth_ARth sor.(SORsetoid) ring_ops_wd sor.(SORrt))).
+exact (ARgen_phiPOS_Psucc (SORsetoid sor) ring_ops_wd
+ (Rth_ARth (SORsetoid sor) ring_ops_wd (SORrt sor))).
Qed.
Lemma clt_pos_morph : forall x y : positive, (x < y)%positive -> phi_pos1 x < phi_pos1 y.
@@ -142,7 +142,7 @@ Qed.
Lemma clt_morph : forall x y : Z, (x < y)%Z -> [x] < [y].
Proof.
intros x y H.
-do 2 rewrite (same_genZ sor.(SORsetoid) ring_ops_wd sor.(SORrt));
+do 2 rewrite (same_genZ (SORsetoid sor) ring_ops_wd (SORrt sor));
destruct x; destruct y; simpl in *; try discriminate.
apply phi_pos1_pos.
now apply clt_pos_morph.
@@ -157,7 +157,7 @@ Lemma Zcleb_morph : forall x y : Z, Z.leb x y = true -> [x] <= [y].
Proof.
unfold Z.leb; intros x y H.
case_eq (x ?= y)%Z; intro H1; rewrite H1 in H.
-le_equal. apply Zring_morph.(morph_eq). unfold Zeq_bool; now rewrite H1.
+le_equal. apply (morph_eq Zring_morph). unfold Zeq_bool; now rewrite H1.
le_less. now apply clt_morph.
discriminate.
Qed.
@@ -172,5 +172,3 @@ apply (Rneq_symm sor). apply (Rlt_neq sor). now apply clt_morph.
Qed.
End InitialMorphism.
-
-
diff --git a/plugins/setoid_ring/Field_theory.v b/plugins/setoid_ring/Field_theory.v
index f5d13053b1..813c521ab0 100644
--- a/plugins/setoid_ring/Field_theory.v
+++ b/plugins/setoid_ring/Field_theory.v
@@ -54,10 +54,10 @@ Record almost_field_theory : Prop := mk_afield {
Section AlmostField.
Variable AFth : almost_field_theory.
-Let ARth := AFth.(AF_AR).
-Let rI_neq_rO := AFth.(AF_1_neq_0).
-Let rdiv_def := AFth.(AFdiv_def).
-Let rinv_l := AFth.(AFinv_l).
+Let ARth := (AF_AR AFth).
+Let rI_neq_rO := (AF_1_neq_0 AFth).
+Let rdiv_def := (AFdiv_def AFth).
+Let rinv_l := (AFinv_l AFth).
Add Morphism radd with signature (req ==> req ==> req) as radd_ext.
Proof. exact (Radd_ext Reqe). Qed.
@@ -115,12 +115,12 @@ Notation "- x" := (copp x) : C_scope.
Infix "=?" := ceqb : C_scope.
Notation "[ x ]" := (phi x) (at level 0).
-Let phi_0 := CRmorph.(morph0).
-Let phi_1 := CRmorph.(morph1).
+Let phi_0 := (morph0 CRmorph).
+Let phi_1 := (morph1 CRmorph).
Lemma ceqb_spec c c' : BoolSpec ([c] == [c']) True (c =? c')%coef.
Proof.
-generalize (CRmorph.(morph_eq) c c').
+generalize ((morph_eq CRmorph) c c').
destruct (c =? c')%coef; auto.
Qed.
@@ -137,7 +137,7 @@ Variable get_sign_spec : sign_theory copp ceqb get_sign.
Variable cdiv:C -> C -> C*C.
Variable cdiv_th : div_theory req cadd cmul phi cdiv.
-Let rpow_pow := pow_th.(rpow_pow_N).
+Let rpow_pow := (rpow_pow_N pow_th).
(* Polynomial expressions : (PExpr C) *)
@@ -428,7 +428,7 @@ Qed.
Lemma pow_pos_cst c p : pow_pos rmul [c] p == [pow_pos cmul c p].
Proof.
-induction p;simpl;trivial; now rewrite !CRmorph.(morph_mul), !IHp.
+induction p;simpl;trivial; now rewrite !(morph_mul CRmorph), !IHp.
Qed.
Lemma pow_pos_mul_l x y p :
@@ -1587,7 +1587,7 @@ Section FieldAndSemiField.
Definition F2AF f :=
mk_afield
- (Rth_ARth Rsth Reqe f.(F_R)) f.(F_1_neq_0) f.(Fdiv_def) f.(Finv_l).
+ (Rth_ARth Rsth Reqe (F_R f)) (F_1_neq_0 f) (Fdiv_def f) (Finv_l f).
Record semi_field_theory : Prop := mk_sfield {
SF_SR : semi_ring_theory rO rI radd rmul req;
@@ -1603,10 +1603,10 @@ End MakeFieldPol.
Definition SF2AF R (rO rI:R) radd rmul rdiv rinv req Rsth
(sf:semi_field_theory rO rI radd rmul rdiv rinv req) :=
mk_afield _ _
- (SRth_ARth Rsth sf.(SF_SR))
- sf.(SF_1_neq_0)
- sf.(SFdiv_def)
- sf.(SFinv_l).
+ (SRth_ARth Rsth (SF_SR sf))
+ (SF_1_neq_0 sf)
+ (SFdiv_def sf)
+ (SFinv_l sf).
Section Complete.
@@ -1621,9 +1621,9 @@ Section Complete.
Notation "x == y" := (req x y) (at level 70, no associativity).
Variable Rsth : Setoid_Theory R req.
Add Parametric Relation : R req
- reflexivity proved by Rsth.(@Equivalence_Reflexive _ _)
- symmetry proved by Rsth.(@Equivalence_Symmetric _ _)
- transitivity proved by Rsth.(@Equivalence_Transitive _ _)
+ reflexivity proved by (@Equivalence_Reflexive _ _ Rsth)
+ symmetry proved by (@Equivalence_Symmetric _ _ Rsth)
+ transitivity proved by (@Equivalence_Transitive _ _ Rsth)
as R_setoid3.
Variable Reqe : ring_eq_ext radd rmul ropp req.
Add Morphism radd with signature (req ==> req ==> req) as radd_ext3.
@@ -1636,10 +1636,10 @@ Section Complete.
Section AlmostField.
Variable AFth : almost_field_theory rO rI radd rmul rsub ropp rdiv rinv req.
- Let ARth := AFth.(AF_AR).
- Let rI_neq_rO := AFth.(AF_1_neq_0).
- Let rdiv_def := AFth.(AFdiv_def).
- Let rinv_l := AFth.(AFinv_l).
+ Let ARth := (AF_AR AFth).
+ Let rI_neq_rO := (AF_1_neq_0 AFth).
+ Let rdiv_def := (AFdiv_def AFth).
+ Let rinv_l := (AFinv_l AFth).
Hypothesis S_inj : forall x y, 1+x==1+y -> x==y.
@@ -1705,10 +1705,10 @@ End AlmostField.
Section Field.
Variable Fth : field_theory rO rI radd rmul rsub ropp rdiv rinv req.
- Let Rth := Fth.(F_R).
- Let rI_neq_rO := Fth.(F_1_neq_0).
- Let rdiv_def := Fth.(Fdiv_def).
- Let rinv_l := Fth.(Finv_l).
+ Let Rth := (F_R Fth).
+ Let rI_neq_rO := (F_1_neq_0 Fth).
+ Let rdiv_def := (Fdiv_def Fth).
+ Let rinv_l := (Finv_l Fth).
Let AFth := F2AF Rsth Reqe Fth.
Let ARth := Rth_ARth Rsth Reqe Rth.
diff --git a/plugins/setoid_ring/InitialRing.v b/plugins/setoid_ring/InitialRing.v
index 15d490a6ab..4886c8b9aa 100644
--- a/plugins/setoid_ring/InitialRing.v
+++ b/plugins/setoid_ring/InitialRing.v
@@ -51,9 +51,9 @@ Section ZMORPHISM.
Notation "x == y" := (req x y).
Variable Rsth : Setoid_Theory R req.
Add Parametric Relation : R req
- reflexivity proved by Rsth.(@Equivalence_Reflexive _ _)
- symmetry proved by Rsth.(@Equivalence_Symmetric _ _)
- transitivity proved by Rsth.(@Equivalence_Transitive _ _)
+ reflexivity proved by (@Equivalence_Reflexive _ _ Rsth)
+ symmetry proved by (@Equivalence_Symmetric _ _ Rsth)
+ transitivity proved by (@Equivalence_Transitive _ _ Rsth)
as R_setoid3.
Ltac rrefl := gen_reflexivity Rsth.
Variable Reqe : ring_eq_ext radd rmul ropp req.
@@ -267,9 +267,9 @@ Section NMORPHISM.
Notation "x + y" := (radd x y). Notation "x * y " := (rmul x y).
Variable Rsth : Setoid_Theory R req.
Add Parametric Relation : R req
- reflexivity proved by Rsth.(@Equivalence_Reflexive _ _)
- symmetry proved by Rsth.(@Equivalence_Symmetric _ _)
- transitivity proved by Rsth.(@Equivalence_Transitive _ _)
+ reflexivity proved by (@Equivalence_Reflexive _ _ Rsth)
+ symmetry proved by (@Equivalence_Symmetric _ _ Rsth)
+ transitivity proved by (@Equivalence_Transitive _ _ Rsth)
as R_setoid4.
Ltac rrefl := gen_reflexivity Rsth.
Variable SReqe : sring_eq_ext radd rmul req.
@@ -392,9 +392,9 @@ Section NWORDMORPHISM.
Notation "x == y" := (req x y).
Variable Rsth : Setoid_Theory R req.
Add Parametric Relation : R req
- reflexivity proved by Rsth.(@Equivalence_Reflexive _ _)
- symmetry proved by Rsth.(@Equivalence_Symmetric _ _)
- transitivity proved by Rsth.(@Equivalence_Transitive _ _)
+ reflexivity proved by (@Equivalence_Reflexive _ _ Rsth)
+ symmetry proved by (@Equivalence_Symmetric _ _ Rsth)
+ transitivity proved by (@Equivalence_Transitive _ _ Rsth)
as R_setoid5.
Ltac rrefl := gen_reflexivity Rsth.
Variable Reqe : ring_eq_ext radd rmul ropp req.
@@ -581,9 +581,9 @@ Section GEN_DIV.
(* Useful tactics *)
Add Parametric Relation : R req
- reflexivity proved by Rsth.(@Equivalence_Reflexive _ _)
- symmetry proved by Rsth.(@Equivalence_Symmetric _ _)
- transitivity proved by Rsth.(@Equivalence_Transitive _ _)
+ reflexivity proved by (@Equivalence_Reflexive _ _ Rsth)
+ symmetry proved by (@Equivalence_Symmetric _ _ Rsth)
+ transitivity proved by (@Equivalence_Transitive _ _ Rsth)
as R_set1.
Ltac rrefl := gen_reflexivity Rsth.
Add Morphism radd with signature (req ==> req ==> req) as radd_ext.
@@ -614,7 +614,7 @@ Section GEN_DIV.
Proof.
constructor.
intros a b;unfold triv_div.
- assert (X:= morph.(morph_eq) a b);destruct (ceqb a b).
+ assert (X:= morph_eq morph a b);destruct (ceqb a b).
Esimpl.
rewrite X; trivial.
rsimpl.
diff --git a/plugins/setoid_ring/Ring_polynom.v b/plugins/setoid_ring/Ring_polynom.v
index 12f716c496..f7cb6b688b 100644
--- a/plugins/setoid_ring/Ring_polynom.v
+++ b/plugins/setoid_ring/Ring_polynom.v
@@ -600,7 +600,7 @@ Section MakeRingPol.
Lemma pow_pos_add x i j : x^(j + i) == x^i * x^j.
Proof.
rewrite Pos.add_comm.
- apply (pow_pos_add Rsth Reqe.(Rmul_ext) ARth.(ARmul_assoc)).
+ apply (pow_pos_add Rsth (Rmul_ext Reqe) (ARmul_assoc ARth)).
Qed.
Lemma ceqb_spec c c' : BoolSpec ([c] == [c']) True (c ?=! c').
@@ -810,7 +810,7 @@ Section MakeRingPol.
Proof.
revert l.
induction P as [c0 | j P IH | P1 IH1 i P2 IH2]; intros l; Esimpl.
- - assert (H := div_th.(div_eucl_th) c0 c).
+ - assert (H := (div_eucl_th div_th) c0 c).
destruct cdiv as (q,r). rewrite H; Esimpl. add_permut.
- destr_factor. Esimpl.
- destr_factor. Esimpl. add_permut.
@@ -827,7 +827,7 @@ Section MakeRingPol.
try (case Pos.compare_spec; intros He);
rewrite ?He;
destr_factor; simpl; Esimpl.
- - assert (H := div_th.(div_eucl_th) c0 c).
+ - assert (H := div_eucl_th div_th c0 c).
destruct cdiv as (q,r). rewrite H; Esimpl. add_permut.
- assert (H := Mcphi_ok P c). destr_factor. Esimpl.
- now rewrite <- jump_add, Pos.sub_add.
@@ -1073,7 +1073,7 @@ Section POWER.
- rewrite IHpe1, IHpe2. now rewrite Pmul_ok.
- rewrite IHpe. Esimpl.
- rewrite Ppow_N_ok by reflexivity.
- rewrite pow_th.(rpow_pow_N). destruct n0; simpl; Esimpl.
+ rewrite (rpow_pow_N pow_th). destruct n0; simpl; Esimpl.
induction p;simpl; now rewrite ?IHp, ?IHpe, ?Pms_ok, ?Pmul_ok.
Qed.
@@ -1329,7 +1329,7 @@ Section POWER.
case_eq (get_sign c);intros.
assert (H1 := (morph_eq CRmorph) c0 cI).
destruct (c0 ?=! cI).
- rewrite (CRmorph.(morph_eq) _ _ (get_sign_spec.(sign_spec) _ H)). Esimpl. rewrite H1;trivial.
+ rewrite (morph_eq CRmorph _ _ (sign_spec get_sign_spec _ H)). Esimpl. rewrite H1;trivial.
rewrite <- r_list_pow_rev;trivial;Esimpl.
apply mkmultm1_ok.
rewrite <- r_list_pow_rev; apply mkmult_rec_ok.
@@ -1340,7 +1340,7 @@ Qed.
Proof.
intros;unfold mkadd_mult.
case_eq (get_sign c);intros.
- rewrite (CRmorph.(morph_eq) _ _ (get_sign_spec.(sign_spec) _ H));Esimpl.
+ rewrite (morph_eq CRmorph _ _ (sign_spec get_sign_spec _ H));Esimpl.
rewrite mkmult_c_pos_ok;Esimpl.
rewrite mkmult_c_pos_ok;Esimpl.
Qed.
@@ -1421,7 +1421,7 @@ Qed.
| xO _ => rpow r (Cp_phi (Npos p))
| 1 => r
end == pow_pos rmul r p.
- Proof. destruct p; now rewrite ?pow_th.(rpow_pow_N). Qed.
+ Proof. destruct p; now rewrite ?(rpow_pow_N pow_th). Qed.
Lemma Pphi_pow_ok : forall P fv, Pphi_pow fv P == P@fv.
Proof.
diff --git a/plugins/setoid_ring/Ring_theory.v b/plugins/setoid_ring/Ring_theory.v
index 6c782269ab..3e835f5c9f 100644
--- a/plugins/setoid_ring/Ring_theory.v
+++ b/plugins/setoid_ring/Ring_theory.v
@@ -358,7 +358,7 @@ Section ALMOST_RING.
rewrite <-(Radd_0_l Rth (- x * y)).
rewrite (Radd_comm Rth), <-(Ropp_def Rth (x*y)).
rewrite (Radd_assoc Rth), <- (Rdistr_l Rth).
- rewrite (Rth.(Radd_comm) (-x)), (Ropp_def Rth).
+ rewrite (Radd_comm Rth (-x)), (Ropp_def Rth).
now rewrite Rmul_0_l, (Radd_0_l Rth).
Qed.
@@ -407,9 +407,9 @@ Section ALMOST_RING.
Variable Ceqe : ring_eq_ext cadd cmul copp ceq.
Add Parametric Relation : C ceq
- reflexivity proved by Csth.(@Equivalence_Reflexive _ _)
- symmetry proved by Csth.(@Equivalence_Symmetric _ _)
- transitivity proved by Csth.(@Equivalence_Transitive _ _)
+ reflexivity proved by (@Equivalence_Reflexive _ _ Csth)
+ symmetry proved by (@Equivalence_Symmetric _ _ Csth)
+ transitivity proved by (@Equivalence_Transitive _ _ Csth)
as C_setoid.
Add Morphism cadd with signature (ceq ==> ceq ==> ceq) as cadd_ext.
@@ -430,7 +430,7 @@ Section ALMOST_RING.
Lemma Smorph_opp x : [-!x] == -[x].
Proof.
- rewrite <- (Rth.(Radd_0_l) [-!x]).
+ rewrite <- (Radd_0_l Rth [-!x]).
rewrite <- ((Ropp_def Rth) [x]).
rewrite ((Radd_comm Rth) [x]).
rewrite <- (Radd_assoc Rth).
@@ -498,12 +498,12 @@ Qed.
Lemma ARdistr_r x y z : z * (x + y) == z*x + z*y.
Proof.
- mrewrite. now rewrite !(ARth.(ARmul_comm) z).
+ mrewrite. now rewrite !(ARmul_comm ARth z).
Qed.
Lemma ARadd_assoc1 x y z : (x + y) + z == (y + z) + x.
Proof.
- now rewrite <-(ARth.(ARadd_assoc) x), (ARth.(ARadd_comm) x).
+ now rewrite <-(ARadd_assoc ARth x), (ARadd_comm ARth x).
Qed.
Lemma ARadd_assoc2 x y z : (y + x) + z == (y + z) + x.
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 20:04:16 +0000