aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--contrib/micromega/CheckerMaker.v6
-rw-r--r--contrib/micromega/NRing.v8
-rw-r--r--contrib/micromega/OrderedRing.v8
-rw-r--r--contrib/micromega/RingMicromega.v18
-rw-r--r--contrib/micromega/ZCoeff.v10
5 files changed, 29 insertions, 21 deletions
diff --git a/contrib/micromega/CheckerMaker.v b/contrib/micromega/CheckerMaker.v
index 8aeada77b..8c491a55e 100644
--- a/contrib/micromega/CheckerMaker.v
+++ b/contrib/micromega/CheckerMaker.v
@@ -2,10 +2,11 @@
(* *)
(* Micromega: A reflexive tactics using the Positivstellensatz *)
(* *)
-(* Frédéric Besson (Irisa/Inria) 2006 *)
+(* Frédéric Besson (Irisa/Inria) 2006 *)
(* *)
(********************************************************************)
+Require Import Setoid.
Require Import Decidable.
Require Import List.
Require Import Refl.
@@ -113,7 +114,8 @@ assert (H2 : make_impl (eval' env) (negate a2 :: normalise_list t1) False) by
now apply check_formulas'_sound with (w := w). clear H1.
pose proof (IH ws H env) as H1. simpl in H2.
assert (H3 : eval' env (negate a2) -> make_impl (eval env) t1 False)
-by auto using normalise_sound_contr. clear H2. rewrite <- make_conj_impl in *.
+by auto using normalise_sound_contr. clear H2.
+rewrite <- make_conj_impl in *.
rewrite make_conj_cons. intro H2. split.
apply <- negate_correct. intro; now elim H3. exact (H1 H2).
Qed.
diff --git a/contrib/micromega/NRing.v b/contrib/micromega/NRing.v
index 77e098d0f..b4c9cffe6 100644
--- a/contrib/micromega/NRing.v
+++ b/contrib/micromega/NRing.v
@@ -67,7 +67,7 @@ Section MakeRingPol.
Add Morphism rmul : rmul_ext. exact (Rmul_ext Reqe). Qed.
Add Morphism ropp : ropp_ext. exact (Ropp_ext Reqe). Qed.
Add Morphism rsub : rsub_ext. exact (ARsub_ext Rsth Reqe ARth). Qed.
- Ltac rsimpl := gen_srewrite 0 1 radd rmul rsub ropp req Rsth Reqe ARth.
+ Ltac rsimpl := gen_srewrite Rsth Reqe ARth.
Ltac add_push := gen_add_push radd Rsth Reqe ARth.
Ltac mul_push := gen_mul_push rmul Rsth Reqe ARth.
@@ -1027,7 +1027,7 @@ Lemma Pmul_ok : forall P P' l, (P**P')@l == P@l * P'@l.
rewrite Padd_ok; rewrite PmulC_ok; rsimpl.
intros i P5 H; rewrite H.
intros HH H1; injection HH; intros; subst; rsimpl.
- rewrite Padd_ok; rewrite PmulI_ok. intros;apply Pmul_ok. rewrite H1; rsimpl.
+ rewrite Padd_ok; rewrite PmulI_ok by (intros; apply Pmul_ok). rewrite H1; rsimpl.
intros i P5 P6 H1 H2 H3; rewrite H1; rewrite H3.
assert (P4 = Q1 ++ P3 ** PX i P5 P6).
injection H2; intros; subst;trivial.
@@ -1226,7 +1226,7 @@ Section POWER.
Lemma Ppow_N_ok : forall l, (forall P, subst_l P@l == P@l) ->
forall P n, (Ppow_N P n)@l == (pow_N P1 Pmul P n)@l.
- Proof. destruct n;simpl. rrefl. rewrite Ppow_pos_ok. trivial. Esimpl. Qed.
+ Proof. destruct n;simpl. rrefl. rewrite Ppow_pos_ok by trivial. Esimpl. Qed.
End POWER.
@@ -1302,7 +1302,7 @@ Section POWER.
rewrite IHpe1;rewrite IHpe2;rrefl.
rewrite IHpe1;rewrite IHpe2. rewrite Pmul_ok. rrefl.
rewrite IHpe;rrefl.
- rewrite Ppow_N_ok. intros;rrefl.
+ rewrite Ppow_N_ok by (intros; rrefl).
rewrite pow_th.(rpow_pow_N). destruct n0;Esimpl3.
induction p;simpl;try rewrite IHp;try rewrite IHpe;repeat rewrite Pms_ok;
repeat rewrite Pmul_ok;rrefl.
diff --git a/contrib/micromega/OrderedRing.v b/contrib/micromega/OrderedRing.v
index ac1833a13..c6dd5ccf0 100644
--- a/contrib/micromega/OrderedRing.v
+++ b/contrib/micromega/OrderedRing.v
@@ -72,9 +72,9 @@ Notation "x <= y" := (rle x y).
Notation "x < y" := (rlt x y).
Add Relation R req
- reflexivity proved by sor.(SORsetoid).(Seq_refl _ _)
- symmetry proved by sor.(SORsetoid).(Seq_sym _ _)
- transitivity proved by sor.(SORsetoid).(Seq_trans _ _)
+ reflexivity proved by sor.(SORsetoid).(@Equivalence_Reflexive _ _)
+ symmetry proved by sor.(SORsetoid).(@Equivalence_Symmetric _ _)
+ transitivity proved by sor.(SORsetoid).(@Equivalence_Transitive _ _)
as sor_setoid.
Add Morphism rplus with signature req ==> req ==> req as rplus_morph.
@@ -417,7 +417,7 @@ Qed.
Theorem Rlt_0_1 : 0 < 1.
Proof.
apply <- Rlt_le_neq. split.
-setoid_replace 1 with (1 * 1) by ring; apply Rtimes_square_nonneg.
+setoid_replace 1 with (1 * 1) by ring. apply Rtimes_square_nonneg.
apply Rneq_0_1.
Qed.
diff --git a/contrib/micromega/RingMicromega.v b/contrib/micromega/RingMicromega.v
index b118f8d99..5aca6e697 100644
--- a/contrib/micromega/RingMicromega.v
+++ b/contrib/micromega/RingMicromega.v
@@ -71,9 +71,9 @@ Record SORaddon := mk_SOR_addon {
Variable addon : SORaddon.
Add Relation R req
- reflexivity proved by sor.(SORsetoid).(Seq_refl _ _)
- symmetry proved by sor.(SORsetoid).(Seq_sym _ _)
- transitivity proved by sor.(SORsetoid).(Seq_trans _ _)
+ reflexivity proved by sor.(SORsetoid).(@Equivalence_Reflexive _ _)
+ symmetry proved by sor.(SORsetoid).(@Equivalence_Symmetric _ _)
+ transitivity proved by sor.(SORsetoid).(@Equivalence_Transitive _ _)
as micomega_sor_setoid.
Add Morphism rplus with signature req ==> req ==> req as rplus_morph.
@@ -90,15 +90,17 @@ exact sor.(SORopp_wd).
Qed.
Add Morphism rle with signature req ==> req ==> iff as rle_morph.
Proof.
-exact sor.(SORle_wd).
+ exact sor.(SORle_wd).
Qed.
Add Morphism rlt with signature req ==> req ==> iff as rlt_morph.
Proof.
-exact sor.(SORlt_wd).
+ exact sor.(SORlt_wd).
Qed.
Add Morphism rminus with signature req ==> req ==> req as rminus_morph.
-Proof (rminus_morph sor). (* We already proved that minus is a morphism in OrderedRing.v *)
+Proof.
+ exact (rminus_morph sor). (* We already proved that minus is a morphism in OrderedRing.v *)
+Qed.
Definition cneqb (x y : C) := negb (ceqb x y).
Definition cltb (x y : C) := (cleb x y) && (cneqb x y).
@@ -111,7 +113,9 @@ Ltac le_equal := rewrite (Rle_lt_eq sor); right; try reflexivity; try assumption
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 addon.(SORcleb_morph).
+Proof.
+ exact addon.(SORcleb_morph).
+Qed.
Lemma cneqb_sound : forall x y : C, x [~=] y = true -> [x] ~= [y].
Proof.
diff --git a/contrib/micromega/ZCoeff.v b/contrib/micromega/ZCoeff.v
index 20c900780..791e00a90 100644
--- a/contrib/micromega/ZCoeff.v
+++ b/contrib/micromega/ZCoeff.v
@@ -30,9 +30,9 @@ Notation "x <= y" := (rle x y).
Notation "x < y" := (rlt x y).
Add Relation R req
- reflexivity proved by sor.(SORsetoid).(Seq_refl _ _)
- symmetry proved by sor.(SORsetoid).(Seq_sym _ _)
- transitivity proved by sor.(SORsetoid).(Seq_trans _ _)
+ reflexivity proved by sor.(SORsetoid).(@Equivalence_Reflexive _ _)
+ symmetry proved by sor.(SORsetoid).(@Equivalence_Symmetric _ _)
+ transitivity proved by sor.(SORsetoid).(@Equivalence_Transitive _ _)
as sor_setoid.
Add Morphism rplus with signature req ==> req ==> req as rplus_morph.
@@ -56,7 +56,9 @@ Proof.
exact sor.(SORlt_wd).
Qed.
Add Morphism rminus with signature req ==> req ==> req as rminus_morph.
-Proof (rminus_morph sor).
+Proof.
+ exact (rminus_morph sor).
+Qed.
Ltac le_less := rewrite (Rle_lt_eq sor); left; try assumption.
Ltac le_equal := rewrite (Rle_lt_eq sor); right; try reflexivity; try assumption.
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-06 06:21:34 +0000