proposition: Lemma sat_gen_form e f : GRing.rformula f -> reflect (GRing.holds e f) (GRing.sat (gen_env e) (gen_form f)).
proof: Proof. have ExP := Exists_rowP; have set_val := set_nth_map_rVval. elim: f e => //. - by move=> b e _; apply: (iffP satP). - rewrite /gen_form => t1 t2 e rt_t; set t := (_ - _)%T. have:= GRing.qf_evalP (gen_env e) (mxrank_form_qf 0 (gen_term t)). rewrite eval_mxrank mxrank_eq0 eval_gen_term // => tP. by rewrite (sameP satP tP) /= subr_eq0 val_eqE; apply: eqP. - move=> f1 IH1 f2 IH2 s /= /andP[/(IH1 s)f1P /(IH2 s)f2P]. by apply: (iffP satP) => [[/satP/f1P ? /satP/f2P] | [/f1P/satP ? /f2P/satP]]. - move=> f1 IH1 f2 IH2 s /= /andP[/(IH1 s)f1P /(IH2 s)f2P]. by apply: (iffP satP) => /= [] []; try move/satP; do [move/f1P | move/f2P]; try move/satP; auto. - move=> f1 IH1 f2 IH2 s /= /andP[/(IH1 s)f1P /(IH2 s)f2P]. by apply: (iffP satP) => /= implP; try move/satP; move/f1P; try move/satP; move/implP; try move/satP; move/f2P; try move/satP. - move=> f1 IH1 s /= /(IH1 s) f1P. by apply: (iffP satP) => /= notP; try move/satP; move/f1P; try move/satP. - move=> k f1 IHf1 s /IHf1 f1P; apply: (iffP satP) => /= [|[[v f1v]]]. by case/ExP=> // x /satP; rewrite set_val => /f1P; exists (inFA x). by apply/ExP=> //; exists v; rewrite set_val; apply/satP/f1P. move=> i f1 IHf1 s /IHf1 f1P; apply: (iffP satP) => /= allf1 => [[v]|]. apply/f1P; case: satP => // notf1x; case: allf1; apply/ExP=> //. by exists v; rewrite set_val. by case/ExP=> //= v []; apply/satP; rewrite set_val; apply/f1P. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq path) mathcomp(div choice fintype tuple finfun bigop prime) mathcomp(ssralg poly polydiv finset fingroup morphism) mathcomp(perm automorphism quotient finalg action zmodp) mathcomp(commutator cyclic center pgroup matrix mxalgebra) mathcomp(mxpoly)