fact: Fixpoint Rnorm R (f : R -> R') (e : RExpr R) : R' := match e in RExpr R return (R -> R') -> R' with | R0 _ => fun => zero | RAdd _ e1 e2 | RnatAdd e1 e2 | RNAdd e1 e2 => fun f => add (Rnorm f e1) (Rnorm f e2) | RMuln _ e1 e2 => fun f => mul (Rnorm f e1) (Rnorm (GRing.natmul 1) e2) | R1 _ => fun => one | RMul _ e1 e2 | RnatMul e1 e2 | RNMul e1 e2 => fun f => mul (Rnorm f e1) (Rnorm f e2) | RExpn _ e1 n | RnatExpn e1 n => fun f => exp (Rnorm f e1) (N_of_large_nat n) | RExpPosz _ e1 n => fun f => exp (Rnorm f e1) (N_of_large_nat n) | RNExp e1 n => fun f => exp (Rnorm f e1) n | RnatS p e => fun f => add (R_of_N (Npos p)) (Rnorm f e) | RnatC n => fun => R_of_N (N_of_large_nat n) | RNC n => fun => R_of_N n | RMorph _ _ g e1 => fun f => Rnorm (fun x => f (g x)) e1 | RnatMorph _ _ e1 => fun => Rnorm (GRing.natmul 1) e1 | RNMorph _ _ e1 => fun => Rnorm (fun n => (N.to_nat n)%:R) e1 | RAdditive _ _ g e1 => fun f => Mnorm (fun x => f (g x)) e1 | RnatAdditive _ g e1 => fun f => mul (f (g 1%N)) (Rnorm (GRing.natmul 1) e1) | RNAdditive _ g e1 => fun f => mul (f (g 1%num)) (Rnorm (fun n => (N.to_nat n)%:R) e1) | RX _ x => fun f => f x | _ => fun => f (Reval e) end f with Mnorm V (f : V -> R') (e : MExpr V) : R' := match e in MExpr V return (V -> R') -> R' with | M0 _ => fun => zero | MAdd _ e1 e2 => fun f => add (Mnorm f e1) (Mnorm f e2) | MMuln _ e1 e2 => fun f => mul (Mnorm f e1) (Rnorm (GRing.natmul 1) e2) | MAdditive _ _ g e1 => fun f => Mnorm (fun x => f (g x)) e1 | MnatAdditive _ g e1 => fun f => mul (f (g 1%N)) (Rnorm (GRing.natmul 1) e1) | MNAdditive _ g e1 => fun f => mul (f (g 1%num)) (Rnorm (fun n => (N.to_nat n)%:R) e1) | MX _ x => fun f => f x | _ => fun => f (Meval e) end f.
imports: elpi(elpi) Coq(QArith) Coq.micromega(OrderedRing RingMicromega) mathcomp(all_ssreflect ssralg ssrnum ssrint) mathcomp.zify(ssrZ zify)