ArgumentFrame.v

From mathcomp Require Export fintype finset ssrbool ssreflect.



Module Type FinTypeSig.
  Parameter T : finType.
End FinTypeSig.

Module Type ArgFrame (FTS : FinTypeSig).
  Import FTS.
  Record AF := mkAF {
    carrier : {set T};
    rel :> {set T * T};
    _ : rel \subset setX carrier carrier;
  }.
End ArgFrame.

Module Type ArgFrameSig (FTS : FinTypeSig) (AF : ArgFrame FTS).
  Import AF.
  Parameter R : AF.
End ArgFrameSig.



Module Type Syntacs (FTS : FinTypeSig ) (AF : ArgFrame FTS)(AFS : ArgFrameSig FTS AF).
  Import FTS AF AFS.
  Check R.

Definition attacks  (S : {set T}) (a : T) :=
  [exists x, (x \in S) && ((x,a) \in R)].

Lemma attacksP (S : {set T}) (a : T) :
  reflect (exists x, x \in S /\ (x,a) \in R) (attacks S a).
Proof.
  apply existsPP => x.
  apply andPP; apply idP.
Qed.


Definition cf  (S : {set T}) :=
  ~~ [exists a, [exists b, (a \in S) && ((b \in S) && ((a,b) \in R))]].

Lemma cfP (S : {set T}) :
  reflect (~ exists a b, a \in S /\ b \in S /\ (a,b) \in R)  (cf S).
Proof.
  apply negPP.
  apply existsPP => a.
  apply existsPP => b.
  apply andPP; [|apply andPP]; apply idP.
Qed.

Definition CF :=
  {S : {set T} | cf(S)}.

Definition deffend (S : {set T}) (a : T) :=
  [forall b, ((b,a) \in R) ==> attacks S b].

Lemma deffendP (S : {set T}) (a : T) :
  reflect (forall b,  (b,a) \in R -> exists x, x \in S /\ (x,b) \in R) (deffend S a).
Proof.
  apply forallPP => b.
  apply implyPP; try apply idP.
  apply existsPP => x.
  apply andPP; apply idP.
Qed.

Definition admissible S :=
  cf S && [forall a, (a \in S) ==> deffend S a].

Lemma admissibleP (S : {set T}) :
  reflect
    ((~ exists a b, a \in S /\ b \in S /\ (a,b) \in R) /\
     (forall a, a \in S -> forall b, (b,a) \in R -> exists x, x \in S /\ (x,b) \in R))
    (admissible S).
Proof.
  apply andPP.
  apply cfP.
  apply forallPP => a.
  apply implyPP; try apply idP.
  apply deffendP.
Qed.


Lemma deff_admi_cup S x :
  admissible S -> deffend S x -> admissible (x |: S).
Proof.
  move => /admissibleP [H1 H2].
  move => /deffendP H3.
  apply /admissibleP; split.
  {
    move => [a [b [/setUP Ha [/setUP Hb [Hab]]]]].
    case Ha, Hb.
    - move /set1P : H0 => F; subst.
      move /set1P : H => F; subst.
      move : (H3 x Hab) => [y [Hy yRx]].
      move : (H3 y yRx) => [z [Hz zRy]].
      apply H1; exists z, y; repeat split; auto.
    - move /set1P : H => F; subst.
      move : (H2 b H0 x Hab) => [y [Hy yRx]].
      move : (H3 y yRx) => [z [Hz zRy]].
      apply H1; exists z,y; repeat split; auto.
    - move /set1P : H0 => F; subst.
      move : (H3 a Hab) => [y [Hy yRa]].
      apply H1; exists y,a; repeat split; auto.
    - apply H1; exists a,b; repeat split; auto.
  }
  {
   move => a /setUP Ha b bRa.
   case Ha.
   - move /set1P => F; subst.
    move : (H3 b bRa) => [y [Hy yRb]].
    exists y; split; auto.
    apply /setUP; right; auto.
  - move => H.
    move : (H2 a H b bRa ) => [y [Hy yRb]].
    exists y; split; auto.
    apply /setUP; right; auto.
  }
Qed.

Lemma deff_admi_cup_ S x x':
  admissible S -> deffend S x' -> deffend (x |: S) x'.
