Votes.v

Module Evote.

  Require Import Notations.
  Require Import Coq.Lists.List.
  Require Import Coq.Arith.Le.
  Require Import Coq.Numbers.Natural.Peano.NPeano.
  Require Import Coq.Arith.Compare_dec.
  Require Import Coq.omega.Omega.
  Import ListNotations.


  Parameter cand : Type.
  Parameter cand_all : list cand.
  Hypothesis cand_fin : forall c: cand, In c cand_all.

  Parameter edge: cand -> cand -> nat.

  Inductive Path (k: nat) : cand -> cand -> Prop :=
  | unit c d : edge c d >= k -> Path k c d
  | cons  c d e : edge c d >= k -> Path k d e -> Path k c e.

  Inductive PathT (k: nat) : cand -> cand -> Type :=
  | unitT : forall c d, edge c d >= k -> PathT k c d
  | consT : forall c d e, edge c d >= k -> PathT k d e -> PathT k c e.

  Definition wins (c: cand) :=
    forall d: cand,
    exists k : nat, ((Path k c d) /\ (forall l, Path l d c -> l <= k))%type.

  Fixpoint all_pairs {A: Type} (l: list A): list (A * A) :=
    match l with
    |   [] => []
    |    c::cs => (c, c)::(all_pairs cs) ++ (map (fun x => (c, x)) cs) ++ (map (fun x => (x, c)) cs)
    end.

  Compute (all_pairs [1; 2; 3]).

  Check filter.
  Check leb.
  Check andb.
  Check fold_left.
  Check true.
  Hypothesis dec_cand : forall n m : cand, {n = m} + {n <> m}.
  Definition bool_cand n m := if dec_cand n m then true else false.
  Program Fixpoint  bool_in (p : (cand * cand)%type) (l : list (cand * cand)%type) : bool:=
    match l with
    | [] => false
    | h :: t => if andb (bool_cand (fst p) (fst h)) (bool_cand (snd p) (snd h)) then true
               else bool_in p t
    end.

  Definition el (k: nat) (p: (cand * cand)%type) := leb (edge (fst p) (snd p)) k.
  Definition mp (k: nat) (p: (cand * cand)%type) (l: list (cand * cand)%type) :=
    let a := fst p in
    let c := snd p in
    fold_left (fun x => fun b => andb x (orb (bool_in (a, b) l)   (el k (b, c)))) cand_all true.

  (* W_k (l) = {(a, c) : edge a c <= k /\ forall b: (a, b) \in l \/ edge b c <= k } *)
  Definition W (k: nat) : list (cand * cand)%type -> list (cand * cand)%type :=
    fun l => filter (fun p => andb (el k p)  (mp k p l) )  (all_pairs cand_all).

  Definition coclosed (k: nat) (l: list (cand * cand)%type) := forall x, In x l -> In x (W k l).

  Notation "'existsT' x .. y , p" :=
    (sigT (fun x => .. (sigT (fun y => p)) ..))
      (at level 200, x binder, right associativity,
       format "'[' 'existsT'  '/  ' x  ..  y ,  '/  ' p ']'")
    : type_scope.

  Definition ev (c: cand) := forall d: cand, existsT (k: nat),
    (PathT k c d) * (existsT (l: list (cand * cand)%type), In (d, c) l /\ coclosed k l).

  Lemma equivalent : forall c d k , PathT k c d -> Path k c d.
  Proof.
    intros. induction X. apply unit. assumption.
    apply cons with (d := d). assumption.
    assumption.
  Qed.


  Lemma forthemoment : forall k p l, mp k p l = true -> forall b, In (fst p, b) l \/ edge b (snd p) <= k.
  Proof. Admitted.

  (*
  Lemma coclosednow : forall k l, coclosed k l -> forall s x y, Path s x y -> In (x, y) l -> s <= l
  Proof. Admitted.
   *)

  Theorem th1: forall c, ev c -> wins c.
  Proof.
    unfold ev, wins.
    intros c H d. destruct (H d).
    exists x. split.
    { destruct p. apply equivalent. assumption. }
    {
      intros.
      destruct p as [H1 H2]. destruct H2.
      destruct a as [H2 H3]. unfold coclosed in H3.
      apply H3 in H2. unfold W in H2.



      induction (all_pairs cand_all).
      inversion H2. simpl in H2.
      (* eliminate the false cases first *)
      remember (el x a) as tmp eqn:H5 in H2; destruct tmp in H2,H5; swap 1 2.
      apply IHl0; assumption.
      remember (mp x a x0) as tmp eqn:H6 in H2; destruct tmp in H2,H6; swap 1 2.
      simpl in H2. apply IHl0; assumption. symmetry in H5.
      apply leb_complete in H5. symmetry in H6.
      destruct H2 as [H7 | H7]; swap 1 2. apply IHl0; trivial.
      rewrite H7 in H5, H6; simpl in H5, H6.
      (* and now the challenge *)
      induction H0. omega.


  e : cand
  H : forall d : cand,
      existsT k : nat,
        PathT k e d * (existsT l : list (cand * cand), In (d, e) l /\ coclosed k l)
  x : nat
  c : cand
  H1 : PathT x e c
  x0 : list (cand * cand)
  a : cand * cand
  l0 : list (cand * cand)
  H5 : edge c e <= x
  H6 : mp x (c, e) x0 = true
  H7 : a = (c, e)
  H3 : forall x1 : cand * cand, In x1 x0 -> In x1 (W x x0)
  l : nat
  d : cand
  H0 : edge c d >= l
  H2 : Path l d e
  IHl0 : In (c, e) (filter (fun p : cand * cand => (el x p && mp x p x0)%bool) l0) -> l <= x
  IHPath : (forall d : cand,
            existsT k : nat,
              PathT k e d * (existsT l : list (cand * cand), In (d, e) l /\ coclosed k l)) ->
           PathT x e d ->
           edge d e <= x ->
           mp x (d, e) x0 = true ->
           a = (d, e) ->
           (In (d, e) (filter (fun p : cand * cand => (el x p && mp x p x0)%bool) l0) -> l <= x) ->
           l <= x
  ============================
   l <= x