coq snippets

fin_semilattice.v

Require Import Relation_Definitions.

Arguments reflexive A/.
Arguments transitive A/.
Arguments symmetric A/.
Arguments antisymmetric A/.

Section FinSemiLattice.
  Variable X : Type.

  Structure order_R := {
    order_r :> relation X;
    order_law : order X order_r;
  }.

  Structure Bin := { (* 可換結合的冪等二項演算 *)
    bin :> X -> X -> X;
    bin_comm : forall x y, bin x y = bin y x;
    bin_assoc : forall x y z, bin x (bin y z) = bin (bin x y) z;
    bin_refl : forall x, bin x x = x;
  }.

  Variable bin : Bin.

  Example both_eq_r : forall (bin : X -> X -> X) x y z, x = y -> bin x z = bin y z.
  Proof.
    intros.
    rewrite H.
    auto.
  Qed.

  Example bin_relation_is_order : order X (fun x y => (bin x y) = y).
  Proof.
    constructor.
    -
      simpl.
      apply bin_refl.
    -
      simpl.
      intros.
      apply (both_eq_r bin _ _ z) in H.
      rewrite H0 in H.
      rewrite <- bin_assoc in H.
      rewrite H0 in H.
      auto.
    -
      simpl.
      intros.
      rewrite bin_comm in H0.
      rewrite H0 in H.
      auto.
  Qed.

  Definition bin_order :=
    Build_order_R (fun x y => (bin x y) = y) bin_relation_is_order.

  Definition is_upper_bound (r:order_R) x y z := 
    (r:relation X) x z /\ (r:relation X) y z.
  Arguments is_upper_bound r x y z/.

  Definition is_join (r:order_R) (x y z:X) :=
    (is_upper_bound r x y z) /\
    (forall w, (is_upper_bound r x y w) -> (r:relation X) z w).
  Arguments is_join r x y z/.

  Example bin_is_join_on_bin_order : forall x y, is_join bin_order x y (bin x y).
  Proof.
    simpl.
    constructor.
    -
      constructor.
      +
        rewrite bin_assoc.
        rewrite bin_refl.
        auto.
      +
        rewrite bin_comm.
        rewrite <- bin_assoc.
        rewrite bin_refl.
        auto.
    -
      intros.
      destruct H.
      rewrite <- bin_assoc.
      rewrite H0.
      rewrite H.
      auto.
  Qed.

  Structure Join r := {
    join :> X -> X -> X;
    join_law : forall x y, is_join r x y (join x y);
  }.

  Variable r : order_R.
  Variable join : Join r.

  (* x ∨ x = x *)
  Example join_is_refl : forall x, join x x = x.
  Proof.
    intros.
    apply (ord_antisym _ _ (order_law r)).
    -
      apply (join_law _ join).
      constructor.
      + apply r.
      + apply r.
    -
      apply (join_law _ join).
  Qed.

  (* x ∨ y = y ∨ x *)
  Example join_is_comm : forall x y, join x y = join y x.
  Proof.
    intros.
    apply (ord_antisym _ _ (order_law r)).
    -
      apply (join_law _ join).
      constructor.
      + apply (join_law _ join).
      + apply (join_law _ join).
    -
      apply (join_law _ join).
      constructor.
      + apply (join_law _ join).
      + apply (join_law _ join).
  Qed.

  (* x ∨ (y ∨ z) = (x ∨ y) ∨ z *)
  Example join_is_assoc : forall x y z,
    join x (join y z) = join (join x y) z.
  Proof.
    intros. 
    apply (ord_antisym _ _ (order_law r)).
    -
      apply (join_law _ join).
      constructor.
      +
        apply (
          ord_trans _ _ (order_law r) _ _ _
            (proj1 (proj1 (join_law _ join x y)))          (* r x (join x y) *)
            (proj1 (proj1 (join_law _ join (join x y) z))) (* r (join x y) (join (join x y) z) *)
        ).
      +
        assert (H:=proj1 (proj1 (join_law _ join (join x y) z))).  (* r (join x y) (join (join x y) z) *)
        assert (H1:=proj2 (proj1 (join_law _ join x y))).          (* r y (join x y) *)
        assert (H2:=ord_trans _ _ (order_law r) _ _ _ H1 H).     (* r y (join (join x y) z) *)
        assert (H3:=proj2 (proj1 (join_law _ join (join x y) z))). (* r z (join (join x y) z) *)
        apply (proj2 (join_law _ join y z) _ (conj H2 H3)).
    -
      apply (join_law _ join).
      constructor.
      +
        assert (H:=proj1 (proj1 (join_law _ join y z))).           (* r y (join y z) *)
        assert (H1:=proj2 (proj1 (join_law _ join x (join y z)))). (* r (join y z) (join x (join y z)) *)
        assert (H2:=proj1 (proj1 (join_law _ join x (join y z)))). (* r x (join x (join y z)) *)
        assert (H3:=ord_trans _ _ (order_law r) _ _ _ H H1).     (* r y (join (join x y) z) *)
        apply (proj2 (join_law _ join x y) _ (conj H2 H3)).
      +
        apply (
          ord_trans _ _ (order_law r) _ _ _
            (proj2 (proj1 (join_law _ join y z)))          (* r z (join y z) *)
            (proj2 (proj1 (join_law _ join x (join y z)))) (* r (join y z) (join x (join y z)) *)
        ).
  Qed.
