(** We verify a DNF-based solver for boolean formulas.
    We also consider tableau predicates for unsatisfiabilty.
 *)

From Coq Require Export Bool Lia List.
Notation "! b" := (negb b) (at level 39).
Import ListNotations.
Notation "x 'el' A" := (In x A) (at level 50).
Notation "x 'nel' A" := (~In x A) (at level 70).

(** We use the Equations package so that we can 
    define the DNF solver as a function with
    non-structural recursion. *)

From Equations Require Export Equations.
Set Equations Transparent.

(** A few facts about decidability *)

Definition dec X := {X} + {~X}.

Lemma dec_transport (X Y : Prop) : 
  (X <-> Y) -> dec X -> dec Y.
Proof.
  unfold dec; tauto.
Qed.

Lemma dec_DN X : 
  dec X -> ~~ X -> X.
Proof. 
  unfold dec; tauto. 
Qed.

(** Formulas and signed formulas are represented with  inductive types *)

Definition var := nat.
Inductive form: Type :=
  Var (x: nat) | Fal | Imp (s t : form).
Notation "s ~> t" := (Imp s t) (at level 41, right associativity).
Notation "-- s" := (s ~> Fal) (at level 35, right associativity).
Implicit Types x y : var.
Implicit Types s t : form.

Inductive sform : Type := Pos (s: form) | Neg (s: form).
Notation "+ s" := (Pos s) (at level 43).
Notation "- s" := (Neg s). (* cannot overwrite reserved level for nat *)
Definition clause := list sform.
Implicit Types S T : sform.
Implicit Types C D E : clause.
Implicit Types L : list clause.

Fact sform_eq_dec S T : dec (S = T).
Proof. 
  unfold dec. repeat decide equality. 
Defined.

Fact clause_eq_dec C D : dec (C = D).
Proof. 
  unfold dec. repeat decide equality. 
Defined.

Fact list_clause_eq_dec L L' : dec (L = L').
Proof. 
  unfold dec. repeat decide equality. 
Defined.

Fact clause_in_dec S C : dec (S el C).
Proof. 
  unfold dec. apply in_dec, sform_eq_dec.
Defined.

(** Evaluation of formulas and clauses *)

Implicit Types alpha beta : var -> bool.

Equations eva alpha s : bool :=
eva alpha (Var x)  := alpha x ;
eva alpha Fal      := false ;
eva alpha (s ~> t) := !eva alpha s || eva alpha t.
Equations evas alpha S : bool :=
evas alpha (+s) := eva alpha s ;
evas alpha (-s) := !eva alpha s.
Equations evac alpha C : bool :=
evac alpha []     := true ;
evac alpha (T::C) := evas alpha T && evac alpha C.
Equations evad alpha L : bool :=
evad alpha []     := false ;
evad alpha (C::L) := evac alpha C || evad alpha L.

(** Using the boolean infix operators !, &&, and || is essential
   so that proof goals remain readable. *)

Notation "alpha '|=' C" := (evac alpha C = true) (at level 70).
Definition satf s := exists alpha, eva alpha s = true. 
Definition satc C := exists alpha, alpha |= C.

Lemma satfc s :
  satf s <-> satc [+s].
Proof.
  split; intros [alpha H]; exists alpha; cbn in *;
    revert H; rewrite andb_true_r; trivial.
Qed.

Lemma evac_app alpha C D :
  evac alpha (C++D) = evac alpha C && evac alpha D.
Proof.
  induction C as [|S C IH]; cbn. reflexivity.
  rewrite IH. apply andb_assoc.
Qed.

