resolution.v

Require Import List Bool  Classical.

Import ListNotations.
From mathcomp Require Import ssreflect ssrbool.
Require Import Ensembles ProofIrrelevance Classical_sets.



Definition var := nat.
Variable fls tru : var.

Inductive prop :=
  | Var : var -> prop
  | Not : prop -> prop
  | And : prop -> prop -> prop
  | Or : prop -> prop -> prop
  | Imp : prop -> prop -> prop
  .



Notation "# p" := (Var p) (at level 1).
Notation "A ∨ B" := (Or A B) (at level 15, right associativity).
Notation "A ∧ B" := (And A B) (at level 15, right associativity).
Notation "A ⊃ B" := (Imp A B) (at level 16, right associativity).
Notation "¬ A" := (Not A) (at level 5).
Notation "⊥" := (# fls).
Notation "⊤" := (# tru).


Definition assign := var -> bool.
Axiom fls_false : forall f : assign, f fls = false.
Axiom tru_true  : forall f : assign, f tru = true.


Fixpoint valuation (v : assign) (A : prop) :=
  match A with
  | # p => v p
  | ¬ A => negb (valuation v A)
  | A ∧ B => andb (valuation v A) (valuation v B)
  | A ∨ B => orb (valuation v A) (valuation v B)
  | A ⊃ B => implb (valuation v A) (valuation v B)
  end.

Definition tautology A :=
  forall v, valuation v A = true.

Inductive literal :=
  | pos : var -> literal
  | neg : var -> literal
  .

Definition l2p (l : literal) :=
  match l with
  | pos v => # v
  | neg v => ¬ # v
  end.

Definition comp l :=
  match l with
  | pos v => neg v
  | neg v => pos v
  end.

Definition clause := Ensemble literal.

Arguments In {U}.
Arguments Singleton {U}.
Arguments Union {U}.
Arguments Setminus {U}.
Arguments Included {U}.
Arguments Couple {U}.
Arguments Empty_set {U}.

Inductive resolve : clause -> clause -> clause -> Prop :=
  | resl (a : literal) (C1 C2 C : Ensemble literal) :
    In C1 a  -> In C2  (comp a) ->
    (* C =  (Union (Setminus C1 (Singleton a)) (Setminus C2 (Singleton (comp a)))) -> *)
    (* resolve C1 C2 C. *)
    resolve C1 C2 (Union (Setminus C1 (Singleton a)) (Setminus C2 (Singleton (comp a)))).


Inductive derive : Ensemble clause -> clause -> Prop :=
  | Drefl S C : In S C -> derive S C
  | Dresolve S C1 C2 C : derive S C1  -> derive S C2 -> resolve C1 C2 C -> derive S C.



Lemma derive_subset S C1 C D :
  ~ In S C1 -> derive (Union S (Singleton C1)) C ->
  exists D', Included D' D /\ derive (Union S (Singleton (Union C1 D))) (Union C D').
Proof.
  move => HC H.
  remember (Union S (Singleton C1)) as S'.
  induction H; subst.
  {
    inversion H; subst.
    - exists Empty_set; split; auto.
      - rewrite /Included.
        move => x F.
        inversion F.
        constructor; left.
        have : Union C Empty_set = C.
        - apply Extensionality_Ensembles; split => x Hx.
          - inversion Hx; auto.
            inversion H1.
          - left; auto.
        move => ->; auto .
    - exists D; split.
      - unfold Included; auto.
      - apply Singleton_inv in H0; subst.
        econstructor. right.
        apply Singleton_intro; auto.
  }
  {
    move : (IHderive1 (eq_refl _)) => [D1 [DD1 IH1]]; clear IHderive1.
    move : (IHderive2 (eq_refl _)) => [D2 [DD2 IH2]]; clear IHderive2.
    inversion H1; subst.

    exists (Union (Setminus D1 (Singleton a)) (Setminus D2 (Singleton (comp a)))); split.
    - unfold Included => x Hx.
      inversion_clear Hx; inversion_clear H4; auto.
     - econstructor 2 with
        (C1 := (Union C0 D1)) (C2 := (Union C2 D2)); auto.
      suff :
        (Union
          (Union (Setminus C0 (Singleton a)) (Setminus C2 (Singleton (comp a))))
          (Union (Setminus D1 (Singleton a)) (Setminus D2 (Singleton (comp a))))) =
        (Union
          (Setminus (Union C0 D1) (Singleton a))
          (Setminus (Union C2 D2) (Singleton (comp a)))). {
        move => ->.
        econstructor 1 with (a := a); try left; auto.
      }
      apply Extensionality_Ensembles.
      unfold Same_set; split => x Hx.
      * inversion_clear Hx; subst.
        + inversion_clear H4.
          - inversion H5.
            left. split; auto.
            left; auto.
          - inversion H5.
            right. split; auto.
            left; auto.
        + inversion_clear H4; subst; inversion_clear H5;
          [left | right]; split; auto; right; auto.
      * inversion_clear Hx; inversion_clear H4; inversion_clear H5.
        - left; left; split; auto.
        - right; left; split; auto.
        - left; right; split; auto.
        - right; right; split; auto.
  }
Qed.

Lemma derive_subset' S C1 C1' C :
  ~ In S C1 -> Included C1' C1 -> derive (Union S (Singleton C1)) C ->
  exists C', Included C' C /\ derive ((Union S (Singleton C1'))) C'.
Proof.
  move => HS HC H.
  remember (Union S (Singleton C1)) as S'.
  induction H; subst.
  {
    inversion_clear H; subst.
    - exists C; split.
      unfold Included; auto.
      constructor. left; auto.
    - apply Singleton_inv in H0; subst.
      exists C1'; split; auto.
      constructor; right; constructor.
  }
  {
    move : (IHderive1 (eq_refl _)) => [D1 [HD1 IH1]]; clear IHderive1.
    move : (IHderive2 (eq_refl _)) => [D2 [HD2 IH2]]; clear IHderive2.
    inversion H1; subst.
    case (classic (In D1 a)) => Ha1.
    case (classic (In D2 (comp a))) => Ha2.
    - exists (Union (Setminus D1 (Singleton a)) (Setminus D2 (Singleton (comp a)))); split.
      {
        unfold Included => x Hx.
        inversion_clear Hx; subst; inversion_clear H4; [left | right]; split; auto.
      }
      {
        econstructor 2 with (C1 := D1) (C2 := D2); auto.
        econstructor 1 with (a := a); auto.
      }
    - exists D2; split; auto.
      unfold Included => x Hx.
      right; split; auto.
      move => F; apply Singleton_inv in F; subst x.
      case (Ha2 Hx).
    - exists D1; split; auto.
      unfold Included => x Hx.
      left; split; auto.
      move => F; apply Singleton_inv in F; subst x.
      case (Ha1 Hx).
  }
Qed.