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 dags.
Require Import CTL_def tab_def tab_dec modular_hilbert tab_translation demo tab_complete.

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

Theorem cert_dec_method (s : form) : {(exists (M:model) (w:M), finite M /\ eval s w)} + { prv (Neg s) }.
Proof.
  case (tab_dec ([fset s^+],aVoid)).
  - move/plain_soundness => H. right. by rewrite <- af1p in H.
  - move/tab_plain_complete => H. left. move: H => [M] [w] [H1 H2]. exists M; exists w.
    rewrite -[s]/(interp (s^+)). split => //. apply: H2. by rewrite fset11.
Qed.

Corollary decidability s : decidable (exists (M:model) (w:M), eval s w).
Proof.
  case (cert_dec_method s) => [H|].
  - left. move: H => [M] [w] [? ?]. by do 2 eexists.
  - move/soundness => H. right. move => [M] [w]. exact: H.
Qed.

Corollary completeness s : (forall (M:model) (w:M), eval s w) -> prv s.
Proof.
  move => valid_s. case (cert_dec_method (Neg s)); last by rule axDN.
  move => [M] [w] [_]. by move: (valid_s M w) => /=.
Qed.

Lemma disjointness s : ~ ((exists (M:model) (w:M), eval (Neg s) w) /\ prv s).
Proof. move => [ /= [M] [w] Hw /soundness H]. by auto. Qed.

Print Assumptions cert_dec_method.