proposition: Lemma eval_normalise : forall env cl (WF : wf cl), eval_clause env cl <-> eval_option (eval_clause env) (Elim.normalise cl).
proof: Proof. intros. induction cl. - simpl. tauto. - simpl. destruct (Elim.normalise cl) eqn:N. + assert (SL : sublist c cl). { apply sublist_normalise in N; auto. } simpl in *. intros. assert (WFTL := wf_tl _ _ WF). specialize (IHcl WFTL). apply wf_normalise in N; auto. generalize (get_polarity_ispec env (var a) c N). destruct (Elim.get_polarity_rec (var a) c) eqn:POL. * destruct p. destruct (eq_dec (make (negb b) (var a)) a); simpl;auto. intros. split ; auto. intros. rewrite IHcl. rewrite H. assert (make b (var a) = Lit.neg a). { rewrite <- e. destruct b; simpl;auto. } rewrite H1. assert (POL':= POL). apply get_polarity_rec_sublist in POL. destruct POL as (POL & IN). rewrite H1 in IN. assert (WFC : wf (a::c)). { eapply wf_cons_sublist;eauto. } assert (WFL : wf (a::l)). { eapply wf_cons_sublist;eauto. } apply wf_cons in WFC. destruct (pol a) eqn:PA. destruct a ; try discriminate. rewrite Forall_forall in WFC. apply WFC in IN. discriminate. destruct a; try discriminate. simpl. unfold eval_lit ; simpl. apply eval_clause_cons_lit_tauto. intros. apply make_var in n. rewrite negb_involutive in n. rewrite n in *. rewrite IHcl. rewrite H. apply cons_lit_twice. * simpl. intros. rewrite IHcl. tauto. + simpl in *. apply wf_tl in WF. rewrite IHcl by auto. unfold eval_lit. destruct (pol a). tauto. tauto. Qed.
imports: ZArith List Bool Lia Morphisms Cdcl.Syntax Cdcl.Lib Cdcl.Lit Cdcl.Clause