Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq.
Require Import choice fintype finfun finset path fingraph bigop.

Require Import edone bcase fset.
Require Import base CTL_def tab_def modular_hilbert.

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

Tableau Refutations to Hilbert Refutations

Associtated Formuals

Notation "[ 'af' C ]" := (\and_(s <- C) interp s) (at level 0, format "[ 'af' C ]").

Lemma af1p (s : form) : prv (s ---> [af [fset s ^+]]).
Proof. apply: bigAI => t. by rewrite !inE => /eqP ->. Qed.

Lemma afp1 s : prv ([af [fset s ^+]] ---> s).
Proof. change s with (interp (s^+)) at 2. apply: bigAE. by rewrite !inE. Qed.

Lemma af1n s : prv (Neg s ---> [af [fset s ^-]]).
Proof. apply: bigAI => t. by rewrite !inE => /eqP ->. Qed.

Lemma afn1 s : prv ([af [fset s ^-]] ---> Neg s).
Proof. change (Neg s) with (interp (s^-)). apply: bigAE. by rewrite !inE. Qed.

Definition hist (H : {fset clause }) := \and_(C <- H ) ~~: [af C].

Definition AU_ (H : {fset clause }) (s t : form) := AU (s :/\: hist H) (t :/\: hist H).

Lemma histU C (H : {fset clause }) :
  prv (hist (C |` H) <--> ~~: [af C ] :/\: hist H).
Proof. rule axAI.
  - rewrite {1}/hist. by rewrite -> andU, bigA1.
  - rewrite {2}/hist. by rewrite -> andU, bigA1.
Qed.

Definition interp_a A :=
  match A with
    | aVoid => Top
    | aAU (s, t, H) => AU (s :/\: hist H) (t :/\: hist H)
    | aAXU (s, t, H) => AX (AU (s :/\: hist H) (t :/\: hist H))
    | aAR (s, t, H) => EU (~~:s :/\: hist H) (~~: t :/\: hist H)
    | aAXR (s, t, H) => EX (EU (~~:s :/\: hist H) (~~: t :/\: hist H))
  end.

Lemma axAUHu s t H : mprv (AU_ H s t ---> (t :/\: hist H ) :\/: ((s :/\: hist H ) :/\: AX (AU_ H s t))).
Proof. rewrite /AU_. by rewrite -> axAUu at 1. Qed.

Lemma dmAUH s t H :
  mprv (~~: AU_ H s t ---> (~~: t :\/: ~~: hist H ) :/\: ((~~: s :\/: ~~: hist H ) :\/: EX (~~: AU_ H s t))).
Proof.
  rewrite /AU_. rewrite -> dmAU at 1. do ! rewrite -> dmA.
  rewrite -> axERu. rewrite -> (dmAi s (hist H)) at 2. rewrite -> (dmAi t (hist H)) at 2.
  rewrite -> dmAUi. done.
Qed.

Lemma box_request (C : clause) : prv ([af C ] ---> AX [af R C ]).
Proof.
  rewrite <- bigABBA. apply: bigAI. case => [s [|]]; last by rewrite (negbTE (Rpos _ _)).
  rewrite RE. exact: bigAE.
Qed.

Lemma annot_request E : prv (interp_a E ---> AX (interp_a (aR E))).
Proof.
  case: E => [[[s t] H]|[[s t] H]|[[s t] H]|[[s t] H]|]; try (Intro; ApplyH axBT).
  exact: axI.
Qed.

Lemma hist0 s : prv (s ---> s :/\: hist fset0).
Proof. Intro. ApplyH axAI. drop. rewrite /hist fset0Es big_nil. exact: axI. Qed.

Translation of History Rules

Lemma AUH_sound (s t : form) (C : clause) H :
  prv ([af C ] ---> ~~: t) ->
  prv ([af C ] ---> s ---> EX (~~: (AU_ (C |` H) s t ))) ->
  prv ([af C ] ---> AU_ H s t ---> Bot).
