Section smt_proof.
Require Import Classical.

Variable obj : Set.

Lemma to_clause_1 : forall a b : Prop, ((a -> b) -> (a -> ~b -> False)).
Proof. intros. apply NNPP. tauto. Qed.
Lemma to_clause_2 : forall a b : Prop, ((a -> b) -> (~b -> a -> False)).
Proof. intros. apply NNPP. tauto. Qed.
Lemma to_clause_1_sn : forall a b : Prop, ((a -> ~b) -> (a -> b -> False)).
Proof. intros. apply NNPP. tauto. Qed.
Lemma to_clause_2_sn : forall a b : Prop, ((a -> ~b) -> (b -> a -> False)).
Proof. intros. apply NNPP. tauto. Qed.
Lemma absurd_n : forall a : Prop, (~a -> False) -> a.
Proof. intros. apply NNPP. tauto. Qed.
Lemma absurd_p : forall a : Prop, (a -> False) -> ~a.
Proof. intros. tauto. Qed.

Lemma and_get : forall a b : Prop, a /\ b -> a.
Proof. intros. apply NNPP. tauto. Qed.
Lemma and_skip : forall a b : Prop, a /\ b -> b.
Proof. intros. apply NNPP. tauto. Qed.

(* not needed in skolemized NNF
Lemma nor_get : forall a b : Prop, ~(a \/ b) -> ~a.
Proof. intros. apply NNPP. tauto. Qed.
Lemma nor_skip : forall a b : Prop, ~(a \/ b) -> ~b.
Proof. intros. apply NNPP. tauto. Qed.

Lemma neg_unit_res : forall a b : Prop, a -> ~(a /\ b) -> ~b.
Proof. intros. tauto. Qed.
*)

Lemma excl_mid_pn : forall a : Prop, a -> ~a -> False.
Proof. intros. apply NNPP. tauto. Qed.
Lemma excl_mid_np : forall a : Prop, ~a -> a -> False.
Proof. intros. apply NNPP. tauto. Qed.

Lemma unit_res_pn : forall a b : Prop, a -> (~ a \/ b) -> b.
Proof. intros. tauto. Qed.
Lemma unit_res_np : forall a b : Prop, ~a -> (a \/ b) -> b.
Proof. intros. tauto. Qed.

Lemma compose : forall a b c : Prop, (b -> c) -> (a -> b) -> (a -> c).
Proof. intros. tauto. Qed.

(* NNF *)
Lemma pos_iff_def : forall a b : Prop, (a <-> b) -> ((~ a \/ b) /\ (~ b \/ a)).
Proof. intros. apply NNPP. tauto. Qed.

Lemma neg_iff_def : forall a b : Prop, ~(a <-> b) -> ~((~ a \/ b) /\ (~ b \/ a)).
Proof. intros. apply NNPP. tauto. Qed.

Lemma pos_implies_def : forall a b : Prop, (a -> b) -> (~ a \/ b).
Proof. intros. apply NNPP. tauto. Qed.

Lemma neg_implies_def : forall a b : Prop, ~(a -> b) -> ~(~ a \/ b).
Proof. intros. apply NNPP. tauto. Qed.

Lemma pos_and_comp : forall a a' b b' : Prop, (a -> a') -> (b -> b') -> (a /\ b -> a' /\ b').
Proof. intros. apply NNPP. tauto. Qed.

Lemma neg_and_comp : forall a a' b b' : Prop, (~a -> a') -> (~b -> b') -> (~(a /\ b) -> a' \/ b').
Proof. intros. apply NNPP. tauto. Qed.

Lemma pos_or_comp : forall a a' b b' : Prop, (a -> a') -> (b -> b') -> (a \/ b -> a' \/ b').
Proof. intros. apply NNPP. tauto. Qed.

Lemma neg_or_comp : forall a a' b b' : Prop, (~a -> a') -> (~b -> b') -> (~(a \/ b) -> a' /\ b').
Proof. intros. apply NNPP. tauto. Qed.

Lemma id : forall a : Prop, a -> a.
Proof. intros. tauto. Qed.

Lemma and_comm : forall a b c d : Prop, ((b /\ c) -> d) -> (a /\ b) /\ c -> a /\ d.
Proof. intros. apply NNPP. tauto. Qed.

Lemma or_comm : forall a b c d : Prop, ((b \/ c) -> d) -> (a \/ b) \/ c -> a \/ d.
Proof. intros. apply NNPP. tauto. Qed.

Lemma nnpp : forall a : Prop, (~ (~ a)) -> a.
Proof. intros. apply NNPP. tauto. Qed.