testfree-PDL.hilbert_ref
(* (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).
(* 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.