Proof.
  move => H0 H1.
  set u := ~~: t :/\: AX (AU_ H s t) :/\: EX (~~: AU_ (C |` H) s t).
  do 2 Intro. Have u.
  Have (~~: t);[by ApplyH H0 | Intro].
  Have ((s :/\: hist H) :/\: AX (AU_ H s t)).
    Rev* 1. rewrite -> axAUHu at 1.
    rewrite /Or. Intro. Apply.
    Intro. Apply* 2. by ApplyH (axAEl t (hist H)).
    do 2 ApplyH axAcase. do 3 Intro. ApplyH axAI. ApplyH axAI. ApplyH H1.
  suff S : prv (u ---> EX u).
    have E: prv (u ---> EG (~~: t)). apply rER_ind_weak => //. exact: axAEl.
    Rev. drop. rewrite /AU_. rewrite -> E, -> axAUAw. exact: axAUEGF.
  rule axAcase. Intro. ApplyH axAcase; do 2 Intro.
  Have (EX ((~~: AU_(C |` H) s t) :/\: AU_ H s t)). by ApplyH axDBD.
  drop. apply: rEXn. rule axAcase. swap; Intro.
  rewrite -> dmAUH at 1. rewrite -> histU, dmA, axDN.
  ApplyH axAcase. Intro.
  Have (hist H). ApplyH (axAUAEr s t (hist H)). Intro.
  Have (~~: t); last Intro.
    Rev* 1. ApplyH axOE; first by drop. ApplyH axOE; first by drop.
    do 2 Intro. by Apply* 1.
  Have (s :/\: AX (AU_ H s t)); last (ApplyH axAcase; do 3 Intro).
    rewrite <- (axAEl s (hist H)) at 2.
    ApplyH axAUHu. ApplyH axAcase. do 2 Intro. Apply* 2.
  ApplyH axAI. ApplyH axAI. Rev. ApplyH axOE; last by drop.
  ApplyH axOE; last ApplyH axOE; Intro.
  - rewrite <- (axBE (EX _)). Apply.
  - ApplyH H1.
  - rewrite <- (axBE (EX _)). Apply.
Qed.

Definition EU_ H s t := EU (s :/\: hist H) (t :/\: hist H).

