(* (c) Copyright Joachim Bard, Saarland University                        *)
(* Distributed under the terms of the CeCILL-B license                    *)

Require Import Relations Classical_Pred_Type.
Require Import mathcomp.ssreflect.ssreflect.
From mathcomp Require Import all_ssreflect.
From libs Require Import edone bcase fset base.
Require Import testfree_PDL_def.

Set Implicit Arguments.
Unset Strict Implicit.
Import Prenex Implicits.

Arguments subsep [T X P].

Implicit Types (S cls X Y : {fset clause}) (C D : clause).

Definition rtrans a C D := R a C `<=` D.

Fixpoint reach_demo cls p : rel clause :=
  match p with
  | pV a => rtrans a
  | pCon p0 p1 => (fun C D => [some C' in cls, reach_demo cls p0 C C' && reach_demo cls p1 C' D])
  | pCh p0 p1 => (fun C D => reach_demo cls p0 C D || reach_demo cls p1 C D)
  | pStar p => (fun C D => connect_in cls (reach_demo cls p) C D)
  end.

Definition D0 cls := forall C, C \in cls -> hintikka C.
Definition D1 cls := forall C, C \in cls -> forall p s, [p]s^- \in C -> [some D in cls, reach_demo cls p C D && (s^- \in D)].

Record demo := Demo {
  cls :> {fset clause} ;
  demoD0 : D0 cls ;
  demoD1 : D1 cls }.

Arguments demoD1 [d C] _ [p s] _.

Canonical demo_predType := mkPredType (fun (S : demo) (C : clause) => nosimpl C \in cls S).

Lemma LCF (S : demo) C : C \in S -> ((fF^+ \in C) = false) * (forall p, (fV p^+ \in C) && (fV p^- \in C) = false).
Proof.
  move/demoD0. case/andP => /andP [/negbTE -> /allP H] _. split => // x.
  case inC: (fV x^+ \in C) => //=. apply: negbTE. apply: H _ inC.
Qed.

Section ModelExistience.
  Variables (S : demo).

  Definition Mtype := seq_sub S.
  Definition Mtrans a : rel Mtype := restrict S (rtrans a).
  Definition Mlabel (x: var) (C : Mtype) := fV x^+ \in val C.

  Definition model_of := FModel Mtrans Mlabel.

  Implicit Types (c d : model_of).

  Unset Printing Records.

  Lemma reach2demo p c d : reachb Mtrans p c d -> reach_demo S p (val c) (val d).
  Proof.
    elim: p c d => [a|p0 IH0 p1 IH1|p0 IH0 p1 IH1|p IHp] c d //=.
    - move/existsP => [z /andP [L R]]. apply/hasP. exists (val z). apply z.
      apply/andP. split. by apply IH0. by apply IH1.
    - move/orP => [H|H]; apply/orP. left. by apply IH0. right. by apply IH1.
    - move => H. apply/existsP. exists c. apply/existsP. exists d => /=. apply/and3P.
      repeat split => //. move: H => /connectP [A H E]. apply/connectP. exists A => //.
      elim: A c H E => [c H E|a A IHA c /andP [cRa H] E] //=.
      rewrite IHp //. by apply: IHA.
  Qed.

  Lemma demo2reach p c d : reach_demo S p (val c) (val d) -> reachb Mtrans p c d.
  Proof.
    elim : p c d => [a|p0 IH0 p1 IH1|p0 IH0 p1 IH1|p IHp] c d //=.
    - move/hasP => [C' inS /andP [L R]]. apply/existsP. exists (SeqSub C' inS). by rewrite IH0 ?IH1.
    - move/orP => [H|H]; by [rewrite /= IH0| rewrite /= IH1].
    - move/existsP => [c' /existsP [d' H]] /=. move: H => /and3P [/eqP eqc /eqP eqd].
      move/connectP => [cs H E]. apply/connectP.
      exists cs; last by rewrite -(val_inj _ _ eqc) -(val_inj _ _ eqd).
      elim: cs c c' eqc H E => [|b cs IHcs] c c' eqc //= /andP [cRb H] E.
      rewrite IHp //=. by rewrite (IHcs b b). by rewrite -eqc.
  Qed.

  Lemma hint_reach_pos p s C D : hintikka C -> [p]s^+ \in C -> reach_demo S p C D -> s^+ \in D.
  Proof.
    elim: p s C D => [a|p0 IH0 p1 IH1|p0 IH0 p1 IH1|p IHp] s C D hint_C.
    - move => /= inC. move/allP => cRd. apply: (cRd (s, _)).
      apply/fimsetP. exists ([pV a]s^+) => //. by rewrite in_fset inC /=.
    - move/hint_box_con => H /= /hasP [c' inS /andP [cRc' c'Rd]].
      apply: IH1; last exact: c'Rd. exact: (demoD0 inS).
      apply: (IH0 _ _ _ hint_C); last exact: cRc'. exact: H.
    - case/hint_box_ch => // H0 H1 /= /orP [cRd|cRd]. exact: IH0. exact: IH1.
    - move => Hstar /connect_inP [A H].
      elim: A s C hint_C Hstar H => [/=| a A IHA] s C hint_C.
      + by case/hint_box_star => // inC _ /= [_ _ ->].
      + case/hint_box_star => // _ inC /= [/and3P [_ inS AsubS] /andP [vRa H] E].
        apply: IHA; [exact: demoD0 | exact: IHp | by rewrite E H /= inS AsubS].
  Qed.

  Lemma hint_eval s b c : (s, b) \in val c -> eval (interp (s, b)) c.
  Proof.
    elim: s b c => [|x|s IHs t IHt|p s IHs] [|] c;
      try by rewrite /= ?(LCF (ssvalP c)); auto.
    - move => /= nx. rewrite /Mlabel. case: (LCF (ssvalP c)) => /= _ H px. move: (H x).
        by rewrite px nx.
    - case/hint_imp_pos; first by case: c => C; exact: demoD0.
      move/IHs => /=. tauto. move/IHt => /=. by auto.
    - case/hint_imp_neg; first by case: c => C; exact: demoD0. move => [/IHs /= Hs /IHt] /=.
      by auto.
    - move => H d cRd. apply: (IHs true).
      apply: (hint_reach_pos (C:= val c)) => //; last by apply: reach2demo; apply/reachP.
      move: H cRd. case c => C CinS _ _. exact: (demoD0 CinS).
    - move => inC /=. apply: ex_not_not_all.
      have /hasP CD: [some D in S , reach_demo S p (val c) D && (s^- \in D)]
        by apply: (demoD1 (ssvalP c)).
      case: CD => D DinS /andP [cRD inD]. exists (SeqSub D DinS). rewrite (rwP (evalP _ s)).
      rewrite (rwP (reachP p c (SeqSub _ DinS))). rewrite (rwP implyP).
      rewrite demo2reach //=. move/evalP. exact: (IHs false).
  Qed.

End ModelExistience.

Section Pruning.

  Variable (F: {fset form}).
  Hypothesis sfc_F : sf_closed F.
  Definition PU := powerset (flipcl F).
  Definition S0 := [fset C in PU | hintikka C && maximal F C].

  Definition P1 C S := ~~ [all u in C, if u is [p]s^- then
    [some D in S, reach_demo S p C D && (s^- \in D)] else true].
  Definition pcond C S := P1 C S.

  Lemma prune_D0 : D0 (prune pcond S0).
  Proof.
    move => C. move/(subP (prune_sub _ _)). rewrite inE. by case/and3P.
  Qed.

  Lemma prune_D1 : D1 (prune pcond S0).
  Proof.
    move => C /pruneE. rewrite negbK. move/allP => H p s Hs. exact: (H ([p]s^-) Hs).
  Qed.

  Definition DD := Demo prune_D0 prune_D1.

  Definition supp S (C: clause) := [some D in S, C `<=` D].

  Local Notation "S |> C" := (supp S C) (at level 30, format "S |> C").

  Definition coref (ref : clause -> Prop) S :=
    forall C, C \in S0 `\` S -> ref C.

  Inductive ref : clause -> Prop :=
  | R1 S C : coref ref S -> C \in PU -> ~~ S |> C -> ref C
  | R2 S C p s : S `<=` S0 -> coref ref S -> C \in S
                 -> [p]s^- \in C -> ~~[some D in S, reach_demo S p C D && (s^- \in D)] -> ref C.

  Lemma corefD1 S C : ref C -> coref ref S -> coref ref (S `\` [fset C]).
  Proof.
    move => rC coS D. rewrite !in_fsetD negb_and andb_orr -in_fsetD negbK in_fset1.
    case/orP; first exact: coS. by case/andP => [_ /eqP ->].
  Qed.

  Lemma coref_DD : coref ref DD.
  Proof.
    apply: prune_ind => [C|C S]; first by rewrite inE andbN.
    case/allPn. case. case => // p s. case => // inC H inS corS sub.
    apply: corefD1 => //. exact: (R2 sub).
  Qed.

  Lemma DD_refute C : C \in PU -> ~~ DD |> C -> ref C.
  Proof. move => inU. apply: R1 _ inU => //. exact: coref_DD. Qed.

End Pruning.

Definition sat (M: cmodel) C := exists (w: M), forall s, s \in C -> eval (interp s) w.

Notation "S |> C" := (supp S C) (at level 30, format "S |> C").

Theorem pruning_completeness F (sfc_F : sf_closed F) (C: clause) :
  C \in PU F -> ref F C + exists2 M: fmodel, sat M C & #|{: M}| <= 2 ^ (2 * size F).
Proof.
  move => inPU. case: (boolP ((DD F) |> C)) => H; [right|left; exact: DD_refute].
  exists (model_of (DD F)).
  - case/hasP : H => D D1 /subP D2. exists (SeqSub _ D1) => s inC.
    move: inPU. move/powersetP => sub. case: s inC => s b inC.
    apply: hint_eval => //=; last exact: D2.
  - rewrite card_seq_sub ?funiq //.
    apply: leq_trans; last by apply: (leq_pexp2l _ (size_flipcl F)).
    rewrite -powerset_size subset_size /DD /S0 //=.
    apply: sub_trans; [exact: prune_sub | exact: subsep].
Qed.