proposition: Lemma enum_npolyE (n : nat) (R : finRingType) s : perm_eq (Finite.enum R) s -> perm_eq (Finite.enum {poly_n R}) (enum_npoly n iter s (@npoly_of_seq _ _)).
proof: Proof. rewrite -!enumT => Rs; rewrite uniq_perm ?enum_uniq //=. admit. move=> /= p; symmetry; rewrite mem_enum inE /=. apply/mapP => /=; exists p; last first. apply/npolyP => i; rewrite coef_poly /= coef_Poly. by case: ltnP => // ?; rewrite big_coef_npoly. elim: n => [|n IHn] in p *. rewrite inE; case: p => [p /=]; rewrite size_poly_leq0 => /eqP->. by rewrite polyseq0. rewrite /= mem_cat. Admitted. Parametricity enum_npoly. Section RnpolyC. Context (A : finRingType). Context (C : Type) (rAC : A -> C -> Type). Context (N : Type) (rN : nat -> N -> Type). Context (n : nat) (n' : N) `{!refines rN n n'}. Context (iter' : forall T, N -> (T -> T) -> T -> T) {iterR : forall T T' RT, refines (rN ==> (RT ==> RT) ==> RT ==> RT) (@iter T) (@iter' T')}. Context (enumC : seq C) {enumR : refines (perm_eq \o list_R rAC) (@Finite.enum A) enumC}. Definition Rnpoly : {poly_n A} -> {poly A} -> Type := fun p q => p = q :> {poly A}. Definition RnpolyC : {poly_n A} -> seqpoly C -> Type := (Rnpoly \o RseqpolyC rAC)%rel. #[export] Instance refines_enum_npoly : refines (perm_eq \o list_R RnpolyC) (Finite.enum {poly_n A}) (enum_npoly n' iter' enumC id). Proof. have [s [sP ?]] := refines_split2 enumR. eapply refines_trans; tc. by rewrite refinesE; apply/enum_npolyE/sP. param enum_npoly_R. Admitted. #[export] Instance refines_RnpolyCpoly (x : {poly_n A}) (y : seqpoly C) `{!refines RnpolyC x y} : refines (RseqpolyC rAC) (poly_of_npoly x) y. Admitted. End RnpolyC. #[export] Instance refines_iter T T' RT : refines (Rnat ==> (RT ==> RT) ==> RT ==> RT) (@iter T) (@iter T'). Proof. param iter_R. Admitted. Section LaurentsProblem. #[export] Instance refines_predn : refines (Rnat ==> Rnat) predn (fun n => (n - 1)%C). Admitted. Lemma test_irred : irreducible_poly ('X^5 + 'X^2 + 1 : {poly 'F_2}). Proof. apply/irreducibleP; rewrite /irreducibleb -[size _]/(sizep _). rewrite -[[forall _, _]]/(_ == _) /= /Pdiv.Ring.rdvdp. by coqeal. Qed.
imports: HB(structures) mathcomp.ssreflect.ssreflect mathcomp(ssrfun ssrbool eqtype ssrnat seq choice fintype tuple) mathcomp(bigop binomial finset finfun zmodp ssralg countalg finalg poly polydiv) mathcomp(perm fingroup) CoqEAL(hrel pos param refinements binnat boolF2 seqpoly poly_op trivial_seq poly_div boolF2)