End FinSemiLattice.

inf_semilattice.v

(* A is a complete join semilattice iff A is a complete meet semilattice *)

Require Import Relation_Definitions.

Section InfSemiLattice.
  Variable X : Type.

  Structure order_R := {
    order_r :> relation X;
    order_law : order X order_r;
  }.

  Variable r : order_R.

  Definition is_upper_bound (S : X -> Prop) a := 
    forall s, S s -> (r:relation X) s a.
  Arguments is_upper_bound S a/.

  Definition is_lower_bound (S : X -> Prop) a := 
    forall s, S s -> (r:relation X) a s.
  Arguments is_lower_bound S a/.

  Definition is_join (S : X -> Prop) a :=
    (is_upper_bound S a) /\
    (forall w, (is_upper_bound S w) -> (r:relation X) a w).
  Arguments is_join S a/.

  Definition is_meet (S : X -> Prop) a :=
    (is_lower_bound S a) /\
    (forall w, (is_lower_bound S w) -> (r:relation X) w a).
  Arguments is_meet S a/.

  Definition lower_bound_set (S : X -> Prop) t := is_lower_bound S t.
  Arguments lower_bound_set S t/.

  Definition upper_bound_set (S : X -> Prop) t := is_upper_bound S t.
  Arguments upper_bound_set S t/.

  Structure Join := {
    join :> (X -> Prop) -> X;
    join_law : forall S : X -> Prop, is_join S (join S);
  }.

  Structure Meet := {
    meet :> (X -> Prop) -> X;
    meet_law : forall S : X -> Prop, is_meet S (meet S);
  }.

  Variable join : Join.
  Variable meet : Meet.

  (* T is lower_bound_set of S. ∧S = ∨T *)
  Theorem meet_eq_join_of_lower_bound_set : forall (S : X -> Prop),
    meet S = join (lower_bound_set S).
  Proof.
    intro.
    apply (ord_antisym _ _ (order_law r)).
    - (* ∧S ≦ ∨T *)
      apply (join_law join (lower_bound_set S)). (* ∧S ∈ T *)
      apply (meet_law meet S).
    - (* ∨T ≦ ∧S *)
      apply (meet_law meet S). (* ∨T is lower bound of S *)
      intros s Ss. (* ∨T ≦ s *)
      apply (join_law join (lower_bound_set S)). (* s is upper bound of T *)
      intros t Tt.
      apply (Tt _ Ss).
  Qed.

  (* T is upper_bound_set of S. ∨S = ∧T *)
  Theorem join_eq_join_of_upper_bound_set : forall (S : X -> Prop),
    join S = meet (upper_bound_set S).
  Proof.
    intro.
    apply (ord_antisym _ _ (order_law r)).
    - (* ∨S ≦ ∧T *)
      apply (join_law join S). (* ∧T is upper bound of S *)
      intros s Ss. (* s ≦ ∧T *)
      apply (meet_law meet (upper_bound_set S)). (* s is upper bound of T *)
      intros t Tt.
      apply (Tt _ Ss).
    - (* ∨T ≦ ∧S *)
      apply (meet_law meet (upper_bound_set S)). (* ∨S ∈ T *)
      apply (join_law join S).
  Qed.

  Theorem complete_join_semilattice_iff_complete_meet_semilattice :
    forall (S : X -> Prop),
      meet S = join (lower_bound_set S) /\
      join S = meet (upper_bound_set S).
  Proof.
    intro.
    apply (
      conj
        (meet_eq_join_of_lower_bound_set S)
        (join_eq_join_of_upper_bound_set S)
    ).
  Qed.
