proposition: Lemma Rnorm_correct_rec R (f : {rmorphism R -> R'}) (e : RExpr R) : f (Reval e) = Rnorm f e.
proof: Proof. pose P R e := forall (f : {rmorphism R -> R'}), f (Reval e) = Rnorm f e. pose P0 V e := forall (f : {additive V -> R'}), f (Meval e) = Mnorm f e. move: f; elim e using (@RExpr_ind' P P0); rewrite {R e}/P {}/P0 //=. - by move=> R f; rewrite rmorph0. - by move=> R e1 IHe1 e2 IHe2 f; rewrite rmorphD IHe1 IHe2. - by move=> e1 IHe1 e2 IHe2 f; rewrite rmorphD IHe1 IHe2. - by move=> e1 IHe1 e2 IHe2 f; rewrite rmorphD IHe1 IHe2. - by move=> R e1 IHe1 e2 IHe2 f; rewrite rmorphMn -mulr_natr IHe1 IHe2. - by move=> R f; rewrite rmorph1. - by move=> R e1 IHe1 e2 IHe2 f; rewrite rmorphM IHe1 IHe2. - by move=> e1 IHe1 e2 IHe2 f; rewrite rmorphM IHe1 IHe2. - by move=> e1 IHe1 e2 IHe2 f; rewrite rmorphM IHe1 IHe2. - by move=> R e1 IHe1 n f; rewrite rmorphXn IHe1 -large_nat_N_nat. - by move=> R e1 IHe1 n f; rewrite rmorphXn IHe1 -large_nat_N_nat. - by move=> e1 IHe1 n f; rewrite rmorphXn IHe1 -large_nat_N_nat. - move=> e1 IHe1 n f. have ->: (Reval e1 ^ n)%num = Reval e1 ^+ N.to_nat n by lia. by rewrite rmorphXn IHe1. - move=> p e1 IHe1 f. by rewrite add_pos_natE rmorphD IHe1 -[Pos.to_nat p in LHS]natn rmorph_nat. - by move=> n f; rewrite -[nat_of_large_nat _]natn rmorph_nat -large_nat_N_nat. - by move=> n f; rewrite -[RHS](rmorph_nat f); congr (f _); lia. - by move=> R S g e1 IHe1 f; rewrite -/(comp f g _) IHe1. - move=> R g e1 IHe1 f; rewrite -/(comp f g _) IHe1; apply: eq_Rnorm => /= n. by rewrite -[RHS](rmorph_nat (f \o g)) natn. - move=> R g e1 IHe1 f; rewrite -/(comp f g _) IHe1; apply: eq_Rnorm => /= n. by rewrite -[RHS](rmorph_nat (f \o g)); congr (f (g _)); lia. - by move=> V R g e1 IHe1 f; rewrite -/(comp f g _) IHe1. - by move=> R g e1 IHe1 f; rewrite -[Reval e1]natn !raddfMn -mulr_natr IHe1. - move=> R g e1 IHe1 f. have ->: Reval e1 = (N.to_nat (Reval e1))%:R by lia. by rewrite !raddfMn -mulr_natr -/(comp _ N.to_nat _) IHe1. - by move=> V f; rewrite raddf0. - by move=> V e1 IHe1 e2 IHe2 f; rewrite raddfD IHe1 IHe2. - by move=> V e1 IHe1 e2 IHe2 f; rewrite raddfMn -mulr_natr IHe1 IHe2. - by move=> V V' g e1 IHe1 f; rewrite -/(comp f g _) IHe1. - by move=> V g e1 IHe1 f; rewrite -[Reval e1]natn !raddfMn -mulr_natr IHe1. - move=> v g e1 IHe1 f. have ->: Reval e1 = (N.to_nat (Reval e1))%:R by lia. by rewrite !raddfMn -mulr_natr -/(comp _ N.to_nat _) IHe1. Qed.
imports: elpi(elpi) Coq(QArith) Coq.micromega(OrderedRing RingMicromega) mathcomp(all_ssreflect ssralg ssrnum ssrint) mathcomp.zify(ssrZ zify)