Require Export DecidableEnumerable.
From Equations Require Import Equations.
Ltac resolve_existT :=
match goal with
| [ H2 : existT _ _ _ = existT _ _ _ |- _ ] => rewrite (inj_pair2 _ _ _ _ _ H2) in *
| _ => idtac
end.
Ltac inv H :=
inversion H; subst; repeat (progress resolve_existT).
Definition ocons X (o : option X) A :=
match o with
| Some a => a :: A
| None => A
end.
Infix "o::" := ocons (at level 55).
Lemma ocons_sub X (a : option X) A B :
A <<= B -> a o:: A <<= a o:: B.
Proof.
intros H. destruct a; cbn.
- intros y []; subst; intuition.
- assumption.
Qed.
Class rule_set (f : Type) :=
{
atomic : f -> Type ;
attack : f -> option f -> Type ;
defense : forall phi adm, attack phi adm -> f -> Type ;
dec_f : eq_dec f
}.
Definition opred X (p : X -> Type) (o : option X) : Type :=
forall x, o = Some x -> p x.
Section SDialogues.
Variable f : Type.
Variable R : rule_set f.
Definition justified A phi := atomic phi -> phi el A.
Lemma justified_weak A B phi :
justified A phi -> A <<= B -> justified B phi.
Proof.
intros Hjust Hsub Hin. intuition.
Qed.
Inductive Dprv (A : list f) (T : f -> Type): Type :=
Def phi :
T phi ->
justified A phi ->
(forall adm (atk : attack phi adm), Dprv (adm o:: A) (defense atk)) ->
Dprv A T
| Att psi adm (atk : attack psi adm) :
psi el A ->
(forall chi, defense atk chi -> Dprv (chi :: A) T) ->
opred (fun a => justified A a) adm ->
opred (fun a => forall adm' (atk' : attack a adm'), Dprv (adm' o:: A) (defense atk')) adm ->
Dprv A T.
Notation "A '⊢D' T" := (Dprv A T) (at level 30).
Inductive challenge : Type :=
C phi adm : attack phi adm -> challenge.
Inductive opening phi : list f -> challenge -> Type :=
OP (H : justified nil phi) adm (atk : attack phi adm) : opening phi (adm o:: nil) (C atk).
Definition deferred : Type := challenge * challenge.
Definition sstate : Type := list f * list f * list deferred.
Inductive spmove : sstate -> challenge -> sstate -> Type :=
| SPAtk pA oA ds c phi adm (atk : attack phi adm) :
phi el oA -> opred (justified oA) adm -> spmove (pA, oA, ds) c (adm o:: pA, oA, (C atk, c) :: ds)
| SPDef pA oA ds phi adm (atk : attack phi adm) psi :
defense atk psi -> justified oA psi -> spmove (pA, oA, ds) (C atk) (psi :: pA, oA, ds).
Inductive somove : sstate -> sstate -> challenge -> Type :=
| SODef pA oA ds c phi adm (atk : attack phi adm) psi :
defense atk psi -> somove (pA, oA, (C atk, c) :: ds) (pA, psi :: oA, ds) c
| SOAtk pA phi pA' oA ds adm (atk : attack phi adm) :
somove (pA ++ phi :: pA', oA, ds) (pA ++ pA', adm o:: oA, ds) (C atk).
Inductive swin_strat s c : Type :=
SWS s' : spmove s c s' -> (forall s'' c', somove s' s'' c' -> swin_strat s'' c') -> swin_strat s c.
Definition svalid phi :=
prod (justified nil phi) (forall A c, opening phi A c -> swin_strat (nil, A, nil) c).
Variable ord : Type.
Variable (olt : ord -> ord -> Type) (oplus : ord -> ord -> ord) (osuc : ord -> ord)
(osup : (nat -> ord) -> ord) (ozero : ord).
Variable enum_att : forall phi, nat -> option (sigT (attack phi)).
Variable enum_def : forall phi adm (atk : attack phi adm), nat -> option (sigT (defense atk)).
Definition subctx A (p : list f -> Type) :=
sigT (fun B => Datatypes.prod (B <<= A) (p B)).
Definition subctx_lift A B p :
A <<= B -> subctx A p -> subctx B p.
Proof.
intros Hsub (C & HsubC & HC). exists C. split; [| apply HC]. firstorder.
Defined.
Definition counter_safe A phi :=
subctx A (fun B => (forall adm (atk : attack phi adm), (adm o:: B) ⊢D defense atk)).
Definition continuation A (d : deferred) :=
match d with
(C atk, C atk') => subctx A (fun B => forall phi, defense atk phi -> (phi :: B) ⊢D defense atk')
end.
Definition plan A c :=
match c with C atk => subctx A (fun B => B ⊢D defense atk) end.
Definition counter_safe_lift A B :
A <<= B -> forall phi, counter_safe A phi -> counter_safe B phi.
Proof.
intros. apply (subctx_lift H X).
Defined.
Definition continuation_lift A B :
A <<= B -> forall d, continuation A d -> continuation B d.
Proof.
intros H [[] []]. apply (subctx_lift H).
Defined.
Definition plan_lift A B :
A <<= B -> forall c, plan A c -> plan B c.
Proof.
intros H []. apply (subctx_lift H).
Defined.
Inductive IVec X (p : X -> Type) : list X -> Type :=
| vNil : IVec p []
| vCons a (H : p a) A : IVec p A -> IVec p (a :: A).
Fixpoint osum X (p : X -> Type) A (v : IVec p A) (f : forall x, p x -> ord) : ord :=
match v with
| vNil _ => ozero
| vCons Ha vA => osuc (oplus (f _ Ha) (osum vA f))
end.
Fixpoint vmap X (p q : X -> Type) (f : forall x, p x -> q x) A (v : IVec p A) : IVec q A :=
match v with
| vNil _ => vNil _
| vCons Ha vA => vCons (f _ Ha) (vmap f vA)
end.
Definition vix X (p : X -> Type) A x B (v : IVec p (A ++ x :: B)) :
p x * IVec p (A ++ B).
Proof.
induction A; depelim v.
- easy.
- destruct (IHA v). eauto using IVec.
Qed.
Inductive Dprv_state : Type :=
| DS oA pA D c : IVec (counter_safe oA) pA -> IVec (continuation oA) D -> plan oA c -> Dprv_state.
Fixpoint Dprv_size (A : list f) (T : f -> Type) (H : Dprv A T) : ord :=
match H with
@Def _ _ phi HT Hjust Hc =>
osuc (osup (fun n => match @enum_att phi n with
Some (existT _ adm atk) => Dprv_size (Hc adm atk)
| None => ozero
end))
| @Att _ _ psi adm atk Hin Hcont Hajust Hadef =>
osuc (oplus (osup (fun n => match @enum_def psi adm atk n with
Some (existT _ chi Hdef) => Dprv_size (Hcont chi Hdef)
| None => ozero
end))
(match adm with
Some phi => fun Hadef' =>
osup (fun n => match @enum_att phi n with
Some (existT _ adm' atk') => Dprv_size (Hadef' phi eq_refl adm' atk')
| None => ozero
end)
| None => fun _ => ozero
end Hadef))
end.
Definition Dprv_state_size (H : Dprv_state) : ord :=
match H with
@DS oA pA D c cs ct pln =>
oplus
(osum cs (fun phi HB => match HB with | existT _ B (_, Hphi) =>
osup (fun n => match @enum_att phi n with
| Some (existT _ adm atk) => Dprv_size (Hphi adm atk)
| None => ozero
end)
end
))
(oplus
(osum ct (fun d => match d with (C atk, C _) =>
fun HB => match HB with existT _ B (_, Hd) =>
osup (fun n => match enum_def atk n with
| Some (existT _ phi Hdef) => Dprv_size (Hd phi Hdef)
| None => ozero
end)
end
end))
(match c return plan oA c -> ord with
C atk => fun HB => match HB with existT _ B (_, pln') => Dprv_size pln' end
end pln))
end.
Hypothesis ord_ind : forall X (p : X -> Type) (f : X -> ord),
(forall x, (forall y, olt (f y) (f x) -> p y) -> p x) -> forall x, p x.
Lemma s_sound (s : Dprv_state) :
match s with @DS oA pA D c _ _ _ => swin_strat (pA, oA, D) c end.
Proof.
apply ord_ind with (f := Dprv_state_size) (x := s). clear s.
intros [oA pA ds c cs ct pln] IH. destruct c. destruct pln as (oA' & Hsub & prv).
inversion prv.
- eapply SWS. 1: exact (SPDef pA ds X (justified_weak H Hsub)). intros s'' c omv.
inversion omv; subst.
+ depelim ct. destruct c. destruct H as (oA'' & Hsub' & prv'). cbn in ct.
assert (Hc : counter_safe (psi :: oA) phi0) by (exists oA'; intuition).
assert (Hp : plan (psi :: oA) (C a0)).
1: exists (psi :: oA''); split; [| apply (prv' psi X1)]; now apply incl_shift.
assert (Hsub'' : oA <<= psi :: oA) by intuition.
apply (IH (DS (vCons Hc (vmap (counter_safe_lift Hsub'') cs))
(vmap (continuation_lift Hsub'') ct)
Hp)).
shelve.
+ assert (Hsub' : oA <<= adm0 o:: oA) by (destruct adm0; cbn; intuition).
destruct pA0; cbn in H1; injection H1; intros <- ->.
* assert (Hp : plan (adm0 o:: oA) (C atk)).
1: exists (adm0 o:: oA'); split; [| apply (X0 adm0 atk)]; destruct adm0; now try (apply incl_shift).
apply (IH (DS (vmap (counter_safe_lift Hsub') cs)
(vmap (continuation_lift Hsub') ct)
Hp)).
shelve.
* destruct (vix cs). destruct c as (oA'' & Hsub'' & Hphi1).
assert (Hc : counter_safe (adm0 o:: oA) phi0) by (exists oA'; destruct adm0; cbn; intuition).
assert (Hp : plan (adm0 o:: oA) (C atk)).
1: exists (adm0 o:: oA''); split; [| apply (Hphi1 adm0 atk)]; destruct adm0; now try (apply incl_shift).
apply (IH (DS (vCons Hc (vmap (counter_safe_lift Hsub') i))
(vmap (continuation_lift Hsub') ct)
Hp)).
shelve.
- assert (H' : psi el oA) by intuition. assert (X0' : opred (fun a => justified oA a) adm0).
1: destruct adm0; unfold opred; eauto using justified_weak. eapply SWS.
1: exact (SPAtk pA ds (C a) atk H' X0'). intros s'' c' omv. inv omv.
+ apply inj_pair2 in H5; resolve_existT.
assert (Hp : plan (psi0 :: oA) (C a)) by (exists oA'; cbn; intuition).
assert (Hsub'' : oA <<= psi0 :: oA) by intuition.
destruct adm0 as [tau |].
* assert (Hc : counter_safe (psi0 :: oA) tau) by (exists oA'; intuition).
apply (IH (DS (vCons Hc (vmap (counter_safe_lift Hsub'') cs))
(vmap (continuation_lift Hsub'') ct)
Hp)).
shelve.
* apply (IH (DS (vmap (counter_safe_lift Hsub'') cs)
(vmap (continuation_lift Hsub'') ct)
Hp)).
shelve.
+ assert (Hc : continuation (adm1 o:: oA) (C atk, C a)) by (exists oA'; destruct adm1; cbn; intuition).
assert (Hsub' : oA <<= adm1 o:: oA) by (destruct adm1; cbn; intuition).
destruct adm0 as [tau |].
* destruct pA0; cbn in H1; injection H1; intros <- ->.
-- assert (Hp : plan (adm1 o:: oA) (C atk0)). 1: exists (adm1 o:: oA').
1: split; [| apply (X1 tau eq_refl adm1 atk0)]; destruct adm1; now try (apply incl_shift).
apply (IH (DS (vmap (counter_safe_lift Hsub') cs)
(vCons Hc (vmap (continuation_lift Hsub') ct))
Hp)).
shelve.
-- destruct (vix cs) as [(oA'' & Hsub'' & Hphi0) cs'].
assert (Hc' : counter_safe (adm1 o:: oA) tau) by (exists oA'; destruct adm1; cbn; intuition).
assert (Hp : plan (adm1 o:: oA) (C atk0)).
1: exists (adm1 o:: oA''); split; [| apply (Hphi0 adm1 atk0)]; destruct adm1; now try (apply incl_shift).
apply (IH (DS (vCons Hc' (vmap (counter_safe_lift Hsub') cs'))
(vCons Hc (vmap (continuation_lift Hsub') ct))
Hp)).
shelve.
* cbn in H1; subst. destruct (vix cs) as [(oA'' & Hsub'' & Hphi0) cs'].
assert (Hp : plan (adm1 o:: oA) (C atk0)).
1: exists (adm1 o:: oA''); split; [| apply (Hphi0 adm1 atk0)]; destruct adm1; now try (apply incl_shift).
apply (IH (DS (vmap (counter_safe_lift Hsub') cs')
(vCons Hc (vmap (continuation_lift Hsub') ct))
Hp)).
shelve.
Admitted.
End SDialogues.