summaryrefslogtreecommitdiff
path: root/plugins/micromega/RingMicromega.v
diff options
context:
space:
mode:
authorGravatar Enrico Tassi <gareuselesinge@debian.org>2015-01-25 14:42:51 +0100
committerGravatar Enrico Tassi <gareuselesinge@debian.org>2015-01-25 14:42:51 +0100
commit7cfc4e5146be5666419451bdd516f1f3f264d24a (patch)
treee4197645da03dc3c7cc84e434cc31d0a0cca7056 /plugins/micromega/RingMicromega.v
parent420f78b2caeaaddc6fe484565b2d0e49c66888e5 (diff)
Imported Upstream version 8.5~beta1+dfsg
Diffstat (limited to 'plugins/micromega/RingMicromega.v')
-rw-r--r--plugins/micromega/RingMicromega.v31
1 files changed, 16 insertions, 15 deletions
diff --git a/plugins/micromega/RingMicromega.v b/plugins/micromega/RingMicromega.v
index a2136506..a0545637 100644
--- a/plugins/micromega/RingMicromega.v
+++ b/plugins/micromega/RingMicromega.v
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
@@ -57,7 +57,7 @@ Variables ceqb cleb : C -> C -> bool.
Variable phi : C -> R.
(* Power coefficients *)
-Variable E : Set. (* the type of exponents *)
+Variable E : Type. (* the type of exponents *)
Variable pow_phi : N -> E.
Variable rpow : R -> E -> R.
@@ -78,9 +78,9 @@ 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 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.
@@ -141,8 +141,8 @@ Qed.
Definition PolC := Pol C. (* polynomials in generalized Horner form, defined in Ring_polynom or EnvRing *)
Definition PolEnv := Env R. (* For interpreting PolC *)
-Definition eval_pol (env : PolEnv) (p:PolC) : R :=
- Pphi rplus rtimes phi env p.
+Definition eval_pol : PolEnv -> PolC -> R :=
+ Pphi rplus rtimes phi.
Inductive Op1 : Set := (* relations with 0 *)
| Equal (* == 0 *)
@@ -412,12 +412,12 @@ Proof.
induction e.
(* PsatzIn *)
simpl ; intros.
- destruct (nth_in_or_default n l (Pc cO, Equal)).
+ destruct (nth_in_or_default n l (Pc cO, Equal)) as [Hin|Heq].
(* index is in bounds *)
- apply H ; congruence.
+ apply H. congruence.
(* index is out-of-bounds *)
inversion H0.
- rewrite e. simpl.
+ rewrite Heq. simpl.
now apply addon.(SORrm).(morph0).
(* PsatzSquare *)
simpl. intros. inversion H0.
@@ -679,7 +679,8 @@ match o with
| OpGt => fun x y : R => y < x
end.
-Definition eval_pexpr (l : PolEnv) (pe : PExpr C) : R := PEeval rplus rtimes rminus ropp phi pow_phi rpow l pe.
+Definition eval_pexpr : PolEnv -> PExpr C -> R :=
+ PEeval rplus rtimes rminus ropp phi pow_phi rpow.
Record Formula (T:Type) : Type := {
Flhs : PExpr T;
@@ -910,7 +911,7 @@ Proof.
unfold pow_N. ring.
Qed.
-Definition denorm (p : Pol C) := xdenorm xH p.
+Definition denorm := xdenorm xH.
Lemma denorm_correct : forall p env, eval_pol env p == eval_pexpr env (denorm p).
Proof.
@@ -947,7 +948,7 @@ Variable phi_C_of_S : forall c, phiS c = phi (C_of_S c).
Fixpoint map_PExpr (e : PExpr S) : PExpr C :=
match e with
| PEc c => PEc (C_of_S c)
- | PEX p => PEX _ p
+ | PEX _ p => PEX _ p
| PEadd e1 e2 => PEadd (map_PExpr e1) (map_PExpr e2)
| PEsub e1 e2 => PEsub (map_PExpr e1) (map_PExpr e2)
| PEmul e1 e2 => PEmul (map_PExpr e1) (map_PExpr e2)
@@ -960,8 +961,8 @@ Definition map_Formula (f : Formula S) : Formula C :=
Build_Formula (map_PExpr l) o (map_PExpr r).
-Definition eval_sexpr (env : PolEnv) (e : PExpr S) : R :=
- PEeval rplus rtimes rminus ropp phiS pow_phi rpow env e.
+Definition eval_sexpr : PolEnv -> PExpr S -> R :=
+ PEeval rplus rtimes rminus ropp phiS pow_phi rpow.
Definition eval_sformula (env : PolEnv) (f : Formula S) : Prop :=
let (lhs, op, rhs) := f in