diff options
| author |  Pierre Boutillier <pierre.boutillier@ens-lyon.org> | 2014-04-23 13:42:25 +0200 |
|---|---|---|
| committer | Pierre Boutillier <pierre.boutillier@ens-lyon.org> | 2014-05-02 11:04:21 +0200 |
| commit | c33ba30ec4e8ed636906d824c300788e10df20b5 (patch) | |
| tree | 9fea5f5aabf3c024413b0ba7c5b193a58b74feea /plugins/micromega/RingMicromega.v | |
| parent | ec9ee383575ed356438644d38c1cc8e05325537f (diff) | |
Eta contractions to please cbn
Diffstat (limited to 'plugins/micromega/RingMicromega.v')
| -rw-r--r-- | plugins/micromega/RingMicromega.v | 13 |
1 files changed, 7 insertions, 6 deletions
diff --git a/plugins/micromega/RingMicromega.v b/plugins/micromega/RingMicromega.v index 018b5c83f..68add5b3d 100644 --- a/plugins/micromega/RingMicromega.v +++ b/plugins/micromega/RingMicromega.v @@ -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 *) @@ -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. @@ -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 |