proposition: Lemma or_clause_cnf_correct : forall env t f, eval_cnf env (or_clause_cnf t f) <-> (eval_clause env t) \/ (eval_cnf env f).
proof: Proof. unfold eval_cnf. unfold or_clause_cnf. intros env t. set (F := (fun (acc : list clause) (e : clause) => match or_clause t e with | Some cl => cl :: acc | None => acc end)). intro f. assert ( make_conj (eval_clause env) (fold_left F f nil) <-> (eval_clause env t \/ make_conj (eval_clause env) f) /\ make_conj (eval_clause env) nil) as H. { generalize (@nil clause) as acc. induction f as [|a f IHf]. - simpl. intros ; tauto. - intros. simpl fold_left. rewrite IHf. rewrite make_conj_cons. unfold F in *; clear F. generalize (or_clause_correct t a env). destruct (or_clause t a). + rewrite make_conj_cons. simpl. tauto. + simpl. tauto. } destruct t ; auto. - unfold eval_clause ; simpl. tauto. - unfold xor_clause_cnf. unfold F in H. rewrite H. unfold make_conj at 2. tauto. Qed.
imports: List Refl Bool Relation_Definitions Setoid