Lemma ARH_sound (s t : form) (C : clause) H :
  prv (t ---> ~~: [af C ]) -> prv (EX (EU_ (C |` H) s t) ---> s ---> ~~: [af C ]) ->
  prv ([af C ] ---> EU_ H s t ---> fF).
Proof.
  move => H1 H2.
  Suff (EU_ H s t ---> ~~: [af C] :/\: EU_ (C |` H) s t).
    do 3 Intro. Rev* 2. ApplyH (axAEl (~~: [af C]) (EU_ (C |` H) s t)). Apply* 1.
  drop. apply: EU_ind.
  - rewrite /EU_. rewrite <- H1. rule axAcase. do 2 Intro. ApplyH axAI.
    ApplyH axEUI. ApplyH axAI. rewrite -> histU, <- H1. by ApplyH axAI.
  - rule axAcase. do 3 Intro.
    Have (EX (EU_ (C |` H) s t)); last Intro.
      Rev; drop. rewrite -> axAC. exact: axEXAEl.
    Have (~~: [af C]); [ApplyH H2| Intro].
    ApplyH axAI. rewrite {3}/EU_. rewrite -> axEUeq. rewrite -/(EU_ _ _ _).
    ApplyH axOIr. do 2 ApplyH axAI. rewrite -> histU. by ApplyH axAI.
Qed.

Translation Theorem

Lemma hilbert_soundness A : tab A -> prv ([af A .1 ] ---> interp_a A .2 ---> Bot).
Proof.
  elim => {A} /=.
  - move => C E. rewrite -> andU, afp1. rule axAcase. exact: axBE.
  - move => p C E. rewrite -> andU,andU,afp1,afn1.
    rule axAcase. Intro. ApplyH axAcase; do 3 Intro. Apply* 2.
  - move => s t C E _ IHs _ IHt. rewrite -> andU, afp1. rule axAcase.
    Intro. Have (~~: s :\/: t). ApplyH axIO. drop. rule axOE.
    + rewrite <- IHs. rewrite -> andU,af1n. exact: axAI.
    + rewrite <- IHt. rewrite -> andU. rewrite -> af1p at 1. exact: axAI.
  - move => s t C R _ IH. rewrite <- IH. do ! rewrite -> andU. rewrite -> afn1, <- af1p, <- af1n.
    rewrite -> dmI, axAA. exact: axI.
  - move => s C E _ IH.
    rewrite -> andU,afn1. rewrite -> box_request, annot_request.
    rewrite <- (axDN s); rewrite -/(EX (~~: s)). rule axAcase. do 3 Intro.
    Have (EX ( ~~: s :/\: (interp_a (aR E) :/\: [af R C]))). ApplyH axDBD. ApplyH axABBA. by ApplyH axAI.
    drop. rewrite <- axDF. apply: rEXn. rule axAcase. Intro. ApplyH axAcase; do 2 Intro.
    ApplyH IH. rewrite -> andU, <- af1n. ApplyH axAI.
  - move => s t C E _ IH1 _ IH2.
    rewrite -> andU, afp1, axAUu. rewrite -> axADr. rule axOE.
    + by rewrite -> af1p, <- andU.
    + rewrite -> (af1p s) at 1. rewrite -> (af1p (AX _)). do 2 rewrite <- andU.
      by rewrite -fsetUA.
  - move => s t C R _ IH1 _ IH2.
    rewrite -> andU,afn1. rewrite -> axAC. rule axAcase. Intro.
    rewrite -> dmAU, axERu. ApplyH axAcase; Intro. ApplyH axOE; Intro.
    - ApplyH IH1. do ! rewrite -> andU. do ! rewrite <- af1n. do ! ApplyH axAI.
    - ApplyH IH2. do ! rewrite -> andU. do ! rewrite <- af1n. ApplyH axAI. ApplyH axAI.
      Rev. drop. do 2 Intro.
      Have (EX (ER (~~: s) (~~: t) :/\: fAU s t)). by ApplyH axDBD.
      drop. rewrite -> axAC, axAUERF. exact: axDF.
  - move => s t C _ IH. rewrite -> andU, afp1.
    do ! rewrite <- hist0 in IH. rule axAcase. do 3 Intro. by ApplyH IH.
  - move => s t H C _ IH1 _ IH2.
    apply: AUH_sound.
    + do 2 Intro. ApplyH IH1. rewrite -> andU, <- af1p. by ApplyH axAI. exact: axsT.
    + do 2 Intro. rewrite /EX /AU_. rewrite -> axDN. ApplyH IH2. rewrite -> andU, <- af1p. by ApplyH axAI.
  - move => s t H C.
    rewrite -> axAUAEr, histU. rewrite -> axAEl. do 2 Intro. Apply.
  - move => C E _ IH.
    rewrite -> box_request, annot_request. do 2 Intro.
    Have (~~: fAX fF). ApplyH ax_serial. rewrite <- (axDN fF) at 1; rewrite -/(EX Top). Intro.
    Have (EX ( Top :/\: (interp_a (aR E) :/\: [af R C]))). ApplyH axDBD. ApplyH axABBA. by ApplyH axAI.
    drop. rewrite <- axDF. apply: rEXn. rule axAcase. drop. rule axAcase; do 2 Intro.
    Rev* 1. Rev. done.
  - move => s t C E _ IH1 _ IH2.
    rewrite -> andU,afp1. rewrite -> axAReq. do 2 rule axAcase. rule axC. rule axOE.
    + do 3 Intro. ApplyH IH1. do 2 rewrite -> andU. do 2 rewrite <- af1p. by do 2 ApplyH axAI.
    + do 3 Intro. ApplyH IH2. do 2 rewrite -> andU. do 2 rewrite <- af1p. by do 2 ApplyH axAI.
  - move => s t C E _ IH1 _ IH2.
    rewrite -> andU,afn1. rewrite -> dmAR. rewrite -> axEUeq. rule axAcase. rule axOE.
    + do 3 Intro. ApplyH IH1. rewrite -> andU. rewrite <- af1n. by ApplyH axAI.
    + rule axAcase. do 3 Intro. ApplyH IH2. do 2 rewrite -> andU. do 2 rewrite <- af1n.
      rewrite -> dmAX. rewrite -> dmAR. by do 2 ApplyH axAI.
  - move => s t C _ IH. rewrite -> andU,afn1,dmAR. rule axAcase. do 3 Intro.
    do 2 rewrite <- hist0 in IH. by ApplyH IH.
  - move => s t H C _ IH1 _ IH2. apply: ARH_sound.
    - rewrite -> andU in IH1. do 2 Intro. ApplyH IH1; last by drop; exact: axI.
      rewrite <- af1n. by ApplyH axAI.
    - do 3 Intro. ApplyH IH2. rewrite -> andU. rewrite <- af1n. by ApplyH axAI.
  - move => s t H C.
    rewrite -> axEUEr. rewrite -> histU,axAEl. exact: axContra.
  - move => s t H C _ IH. rewrite -> box_request. do 2 Intro.
    Suff (EX fF). drop. Intro. Apply. drop. exact: axBT.
    Suff (EX ([af R C] :/\: EU (~~: s :/\: hist H) (~~: t :/\: hist H))).
      drop. apply: rEXn. by rule axAcase.
    rewrite <- (axAC _ [af R C]). ApplyH axDBD.
Qed.

Lemma plain_soundness C : tab (C ,aVoid ) -> prv (~~: [af C ]).
Proof. move/hilbert_soundness => /= H. Intro. ApplyH H. by drop. Qed.