proposition: Lemma abst_iff_correct : forall (k: kind) (f1 f2 : GFormula k) (IHf1 : forall pol : bool, xcnf pol f1 = xcnf pol (abst_form pol f1)) (IHf2 : forall pol : bool, xcnf pol f2 = xcnf pol (abst_form pol f2)) (pol : bool), xcnf pol (IFF f1 f2) = xcnf pol (abst_iff abst_form pol f1 f2).
proof: Proof. intros k f1 f2 IHf1 IHf2 pol; simpl. assert (D1 :mk_iff xcnf pol f1 f2 = mk_iff xcnf pol (abst_simpl f1) (abst_simpl f2)). { simpl. unfold mk_iff. rewrite <- !abst_simpl_correct. reflexivity. } rewrite mk_iff_is_bool. unfold abst_iff,abs_iff. destruct ( or_is_X (abst_form (negb pol) f1) (abst_form false f2) && or_is_X (abst_form pol f1) (abst_form true f2) ) eqn:EQ1. + simpl. rewrite andb_true_iff in EQ1. destruct EQ1 as (EQ1 & EQ2). apply or_is_X_inv in EQ1. apply or_is_X_inv in EQ2. destruct EQ1 as (b1 & EQ1). destruct EQ2 as (b2 & EQ2). rewrite if_same. unfold mk_iff. rewrite !IHf1. rewrite !IHf2. destruct EQ1 as [EQ1 | EQ1] ; apply is_X_inv in EQ1; destruct EQ2 as [EQ2 | EQ2] ; apply is_X_inv in EQ2; rewrite EQ1; rewrite EQ2; simpl; repeat rewrite if_same ; cnf_simpl; auto. + simpl. rewrite mk_iff_is_bool. unfold mk_iff. rewrite <- ! abst_simpl_correct. reflexivity. Qed.
imports: List Refl Bool Relation_Definitions Setoid