proposition: Lemma Rnorm_correct_rec (invb : bool) R (f : {rmorphism R -> F}) (e : RExpr R) : (if invb then (f (Reval e))^-1 else f (Reval e)) = Rnorm invb f e.
proof: Proof. pose P R e := forall invb (f : {rmorphism R -> F}), (if invb then (f (Reval e))^-1 else f (Reval e)) = Rnorm invb f e. pose P0 V e := forall invb (f : {additive V -> F}), (if invb then (f (Meval e))^-1 else f (Meval e)) = Mnorm invb f e. move: invb f; elim e using (@RExpr_ind' P P0); rewrite {R e}/P {}/P0 //=. - by move=> R invb f; rewrite rmorph0 invr0 if_same. - by move=> R e1 IHe1 e2 IHe2 invb f; rewrite rmorphD (IHe1 false) (IHe2 false). - by move=> e1 IHe1 e2 IHe2 invb f; rewrite rmorphD (IHe1 false) (IHe2 false). - by move=> e1 IHe1 e2 IHe2 invb f; rewrite rmorphD (IHe1 false) (IHe2 false). - by move=> e1 IHe1 e2 IHe2 invb f; rewrite rmorphD (IHe1 false) (IHe2 false). - move=> R e1 IHe1 e2 IHe2 invb f; rewrite rmorphMn -mulr_natr invfM. by rewrite (IHe1 true) (IHe2 true) (IHe1 false) (IHe2 false); case: invb. - move=> R e1 IHe1 invb f. by rewrite rmorphN invrN (IHe1 true) (IHe1 false); case: invb. - move=> e1 IHe1 invb f. by rewrite rmorphN invrN (IHe1 true) (IHe1 false); case: invb. - by move=> e1 IHe1 e2 IHe2 invb f; rewrite rmorphB (IHe1 false) (IHe2 false). - move=> R e1 IHe1 e2 IHe2 invb f; rewrite rmorphMz -mulrzr invfM. by rewrite (IHe1 true) (IHe2 true) (IHe1 false) (IHe2 false); case: invb. - by move=> R invb f; rewrite rmorph1 invr1 if_same. - move=> R e1 IHe1 e2 IHe2 invb f; rewrite rmorphM invfM. by rewrite (IHe1 true) (IHe2 true) (IHe1 false) (IHe2 false); case: invb. - move=> e1 IHe1 e2 IHe2 invb f; rewrite rmorphM invfM. by rewrite (IHe1 true) (IHe2 true) (IHe1 false) (IHe2 false); case: invb. - move=> e1 IHe1 e2 IHe2 invb f; rewrite rmorphM invfM. by rewrite (IHe1 true) (IHe2 true) (IHe1 false) (IHe2 false); case: invb. - move=> e1 IHe1 e2 IHe2 invb f; rewrite rmorphM invfM. by rewrite (IHe1 true) (IHe2 true) (IHe1 false) (IHe2 false); case: invb. - move=> R e1 IHe1 n invb f; rewrite rmorphXn -exprVn (IHe1 true) (IHe1 false). by rewrite -large_nat_N_nat; case: invb. - move=> R e1 IHe1 n invb f; rewrite rmorphXn -exprVn (IHe1 true) (IHe1 false). by rewrite -large_nat_N_nat; case: invb. - move=> R e1 IHe1 n invb f; rewrite fmorphV rmorphXn invrK -exprVn. rewrite (IHe1 true) (IHe1 false) -large_nat_N_nat. by case: invb; congr (_ ^+ _); lia. - move=> e1 IHe1 n invb f; rewrite rmorphXn -exprVn (IHe1 true) (IHe1 false). by rewrite -large_nat_N_nat; case: invb. - move=> e1 IHe1 n invb f. have ->: (Reval e1 ^ n)%num = Reval e1 ^+ N.to_nat n by lia. by rewrite rmorphXn -exprVn (IHe1 true) (IHe1 false); case: invb. - move=> e1 IHe1 [|p|p] invb f; rewrite ?(rmorph0, rmorph1, invr0, invr1, if_same) //=. rewrite /Rnorm /= -/(Rnorm _) -IHe1 (fun_if (fun x => GRing.exp x _)). by rewrite exprVn -rmorphXn; congr (if _ then (f _)^-1 else f _); lia. - by move=> R e1 IHe1 invb f; rewrite fmorphV invrK -if_neg IHe1. - move=> p e1 IHe1 invb f; rewrite add_pos_natE rmorphD (IHe1 false). by rewrite -[Pos.to_nat p in LHS]natn rmorph_nat. - move=> n invb f. by rewrite -[nat_of_large_nat _]natn rmorph_nat pmulrn -large_nat_Z_int. - move=> e1 IHe1 invb f; rewrite -[Posz _]intz rmorph_int -pmulrn. by rewrite (IHe1 true) (IHe1 false); case: invb. - move=> e1 IHe1 invb f. by rewrite -[Negz _]intz rmorph_int /intmul mulrS (IHe1 false). - move=> n invb f; rewrite /Rnorm. have ->: int_of_Z (Z_of_N n) = nat_of_N n by lia. rewrite -[_%:~R](rmorph_nat f). by case: invb; [congr (_ ^-1)|]; congr (f _); lia. - move=> n invb f; rewrite /Rnorm -(rmorph_int f). by case: invb; [congr (_ ^-1)|]; congr (f _); lia. - by move=> R S g e1 IHe1 invb f; rewrite -/(comp f g _) IHe1. - move=> R g e1 IHe1 invb f; rewrite -/(comp f g _) IHe1. by apply: eq_Rnorm => /= n; rewrite -[RHS](rmorph_nat (f \o g)) natn. - move=> R g e1 IHe1 invb f; rewrite -/(comp f g _) IHe1. apply: eq_Rnorm => /= n; rewrite -[RHS](rmorph_nat (f \o g)). by congr (f (g _)); lia. - move=> R g e1 IHe1 invb f; rewrite -/(comp f g _) IHe1. apply: eq_Rnorm => /= n; rewrite -[RHS](rmorph_int (f \o g)). by congr (f (g _)); lia. - move=> R g e1 IHe1 invb f; rewrite -/(comp f g _) IHe1. apply: eq_Rnorm => /= n; rewrite -[RHS](rmorph_int (f \o g)). by congr (f (g _)); lia. - by move=> V R g e1 IHe1 invb f; rewrite -/(comp f g _) IHe1. - move=> R g e1 IHe1 invb f. rewrite -[Reval e1]natn !raddfMn -mulr_natr ?invfM. by rewrite (IHe1 true) (IHe1 false); case: invb. - move=> R g e1 IHe1 invb f. have ->: Reval e1 = (N.to_nat (Reval e1))%:R by lia. rewrite !raddfMn -mulr_natr -/(comp _ N.to_nat _) ?invfM. by rewrite (IHe1 true) (IHe1 false); case: invb. - move=> R g e1 IHe1 invb f. rewrite -[Reval e1]intz ![f _](raddfMz (f \o g)) -mulrzr ?invfM. by rewrite (IHe1 true) (IHe1 false); case:invb. - move=> R g e1 IHe1 invb f. have ->: Reval e1 = (int_of_Z (Reval e1))%:~R by lia. rewrite [f _](raddfMz (f \o g)) -mulrzr -/(comp _ int_of_Z _) ?invfM. by rewrite (IHe1 true) (IHe1 false); case:invb. - by move=> V invb f; rewrite raddf0 invr0 if_same. - by move=> V e1 IHe1 e2 IHe2 invb f; rewrite raddfD (IHe1 false) (IHe2 false). - move=> V e1 IHe1 e2 IHe2 invb f; rewrite raddfMn -mulr_natr invfM. by rewrite (IHe1 true) (IHe2 true) (IHe1 false) (IHe2 false); case: invb. - move=> V e1 IHe1 invb f. by rewrite raddfN invrN (IHe1 true) (IHe1 false); case: invb. - move=> V e1 IHe1 e2 IHe2 invb f; rewrite raddfMz -mulrzr invfM. by rewrite (IHe1 true) (IHe2 true) (IHe1 false) (IHe2 false); case: invb. - by move=> V V' g e1 IHe1 invb f; rewrite -/(comp f g _) IHe1. - move=> V g e1 IHe1 invb f; rewrite -[Reval e1]natn !raddfMn -mulr_natr invfM. by rewrite (IHe1 true) (IHe1 false); case: invb. - move=> V g e1 IHe1 invb f. have ->: Reval e1 = (N.to_nat (Reval e1))%:R by lia. rewrite !raddfMn -mulr_natr invfM -/(comp _ N.to_nat _). by rewrite (IHe1 true) (IHe1 false); case: invb. - move=> V g e1 IHe1 invb f. rewrite -[Reval e1]intz ![f _](raddfMz (f \o g)) -mulrzr invfM. by rewrite (IHe1 true) (IHe1 false); case: invb. - move=> V g e1 IHe1 invb f. have ->: Reval e1 = (int_of_Z (Reval e1))%:~R by lia. rewrite [f _](raddfMz (f \o g)) -mulrzr -/(comp _ int_of_Z _) invfM. by rewrite (IHe1 true) (IHe1 false); case: invb. Qed.
imports: elpi(elpi) Coq(QArith) Coq.micromega(OrderedRing RingMicromega) mathcomp(all_ssreflect ssralg ssrnum ssrint) mathcomp.zify(ssrZ zify)