End InfSemiLattice.

order_on_preorder_eq_class.v

(* R == preorder on X                  *)
(* x ~ y == x R y ∧ y R x              *)
(* ~ is a equivalence relation         *)
(* [x] == equivalence class of x ∈ X   *)
(* [x] R' [y] == x R y                 *)
(* R' is well-defined and order on X/~ *)

Require Import Relation_Definitions.
Require Import Ensembles.

Arguments In U/.
Arguments Same_set U/.
Arguments Included U/.
Arguments reflexive A/.
Arguments transitive A/.
Arguments symmetric A/.
Arguments antisymmetric A/.

Section Equiv.
  Variable X : Type.

  (* ~ *)
  Structure eq_R := {
    eq_r :> relation X;
    eq_law : equivalence X eq_r;
  }.

  Variable eq_r : eq_R.

  (* X/~ *)
  Structure eq_class := {
    eq_class_set :> Ensemble X;
    eq_class_rep : X;
    eq_class_eq :
      eq_class_set =
      (fun y => (eq_r:relation X) eq_class_rep y);
  }.

  (* [x] *)
  Definition build_eq_class (x:X) :=
    Build_eq_class (fun y : X => (eq_r:relation X) x y) x eq_refl.

  Axiom Extensionality_EqClass : forall X' Y' : eq_class, Same_set X X' Y' -> X' = Y'.

  Example eq_class_eq_rep_eq_class : forall X' : eq_class, build_eq_class (eq_class_rep X') = X'. 
  Proof.
    intros.
    apply Extensionality_EqClass.
    simpl.
    constructor.
    -
      intros.
      simpl.
      rewrite eq_class_eq.
      auto.
    -
      intros.
      rewrite eq_class_eq in H.
      auto.
  Qed.

  Example eq_r__eq_class_eq : forall (x y : X), (eq_r:relation X) x y -> (build_eq_class x) = (build_eq_class y).
  Proof.
    intros.
    apply Extensionality_EqClass.
    simpl.
    constructor.
    -
      intros.
      apply (equiv_sym _ _ (eq_law eq_r)) in H.
      apply (equiv_trans _ _ (eq_law eq_r) _ _ _ H H0).
    -
      intros.
      apply (equiv_trans _ _ (eq_law eq_r) _ _ _ H H0).
  Qed.
End Equiv.

Section Preord.
  Variable X : Type.

  Structure pre_R := {
    pre_r :> relation X;
    preord : preorder X pre_r;
  }.

  Variable pre_r : pre_R.

  Example pre_eq_r_is_equiv : equivalence X (fun (x y : X) => (pre_r:relation X) x y /\ (pre_r:relation X) y x).
  Proof.
    constructor.
    -
      simpl.
      intros.
      constructor.
      + apply pre_r.
      + apply pre_r.
    -
      simpl.
      intros.
      destruct H.
      destruct H0.
      constructor.
      + apply ((preord_trans _ _ (preord pre_r)) _ _ _ H H0).
      + apply ((preord_trans _ _ (preord pre_r)) _ _ _ H2 H1).
    - 
      simpl.
      intros.
      apply and_comm.
      auto.
  Qed.

  (* x ~ y ≡ x R y ∧ y R x *)
  Definition pre_eq_r := Build_eq_R _ _ pre_eq_r_is_equiv.

  (* [x]R'[y] ≡ xRy *)
  Definition R' (A B : eq_class X pre_eq_r) :=
    (pre_r:relation X)
      (eq_class_rep X pre_eq_r A)
      (eq_class_rep X pre_eq_r B).
 
  Example R'_is_well_defined : forall x x' y y' : X,
    (pre_eq_r:relation X) x x' ->
    (pre_eq_r:relation X) y y' -> (
      (R' (build_eq_class _ pre_eq_r x) (build_eq_class _ pre_eq_r y)) <->
      (R' (build_eq_class _ pre_eq_r x') (build_eq_class _ pre_eq_r y'))
    ).
  Proof.
    unfold R'.
    constructor.
    -
      intros.
      rewrite (eq_r__eq_class_eq _ pre_eq_r _ _ H) in H1.
      rewrite (eq_r__eq_class_eq _ pre_eq_r _ _ H0) in H1.
      auto.
    -
      intros.
      rewrite (eq_r__eq_class_eq _ pre_eq_r _ _ H).
      rewrite (eq_r__eq_class_eq _ pre_eq_r _ _ H0).
      auto.
  Qed.

  Example R'_is_reflextive : reflexive (eq_class X pre_eq_r) R'.
  Proof.
    simpl.
    intros.
    apply (preord pre_r).
  Qed.

  Example R'_is_transitive : transitive (eq_class X pre_eq_r) R'.
  Proof.
    simpl.
    unfold R'.
    intros.
    apply (preord_trans _ _ (preord pre_r) _ _ _ H H0).
  Qed.

  Example R'_is_antisymmetric : antisymmetric (eq_class X pre_eq_r) R'.
  Proof.
    simpl.
    unfold R'.
    intros.
    apply (conj H) in H0.
    apply (eq_r__eq_class_eq _ pre_eq_r _ _) in H0.
    rewrite eq_class_eq_rep_eq_class in H0.
    rewrite eq_class_eq_rep_eq_class in H0.
    auto.
  Qed.

  Example R'_is_order : order (eq_class X pre_eq_r) R'.
  Proof.
    constructor.
    - apply R'_is_reflextive.
    - apply R'_is_transitive.
    - apply R'_is_antisymmetric.
  Qed.
End Preord.

tableau.v

Require Import Bool.

Inductive atom : Type :=
| atom_init (n : nat) : atom
| atom_neg_init (n : nat) : atom
.

Axiom atom_not_eq : forall n, atom_init n <> atom_neg_init n.
Axiom assign_atom_not_eq : forall n (f:atom -> bool), f (atom_init n) <> f (atom_neg_init n).

Inductive prop : Type :=
| atomp : atom -> prop
| andp : prop -> prop -> prop
| negp : prop -> prop
.

Notation "p ∧ q" := (andp p q) (at level 12).
Notation "¬ p" := (negp p) (at level 11).
Notation "p ∨ q" := (¬ (¬ p ∧ ¬ q)) (at level 12).
Notation "p → q" := (¬ p ∨ q) (at level 12).

Fixpoint V (f : atom -> bool) (p : prop) : bool :=
  match p with
  | atomp (atom_init n) => f (atom_init n)
  | atomp (atom_neg_init n) => (f (atom_neg_init n))
  | p ∧ q => andb (V f p) (V f q)
  | ¬ p => negb (V f p)
  end.

Inductive branch : prop -> Type :=
| branch_atom (a : atom) : branch (atomp a)
| branch_and {p1 p2 : prop} (b1 : branch p1) (b2 : branch p2) : branch (p1 ∧ p2)
| branch_or_l {p1 : prop} (p2 : prop) (b1 : branch p1) : branch (p1 ∨ p2)
| branch_or_r {p2 : prop} (p1 : prop) (b2 : branch p2) : branch (p1 ∨ p2)
| branch_neg_and_l {p1 : prop} (p2 : prop) (b1 : branch (¬ p1)) : branch (¬ (p1 ∧ p2))
| branch_neg_and_r {p2 : prop} (p1 : prop) (b2 : branch (¬ p2)) : branch (¬ (p1 ∧ p2))
| branch_neg_or {p1 p2 : prop} (b1 : branch (¬ p1)) (b2 : branch (¬ p2)) : branch (¬ (p1 ∨ p2))
| branch_neg_neg {p : prop} (b : branch p) : branch (¬ ¬ p)
.

Definition atom_true_neg_atom_true_map (a : atom) : bool :=
  match a with
  | atom_init _ => true
  | atom_neg_init _ => true
  end.

Fixpoint branch_in (a : atom) {p : prop} (b : branch p) : Prop :=
  match b with
  | branch_atom a' => a = a'
  | branch_and b1 b2 => branch_in a b1 \/ branch_in a b2
  | branch_or_l p2 b1 => branch_in a b1
  | branch_or_r p1 b2 => branch_in a b2
  | branch_neg_and_l p2 b1 => branch_in a b1
  | branch_neg_and_r p1 b2 => branch_in a b2
  | branch_neg_or b1 b2 => branch_in a b1 \/ branch_in a b2
  | branch_neg_neg b => branch_in a b
  end.

Fixpoint branch_not_in (a : atom) {p : prop} (b : branch p) : Prop :=
  match b with
  | branch_atom a' => ~ a = a'
  | branch_and b1 b2 => branch_not_in a b1 /\ branch_not_in a b2
  | branch_or_l p2 b1 => branch_not_in a b1
  | branch_or_r p1 b2 => branch_not_in a b2
  | branch_neg_and_l p2 b1 => branch_not_in a b1
  | branch_neg_and_r p1 b2 => branch_not_in a b2
  | branch_neg_or b1 b2 => branch_not_in a b1 /\ branch_not_in a b2
  | branch_neg_neg b => branch_not_in a b
  end.

Definition closed_branch {p : prop} (b : branch p) := exists n:nat, branch_in (atom_init n) b /\ branch_in (atom_neg_init n) b.

Definition open_branch {p : prop} (b : branch p) := forall n:nat, branch_not_in (atom_init n) b \/ branch_not_in (atom_neg_init n) b.

Axiom open_branch_iff : forall {p : prop} (b : branch p),
  open_branch b <-> ~ closed_branch b.

Definition atom_to_prop (a : atom) : prop := atomp a.
Coercion atom_to_prop : atom >-> prop.

Fixpoint branch_to_prop {p : prop} (b : branch p) : prop :=
  match b with
  | branch_atom a => atomp a
  | branch_and b1 b2 => (branch_to_prop b1) ∧ (branch_to_prop b2)
  | branch_or_l p2 b1 => branch_to_prop b1
  | branch_or_r p1 b2 => branch_to_prop b2
  | branch_neg_and_l p2 b1 => branch_to_prop b1
  | branch_neg_and_r p1 b2 => branch_to_prop b2
  | branch_neg_or b1 b2 => branch_to_prop b1 ∧ branch_to_prop b2
  | branch_neg_neg b => branch_to_prop b
  end.
Coercion branch_to_prop : branch >-> prop.

Axiom neg_branch_exists : forall p f (b : branch p),
  V f p = V f b -> exists b' : branch (¬ p), V f b' <> V f p.

Definition sat (p : prop) : Prop :=
  exists f : (atom -> bool), V f p = true.
Definition unsat (p : prop) : Prop :=
  forall f : (atom -> bool), V f p = false.

Axiom atomp_eq : forall (a1 a2 : atom), atomp a1 = atomp a2 -> a1 = a2.

Lemma forall_and_or_l : forall t:Type, forall P Q R S : t -> Prop,
  (forall x:t, (P x /\ Q x) \/ (R x /\ S x)) -> (forall x:t, P x \/ R x).
Proof.
  intros.
  specialize (H x).
  destruct H.
  -
    destruct H.
    left.
    auto.
  -
    destruct H.
    right.
    auto.
Qed.

Lemma forall_and_or_r : forall t:Type, forall P Q R S : t -> Prop,
  (forall x:t, (P x /\ Q x) \/ (R x /\ S x)) -> (forall x:t, Q x \/ S x).
Proof.
  intros.
  specialize (H x).
  destruct H.
  -
    destruct H.
    left.
    auto.
  -
    destruct H.
    right.
    auto.
Qed.

Lemma open_branch_exists__sat p :
  (exists b : branch p, open_branch b) -> sat p.
Proof.
  unfold open_branch.
  unfold sat.
  intro.
  destruct H as [b].
  exists atom_true_neg_atom_true_map.
  induction b.
  - (* branch_atom *)
    destruct a.
    + auto.
    + auto.
  - (* branch_and *)
    simpl in H.
    assert (H0 := (forall_and_or_l nat
      (fun n => branch_not_in (atom_init n) b1)
      (fun n => branch_not_in (atom_init n) b2)
      (fun n => branch_not_in (atom_neg_init n) b1)
      (fun n => branch_not_in (atom_neg_init n) b2)
    ) H).
    specialize (IHb1 H0).
    assert (H1 := (forall_and_or_r nat
      (fun n => branch_not_in (atom_init n) b1)
      (fun n => branch_not_in (atom_init n) b2)
      (fun n => branch_not_in (atom_neg_init n) b1)
      (fun n => branch_not_in (atom_neg_init n) b2)
    ) H).
    specialize (IHb2 H1).
    simpl.
    rewrite IHb1.
    rewrite IHb2.
    auto.
  - (* branch_or_l *)
    simpl in H.
    specialize (IHb H).
    simpl.
    rewrite IHb.
    auto.
  - (* branch_or_r *)
    simpl in H.
    specialize (IHb H).
    simpl.
    rewrite IHb.
    simpl.
    rewrite negb_andb.
    rewrite orb_comm.
    auto.
  - (* branch_neg_and_l *)
    simpl in H.
    specialize (IHb H).
    simpl in IHb.
    simpl.
    rewrite negb_andb.
    rewrite IHb.
    auto.
  - (* branch_neg_and_r *)
    simpl in H.
    specialize (IHb H).
    simpl in IHb.
    simpl.
    rewrite negb_andb.
    rewrite IHb.
    rewrite orb_comm.
    auto.
  - (* branch_neg_or *)
    simpl in H.
    assert (H0 := (forall_and_or_l nat
      (fun n => branch_not_in (atom_init n) b1)
      (fun n => branch_not_in (atom_init n) b2)
      (fun n => branch_not_in (atom_neg_init n) b1)
      (fun n => branch_not_in (atom_neg_init n) b2)
    ) H).
    specialize (IHb1 H0).
    assert (H1 := (forall_and_or_r nat
      (fun n => branch_not_in (atom_init n) b1)
      (fun n => branch_not_in (atom_init n) b2)
      (fun n => branch_not_in (atom_neg_init n) b1)
      (fun n => branch_not_in (atom_neg_init n) b2)
    ) H).
    specialize (IHb2 H1).
    simpl in IHb1.
    simpl in IHb2.
    simpl.
    rewrite negb_involutive.
    rewrite IHb1.
    rewrite IHb2.
    auto.
  - (* branch_neg_neg *)
    simpl in H.
    specialize (IHb H).
    simpl.
    rewrite negb_involutive.
    auto.
Qed.

Axiom exists_branch_pred__exists_neg_branch_pred : forall p f, (exists b : branch p, V f (¬ p) = V f (¬ b)) -> (exists b : branch (¬ p), V f (¬ p) = V f b).

Lemma prop__exists_branch : forall p f,
  exists b : branch p, V f p = V f b.
Proof.
  intros.
  induction p.
  -
    exists (branch_atom a).
    auto.
  -
    destruct IHp1 as [b].
    destruct IHp2 as [b0].
    simpl.
    exists (branch_and b b0).
    rewrite H.
    rewrite H0.
    auto.
  -
    destruct IHp as [b].
    apply exists_branch_pred__exists_neg_branch_pred.
    exists b.
    simpl.
    rewrite H.
    auto.
Qed.

Lemma prop_sat__exists_sat_branch p :
  sat p -> (exists b : branch p, sat b).
Proof.
  intro.
  destruct H as [f].
  assert (H0 := prop__exists_branch p f).
  destruct H0 as [b].
  exists b.
  exists f.
  rewrite <- H0.
  auto.
Qed.

Axiom V_f_decidable : forall p (f : atom -> bool),
  V f p = true \/ V f p = false.

Axiom neg_atom_true : forall (f : atom -> bool) n,
  f (atom_neg_init n) = true -> f (atom_init n) = false.

Axiom orb_false_or_iff : forall b b',
  b = false \/ b' = false <-> ~(b = true /\ b' = true).

Axiom sat__branch_in_atom_assign_true : forall f p (b : branch p) a,
  V f b = true -> branch_in a b -> f a = true.

Lemma closed_branch_is_unsat : forall p (b : branch p),
  closed_branch b -> unsat b.
Proof.
  unfold closed_branch.
  intros.
  destruct H as [n].
  destruct H.
  induction b.
  -
    simpl in H.
    rewrite <- H0 in H.
    contradiction (atom_not_eq n H).
  -
    simpl in H.
    intro.
    simpl.
    destruct H.
    +
      destruct H0.
      *
        specialize (IHb1 H).
        specialize (IHb1 H0).
        specialize (IHb1 f).
        rewrite IHb1.
        apply andb_false_l.
      * 
        apply andb_false_iff.
        apply orb_false_or_iff.
        intro.
        destruct H1.
        assert (H3 := sat__branch_in_atom_assign_true f p1 b1 (atom_init n) H1 H).
        assert (H4 := sat__branch_in_atom_assign_true f p2 b2 (atom_neg_init n) H2 H0).
        rewrite <- H4 in H3.
        contradiction (assign_atom_not_eq n f H3).
    +
      destruct H0.
      *
        apply andb_false_iff.
        apply orb_false_or_iff.
        intro.
        destruct H1.
        assert (H3 := sat__branch_in_atom_assign_true f p2 b2 (atom_init n) H2 H).
        assert (H4 := sat__branch_in_atom_assign_true f p1 b1 (atom_neg_init n) H1 H0).
        rewrite <- H4 in H3.
        contradiction (assign_atom_not_eq n f H3).
      * 
        specialize (IHb2 H).
        specialize (IHb2 H0).
        specialize (IHb2 f).
        rewrite IHb2.
        apply andb_false_r.
  - 
    simpl in H.
    simpl in H0.
    specialize (IHb H).
    specialize (IHb H0).
    simpl.
    auto.
  -
    simpl in H.
    simpl in H0.
    specialize (IHb H).
    specialize (IHb H0).
    simpl.
    auto.
  -
    simpl in H.
    simpl in H0.
    specialize (IHb H).
    specialize (IHb H0).
    simpl.
    auto.
  -
    simpl in H.
    simpl in H0.
    specialize (IHb H).
    specialize (IHb H0).
    simpl.
    auto.
  -
    simpl in H.
    intro.
    simpl.
    destruct H.
    +
      destruct H0.
      *
        specialize (IHb1 H).
        specialize (IHb1 H0).
        specialize (IHb1 f).
        rewrite IHb1.
        apply andb_false_l.
      * 
        apply andb_false_iff.
        apply orb_false_or_iff.
        intro.
        destruct H1.
        assert (H3 := sat__branch_in_atom_assign_true f (¬ p1) b1 (atom_init n) H1 H).
        assert (H4 := sat__branch_in_atom_assign_true f (¬ p2) b2 (atom_neg_init n) H2 H0).
        rewrite <- H4 in H3.
        contradiction (assign_atom_not_eq n f H3).
    +
      destruct H0.
      *
        apply andb_false_iff.
        apply orb_false_or_iff.
        intro.
        destruct H1.
        assert (H3 := sat__branch_in_atom_assign_true f (¬ p2) b2 (atom_init n) H2 H).
        assert (H4 := sat__branch_in_atom_assign_true f (¬ p1) b1 (atom_neg_init n) H1 H0).
        rewrite <- H4 in H3.
        contradiction (assign_atom_not_eq n f H3).
      * 
        specialize (IHb2 H).
        specialize (IHb2 H0).
        specialize (IHb2 f).
        rewrite IHb2.
        apply andb_false_r.
  -
    apply (IHb H H0).
Qed.

Lemma exists_sat_branch__exists_open_branch p :
  (exists b : branch p, sat b) -> (exists b : branch p, open_branch b).
Proof.
  intro.
  destruct H as [b].
  destruct H as [f].
  exists b.
  apply open_branch_iff.
  intro.
  apply closed_branch_is_unsat in H0.
  specialize (H0 f).
  rewrite H in H0.
  apply diff_true_false in H0.
  auto.
Qed.