valid_ballot.v

Require Import Coq.ZArith.ZArith. (* integers *)
Require Import Coq.Lists.List.    (* lists *)

Section Count.

  Variable cand : Type.
  Variable c : cand.
  Variable cand_all : list cand.
  Hypothesis cand_fin : forall c : cand, In c cand_all /\ NoDup cand_all.

  (* [[x1, x2], [x3], [x4, x5, x6]] *)
  Definition ballot := list (list cand).

  Definition ballot_valid (b: ballot) : Prop :=
    forall c: cand, In c (concat b) /\ NoDup (concat b).

  (* https://github.com/uwplse/StructTact *)
  Ltac subst_max :=
    repeat match goal with
           | [ H : ?X = _ |- _ ]  => subst X
           | [H : _ = ?X |- _] => subst X
           end.
  Ltac inv H := inversion H; subst_max.
  Ltac invc H := inv H; clear H.
  Ltac invc_NoDup :=
    repeat match goal with
           | [ H : NoDup (_ :: _) |- _ ] => invc H
           end.
  Ltac do_in_app :=
    match goal with
    | [ H : In _ (_ ++ _) |- _ ] => apply in_app_iff in H
    end.
  
  Lemma NoDup_disjoint_append :
    forall (A : Type) (l : list A) l',
      NoDup l -> NoDup l' -> (forall a, In a l -> ~ In a l') ->
      NoDup (l ++ l').
   Proof.
    induction l; intros.
    - auto.
    - simpl. invc_NoDup. constructor.
      + intro. do_in_app. intuition eauto with *.
      + intuition eauto with *.
   Qed.
   
  Lemma valid_or_invalid_ballot : forall b : ballot, {ballot_valid b} + {~ballot_valid b}.
  Proof.
    induction b. right. unfold not, ballot_valid; simpl; intros H.
    specialize (H c). intuition.
    unfold not, ballot_valid in *. simpl in *. destruct IHb.   
    left. intros c0. split. apply in_or_app. firstorder.
    apply NoDup_disjoint_append. 
   
   
  cand : Type
  c : cand
  cand_all : list cand
  cand_fin : forall c : cand, In c cand_all /\ NoDup cand_all
  a : list cand
  b : list (list cand)
  a0 : forall c : cand, In c (concat b) /\ NoDup (concat b)
  c0 : cand
  ============================
  NoDup a

subgoal 2 (ID 90) is:
 NoDup (concat b)
subgoal 3 (ID 91) is:
 forall a1 : cand, In a1 a -> ~ In a1 (concat b)
subgoal 4 (ID 71) is:
 {(forall c0 : cand, In c0 (a ++ concat b) /\ NoDup (a ++ concat b))} +
 {(forall c0 : cand, In c0 (a ++ concat b) /\ NoDup (a ++ concat b)) -> False}