Arguments.v

From mathcomp Require Import all_ssreflect.


Variables argument position : finType.
Definition A := [set : argument].
Definition X := [set : position].

Definition Rel := rel position.

Axiom axiomA : 0 < #|argument|.
Axiom axiomX : 1 < #|position|.

Theorem ex_elm_A :
  exists a, a \in A.
Proof.
  apply /card_gt0P.
  rewrite cardsT.
  apply axiomA.
Qed.


Theorem ex_elm_X :
  exists x y, [/\ x \in X, y \in X & x != y].
Proof.
  apply /card_gt1P.
  rewrite cardsT.
  apply axiomX.
Qed.

Definition partial_order (R : Rel) :=
  antisymmetric R /\ transitive R.

Definition linear_order (R : Rel) :=
  antisymmetric R /\ transitive R /\ total R.

Definition maximal (x : position) (R : Rel) (H : antisymmetric R) :=
  ~~ [exists y, R y x].

Theorem partial_maximal R (H : partial_order R) :
  exists x H, maximal x R H.
Proof.
Admitted.


Definition valuation := position -> position -> {set argument}.


Axiom asymp : forall (p : valuation) x y,
  setI (p x y)  (p y x) != set0.

Axiom irreflp : forall (p : valuation) x,
    p x x = set0.

Definition totalp (p : valuation) :=
  forall x y a, a \in p x y \/ a \in p y x.

Definition transp (p : valuation) :=
  forall x y z, setI (p x y) (p y z) \subset p x z.


Theorem totalp' (p : valuation) :
  totalp p <->
    (forall x y, setU (p x y) (p y x) = A).
Proof.
  split => H.
  - move => x y.
    apply /setP /subset_eqP /andP; split; apply /subsetP => a.
    - case /setUP; apply /subsetP /subsetT.
    - move => _; apply /setUP; auto.
  - move => x y a.
    suff : (a \in A).
    - rewrite <- (H x y).
      case /setUP => Ha; [left|right]; auto.
    - apply in_setT.
Qed.


Axiom constituent : valuation -> argument -> Rel.
Axiom axiom_constituent :
  forall p x y a, constituent p a x y <-> a \in p x y.

Lemma transitive_stransp p :
  transp p <-> forall a, transitive (constituent p a).
Proof.
  split => H.
  - move => a x y z /axiom_constituent Hyx /axiom_constituent Hxz.
    apply  /axiom_constituent.
    move /subsetP : (H y x z ).
    apply.
    apply /setIP; auto.
  - move => x y z.
    apply /subsetP => a.
    case /setIP => /axiom_constituent Hxy  /axiom_constituent Hyz.
    apply axiom_constituent.
    apply : (H a y x z); auto.
Qed.

Lemma total_totalp p :
  totalp p <-> forall a, total (constituent p a).
Proof.
  split => H.
  - move => a x y.
    apply /orP.
    case : (H x y a) => Hp; [left|right]; apply axiom_constituent; auto.
  - move => x y a.
    case /orP : (H a x y); move /axiom_constituent; auto.
Qed.

Definition unassailable (p : valuation) : Rel :=
  fun x y => p y x == set0.


Definition UA (p : valuation) :=
  [set x | [forall y, unassailable p x y]].

Definition dominate (p : valuation) (x y : position)  :=
  (p x y != set0) && [forall z, p z x \subset p z y].

Definition UD p :=
  [set x | ~~ [exists y, dominate p y x]].

Theorem UA_UD p :
  UA p \subset UD p.
Proof.
  rewrite /UA /UD.
  apply /subsetP => x.
  rewrite in_set => /forallP H.
  rewrite in_set.
  apply /negP => /existsP [y /andP [Hxy _]].
  move /negP : Hxy; apply; eauto.
Qed.

Theorem dominate_partial_order p :
  partial_order (dominate p).
Proof.
  split.
  - move => x y /andP; case.
    rewrite /dominate.
    move => /andP [_ /forallP Hxy].
    move : (Hxy y).
    rewrite (irreflp p y) => F.
    move => /andP [yx0 _].
    move /set0Pn : yx0 => [a Ha].
    move /subsetP : F.
    move /(_ a Ha) => F.
    move : (in_set0 a); rewrite F => contra.
    inversion contra.
  - move => y x z.
    rewrite /dominate.
    move => /andP [xy0 /forallP Hxy].
    move => /andP [yz0 /forallP Hyz].
    apply /andP; split.
    - apply /eqP => F.
      move /set0Pn : xy0 => [a Ha].
      move : (Hyz x).
      move /subsetP /(_ a Ha).
      rewrite F => set0a.
      move : (in_set0 a); rewrite set0a; auto.
    - apply /forallP => w; apply /subsetP => a H.
      move /subsetP : (Hxy w); move /(_ a H) => wy.
      move /subsetP : (Hyz w); apply; auto.
Qed.

Lemma ex_undominat p :
  exists x, x \in UD p.
Proof.
  move : (partial_maximal _ (dominate_partial_order p)) => [x [H /negP Hx]].
  rewrite /maximal in Hx.
  exists x.
  rewrite /UD.
  rewrite in_set.
  apply /negP => /existsP [y Hy].
  apply Hx.
  apply /existsP; exists y; auto.
Qed.

Definition projection (p : valuation) : Rel :=
  fun x y => [exists a, a \in p x y].

Theorem projection_UA p (H : antisymmetric (projection p)) :
  [set x | maximal x (projection p) H] = UA p.
Proof.
  apply /setP.
  apply /subset_eqP /andP; split;
    apply /subsetP => x;
      rewrite /UA /maximal /unassailable /projection;
      repeat rewrite in_set.
  - move /existsPn => Hx; apply /forallP => y.
    move /existsPn : (Hx y) => Ha.
    apply /negPn /negP => /set0Pn [a F].
    move : (Ha a); rewrite F; auto.
  - move /forallP => Hxy.
    apply /negP => /existsP F.
    move : F => [y /existsP [a Ha]].
    move : (Hxy y) Ha.
    move /eqP ->.
    rewrite in_set; auto.
Qed.





Inductive closure (p : valuation) : position -> position -> Prop :=
  | cls_nil x y : projection p x y -> closure p x y
  | cls_cons x y z : projection p x y -> closure p y z -> closure p x z.

Lemma transitive_closure p :
  forall x y z, closure p x y -> closure p y z -> closure p x z.
Proof.
  move => x y z H.
  generalize dependent z.
  induction H; intros; constructor 2 with y; auto.
Qed.

Definition TC p x :=
  forall y , closure p y x -> closure p x y.

Lemma UA_TC p x :
  x \in UA p -> TC p x.
Proof.
  rewrite /UA /TC.
  rewrite in_set; move /forallP => H y Hyx.
  rewrite /unassailable in H.
  induction Hyx.
  - rewrite /projection in H0.
    move /existsP : H0 => [a].
    move : (H x).
    rewrite /unassailable.
    move /eqP ->; rewrite in_set => F; inversion F.
  - clear IHHyx H0.
    induction Hyx.
    - move /existsP : H0; case => a.
      move /eqP : (H x0) ->; rewrite in_set => F; inversion F.
    - apply IHHyx; auto.
Qed.