proposition: Lemma get_polarity_ispec : forall env p cl (WF : wf cl), match Elim.get_polarity_rec p cl with | None => ~ is_var_of_clause p cl | Some (b,cl') => eval_clause env cl <-> eval_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. + apply wf_cons in WF. destruct (pol (make b p)) eqn:POL. rewrite eval_clause_cons_lit_POS by auto. tauto. rewrite eval_clause_cons_lit_NEG by auto. tauto. + destruct (Elim.get_polarity_rec p cl) eqn:GP'. destruct p0 as (b,cl'). simpl. assert (WFT := wf_tl a cl WF). apply wf_cons in WF. destruct (pol a) eqn:PA. * simpl. rewrite IHcl by auto. apply get_polarity_rec_all_pos in GP';auto. destruct GP';subst. rewrite <- !eval_clause_cons_lit_POS; auto. simpl. destruct a ; try discriminate. unfold eval_lit ; simpl. tauto. * simpl. rewrite IHcl by auto. destruct b; simpl. unfold make. tauto. rewrite! cons_lit_POS_false by reflexivity. simpl. destruct a; try discriminate. unfold eval_lit. simpl. tauto. * apply wf_tl in WF. apply get_pol_None in GP. rewrite is_var_of_clause_cons. intuition congruence. Qed.
imports: ZArith List Bool Lia Morphisms Cdcl.Syntax Cdcl.Lib Cdcl.Lit Cdcl.Clause