Require Import Sorensen.
Require Import Gentzen.
Section DialogFragment.
Context {Sigma : Signature}.
Context {HdF : eq_dec Funcs} {HdP : 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)
| AAll phi : term -> 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'; [discriminate | | 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'; [discriminate | 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
| DAll phi t : defense_form (AAll phi t) (phi[t .: ids]).
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 sprv_Dprv A phi psi :
sprv expl A phi psi -> forall rho, Dprv form_rules (List.map (subst_form rho) (phi o:: A)) (fun chi => chi = psi [rho]).
Proof.
induction 1; intros rho; cbn in *; asimpl in *.
- apply (Dprv_weak (IHsprv rho)). intros x []; subst; intuition (now apply in_map). tauto.
- apply (@Def _ _ _ _ (phi[rho] --> psi[rho])). reflexivity.
firstorder. intros adm atk. apply (attack_form_inv_impl atk).
apply (Dprv_weak (IHsprv rho)); intuition. subst. apply DImpl.
- 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 (IHsprv (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).
now asimpl.
- apply Dprv_exp with (T := @defense _ form_rules ⊥ None ABot).
eapply (Dprv_defend (IHsprv rho)) with (adm := None). tauto. intros ?; inversion 1.
- apply (@Dprv_ax _ form_rules _ _ _ (phi [rho]) sf_well_founded sf_form_rules); intuition.
- refine (@Dprv_just _ _ _ _ _ (phi [rho]) (Dprv_weak (IHsprv1 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 (IHsprv2 rho)). 2: tauto. firstorder.
+ now intros ? [= <-].
+ intros ? [= <-] adm atk. refine (Dprv_weak (Dprv_defend (IHsprv1 rho) _ atk) _ _).
tauto. destruct adm; cbn; firstorder. tauto.
- 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 (IHsprv rho)); asimpl in *; firstorder.
Qed.
Lemma ND_defend A phi :
(forall adm (atk : attack phi adm), (exists psi, defense atk psi /\ (adm o:: A) ⊢IE psi) \/ forall phi, (adm o:: A) ⊢IE phi) ->
justified _ A phi -> A ⊢IE phi.
Proof.
destruct phi; intros Hatk Hjust.
- destruct (Hatk None ABot) as [(phi & Hdef & _) | Hprv]; [inversion Hdef | apply Hprv].
- ctx. now apply Hjust.
- destruct (Hatk (Some phi1) (AImpl phi1 phi2)) as [(psi & Hdef & Hprv) | Hprv];
try inversion Hdef; subst; apply II, Hprv.
- ointros. destruct (find_unused_L (phi :: A)) as [x Hx]. apply (@nameless_equiv _ intu expl A phi x).
+ intros psi Hel. apply (Hx x (le_n x)). now right.
+ apply (Hx (S x)). omega. now left.
+ destruct (Hatk None (AAll phi (var_term x))) as [(psi & Hdef & Hprv) | Hprv].
try inversion Hdef; subst; apply Hprv. apply Hprv.
Qed.
Lemma Dprv_ND A T :
Dprv form_rules A T -> (exists phi, T phi /\ A ⊢IE phi) \/ forall phi, A ⊢IE phi.
Proof.
induction 1.
- left; exists phi; split; [assumption |]. now apply ND_defend.
- destruct psi; inversion atk; subst.
+ right. intros phi. oexfalso. now ctx.
+ specialize (H4 psi1 eq_refl). specialize (H2 psi1 eq_refl). assert (A ⊢IE psi1) by now apply ND_defend.
revert H1. apply (attack_form_inv_impl atk). intros IH.
destruct (IH psi2 (DImpl psi1 psi2)) as [(phi & HT & Hprv) | Hprv].
* left; exists phi; split; [exact HT |]. oassert psi2. eapply IE. ctx. assumption. assumption.
* right. intros phi. oassert psi2. eapply IE. ctx. assumption. apply Hprv.
+ revert H1. apply (attack_form_inv_all atk). intros t IH.
destruct (IH (psi [t .: ids]) (DAll psi t)) as [(phi & HT & Hprv) | Hprv]; [left | right].
* exists phi; split; [exact HT |]. oassert (psi [t..]). apply (AllE t). now ctx. assumption.
* intros phi. oassert (psi [t..]). apply (AllE t). now ctx. apply Hprv.
Qed.
End DialogFragment.