proposition: Lemma beval_normalise : forall env cl, beval_clause env cl = beval_option (beval_clause env) (Elim.normalise cl).
proof: Proof. induction cl. - simpl. reflexivity. - simpl. destruct (Elim.normalise cl) eqn:N. simpl in *. rewrite IHcl. generalize (get_polarity_spec env (var a) c). destruct (Elim.get_polarity_rec (Lit.var a) c) eqn:GP. destruct p. destruct (Lit.eq_dec (Lit.make (negb b) (Lit.var a)) a). + rewrite beval_clause_cons_lit. simpl. intro E. rewrite E. rewrite <- e at 1. rewrite orb_assoc. rewrite eval_lit_negb_make. rewrite negb_involutive. rewrite orb_negb_l. reflexivity. + intros. simpl. rewrite H. rewrite beval_clause_cons_lit. simpl. apply make_var in n. rewrite negb_involutive in n. rewrite n. btauto. + simpl. auto. + simpl in *. rewrite IHcl. btauto. Qed.
imports: ZArith List Bool Lia Morphisms Cdcl.Syntax Cdcl.Lib Cdcl.Lit Cdcl.Clause