From 40448753107577bdb17b089ecc3af64e0beabfd3 Mon Sep 17 00:00:00 2001 From: notin Date: Fri, 25 Apr 2008 18:12:30 +0000 Subject: Adaptation des fichiers de micromega suite aux changements dans setoid_rewrite, et dans Romega. MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Pour info, ces fichiers ne sont pas compilés... (?) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10851 85f007b7-540e-0410-9357-904b9bb8a0f7 --- contrib/micromega/RingMicromega.v | 18 +++++++++++------- 1 file changed, 11 insertions(+), 7 deletions(-) (limited to 'contrib/micromega/RingMicromega.v') 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. -- cgit v1.2.3