diff options
Diffstat (limited to 'plugins/micromega/RingMicromega.v')
| -rw-r--r-- | plugins/micromega/RingMicromega.v | 31 |
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 |