Lemma evad_app alpha L L' :
  evad alpha (L++L') = evad alpha L || evad alpha L'.
Proof.
  induction L as [|C L IH]; cbn. reflexivity.
  rewrite IH. apply orb_assoc.
Qed.

Lemma evac_false S C alpha :
  S el C -> evas alpha S = false -> evac alpha C = false.
Proof.
  intros H1 H2. induction C as [|T C IH]; cbn.
  - destruct H1.
  - destruct H1 as [->|H1]. now rewrite H2.
    rewrite (IH H1). apply andb_false_r.
Qed.

(** We now define the DNF solver using well-founded recursion.
    Termination is based on the size of clauses.
 *)

Equations sizeF s : nat :=
sizeF (s1 ~> s2) := 1 + sizeF s1 + sizeF s2 ;
sizeF _          := 1.     
Equations size C : nat :=
size nil := 0 ;
size (+s::C) := sizeF s + size C ;
size (-s::C) := sizeF s + size C.

Equations? dnf C D : list clause by wf (size D) lt := 
dnf C [] := [C] ;
dnf C (+Fal :: _) := [] ;
dnf C (-Fal :: D) := dnf C D ;
dnf C (+Imp s t :: D) := dnf C (-s::D) ++ dnf C (+t::D) ;
dnf C (-Imp s t :: D) := dnf C (+s::-t::D) ;
dnf C (+Var x :: D) with clause_in_dec (-Var x) C :=
      { | left _ => [] ;
        | right _ => dnf (+Var x :: C) D } ;
dnf C (-Var x :: D) with clause_in_dec (+Var x) C :=
      { | left _ => [] ;
        | right _ => dnf (-Var x :: C) D } .
Proof.
  (* Proof obligations for termination *)
  all: lia. 
Qed.
(* We hide the kernel definition of dnf generated by 
   the Equations package. *)
Opaque dnf.

Compute dnf [] [- (-- (Var 0 ~> -- Var 1))].

Lemma dnf_eq' alpha C D :
  evad alpha (dnf C D) = evac alpha D && evac alpha C.
Proof.
  (** The lemma is proved with functional induction.
      Unfortunately, the tactic funelim for functional induction
      does not generate names meaningful for human readers.
      We thus rename some of the generated names.  *)     
  funelim (dnf C D);  
    try rename l into D;
    try clear Heq; try rename H into IH; try rename H0 into IH';
    try rename i into H; try rename n into H;
    cbn.
  - apply orb_false_r.
  - reflexivity.
  - rewrite evad_app, IH, IH'; cbn.
    repeat destruct (eva alpha _), (evac alpha _); trivial.
  - now rewrite IH.
  - rewrite IH; cbn. repeat destruct (eva alpha _); trivial.
  - destruct (evac alpha D), (alpha x) eqn:H1; cbn; trivial.
    symmetry. eapply evac_false. exact H. cbn. now rewrite H1.
  - rewrite IH. cbn. destruct (alpha x), (evac alpha D); trivial.
  - destruct (evac alpha D), (alpha x) eqn:H1; cbn; trivial.
    symmetry. eapply evac_false. exact H. cbn. now rewrite H1.
  - rewrite IH. cbn. destruct (alpha x), (evac alpha D); trivial.
Qed.


Lemma dnf_eq alpha C :
  evad alpha (dnf [] C) = evac alpha C.
Proof.
  rewrite dnf_eq'. apply andb_true_r.
Qed.

Print Assumptions dnf_eq.
 
(** Function dnf yields solved clauses *)

Inductive solved : clause -> Prop :=
| solved_nil :solved []
| solved_pos x C : -Var x nel C -> solved C -> solved (+Var x::C)
| solved_neg x C : +Var x nel C -> solved C -> solved (-Var x::C).

Lemma dnf_solved' C C' D :
  solved C -> D el dnf C C' -> solved D.
Proof.
  funelim (dnf C C');
    try rename l into C';
    try clear Heq; try rename H into IH; try rename H0 into IH';
      try rename i into H; try rename n into H;
        cbn; auto using solved; try tauto.
  - intuition congruence.
  - intros H1 H2%in_app_iff. intuition.
Qed.

Lemma dnf_solved C D :
  C el dnf [] D -> solved C.
Proof.
  apply dnf_solved'. constructor.
Qed.

(** Verification of a function that yields 
    solutions of solved clauses is surprisingly tricky *)

Definition sol C x := if clause_in_dec (+Var x) C then true else false.

Lemma evac_forall alpha C :
  alpha |= C <-> forall S, S el C -> evas alpha S = true.
Proof.
  induction C as [|T C IH]; cbn.
  - firstorder.
  - rewrite andb_true_iff, IH; clear. firstorder; congruence.
Qed.

Lemma solved_in {S C} :
  solved C -> S el C ->
  exists x, S = + Var x /\ -Var x nel C \/
       S = - Var x /\ +Var x nel C.
Proof.
  induction 1 as [|x C H1 _ IH|x C H1 _ IH]; cbn.
  - tauto.
  - intros [<-|H2].
    + exists x. intuition congruence.
    + destruct (IH  H2) as [x' [[-> H3]|[-> H3]]]; 
        exists x'; intuition congruence.
  - intros [<-|H2].
    + exists x. intuition congruence.
    + destruct (IH  H2) as [x' [[-> H3]|[-> H3]]]; 
        exists x'; intuition congruence.
Qed.

Lemma sol_solved C :
  solved C -> sol C |= C.
Proof.
  intros H. apply evac_forall. intros S H1.
  destruct (solved_in H H1) as [x [[-> H2]|[-> H2]]]; cbn;
    unfold sol; destruct clause_in_dec as [H3|H3]; tauto.
Qed.

(** We continue with verification of dnf *)

Lemma dnf_sol C D L :
  dnf [] C = D::L -> sol D |= C.
Proof.
  intros H. rewrite <- dnf_eq, H. cbn.
    rewrite sol_solved. reflexivity.
    eapply dnf_solved. rewrite H.
    apply in_eq.
Qed.

Lemma dnf_sat C :
  satc C <-> dnf [] C <> [].
Proof.
  split.
  - intros [alpha H] H1. revert H.
    rewrite <- dnf_eq, H1. cbn. discriminate.
  - destruct (dnf [] C) as [|D L] eqn:H. tauto.
    intros _. exists (sol D). eapply dnf_sol, H.
Qed.

Lemma dnf_unsat C :
  ~satc C <-> dnf [] C = [].
Proof.
  rewrite dnf_sat.
  destruct (list_clause_eq_dec (dnf [] C) []); tauto.
Qed.

Lemma satc_dec C :
  dec (satc C).
Proof.
  eapply dec_transport.
  - symmetry. apply dnf_sat.
  - unfold dec.
    destruct (list_clause_eq_dec (dnf [] C) nil); tauto.
Qed.

Lemma satf_dec s :
  dec (satf s).
Proof.
  eapply dec_transport.
  - symmetry. apply satfc.
  - apply satc_dec.
Qed.

Lemma sat_solve C :
  { alpha | alpha |= C } + { ~satc C }.
Proof.
  destruct (dnf [] C) as [|D L] eqn:H.
  - right. intros H1%dnf_sat. auto.
  - left. exists (sol D). eapply dnf_sol, H. 
Qed.

(** Tableau predicate for signed clauses *)

Inductive tab : list sform -> Prop :=
| tabM S C D: tab (S::C++D) -> tab (C++S::D)
| tabF C: tab (+Fal::C)
| tabC x C: tab (+Var x::-Var x::C)
| tabpI s t C: tab (-s::C) -> tab (+t::C) -> tab (+(s~>t)::C)
| tabnI s t C: tab (+s::-t::C) -> tab (-(s~>t)::C).

Lemma tab_sound C alpha :
  tab C -> alpha |= C -> False.
Proof.
  induction 1; cbn in *.
  - contradict IHtab. revert IHtab. cbn.
    do 2 rewrite evac_app. cbn.
    destruct (evac alpha C), (evas alpha S) ; auto.
  - discriminate.
  - destruct (alpha x); cbn; discriminate.
  - revert IHtab1 IHtab2.
    destruct (eva alpha s), (eva alpha t); cbn; auto.
  - revert IHtab. destruct (eva alpha s), (eva alpha t); cbn; auto.
Qed.

Lemma tabW C S:
  tab C -> tab (S::C).
Proof.
  induction 1.
  - apply (@tabM S0 (S::C)).
    apply (@tabM S [S0]), IHtab.
  - apply (@tabM (+Fal) [S]), tabF.
  - apply (@tabM (-Var x) [S;+Var x]).
    apply (@tabM (+Var x) [-Var x;S]), tabC.
  - apply (@tabM (+(s~>t)) [S]), tabpI.
    + apply (@tabM S [-s]), IHtab1.
    + apply (@tabM S [+t]), IHtab2.
  - apply (@tabM (-(s~>t)) [S]), tabnI.
    apply (@tabM S [+s;-t]), IHtab.
Qed.

Lemma tabR C D E :
  tab (rev D++C++E) -> tab (C++D++E).
Proof.
  induction D as [|S D IH] in C |-*; cbn; intros H.
  - exact H.
  - apply (@tabM S C).
    apply (IH (S::C)).
    change (S::C) with ([S]++C).
    revert H. do 2 rewrite <-app_assoc. trivial.
Qed.
    
Lemma tabL C D E :
  tab (C++D++E) -> tab (D++C++E).
Proof.
  intros H. apply tabR. apply tabR with (C:=[]).
  rewrite rev_involutive. exact H.
Qed.

Lemma tabM' C D S :
  tab (C++S::D) -> tab (S::C++D).
Proof.
  apply tabL with (D:=[S]).
Qed.

Lemma dnf_tab C D :
  dnf C D = [] -> tab (D ++ C).
Proof.
  funelim (dnf C D); cbn;
    try rename l into D;
    try clear Heq; try rename H into IH; try rename H0 into IH';
      try rename i into H; try rename n into H.
  - intros [=].
  - intros _. apply tabF.
  - intros [H1%IH H2%IH'] %app_eq_nil. now apply tabpI.
  - intros H1%IH. revert H1. apply tabW.
  - intros H1%IH. now apply tabnI.
  - intros _. apply in_split in H as (C1&C2&->).
    rewrite app_assoc.
    apply tabM with (C:=+Var x::D++C1).
    apply tabM with (C:=[-Var x]), tabC.
  - intros H1%IH. revert H1. apply tabM'.
  - intros _. apply in_split in H as (C1&C2&->).
    rewrite app_assoc.
    apply tabM with (C:=-Var x::D++C1), tabC.
  - intros H1%IH. revert H1. apply tabM'.
Qed.

Lemma tab_unsat C :
  tab C <-> ~ satc C.
Proof.
  split.
  - intros H [alpha H1]. revert H H1. apply tab_sound.
  - intros H%dnf_unsat%dnf_tab. rewrite app_nil_r in H. exact H.
Qed.

Lemma tab_solve C :
  { alpha | alpha |= C } + { tab C }.
Proof.
  destruct (sat_solve C) as [H|H]. now auto.
  right. apply tab_unsat, H.
Qed.

(** Refutation predicates *)

Implicit Types (A B: list form).

Equations eval alpha A : bool :=
eval alpha []     := true ;
eval alpha (s::A) := eva alpha s && eval alpha A.
Notation "alpha |== A" := (eval alpha A = true) (at level 70).
Definition sat A := exists alpha, alpha |== A.

Lemma map_pos alpha A :
  evac alpha (map Pos A) = eval alpha A.
Proof.
  induction A as [|s A IH]; cbn. reflexivity.
  f_equal. exact IH.
Qed.

Definition uns S : form :=
  match S with +s => s | -s => --s end.

Lemma uns_pos A :
  map uns (map Pos A) = A.
Proof.
  induction A as [|s A IH]; cbn. reflexivity.
  f_equal. exact IH.
Qed.

Section Refutation.
  Variables (rho: list form -> Prop)
            (Move: forall s A B, rho(s::A++B) -> rho(A++s::B))
            (Clash: forall x A, rho(Var x :: --Var x :: A))
            (Falsity: forall A, rho(Fal::A))
            (Posimp: forall s t A, rho(--s::A) -> rho(t::A) -> rho(s~>t::A))
            (Negimp: forall s t A, rho(s::--t::A) -> rho(--(s~>t)::A)).

  Lemma tab_rho C :
    tab C -> rho(map uns C).
  Proof.
    induction 1; cbn in *.
    - revert IHtab. rewrite !map_app. cbn. apply Move.
    - apply Falsity.
    - apply Clash.
    - now apply Posimp.
    - now apply Negimp.
  Qed.
  
  Theorem rho_solve A :
    { alpha | alpha |== A } + { rho A }.
  Proof.
    destruct (tab_solve (map Pos A)) as [[alpha H]|H].
    - left. exists alpha. rewrite map_pos in H. exact H.
    - right. apply tab_rho in H. rewrite uns_pos in H. exact H.
  Qed.
  
  Variable Sound: forall A , rho A -> ~sat A.

  Lemma rho_complete A :
    rho A <-> ~sat A.
  Proof.
    split. { apply Sound. } intros H.
    destruct (rho_solve A) as [[alpha H1]|H1]. 2:exact H1.
    exfalso. apply H. unfold sat; eauto.
  Qed.

  Lemma rho_dec A :
    dec (rho A).
  Proof.
    destruct (rho_solve A) as [[alpha H]|H].
    - right. intros H1%Sound. apply H1; unfold sat; eauto.
    - left. exact H.
  Qed.
End Refutation.

(** Validity *)

Definition valid s := forall alpha, eva alpha s = true.

Fact valid_unsat s :
  valid s <-> ~satf (--s).
Proof.
  split; intros H.
  - intros [alpha H1]. specialize (H alpha).
    revert H1. cbn. rewrite H. cbn. discriminate.
  - intros alpha. destruct (eva alpha s) eqn:H1. reflexivity.
    contradiction H. exists alpha. cbn. rewrite H1. trivial.
Qed.

Fact sat_valid s :
  satf s <-> ~valid (--s).
Proof.
  split.
  - intros [alpha H] H1. specialize (H1 alpha).
    revert H1. cbn. rewrite H. cbn.  discriminate.
  - intros H.  apply dec_DN. { apply satf_dec. }
    contradict H. intros alpha. cbn.
    destruct (eva alpha s) eqn:H1. 2:reflexivity.
    contradiction H. exists alpha. exact H1.
Qed.

Fact valid_solve s :
  { alpha | eva alpha s = false } + { valid s }.
Proof.
  destruct (sat_solve [-s]) as [[alpha H]|H].
  - left. exists alpha. revert H. cbn.
    destruct (eva alpha s); cbn; auto.
  - right. apply valid_unsat, H.
Qed.