From Undecidability.FOLC Require Export Sorensen.
From Undecidability.FOLC Require Export FullSequent.
Section DialogFull.
Context {Sigma : Signature}.
Hypothesis eq_dec_Funcs : eq_dec Funcs.
Hypothesis eq_dec_Preds : eq_dec Preds.
Definition atomic_form (phi : form) : Prop :=
match phi with
| Pred _ _ => True
| _ => False
end.
Lemma atomic_dec phi :
atomic_form phi \/ ~ atomic_form phi.
Proof.
destruct phi; cbn; intuition.
Qed.
Inductive attack_form : form -> option form -> Type :=
| ABot : attack_form ⊥ None
| AImpl phi psi : attack_form (phi --> psi) (Some phi)
| AAnd phi psi : bool -> attack_form (phi ∧ psi) None
| AOr phi psi : attack_form (phi ∨ psi) None
| AAll phi : term -> attack_form (∀ phi) None
| AExt phi : attack_form (∃ phi) None.
Lemma attack_form_inv_impl phi psi adm (atk : attack_form (phi --> psi) adm)
(P : forall chi adm, attack_form chi adm -> Type) :
P (phi --> psi) (Some phi) (AImpl phi psi) -> P (phi --> psi) adm atk.
Proof.
enough (H : forall chi adm (atk : attack_form chi adm),
chi = (phi --> psi) -> P (phi --> psi) (Some phi) (AImpl phi psi) -> P chi adm atk)
by now apply (H (phi --> psi) adm atk).
intros chi adm' atk' Hchi Hadm. destruct atk'; try discriminate. injection Hchi. now intros -> ->.
Qed.
Lemma attack_form_inv_and phi psi adm (atk : attack_form (phi ∧ psi) adm)
(P : forall chi adm, attack_form chi adm -> Type) :
(forall l, P (phi ∧ psi) None (AAnd phi psi l)) -> P (phi ∧ psi) adm atk.
Proof.
enough (H : forall chi adm (atk : attack_form chi adm),
chi = (phi ∧ psi) -> (forall l, P (phi ∧ psi) None (AAnd phi psi l)) -> P chi adm atk)
by now apply (H (phi ∧ psi) adm atk).
intros chi adm' atk' Hchi Hadm. destruct atk'; try discriminate. injection Hchi. now intros -> ->.
Qed.
Lemma attack_form_inv_or phi psi adm (atk : attack_form (phi ∨ psi) adm)
(P : forall chi adm, attack_form chi adm -> Type) :
P (phi ∨ psi) None (AOr phi psi) -> P (phi ∨ psi) adm atk.
Proof.
enough (H : forall chi adm (atk : attack_form chi adm),
chi = (phi ∨ psi) -> P (phi ∨ psi) None (AOr phi psi) -> P chi adm atk)
by now apply (H (phi ∨ psi) adm atk).
intros chi adm' atk' Hchi Hadm. destruct atk'; try discriminate. injection Hchi. now intros -> ->.
Qed.
Lemma attack_form_inv_all phi adm (atk : attack_form (∀ phi) adm) (P : forall chi adm, attack_form chi adm -> Type) :
(forall t, P (∀ phi) None (AAll phi t)) -> P (∀ phi) adm atk.
Proof.
enough (H : forall chi adm (atk : attack_form chi adm),
chi = ∀ phi -> (forall t, P (∀ phi) None (AAll phi t)) -> P chi adm atk)
by now apply (H (∀ phi) adm atk).
intros chi adm' atk' Hchi Hadm. destruct atk'; try discriminate. injection Hchi. now intros ->.
Qed.
Lemma attack_form_inv_ext phi adm (atk : attack_form (∃ phi) adm)
(P : forall chi adm, attack_form chi adm -> Type) :
P (∃ phi) None (AExt phi) -> P (∃ phi) adm atk.
Proof.
enough (H : forall chi adm (atk : attack_form chi adm),
chi = (∃ phi) -> P (∃ phi) None (AExt phi) -> P chi adm atk)
by now apply (H (∃ phi) adm atk).
intros chi adm' atk' Hchi Hadm. destruct atk'; try discriminate. injection Hchi. now intros ->.
Qed.
Inductive defense_form : forall phi adm, attack_form phi adm -> form -> Prop :=
| DImpl phi psi : defense_form (AImpl phi psi) psi
| DAndL phi psi : defense_form (AAnd phi psi true) phi
| DAndR phi psi : defense_form (AAnd phi psi false) psi
| DOrL phi psi : defense_form (AOr phi psi) phi
| DOrR phi psi : defense_form (AOr phi psi) psi
| DAll phi t : defense_form (AAll phi t) (phi[t .: ids])
| DExt phi t : defense_form (AExt phi) (phi [t .: ids]).
Hint Constructors defense_form.
Instance form_rules : rule_set form :=
{| atomic := atomic_form ; attack := attack_form ; defense := defense_form ; dec_f := dec_form _ _ |}.
Lemma sf_form_rules phi adm (atk : attack phi adm) :
opred (fun a => sf a phi) adm /\ forall chi, defense atk chi -> sf chi phi.
Proof.
destruct atk; cbn; split; try discriminate; try (intros ?; inversion 1; constructor).
Qed.
Lemma eq_incl X (A B : list X) :
A = B -> A <<= B.
Proof.
intros ->; intuition.
Qed.
Lemma fprv_Dprv A phi :
A ⊢f phi -> forall rho, [psi[rho] | psi ∈ A] ⊢D (fun psi => psi = phi[rho]).
Proof.
induction 1; intros rho; cbn in *; asimpl in *.
- apply Dprv_ax with (phi := phi[rho]) (Q := sf). apply sf_well_founded. apply sf_form_rules. all: intuition.
- apply (Dprv_weak (IHfprv rho)). all: intuition.
- apply (Dprv_weak (IHfprv rho)). all: intuition.
- apply (Dprv_weak (IHfprv rho)). 2: tauto. repeat (rewrite map_app; cbn).
intros a [? | [-> | [-> | ?]]] % in_app_or; apply in_or_app. all: eauto.
- apply Dprv_exp with (T := @defense _ form_rules ⊥ None ABot).
eapply (Dprv_defend (IHfprv rho)) with (adm := None). tauto. intros ?; inversion 1.
- refine (@Dprv_just _ _ _ _ _ (phi [rho]) (Dprv_weak (IHfprv1 rho) _ (fun a H => H)) _ _);
[intuition | intuition |]. intros B Hsub Hjust.
apply (@Att _ form_rules _ _ (phi[rho] --> psi[rho]) (Some phi[rho]) (AImpl phi[rho] psi[rho]));
[intuition | | |].
+ intros chi'. inversion 1; subst. apply (Dprv_weak (IHfprv2 rho)). 2: tauto. firstorder.
+ now intros ? [= <-].
+ intros ? [= <-] adm atk. refine (Dprv_weak (Dprv_defend (IHfprv1 rho) _ atk) _ _).
tauto. destruct adm; cbn; firstorder. tauto.
- apply (@Def _ _ _ _ (phi[rho] --> psi[rho])). reflexivity.
firstorder. intros adm atk. apply (attack_form_inv_impl atk).
apply (Dprv_weak (IHfprv rho)); intuition. subst. apply DImpl.
- apply Att with (atk := AAnd phi[rho] psi[rho] true); [intuition | | discriminate | discriminate].
intros ?. inversion 1; subst.
apply Att with (atk := AAnd phi[rho] psi[rho] false); [intuition | | discriminate | discriminate].
intros ?. inversion 1; subst. apply (Dprv_weak (IHfprv rho)); firstorder.
- apply Def with (phi := phi[rho] ∧ psi[rho]). reflexivity. inversion 1.
intros ? atk. apply (attack_form_inv_and atk); intros []; cbn.
+ apply (Dprv_weak (IHfprv1 rho)). intuition. intros ? ->. constructor.
+ apply (Dprv_weak (IHfprv2 rho)). intuition. intros ? ->. constructor.
- apply Att with (atk := AOr phi[rho] psi[rho]); [intuition | | discriminate | discriminate].
intros chi'; inversion 1; subst.
+ apply (Dprv_weak (IHfprv1 rho)). intuition. intros ? ->. constructor.
+ apply (Dprv_weak (IHfprv2 rho)). intuition. intros ? ->. constructor.
- apply Def with (phi := phi[rho] ∨ psi[rho]). reflexivity. inversion 1.
intros ? atk. apply (attack_form_inv_or atk); subst; cbn. apply (Dprv_weak (IHfprv rho)).
reflexivity. intros ? ->; constructor.
- apply Def with (phi := phi[rho] ∨ psi[rho]). reflexivity. inversion 1.
intros ? atk. apply (attack_form_inv_or atk); subst; cbn. apply (Dprv_weak (IHfprv rho)).
reflexivity. intros ? ->; constructor.
- apply (@Att _ form_rules _ _ _ None (AAll (phi [var_term O .: rho >> (subst_term form_shift)]) (t [rho])));
[intuition | | discriminate | discriminate].
intros chi Hdef; inversion Hdef; subst; apply (Dprv_weak (IHfprv rho)); asimpl in *.
+ intros ? [ <- | ].
* left. asimpl. erewrite ext_form. reflexivity.
intros []. now asimpl. asimpl. erewrite ext_term. now asimpl. intros []; now asimpl.
* right. now right.
+ firstorder.
- apply Def with (phi := ∀ (phi [var_term O .: rho >> (subst_term form_shift)])); [easy | firstorder |].
intros adm atk. apply (attack_form_inv_all atk). intros t; cbn; asimpl.
apply (Dprv_weak (IHfprv (t .: rho))).
+ rewrite map_map. apply eq_incl, map_ext. intros a. now asimpl.
+ intros ? ->. enough ((phi [var_term O .: rho >> (subst_term form_shift)]) [t .: ids] =
(subst_form (@scons term t rho) phi)) as <- by apply (DAll _ t).
asimpl. erewrite ext_form. reflexivity.
intros []. now asimpl. asimpl. erewrite ext_term. now asimpl. intros []; now asimpl.
- apply Att with (atk := AExt phi[var_term O .: rho >> (subst_term form_shift)]);
[intuition | | discriminate | discriminate].
intros ?; inversion 1; subst; asimpl. apply (Dprv_weak (IHfprv (t .: rho))).
+ assert (phi[t .: rho >> subst_term (↑ >> subst_term (t .: var_term))] = phi[t .: rho]).
asimpl.
erewrite ext_form. reflexivity.
intros []. now asimpl. asimpl. erewrite ext_term. now asimpl. intros []; now asimpl.
setoid_rewrite H1. clear H1.
apply incl_shift, incl_tl. rewrite map_map. apply eq_incl, map_ext. intros a; now asimpl.
+ intros ? ->. now asimpl.
- apply Def with (phi := ∃ phi[var_term O .: rho >> (subst_term form_shift)]); [easy | firstorder |].
intros ? atk. apply (attack_form_inv_ext atk). cbn. apply (Dprv_weak (IHfprv rho)).
reflexivity. intros ? ->. asimpl. enough ((phi [var_term O .: rho >> (subst_term form_shift)]) [t[rho] .: ids]
= (subst_form (@scons term (subst_term rho t) rho) phi)) as <- by apply (DExt _ t[rho]).
asimpl.
erewrite ext_form. reflexivity.
intros []. now asimpl. asimpl. erewrite ext_term. now asimpl. intros []; now asimpl.
Qed.
Hint Constructors fprv.
Ltac Hatk_inv H := apply H; intros ?; inversion 1; subst; cbn; intuition.
Lemma fprv_defend A phi :
(forall (adm : option form) (atk : attack phi adm) (phi0 : form),
(forall B psi, psi ∈ defense atk -> (adm o:: A) <<= B -> B ⊢f psi -> B ⊢f phi0) -> (adm o:: A) ⊢f phi0)
-> justified _ A phi
-> A ⊢f phi.
Proof.
destruct phi; intros Hatk Hjust.
- Hatk_inv (Hatk None ABot ⊥).
- apply (focus_el (Hjust I)), Ax.
- apply IR. Hatk_inv (Hatk (Some phi1) (AImpl phi1 phi2)).
- apply AR; [Hatk_inv (Hatk None (AAnd phi1 phi2 true)) | Hatk_inv (Hatk None (AAnd phi1 phi2 false))].
- Hatk_inv (Hatk (@None form) (AOr phi1 phi2)).
- destruct (find_unused_L (phi :: A)) as [x Hx]. apply AllR. cbn.
apply nameless_equiv with (n := x) (A0 := A). use_free Hx. use_free Hx.
Hatk_inv (Hatk None (AAll phi (var_term x))).
- Hatk_inv (Hatk None (AExt phi)). eauto.
Qed.
Ltac use_inv H0 H1 H2 H3 H4 H :=
revert H0 H1 H2 H3 H4; apply H; intros H0 H1 H2 H3 H4; cbn in *.
Lemma Dprv_fprv' A T :
A ⊢D T -> (forall phi, (forall B psi, psi ∈ T -> A <<= B -> B ⊢f psi -> B ⊢f phi) -> A ⊢f phi).
Proof with eauto.
induction 1.
- intros psi Hpsi. apply (Hpsi _ _ H). 1: auto. now apply fprv_defend.
- intros phi Hphi. destruct psi.
+ apply Exp, (focus_el H), Ax.
+ inversion atk.
+ use_inv H0 H1 H2 H3 H4 (attack_form_inv_impl atk). apply (focus_el H), IL.
* specialize (H4 psi1 eq_refl). specialize (H2 psi1 eq_refl). now apply fprv_defend.
* apply (H1 psi2 (DImpl psi1 psi2))...
+ use_inv H0 H1 H2 H3 H4 (attack_form_inv_and atk). intros H5. destruct H0.
* eapply (focus_el H), AL, weaken. 1: apply (H2 psi1 (DAndL psi1 psi2))... intuition.
* eapply (focus_el H), AL, weaken. 1: apply (H2 psi2 (DAndR psi1 psi2))... intuition.
+ use_inv H0 H1 H2 H3 H4 (attack_form_inv_or atk). apply (focus_el H), OL.
* apply (H1 psi1 (DOrL psi1 psi2))...
* apply (H1 psi2 (DOrR psi1 psi2))...
+ use_inv H0 H1 H2 H3 H4 (attack_form_inv_all atk). intros H5. rename H0 into t.
apply (focus_el H), (@AllL _ _ _ _ t), (H2 (psi[t..]) (DAll psi t))...
+ use_inv H0 H1 H2 H3 H4 (attack_form_inv_ext atk). destruct (find_unused_L (psi :: phi :: A)) as [x Hx].
apply (focus_el H), ExL, nameless_equiv' with (n := x) (A0 := A). use_free Hx. use_free Hx.
apply (H1 (psi[(var_term x)..]) (DExt psi (var_term x)))...
Qed.
Lemma Dprv_fprv A phi :
A ⊢D (fun psi => psi = phi) -> A ⊢f phi.
Proof.
intros H. apply (Dprv_fprv' H). now intros ? ? ->.
Qed.
Corollary Dprv_fprv_equiv A phi :
A ⊢D (fun psi => psi = phi) <-> A ⊢f phi.
Proof.
split. 1: apply Dprv_fprv. intros H. specialize (fprv_Dprv H var_term) as H'. asimpl in H'.
unfold id in H'. now rewrite map_id in H'.
Qed.
Corollary evalid_fprv_equiv phi :
evalid form_rules phi <-> [] ⊢f phi.
Proof.
rewrite eequiv. apply Dprv_fprv_equiv.
Qed.
End DialogFull.