decidability_ballot.v

Require Import Coq.ZArith.ZArith. (* integers *)
Require Import Coq.Lists.List.    (* lists *)
Require Import Coq.Lists.ListDec.
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.
Section Count.

  Variable cand : Type.
  Variable cand_all : list cand.
  Hypothesis dec_cand : forall n m : cand, {n = m} + {n <> m}.
  Hypothesis cand_fin : forall c : cand, In c cand_all.
  Variable wins:  cand -> (cand -> cand -> Z) -> Type.
  Variable loses: cand -> (cand -> cand -> Z) -> Type.
  Definition ballot := cand -> nat.
  Definition ballot_valid (p : ballot) : Prop :=
    forall c : cand, p c > 0.
    
  Lemma valid_or_invalid_ballot : forall b : ballot, {ballot_valid b} + {~ballot_valid b}.
  Proof.
  
  cand : Type
  cand_all : list cand
  dec_cand : forall n m : cand, {n = m} + {n <> m}
  cand_fin : forall c : cand, In c cand_all
  wins : cand -> (cand -> cand -> Z) -> Type
  loses : cand -> (cand -> cand -> Z) -> Type
  is_marg : (cand -> cand -> Z) -> list ballot -> Prop
  ============================
  forall b : ballot, {ballot_valid b} + {~ ballot_valid b}

Theorem indecidable :
forall (b : ballot) (l : list cand),
{forall c : cand, In c l -> b c > 0} + {~(forall c : cand, In c l -> b c > 0)}.
Proof.
intros b. induction l.
left. intros. inversion H.
destruct IHl. left.
intros c H. apply in_inv in H. destruct H.
admit
firstorder.
right. firstorder.

Lemma valid_or_invalid_ballot : forall b : ballot, {ballot_valid b} + {~ballot_valid b}.
Proof.
intros b. pose proof indecidable b cand_all.
destruct H. left. unfold ballot_valid. intros c.
apply g. specialize (cand_fin c). assumption.
unfold not in n. right. unfold not, ballot_valid; intros H.
apply n; intros. specialize (H c). assumption.
Qed.