fact: Fixpoint Reval R (e : RExpr R) : R := match e with | R0 _ => 0%R | RAdd _ e1 e2 => Reval e1 + Reval e2 | RnatAdd e1 e2 => addn (Reval e1) (Reval e2) | RNAdd e1 e2 => N.add (Reval e1) (Reval e2) | RZAdd e1 e2 => Z.add (Reval e1) (Reval e2) | RMuln _ e1 e2 => Reval e1 *+ Reval e2 | ROpp _ e1 => - Reval e1 | RZOpp e1 => Z.opp (Reval e1) | RZSub e1 e2 => Z.sub (Reval e1) (Reval e2) | RMulz _ e1 e2 => Reval e1 *~ Reval e2 | R1 _ => 1%R | RMul _ e1 e2 => Reval e1 * Reval e2 | RnatMul e1 e2 => muln (Reval e1) (Reval e2) | RNMul e1 e2 => N.mul (Reval e1) (Reval e2) | RZMul e1 e2 => Z.mul (Reval e1) (Reval e2) | RExpn _ e1 n => Reval e1 ^+ nat_of_large_nat n | RExpPosz _ e1 n => Reval e1 ^ Posz (nat_of_large_nat n) | RExpNegz _ e1 n => Reval e1 ^ Negz (nat_of_large_nat n) | RnatExpn e1 n => expn (Reval e1) (nat_of_large_nat n) | RNExp e1 n => N.pow (Reval e1) n | RZExp e1 n => Z.pow (Reval e1) n | RInv _ e1 => (Reval e1)^-1 | RnatS p e => add_pos_nat p (Reval e) | RnatC n => nat_of_large_nat n | RPosz e1 => Posz (Reval e1) | RNegz e2 => Negz (Reval e2) | RMorph _ _ f e1 | RnatMorph _ f e1 | RNMorph _ f e1 | RintMorph _ f e1 | RZMorph _ f e1 | RnatAdditive _ f e1 | RNAdditive _ f e1 | RintAdditive _ f e1 | RZAdditive _ f e1 => f (Reval e1) | RAdditive _ _ f e1 => f (Meval e1) | RNC n | RZC n => n | RX _ x => x end with Meval V (e : MExpr V) : V := match e with | M0 _ => 0%R | MAdd _ e1 e2 => Meval e1 + Meval e2 | MMuln _ e1 e2 => Meval e1 *+ Reval e2 | MOpp _ e1 => - Meval e1 | MMulz _ e1 e2 => Meval e1 *~ Reval e2 | MAdditive _ _ f e1 => f (Meval e1) | MnatAdditive _ f e1 | MNAdditive _ f e1 | MintAdditive _ f e1 | MZAdditive _ f e1 => f (Reval e1) | MX _ x => x end.
imports: elpi(elpi) Coq(QArith) Coq.micromega(OrderedRing RingMicromega) mathcomp(all_ssreflect ssralg ssrnum ssrint) mathcomp.zify(ssrZ zify)