gistfile1.txt

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.
  Require Import Bool.Sumbool.
  Require Import Bool.Bool.
  Import ListNotations.

  (* type level existential quantifier *)
  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.

  (* candidates are a finite type with decidable equality *)
  Parameter cand : Type.
  Parameter cand_all : list cand.
  Hypothesis cand_fin : forall c: cand, In c cand_all.
  Hypothesis dec_cand : forall n m : cand, {n = m} + {n <> m}.

  (* edge is the margin in Schulze counting, i.e. edge c d is the number of 
     voters that perfer c over d *)
  (* TODO: possibly rename? *)
  Parameter edge: cand -> cand -> nat.

  (* prop-level path *)
  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.

  (* type-level path *)
  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.

  (* winning condition in Schulze counting *)
  Definition wins (c: cand) :=
    forall d : cand, exists k : nat, 
      ((Path k c d) /\ (forall l, Path l d c -> l <= k)).

  (* auxilary functions: all pairs that can be formed from a list *)
  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.

  (* boolean equality on candidates derived from decidable equality *)
  Definition cand_eqb (c d: cand) := proj1_sig (bool_of_sumbool (dec_cand c d)).

  (* boolean membership in lists of pairs *)
  Definition bool_in (p: (cand * cand)%type) (l: list (cand * cand)%type) :=
    existsb (fun q => (andb (cand_eqb (fst q) (fst p))) ((cand_eqb (snd q) (snd p)))) l. 

  (* towards the definition of co-closed sets *)
  (* el is a boolean function that returns true if the edge between two cands is <= k *)
  Definition el (k: nat) (p: (cand * cand)%type) := Compare_dec.leb (edge (fst p) (snd p)) k.

  (* mp k (a, c) l (for midpoint) returns true if there's a midpoint b st. either the edge between 
     a and b is <= k or else the pair (b, c) is in l *)
  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 (b, c) l) (el k (a,b)))) cand_all true.

  (* W k is the dual of the operator the least fixpoint of which inductively defines paths *)
  (* W_k (l) = {(a, c) : edge a c <= k /\ forall b: (b, c) \in l \/edge a c <= k } *)
  (* Wf is the boolean predicate that expresses the operator *)
  Definition Wf k l :=  (fun p => andb (el k p)  (mp k p l) ).
  Definition W (k: nat) : list (cand * cand)%type -> list (cand *cand)%type :=
    fun l => filter (Wf k l) (all_pairs cand_all).

  (* a k-coclosed set is a set that is co-closed under W_k *)
  (* idea: the greatest co-closed (and indeed any co-closed set) only *)
  (* contains pairs (x, y) s.t. there's no path of strength >= k between x and y *)
  Definition coclosed (k: nat) (l: list (cand * cand)%type) :=
    forall x, In x l -> In x (W k l).

  (* evidence for winning a Schulze election. *)
  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).

  (* type-level paths allow to construct evidence for the existence of paths *)
  (* TODO: change name of lemma? *)
  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.

  (* logical interpretation of the midpoint function *)
  (* TODO: change name of lemma? *)
  Lemma edge_prop : forall a b k, el k (a, b) = true -> edge a b <= k.
  Proof.
    intros a b k H; unfold el in H; simpl in H;
    apply leb_complete in H; assumption.
  Qed.

  Lemma boolin_prop :  forall a b l, bool_in (a, b) l = true -> In (a, b) l.
  Proof. Admitted. 

  Lemma fold_left_true :
    forall (p : cand * cand) (l : list (cand * cand)) (k : nat), 
    fold_left (fun (x : bool) (b : cand)
               => andb x (orb (bool_in (b, snd p) l)
                            (el k (fst p, b)))) cand_all true = true ->
    forall c , (bool_in (c, snd p) l) = true \/  (el k (fst p, c)) = true.
  Proof.
    intros. 
      


    
  Program Lemma forthemoment : forall k p l, mp k p l = true -> 
    forall b, In (b, snd p) l \/ edge (fst p) b <= k.
  Proof. 
    intros k (u, v) l H b. unfold mp in H.
    apply fold_left_true with (c := b) in H.
    simpl in H; simpl. destruct H as [H | H].
    apply boolin_prop in H. left; assumption.
    apply edge_prop in H. right; assumption.
  Qed.
    
  (* generic property of coclosed sets as commented above *)
  Lemma coclosednow : forall k l, coclosed k l -> forall s x y,
    Path s x y -> In (x, y) l -> s <= k.
  Proof.
    intros k l Hcc.
    intros s x y.
    intro p.
    induction p.
    (* path of length one *)
    intro Hin.
    unfold coclosed in Hcc.
    specialize (Hcc (c, d)).
    specialize (Hcc Hin).
    unfold W in Hcc.
    Check filter_In.
    assert (HW: In (c, d) (all_pairs cand_all) /\  (Wf k l)  (c, d) = true).
    apply filter_In.
    assumption.
    destruct HW as [HW1 HW2].
    unfold Wf in HW2.

    assert ( el k (c, d) = true /\ mp k (c, d) l = true).
    apply andb_true_iff. assumption.
    destruct H0 as [He Hc].
    unfold el in He.
    simpl in He.
    assert (Hle: edge c d <= k). apply leb_complete. assumption.
    omega.
    (* non-unit path *)
    intro Hin.
    unfold coclosed in Hcc.
    specialize (Hcc (c, e)).   specialize (Hcc Hin). 
    unfold W in Hcc.
    assert (HW: In (c, e) (all_pairs cand_all) /\  (Wf k l)  (c, e) = true).
    apply filter_In. assumption.
    destruct HW as [HW1 HW2].
    unfold Wf in HW2.
    assert ( el k (c, e) = true /\ mp k (c, e) l = true).
    apply andb_true_iff. assumption.
    destruct H0 as [He Hc].
    unfold el in He.
    simpl in He.
    assert (Hle: edge c e <= k). apply leb_complete. assumption.
  (*  forall b, In (b, snd p) l \/ edge (fst p) b <= k. *)
    assert (Hmp: forall m, In (m, (snd (c, e))) l \/ edge (fst (c, e)) m <= k).
    apply  forthemoment. assumption.
    simpl in Hmp.
    specialize (Hmp d).
    destruct Hmp as [Hm1 | Hm2].
    (* case 2nd part of path in coclosed list *)
    specialize (IHp Hm1).
    assumption.
    (* case first edge of small weight *)
    omega.
Qed.

  Theorem th1: forall c, ev c -> wins c.
  Proof.
    intros c H.
    unfold wins. unfold ev in H.
    intro d.
    specialize (H d).
    destruct H as [k H].
    destruct H as [Hp Hc].
    exists k.
    split.
    apply equivalent. assumption.
    intros s p.
    destruct Hc as [l Hc].
    destruct Hc as [Hin Hcc].
    apply coclosednow with (x := d) (y := c) (l := l).
    assumption.
    assumption.
    assumption.
Qed.