proposition: Lemma ring_correct (R : target_comRing) (n : nat) (l : seq R) (lpe : seq (RExpr R * RExpr R * PExpr Z * PExpr Z)) (re1 re2 : RExpr R) (pe1 pe2 : PExpr Z) : Reval_eqs lpe -> (forall R_of_Z zero opp add sub_ one mul exp, Ring.Rnorm R_of_Z zero add opp sub_ one mul exp (@target_comRingMorph R) re1 :: Ring.Rnorm R_of_Z zero add opp sub_ one mul exp (@target_comRingMorph R) re2 :: Rnorm_list R_of_Z zero add opp sub_ one mul exp lpe = PEeval zero one add mul sub_ opp R_of_Z id exp l pe1 :: PEeval zero one add mul sub_ opp R_of_Z id exp l pe2 :: PEeval_list R_of_Z zero opp add sub_ one mul exp l lpe) -> (let norm_subst' := norm_subst 0 1 Z.add Z.mul Z.sub Z.opp Z.eqb (triv_div 0 1 Z.eqb) n (mk_monpol_list 0 1 Z.add Z.mul Z.sub Z.opp Z.eqb (triv_div 0 1 Z.eqb) (map (fun '(_, _, lhs, rhs) => (lhs, rhs)) lpe)) in Peq Z.eqb (norm_subst' pe1) (norm_subst' pe2)) -> Reval re1 = Reval re2.
proof: Proof. move=> Hlpe' /(_ (fun n => (int_of_Z n)%:~R) 0%R -%R +%R (fun x y => x - y)). move=> /(_ 1%R *%R (fun x n => x ^+ nat_of_N n)) /=. have /Ring.eq_Rnorm Hnorm: @target_comRingMorph R =1 id by case R => //= ?; lia. rewrite !Hnorm -!Ring.Rnorm_correct => -[-> -> Hlpe]; apply: Rcorrect. elim: lpe Hlpe Hlpe' => [|[[[{}re1 {}re2] {}pe1] {}pe2] lpe IHlpe] //=. rewrite /= -!Ring.Rnorm_correct //. by move=> [-> ->] Hlpe [Hpe /(IHlpe Hlpe)] {IHlpe Hlpe} /=; case: lpe. Qed.
imports: elpi(elpi) Coq(ZArith Ring Ring_polynom Field_theory) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat choice seq) mathcomp(fintype finfun bigop order ssralg ssrnum ssrint) mathcomp.zify(ssrZ zify) mathcomp.algebra_tactics(common)