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

Require Import Relations Omega.
Require Import mathcomp.ssreflect.ssreflect.
From mathcomp Require Import all_ssreflect.
From libs Require Import edone bcase fset base modular_hilbert.
Require Import testfree_PDL_def demo.

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

Implicit Types (C D : clause).

Section RefPred.
  Variable (F : {fset form}).
  Hypothesis (sfc_F : sf_closed F).

  Local Notation S0 := (S0 F).
  Local Notation PU := (PU F).
  Local Notation xaf := (fun C => [af C]).

  Definition ref C := prv ([af C] ---> Bot).

  Lemma refI1n s C : prv ([af C] ---> s) -> ref (s^- |` C).
  Proof.
    move => H. rewrite /ref. rewrite -> andU,H,bigA1,axAC.
    rule axAcase. exact: axContra.
  Qed.

  Lemma refE1n s C : ref (s^- |` C) -> prv ([af C] ---> s).
  Proof.
    move => H. rewrite /ref in H. rewrite -> andU,bigA1 in H.
    Intro. ApplyH axDN. Intro. ApplyH H. by ApplyH axAI.
  Qed.

  Lemma ax_cons C : ~~ lcons C -> prv ([af C] ---> Bot).
  Proof.
    rewrite negb_and -has_predC negbK.
    case/orP => [inC|/hasP [s sinC /=]].
    - rewrite -> (bigAE _ inC). exact: axI.
    - rewrite negbK => nsinC.
      rewrite -> (axA2 [af C]). rewrite -> (bigAE _ sinC) at 2.
      rewrite -> (bigAE _ nsinC). simpl. rule axAcase. case: s sinC nsinC => s [|] _ _ /=.
      exact: axI. exact: axContra.
  Qed.

  Section ContextRefutations.
    Variable S : {fset clause}.
    Hypothesis sub_S : S `<=` S0.
    Hypothesis coref_S : coref F ref S.

    Lemma not_hint_max C : C \in PU -> maximal F C -> ~~ hintikka C -> prv ([af C] ---> Bot).
    Proof.
      rewrite powersetE => /subP Csub. move/allP => M. rewrite negb_and.
      case/orP; first exact: ax_cons.
      rewrite -has_predC. case/hasP. move => s inC /=. move: (Csub _ inC). move/flip_drop_sign.
      case: s inC. move => [|x|s t|[a|p0 p1|p0 p1|p] s] [|] //= inC inF.
      - move: (sfc_F inF) => /=. case/andP => sinF tinF.
        rewrite negb_or. case/andP => /negbTE sninC /negbTE tninC. move: (M s sinF).
        rewrite sninC orbF => sinC. move: (M t tinF). rewrite tninC /= => tinC.
        do 2 rule axDup. rewrite -> (bigAE _ inC) at 1. rewrite -> (bigAE _ tinC) at 1.
        rewrite -> (bigAE _ sinC) => /=. exact: ax_contraNN.
      - move: (sfc_F inF) => /=. case/andP => sinF tinF. rewrite negb_and.
        case/orP => [/negbTE sninC | /negbTE tninC].
        + move: (M s sinF). rewrite sninC /= => sinC. rule axDup.
          rewrite -> (bigAE _ inC) at 1. rewrite -> (bigAE _ sinC). do 2 Intro. Apply* 1. Intro.
          rewrite <- (axBE t). by Apply* 1.
        + move: (M t tinF). rewrite tninC orbF => tinC. rule axDup. rewrite -> (bigAE _ inC) at 1.
          rewrite -> (bigAE _ tinC). do 2 Intro. Apply* 1. Intro. by Asm.
      - move/negbTE => ninC. move: (sfc_F inF). case/andP => inF' _. move: (M _ inF').
        rewrite ninC /= => inC'. rule axDup. rewrite -> (bigAE _ inC') at 1.
        rewrite -> (bigAE _ inC) => /=. rewrite -> axConE. exact: axI.
      - move/negbTE => ninC. move: (sfc_F inF). case/andP => inF' _. move: (M _ inF').
        rewrite ninC orbF => inC'. rule axDup. rewrite -> (bigAE _ inC') at 2.
        rewrite -> (bigAE _ inC) => /=. rewrite <- axCon. exact: axI.
      - move: (sfc_F inF) => /=. case/and3P => inF0 inF1 _. rewrite negb_and.
        case/orP => [/negbTE ninC0 | /negbTE ninC1].
        + move: (M _ inF0). rewrite ninC0 /= => inC0. rule axDup. rewrite -> (bigAE _ inC0) at 1.
          rewrite -> (bigAE _ inC) => /=. rewrite -> axChEl. exact: axI.
        + move: (M _ inF1). rewrite ninC1 /= => inC1. rule axDup. rewrite -> (bigAE _ inC1) at 1.
          rewrite -> (bigAE _ inC) => /=. rewrite -> axChEr. exact: axI.
      - move: (sfc_F inF). case/and3P => inF0 inF1 _. rewrite negb_or.
        case/andP => /negbTE ninC0 /negbTE ninC1. move: (M _ inF0) (M _ inF1).
        rewrite ninC0 ninC1 !orbF => inC0 inC1. do 2 rule axDup. rewrite -> (bigAE _ inC0) at 1.
        rewrite -> (bigAE _ inC1) at 1. rewrite -> (bigAE _ inC) => /=.
        rewrite -> (axDNE [p0 + p1]s). exact: axCh.
      - move: (sfc_F inF). case/andP => pinF sinF. rewrite negb_and.
        case/orP => [/negbTE sninC | /negbTE pninC].
        + move: (M _ sinF). rewrite sninC /= => sinC. rule axDup. rewrite -> (bigAE _ sinC) at 1.
          rewrite -> (bigAE _ inC) => /=. rewrite -> axStarEl. exact: axI.
        + move: (M _ pinF). rewrite pninC /= => pinC. rule axDup.
          rewrite -> (bigAE _ inC) at 2 => /=. rewrite -> axStarEr.
          rewrite -> (bigAE _ pinC) => /=. exact: axI.
      - move: (sfc_F inF). case/andP => pinF sinF. rewrite negb_or.
        case/andP => /negbTE sninC /negbTE pninC. move: (M _ pinF) (M _ sinF).
        rewrite sninC pninC !orbF => pinC sinC. do 2 rule axDup.
        rewrite -> (bigAE _ inC) at 3 => /=. rewrite -> (axDNE [p^*]s).
        rewrite -> (bigAE _ sinC) at 1. rewrite -> (bigAE _ pinC). exact: axStar.
    Qed.

    Lemma bigxm C s : prv ([af C] ---> [af s^+ |` C] :\/: [af s^- |` C]).
    Proof.
      apply: (rMP (s := s :\/: ~~:s)); last exact: axI. rule axOE.
      - rewrite <- axOIl. do 2 Intro. apply: bigAI => t. rewrite !inE. case/orP.
        + move/eqP => -> /=. Asm.
        + move => inC. Rev. drop. exact: bigAE.
      - rewrite <- axOIr. do 2 Intro. apply: bigAI => t. rewrite !inE. case/orP.
        + move/eqP => -> /=. Asm.
        + move => inC. Rev. drop. exact: bigAE.
    Qed.

    Lemma baseP0 C : C \in PU ->
      prv ([af C] ---> \or_(D <- [fset D in S0 | C `<=` D]) [af D]).
    Proof.
      rewrite powersetE. apply: (slack_ind (P := fun C => prv ([af C] ---> _))) => D IH sub.
      case (boolP (maximal F D)).
      - case (boolP (hintikka D)).
        + move => H M. apply: bigOI. rewrite !inE powersetE sub H M /=. by apply/allP.
        + move: sub. rewrite -powersetE => sub nH M. rewrite -> (not_hint_max sub M nH).
          exact: axBE.
      - rewrite -has_predC. case/hasP => s inF /=. rewrite negb_or. case/andP => sninD fsninD.
        rewrite -> (bigxm D s). rule axOE; (rewrite -> IH; last by rewrite fproper1).
        + apply: or_sub. move => E. rewrite !inE. case/andP => /and3P [-> -> ->] /=.
          by case/fsubUsetP.
        + rewrite fsubUset sub fsub1 /= andbT. apply/cupP. exists s. by rewrite inF !inE eqxx.
        + apply: or_sub. move => E. rewrite !inE. case/andP => /and3P [-> -> ->] /=.
          by case/fsubUsetP.
        + rewrite fsubUset sub fsub1 /= andbT. apply/cupP. exists s. by rewrite inF !inE eqxx.
    Qed.

    Lemma baseP C : C \in PU ->
      prv ([af C] ---> \or_(D <- [fset D in S | C `<=` D]) [af D]).
    Proof.
      move => Csub. rewrite -> baseP0 => //. apply: bigOE => D. rewrite !inE.
      case/andP => /and3P [Dsub M H] CsubD.
      case inS: (D \in S).
      - apply: bigOI. by rewrite !inE inS CsubD.
      - rewrite -> coref_S; first exact: axBE. by rewrite !inE Dsub M H inS.
    Qed.

    Lemma or_S : prv (\or_(C <- S) [af C]).
    Proof.
      apply (rMP (s := [af fset0])).
      - rewrite -> baseP; last by rewrite powersetE sub0x. apply: bigOE => C. rewrite inE.
        case/andP => inS _. exact: bigOI.
      - mp; last exact: axT. apply: bigAI => s. by rewrite inE.
    Qed.

    Lemma neg_or A : A `<=` S -> prv ((~~: \or_(C <- A) [af C]) ---> \or_(C <- S `\` A) [af C]).
    Proof.
      move => sub. mp; last exact: or_S. apply: bigOE => C inS. case inA: (C \in A).
      - rewrite <- (bigOI _ inA). exact: axContra.
      - rule axC. drop. apply: bigOI. by rewrite inE inS inA.
    Qed.

    Lemma nsub_contra C D :
      C \in S -> D \in S -> ~~ (C `<=` D) -> prv ([af C] ---> [af D] ---> fF).
    Proof.
      move => /(subP sub_S). rewrite inE powersetE. case/and3P => sub _ _.
      move/(subP sub_S). rewrite inE. case/and3P => _ _ /allP maxD. case/subPn.
      case => s [|]; move => inC ninD; move: (maxD s); rewrite (negbTE ninD) ?orbF /=;
      rewrite -> (bigAE _ inC); move: inC => /(subP sub) => inF;
      rewrite (flip_drop_sign inF) => inD; rule axC; (rewrite -> bigAE;
      last exact: inD); [done| by rule axC].
    Qed.

    Lemma neq_contra C D : C \in S -> D \in S -> C != D -> prv ([af C] ---> [af D] ---> fF).
    Proof.
      move => CinS DinS. rewrite eqEsub negb_and.
      case/orP => H; [exact: nsub_contra | rule axC; exact: nsub_contra].
    Qed.

    Lemma R1 C : C \in PU -> ~~ S |> C -> ref C.
    Proof.
      rewrite /ref => H1 H2. rewrite -> baseP => //.
      apply: bigOE => D. rewrite inE => /andP [D1 D2]. case: notF.
      apply: contraNT H2 => _. by apply/hasP; exists D.
    Qed.

    Lemma R2_aux C D p :
      C \in S -> D \in S -> ~~ reach_demo S p C D -> prv ([af C] ---> [p]~~:[af D]).
    Proof.
      elim: p C D => [a|p0 IH0 p1 IH1|p0 IH0 p1 IH1|p IHp] C D CinS DinS /=.
      - rewrite -has_predC. case/hasP. case => s [|]; last by rewrite (negbTE (Rpos _ _ _)).
        rewrite RE /= => inC ninD.
        move: CinS => /(subP sub_S). rewrite inE powersetE. case/and3P => sub _ _.
        move: DinS => /(subP sub_S). rewrite inE. case/and3P => _ _ /allP maxD. move: (maxD s).
        rewrite (negbTE ninD) /= => inD.
        rewrite <- (axDN ([pV a](~~: [af D]))).
        rewrite -> (dmAX (pV a) (~~: [af D])). rewrite -> rEXn; last exact: axDN.
        rewrite -> (bigAE _ inC). rewrite -> (rEXn (pV a) (t:= ~~: s)).
        + rule axC. do 2 Intro. rule axB; last by do 2 Rev; exact: axDBD.
          rewrite -> rEXn; first exact: axnEXF. rewrite -> (axDNE (~~: s ---> ~~: s)). exact: axI.
        + rewrite -> bigAE; last apply: inD; first exact: axI. apply: (@flip_drop_sign _ (s^+)).
          apply: flipcl_refl. apply: sf_closed_box => //. apply: (@flip_drop_sign _ ([pV a]s^+)).
          by apply/(subP sub).
      - rewrite -all_predC. move/allP => H. rewrite <- axCon.
        rewrite <- (axDN ([p0][p1](~~: [af D]))).
        rewrite -> (dmAX p0 ([p1](~~: [af D]))).
        rewrite -> (rEXn p0 (t:= (\or_(E <- S) [af E]) :/\: EX p1 [af D])); last
          by apply: (rMP _ or_S); exact: axAI.
        rewrite -> rEXn; last by rewrite -> bigODr; exact: axI. rewrite -> bigEOOE.
        rule axC. apply: bigOE => E inS. move: (H E inS) => /=. rewrite negb_and.
        case/orP => [H0|H1].
        + rewrite -> (IH0 C E) => //. do 2 Intro. rule axB; last by do 2 Rev; exact: axDBD.
          rewrite -> rEXn; first exact: axnEXF. do 2 rule axAcase. rule axC. drop.
          exact: axContra.
        + rule axC. drop. rewrite -> rEXn; first exact: axnEXF.
          rule axDup. rewrite -> axAEl at 2. rewrite -> axAEr. by rewrite -> (IH1 E D).
      - rewrite negb_or. case/andP => H0 H1. rewrite <- axDup. rewrite -> IH0 at 1 => //.
        rewrite -> (IH1 C D) => //. exact: axCh.
      - move => H.
        set I := [fset E in S | reach_demo S (p^*) C E].
        rewrite <- (rStar_ind (u:= \or_(E <- I)[af E])).
        + apply: bigOI. by rewrite !inE CinS /= connect_in0.
        + rewrite <- (axDN ([p](\or_(E<-I) [af E]))). rewrite -> (dmAX p (\or_(E<-I) [af E])).
          apply: bigOE => E EinI. rewrite -> rEXn; last by apply: neg_or; exact: subsep.
          rewrite -> bigEOOE. rule axC. apply: bigOE => G GninI. rewrite -> (IHp E G) => //.
          * apply: (subP subsep). exact: EinI.
          * apply: (subP (fsubDl _ _)). exact: GninI.
          * apply/negP => ERG. move: GninI. rewrite inE. case/andP => GinS. apply/negP.
            apply/negPn. rewrite inE GinS /=. apply: connect_in_trans. move: EinI.
            case/sepP => _ CE. exact: CE. apply: connect_in1 => //. apply: (subP subsep).
            exact: EinI.
        + apply: bigOE => E inI.
          apply: neq_contra => //; first by apply/(subP subsep); exact: inI.
          apply/negP. move/eqP => eq. move: inI. by rewrite eq inE DinS /= (negbTE H).
    Qed.

    Lemma R2 C p s :
      C \in S -> [p]s^- \in C -> ~~[some D in S, reach_demo S p C D && (s^- \in D)]
        -> ref C.
    Proof.
      move => inS inC. rewrite -all_predC. move/allP => nR.
      set X := [fset D in S | [fset s^-] `<=` D].
      have AAX: prv ([af C] ---> [p]\and_(D <- X) ~~:[af D]).
      { rewrite <- bigABBA. apply: bigAI => D. rewrite inE fsub1. case/andP => DinS inD.
        apply: R2_aux => //. move: (nR D DinS) => /=. by rewrite negb_and inD orbF.
      }
      have EOX: prv ([af C] ---> EX p (\or_(D <- X) [af D])).
      { rewrite <- rEXn; first by rewrite <- dmAX; exact: (bigAE _ inC).
        rewrite /X. rewrite <- (baseP (C:= [fset s^-])).
        - apply: bigAI => t. rewrite inE. move/eqP => -> /=. exact: axI.
        - apply/powersetP => t. rewrite inE. move/eqP => ->. apply: flipcl_refl.
          apply (@sf_closed_box F p s sfc_F).
          move: sub_S => /subP sub. move: inS => /sub.
          rewrite inE powersetE. move/andP => [/subP H _].
          apply: (@flip_drop_sign _ ([p]s^-)). exact: H.
      }
      rule axDup. rewrite -> EOX at 1. rewrite -> AAX. do 2 Intro.
      rule axB; last by do 2 Rev; exact: axDBD.
      rewrite -> rEXn; first exact: axnEXF.
      rewrite <- (axAcase (\or_(D<-X) [af D]) (\and_(D<-X) ~~: [af D]) Bot).
      apply: bigOE => D inX. rule axC. exact: bigAE.
    Qed.

  End ContextRefutations.

  Theorem href_of C : demo.ref F C -> ref C.
  Proof. elim => *;[ apply: R1 | apply: R2 ]; eassumption. Qed.

End RefPred.

Lemma prv_ref_sound C : prv ([af C] ---> Bot) -> ~ (exists M: fmodel, sat M C).
Proof. move => H [M] [w] X. apply satA in X. exact: finite_soundness H M w X. Qed.

Theorem informative_completeness s :
    prv (fImp s fF)
  + (exists2 M: fmodel, #|M| <= 2^(2 * f_size s) & exists w: M, eval s w).
Proof.
  set F := ssub s. have sfc_s := @sfc_ssub s.
  case: (@pruning_completeness F _ [fset s^+]) => //.
  - by rewrite powersetE fsub1 flipcl_refl // ssub_refl.
  - move => /href_of H. left. rewrite /ref in H. rewrite <- H => //. apply: bigAI => t.
    by rewrite inE => /eqP ->.
  - move => H. right. move: H => [M] [w] /(_ (s^+) (fset11 _)) /= ? S.
    exists M; last by exists w.
    apply: leq_trans S _. by rewrite leq_exp2l ?leq_mul ?size_ssub.
Qed.

Corollary completeness s : valid s -> prv s.
Proof.
  case: (informative_completeness (~~: s)) => [H|[M] _ [w] H] V.
  - by rule axDN.
  - exfalso. apply: H. exact: (V (cmodel_of_fmodel M)).
Qed.

Corollary prv_dec s : decidable (prv s).
Proof.
  case: (informative_completeness (~~: s)) => H; [left|right].
  - by rule axDN.
  - move => prv_s. case: H => M _ [w]. apply. exact: (@soundness _ prv_s M).
Qed.

Corollary sat_dec s : decidable (exists (M: cmodel) (w: M), eval s w).
Proof.
  case: (informative_completeness s) => H; [right|left].
  - case => M [w] Hw. exact: (@soundness _ H M).
  - case: H => M _ [w] ?. by exists M; exists w.
Qed.

Corollary valid_dec s : decidable (forall (M: cmodel) (w: M), eval s w).
Proof.
  case (sat_dec (fImp s fF)) => /= H; [by firstorder|left => M w].
  by case (modelP s w); firstorder.
Qed.

Corollary small_models s:
  (exists (M: cmodel) (w: M), eval s w) ->
  (exists2 M: fmodel, #|M| <= 2^(2 * f_size s) & exists w: M, eval s w).
Proof.
  case: (informative_completeness s) => // /(soundness) H [M] [w] w_s.
  exfalso. exact: H w_s.
Qed.