proposition: Lemma xcnf_correct : forall (k: kind) (f : @GFormula Term rtyp Annot unit k) pol env, eval_cnf env (xcnf pol f) -> hold k (eval_f e_rtyp (eval env) (if pol then f else NOT f)).
proof: Proof. intros k f; induction f as [| | | |? ? IHf1 ? IHf2|? ? IHf1 ? IHf2|? ? IHf |? ? IHf1 ? ? IHf2|? ? IHf1 f2 IHf2|f1 IHf1 f2 IHf2]; intros pol env H. - unfold eval_cnf. simpl. destruct pol ; intros; simpl; auto with tauto. rewrite eval_cnf_ff in H. tauto. - destruct pol ; simpl in *; intros; auto with tauto. + rewrite eval_cnf_ff in H. tauto. - simpl. destruct pol ; intros ;simpl. + rewrite eval_cnf_ff in H. tauto. + rewrite eval_cnf_ff in H. tauto. - simpl. destruct pol ; simpl. + intros. eapply normalise_correct ; eauto. + intros. eapply negate_correct ; eauto. - destruct pol ; simpl in H. + intros. rewrite eval_cnf_and_opt in H. unfold and_cnf in H. rewrite eval_cnf_app in H. destruct H as [H H0]. apply hold_eAND; split. * apply (IHf1 _ _ H). * apply (IHf2 _ _ H0). + intros. apply hold_eNOT. rewrite hold_eAND. rewrite or_cnf_opt_correct in H. rewrite or_cnf_correct in H. destruct H as [H | H]. * generalize (IHf1 false env H). simpl. rewrite hold_eNOT. tauto. * generalize (IHf2 false env H). simpl. rewrite hold_eNOT. tauto. - simpl in H. destruct pol. + intros. unfold mk_or in H. rewrite or_cnf_opt_correct in H. rewrite or_cnf_correct in H. destruct H as [H | H]. * generalize (IHf1 _ env H). simpl. rewrite hold_eOR. tauto. * generalize (IHf2 _ env H). simpl. rewrite hold_eOR. tauto. + intros. unfold mk_or in H. rewrite eval_cnf_and_opt in H. unfold and_cnf. rewrite eval_cnf_app in H. destruct H as [H0 H1]. simpl. generalize (IHf1 _ _ H0). generalize (IHf2 _ _ H1). simpl. rewrite ! hold_eNOT. rewrite ! hold_eOR. tauto. - simpl. destruct pol ; simpl. + intros. apply (IHf false) ; auto. + intros. generalize (IHf _ _ H). rewrite ! hold_eNOT. tauto. - apply xcnf_impl; auto. - apply xcnf_iff ; auto. - simpl in H. destruct (is_bool f2) as [b|] eqn:EQ. + apply is_bool_inv in EQ. destruct b; subst; intros; apply IHf1 in H; destruct pol ; simpl in * ; auto. * unfold is_true in H. rewrite negb_true_iff in H. congruence. * unfold is_true in H. rewrite negb_true_iff in H. congruence. * unfold is_true in H. congruence. + intros. rewrite <- mk_iff_is_bool in H. apply xcnf_iff in H; auto. simpl in H. destruct pol ; simpl in *. * rewrite <- hold_eEQ. simpl; auto. * rewrite <- hold_eEQ. simpl; auto. unfold is_true in *. rewrite negb_true_iff in H. congruence. Qed.
imports: List Refl Bool Relation_Definitions Setoid