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.
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 ^+]]).

Lemma afp1 s : prv ([af [fset s ^+]] ---> s).

Lemma af1n s : prv (Neg s ---> [af [fset s ^-]]).

Lemma afn1 s : prv ([af [fset s ^-]] ---> Neg s).

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).

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))).

Lemma dmAUH s t H :
  mprv (~~: AU_ H s t ---> (~~: t :\/: ~~: hist H ) :/\: ((~~: s :\/: ~~: hist H ) :\/: EX (~~: AU_ H s t))).

Lemma box_request (C : clause) : prv ([af C ] ---> AX [af R C ]).

Lemma annot_request E : prv (interp_a E ---> AX (interp_a (aR E))).

Lemma hist0 s : prv (s ---> s :/\: hist fset0).

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).

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).