proposition: Lemma quantifier_elim_rformP e f : rformula f -> reflect (holds e f) (qf_eval e (quantifier_elim f)).
proof: Proof. pose rc e n f := exists x, qf_eval (set_nth 0 e n x) f. have auxP f0 e0 n0: qf_form f0 && rformula f0 -> reflect (rc e0 n0 f0) (qf_eval e0 (elim_aux f0 n0)). + rewrite /elim_aux => cf; set bcs := qf_to_dnf f0 false. apply: (@iffP (rc e0 n0 (dnf_to_form bcs))); last first. - by case=> x; rewrite -qf_to_dnfP //; exists x. - by case=> x; rewrite qf_to_dnfP //; exists x. have: all dnf_rterm bcs by case/andP: cf => _; apply: qf_to_dnf_rterm. elim: {f0 cf}bcs => [|bc bcs IHbcs] /=; first by right; case. case/andP=> r_bc /IHbcs {IHbcs}bcsP. have f_qf := dnf_to_form_qf [:: bc]. case: ok_proj => //= [ex_x|no_x]. left; case: ex_x => x /(qf_evalP _ f_qf); rewrite /= orbF => bc_x. by exists x; rewrite /= bc_x. apply: (iffP bcsP) => [[x bcs_x] | [x]] /=. by exists x; rewrite /= bcs_x orbT. case/orP => [bc_x|]; last by exists x. by case: no_x; exists x; apply/(qf_evalP _ f_qf); rewrite /= bc_x. elim: f e => //. - by move=> b e _; apply: idP. - by move=> t1 t2 e _; apply: eqP. - move=> f1 IH1 f2 IH2 e /= /andP[/IH1[] f1e]; last by right; case. by case/IH2; [left | right; case]. - move=> f1 IH1 f2 IH2 e /= /andP[/IH1[] f1e]; first by do 2!left. by case/IH2; [left; right | right; case]. - move=> f1 IH1 f2 IH2 e /= /andP[/IH1[] f1e]; last by left. by case/IH2; [left | right; move/(_ f1e)]. - by move=> f IHf e /= /IHf[]; [right | left]. - move=> n f IHf e /= rf; have rqf := quantifier_elim_wf rf. by apply: (iffP (auxP _ _ _ rqf)) => [] [x]; exists x; apply/IHf. move=> n f IHf e /= rf; have rqf := quantifier_elim_wf rf. case: auxP => // [f_x|no_x]; first by right=> no_x; case: f_x => x /IHf[]. by left=> x; apply/IHf=> //; apply/idPn=> f_x; case: no_x; exists x. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat div seq) mathcomp(choice fintype finfun bigop prime binomial)