proposition: Lemma semiring_correct (R : target_comSemiRing) (n : nat) (l : seq R) (lpe : seq (RExpr R * RExpr R * PExpr N * PExpr N)) (re1 re2 : RExpr R) (pe1 pe2 : PExpr N) : Reval_eqs lpe -> (forall R_of_N zero add one mul exp, SemiRing.Rnorm R_of_N zero add one mul exp (@target_comSemiRingMorph R) re1 :: SemiRing.Rnorm R_of_N zero add one mul exp (@target_comSemiRingMorph R) re2 :: Snorm_list R_of_N zero add one mul exp lpe = PEeval zero one add mul add id R_of_N id exp l pe1 :: PEeval zero one add mul add id R_of_N id exp l pe2 :: PEeval_list R_of_N zero id add add one mul exp l lpe) -> (let norm_subst' := norm_subst 0 1 N.add N.mul N.add id N.eqb (triv_div 0 1 N.eqb) n (mk_monpol_list 0 1 N.add N.mul N.add id N.eqb (triv_div 0 1 N.eqb) (map (fun '(_, _, lhs, rhs) => (lhs, rhs)) lpe)) in Peq N.eqb (norm_subst' pe1) (norm_subst' pe2)) -> Reval re1 = Reval re2.
proof: Proof. move=> Hlpe' /(_ (fun n => (nat_of_N n)%:R) 0%R +%R). move=> /(_ 1%R *%R (fun x n => x ^+ nat_of_N n)) /=. have /SemiRing.eq_Rnorm Hnorm: @target_comSemiRingMorph R =1 id. by case R => //= ?; lia. rewrite !{}Hnorm -!SemiRing.Rnorm_correct => -[-> -> Hlpe]; apply: Scorrect. elim: lpe Hlpe Hlpe' => [|[[[{}re1 {}re2] {}pe1] {}pe2] lpe IHlpe] //=. rewrite /= -!SemiRing.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)