proposition: Lemma get_polarity_spec : forall env p cl, match Elim.get_polarity_rec p cl with | None => ~ is_var_of_clause p cl | Some (b,cl') => beval_clause env cl = beval_clause env (cons_lit (Lit.make b p) cl') end.
proof: Proof. induction cl. - simpl. rewrite is_var_of_clause_nil. tauto. - intros. simpl. destruct (Lit.get_pol p a) eqn:GP. apply Lit.get_pol_inv in GP. subst. + rewrite beval_clause_cons_lit. reflexivity. + destruct (Elim.get_polarity_rec p cl). destruct p0. rewrite beval_clause_cons_lit in *. rewrite IHcl. simpl. rewrite orb_comm. rewrite <- orb_assoc. f_equal. rewrite orb_comm. reflexivity. * rewrite is_var_of_clause_cons. apply Lit.get_pol_None in GP. intro. intuition congruence. Qed.
imports: ZArith List Bool Lia Morphisms Cdcl.Syntax Cdcl.Lib Cdcl.Lit Cdcl.Clause