Proof.
  move => HS Hx'.
  apply /deffendP => a aRx'.
  move /deffendP : Hx'.
  move /(_ a aRx') => [z [Hz zRa]].
  exists z; split; auto.
  apply /setUP; right; auto.
Qed.

Lemma ex_addmi :
  exists B, admissible B.
Proof.
  exists set0.
  apply /admissibleP; split.
  - move => [a [b [F _]]].
    rewrite in_set0 in F; inversion F.
  - move => a F.
    rewrite in_set0 in F; inversion F.
Qed.

Definition compl E :=
  admissible E && [forall e, deffend E e ==> (e \in E)].

Definition pref E :=
  admissible E && [forall E', admissible E' ==> (E' \subset E)].

Definition ground E :=
  compl E && [forall E', compl E' ==> (E \subset E')].

Definition stable E :=
  cf E && [forall a, (a \notin E) ==> (attacks E a)].

Lemma stable_not_attacked S :
  stable S <-> S = [set x | ~~ attacks S x].
Proof.
  split.
  - move /andP; case => /cfP HS.
    move /forallP => H.
    apply /setP /subset_eqP /andP => //; split; apply /subsetP => x Hx.
    * rewrite in_set.
      apply /negP => /attacksP [y [Hy yRx]].
      apply HS. exists y,x; repeat split; auto.
    * rewrite in_set in Hx.
      apply /negPn.
      apply /negP => F.
      move /negP : Hx; apply.
      move : (H x); move /implyP; apply; auto.
  - move => H0. rewrite H0.
    apply /andP; split.
    * apply /cfP => F.
      move : F => [a [b [Ha [Hb H]]]].
      rewrite in_set in Ha.
      rewrite in_set in Hb.
      move /negP : Hb. apply.
      rewrite /attacks.
      apply /existsP; exists a; apply /andP; split; auto.
      rewrite H0 in_set; auto.
    * apply /forallP => x.
      apply /implyP. rewrite in_set.
      move /negPn /attacksP => [y [Hy yRx]].
      rewrite H0 in_set in Hy.
      apply /attacksP.
      exists y; split; auto.
      rewrite in_set; auto.
Qed.


Theorem compl_admi S :
  compl S -> admissible S.
Proof.
  rewrite /compl.
  move /andP; case; auto.
Qed.

Theorem pref_compl S :
  pref S -> compl S.
Proof.
  rewrite /pref /compl.
  move /andP => [H1 H2].
  apply /andP; split; auto.
  apply /forallP => e.
  apply /implyP => He.
  move : (deff_admi_cup S e H1 He) => HSe.
  move /forallP : H2.
  move /(_ (e |: S))  /implyP /(_ HSe) /subsetP; apply.
  apply /setUP; left; apply /set1P; auto.
Qed.

Lemma ex_pref :
  exists S, pref S.
Proof.
  rewrite /pref /admissible.
  exists set0.
  apply /andP; split.
  - apply /admissibleP; split.
    * move => [a [b [Ha _]]].
      rewrite in_set0 in Ha; inversion Ha.
    * move => a. rewrite in_set0 => F; inversion F.
  - rewrite /admissible.

Admitted.

Lemma stable_pref S :
  stable S -> pref S.
Proof.
  rewrite /stable /pref /cf.
  move /andP => [H1 H2].
  apply /andP; split.
  - apply /admissibleP; split.
    * move => [a [b [Ha [Hb H]]]].
      move /negP : H1; apply.
      apply /existsP; exists a.
      apply /existsP; exists b.
      apply /andP; split; auto.
      apply /andP; split; auto.
    * move => a Ha b bRa.
      move /existsPn : H1.
      move /(_ b) /existsPn /(_ a).
      move /nandP; case; [|move /nandP; case].
      - move => F; move /forallP : H2; move /(_ b).
        move /implyP; move /(_ F) /attacksP; auto.
      - rewrite Ha => F; inversion F.
      - rewrite bRa => F; inversion F.
  - apply /forallP => E'; apply /implyP  => /admissibleP [HE1 HE2].
    apply /subsetP => x Hx.
    move : (HE2 x Hx).

Admitted.

End Syntacs.

Module Type ArgFrameEx (FTS : FinTypeSig) (AF : ArgFrame FTS) <: ArgFrameSig FTS AF.
  Import FTS AF.
  Parameter a b c d e : T.
  Definition A := [set a; b; c; d; e].
  Definition Rel := [set (a,b); (c,b); (c,d); (d,c); (d,e); (e,e)].
  Lemma axiom :
    Rel \subset setX A A.
  Proof.
  Admitted.
  Definition R := mkAF A Rel axiom.
End ArgFrameEx.


Module ex (FTS : FinTypeSig ) (AF : ArgFrame FTS) (AFE : ArgFrameEx FTS AF)(SYN : Syntacs FTS AF AFE).

Import FTS AF AFE SYN.

Goal admissible [set a; d].
Proof.
  apply /admissibleP; split.
  - move => [x [y [Hx [Hy ]]]].
    rewrite in_set.
Admitted.

End ex.