proposition: Lemma qf_to_dnfP e : let qev f b := qf_eval e (dnf_to_form (qf_to_dnf f b)) in forall f, qf_form f && rformula f -> qev f false = qf_eval e f.
proof: Proof. move=> qev; have qevT f: qev f true = ~~ qev f false. rewrite {}/qev; elim: f => //=; do [by case | move=> f1 IH1 f2 IH2 | ]. - by move=> t1 t2; rewrite !andbT !orbF. - by rewrite and_dnfP cat_dnfP negb_and -IH1 -IH2. - by rewrite and_dnfP cat_dnfP negb_or -IH1 -IH2. - by rewrite and_dnfP cat_dnfP /= negb_or IH1 -IH2 negbK. by move=> t1 ->; rewrite negbK. rewrite /qev; elim=> //=; first by case. - by move=> t1 t2 _; rewrite subr_eq0 !andbT orbF. - move=> f1 IH1 f2 IH2; rewrite andbCA -andbA andbCA andbA; case/andP. by rewrite and_dnfP /= => /IH1-> /IH2->. - move=> f1 IH1 f2 IH2; rewrite andbCA -andbA andbCA andbA; case/andP. by rewrite cat_dnfP /= => /IH1-> => /IH2->. - move=> f1 IH1 f2 IH2; rewrite andbCA -andbA andbCA andbA; case/andP. by rewrite cat_dnfP /= [qf_eval _ _]qevT -implybE => /IH1 <- /IH2->. by move=> f1 IH1 /IH1 <-; rewrite -qevT. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat div seq) mathcomp(choice fintype finfun bigop prime binomial)