proposition: Lemma field_correct (F : fieldType) (n : nat) (l : seq F) (lpe : seq (RExpr F * RExpr F * PExpr Z * PExpr Z)) (re1 re2 : RExpr F) (fe1 fe2 : FExpr Z) : Reval_eqs lpe -> (forall R_of_Z zero opp add sub_ one mul exp div inv, Field.Rnorm R_of_Z zero add opp sub_ one mul exp inv id re1 :: Field.Rnorm R_of_Z zero add opp sub_ one mul exp inv id re2 :: Rnorm_list R_of_Z zero add opp sub_ one mul exp lpe = FEeval zero one add mul sub_ opp div inv R_of_Z id exp l fe1 :: FEeval zero one add mul sub_ opp div inv R_of_Z id exp l fe2 :: PEeval_list R_of_Z zero opp add sub_ one mul exp l lpe) -> (forall is_true_ negb_ andb_ zero one add mul sub_ opp Feqb F_of_nat exp l', is_true_ = is_true -> negb_ = negb -> andb_ = andb -> zero = 0 -> one = 1 -> add = +%R -> mul = *%R -> sub_ = (fun x y => x - y) -> opp = -%R -> Feqb = eq_op -> F_of_nat = GRing.natmul 1 -> exp = @GRing.exp F -> l' = l -> let F_of_pos p := if p is xH then one else F_of_nat (Pos.to_nat p) in let F_of_Z n := match n with Z0 => zero | Zpos p => F_of_pos p | Zneg p => opp (F_of_pos p) end in 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 let nfe1 := Field_theory.Fnorm 0 1 Z.add Z.mul Z.sub Z.opp Z.eqb fe1 in let nfe2 := Field_theory.Fnorm 0 1 Z.add Z.mul Z.sub Z.opp Z.eqb fe2 in Peq Z.eqb (norm_subst' (PEmul (num nfe1) (denum nfe2))) (norm_subst' (PEmul (num nfe2) (denum nfe1))) /\ is_true_ (PCond' true negb_ andb_ zero one add mul sub_ opp Feqb F_of_Z nat_of_N exp l' (Fapp (Fcons00 0 1 Z.add Z.mul Z.sub Z.opp Z.eqb (triv_div 0 1 Z.eqb)) (condition nfe1 ++ condition nfe2) [::]))) -> 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) (fun x y => x / y) GRing.inv). rewrite -!Field.Rnorm_correct => -[-> -> Hlpe]. move=> /(_ _ _ _ _ _ _ _ _ _ _ _ _ _ erefl erefl erefl erefl erefl erefl erefl). move=> /(_ _ _ _ _ _ _ erefl erefl erefl erefl erefl erefl) [Heq Hcond]. apply: (Fcorrect _ erefl erefl erefl Heq). elim: {Heq Hcond}lpe Hlpe Hlpe' => // -[[[{}re1 {}re2] {}pe1] {}pe2]. move=> lpe IHlpe /=; rewrite -!Ring.Rnorm_correct. by move=> [-> ->] Hlpe [Hpe /(IHlpe Hlpe)] {IHlpe Hlpe} /=; case: lpe. by apply: Pcond_simpl_gen; [ exact: Eq_ext | exact/F2AF/RF/Eq_ext | exact: RZ | exact: PN | exact/triv_div_th/RZ/Rth_ARth/RR/Eq_ext/Eq_ext/Eqsth | move=> _ ->; exact/PCondP ]. 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)