proposition: Lemma cnf_of_list_correct : forall {T : Type} (tg:T) (f : list (NFormula Z)) env, eval_cnf eval_nformula env (cnf_of_list tg f) <-> make_conj (fun x : NFormula Z => eval_nformula env x -> False) f.
proof: Proof. unfold cnf_of_list. intros T tg f env. set (F := (fun (x : NFormula Z) (acc : list (list (NFormula Z * T))) => if Zunsat x then acc else ((x, tg) :: nil) :: acc)). set (E := ((fun x : NFormula Z => eval_nformula env x -> False))). induction f as [|a f IHf]. - compute. tauto. - rewrite make_conj_cons. simpl. unfold F at 1. destruct (Zunsat a) eqn:EQ. + rewrite IHf. unfold E at 1. specialize (Zunsat_sound _ EQ env). tauto. + rewrite <- eval_cnf_cons_iff. rewrite IHf. simpl. unfold E at 2. unfold eval_tt. simpl. tauto. Qed.
imports: List Bool OrderedRing RingMicromega ZCoeff Refl ZArith_base ZArithRing Ztac EnvRing Coq.micromega.Tauto BinNums