proposition: Lemma abst_form_correct : forall b (f:TFormula TX AF b) pol, xcnf pol f = xcnf pol (abst_form pol f).
proof: Proof. intros b f; induction f as [| | | |? ? IHf1 ? IHf2|? ? IHf1 ? IHf2|? f IHf |? f1 IHf1 o f2 IHf2|? IHf1 ? IHf2|]; intros pol. - simpl. destruct pol ; reflexivity. - simpl. destruct pol ; reflexivity. - simpl. reflexivity. - simpl. rewrite needA_all. reflexivity. - simpl. unfold mk_and. specialize (IHf1 pol). specialize (IHf2 pol). rewrite IHf1. rewrite IHf2. destruct pol. + apply abs_and_pol; auto. + apply abs_or_pol. - simpl. unfold mk_or. specialize (IHf1 pol). specialize (IHf2 pol). rewrite IHf1. rewrite IHf2. destruct pol. + apply abs_or_pol; auto. + apply abs_and_pol; auto. - simpl. unfold abs_not. specialize (IHf (negb pol)). destruct (is_X (abst_form (negb pol) f)) eqn:EQ1. + apply is_X_inv in EQ1. rewrite EQ1 in *. simpl in *. destruct pol ; auto. + simpl. congruence. - simpl. unfold mk_impl. specialize (IHf1 (negb pol)). specialize (IHf2 pol). destruct pol. + simpl in *. unfold abs_or. destruct (is_X (abst_form false f1)) eqn:EQ1; destruct (is_X (abst_form true f2)) eqn:EQ2 ; simpl. * apply is_X_inv in EQ1. apply is_X_inv in EQ2. rewrite EQ1 in *. rewrite EQ2 in *. rewrite IHf1. rewrite IHf2. simpl. reflexivity. * apply is_X_inv in EQ1. rewrite EQ1 in *. rewrite IHf1. simpl. rewrite xcnf_true_mk_arrow_l. rewrite or_cnf_opt_cnf_ff. congruence. * apply is_X_inv in EQ2. rewrite EQ2 in *. rewrite IHf2. simpl. rewrite xcnf_true_mk_arrow_r. rewrite or_cnf_opt_cnf_ff_r. congruence. * destruct o ; simpl ; try congruence. rewrite EQ1. simpl. congruence. + simpl in *. unfold abs_and. destruct (is_X (abst_form true f1)) eqn:EQ1; destruct (is_X (abst_form false f2)) eqn:EQ2 ; simpl. * apply is_X_inv in EQ1. apply is_X_inv in EQ2. rewrite EQ1 in *. rewrite EQ2 in *. rewrite IHf1. rewrite IHf2. simpl. reflexivity. * apply is_X_inv in EQ1. rewrite EQ1 in *. rewrite IHf1. simpl. reflexivity. * apply is_X_inv in EQ2. rewrite EQ2 in *. rewrite IHf2. simpl. unfold and_cnf_opt. rewrite orb_comm. reflexivity. * destruct o; simpl. -- rewrite EQ1. simpl. congruence. -- congruence. - apply abst_iff_correct; auto. - apply abst_eq_correct; auto. Qed.
imports: List Refl Bool Relation_Definitions Setoid