proposition: Theorem bertrand_ballot_bool p q : q <= p -> let l := filter (sumtrue p) (pickbools (p + q)) in (p + q) * length (filter (throughout winb) l) = (p - q) * length (filter winb l).
proof: Proof. intros L l. remember (p + q) as n. revert p q L Heqn l. induction n; intros p q L Heqn l. { assert (p = 0) by lia. assert (q = 0) by lia. subst; simpl. reflexivity. } assert (D : q = p \/ q < p) by lia. destruct D as [D | D]. { subst l. rewrite Heqn. destruct p as [ | p ]. subst; reflexivity. apply (bertrand_ballot_bool_eq (S p) q); auto. } destruct p as [ | p]; [ | destruct q as [ | q ] ]. - lia. - assert (n = p) by lia; subst n. f_equal. subst l. clear. f_equal. rewrite pickbools_length. repeat rewrite filter_filter. apply filter_ext. intros x. destruct (length x =? S p) eqn:El. 2:reflexivity. destruct (sumtrue (S p) x) eqn:Ep. 2:reflexivity. simpl. unfold sumtrue in Ep. rewrite Nat.eqb_eq in *. assert (F : countb false x = 0). { rewrite countb_false. lia. } assert (E : forall x, length x <> 0 -> countb false x = 0 -> winb x = true). { clear. intros. unfold winb. rewrite Nat.ltb_lt. rewrite countb_false in *. lia. } rewrite E; auto. 2:lia. assert (E' : forall x, length x <> 0 -> countb false x = 0 -> throughout winb x = true). { unfold throughout. clear -E. intros x L F. induction x as [| [ | ] l IHl]. - tauto. - simpl. rewrite E; try lia. destruct l as [ | [ | ] l ]. + reflexivity. + apply IHl. simpl. lia. auto. + discriminate. - discriminate. } apply E'. lia. auto. - pose proof IHn (S p) q ltac:(lia) ltac:(lia) as Hsp. pose proof IHn p (S q) ltac:(lia) ltac:(lia) as Hp. clear IHn. replace (filter winb l) with l; swap 1 2. { subst l. rewrite Heqn. rewrite counting_wins; auto. } rewrite Heqn. eapply recurrence; try lia; swap 1 3; swap 2 6. { subst l. rewrite Heqn. rewrite first_vote_split. rewrite app_length. reflexivity. } { subst l. rewrite Heqn. rewrite first_vote_split. rewrite filter_app. do 2 rewrite map_filter. rewrite app_length. reflexivity. } + subst l. rewrite Heqn. clear. rewrite map_length. do 2 rewrite count_sumtrue. simpl (_ + _). assert (L : p <= p + S q) by lia. revert L. generalize (p + S q); intros n L. apply binomial_S. auto. + injection Heqn as ->. clear Hsp l. simpl in Hp. do 2 rewrite map_length. replace (S p - 1 + S q) with (p + S q) by lia. replace (S p - S q - 1) with (p - S q) by lia. rewrite pickbools_wins_minus. 2:lia. rewrite <-Hp. clear Hp. f_equal. f_equal. repeat rewrite filter_filter. apply filter_ext; intros x. f_equal. unfold throughout. simpl. destruct x. simpl. reflexivity. simpl. rewrite Bool.andb_assoc. f_equal. generalize (b :: x); clear; intros l. unfold winb. simpl. generalize (countb false l). generalize (countb true l). clear. intros a b. destruct (b <? a) eqn:Ea, (b <? S a) eqn:Esa; auto. rewrite Nat.ltb_lt in *. rewrite Nat.ltb_nlt in *. lia. + injection Heqn as ->. clear Hp l. replace (S p - 1 + S q) with (p + S q) by lia. replace (S p - (S q - 1)) with (S p - q) by lia. do 2 rewrite map_length. replace ((S p - q) * length (filter (sumtrue (1 + p)) (pickbools (p + S q)))) with ((S p - q) * length (filter winb (filter (sumtrue (1 + p)) (pickbools (p + S q))))); swap 1 2. { replace (p + S q) with (S p + q) by lia. rewrite pickbools_wins_minus. 2:lia. auto. } simpl in *. rewrite <-Hsp. f_equal. f_equal. rewrite pickbools_length. repeat rewrite filter_filter. apply filter_ext; intros x. clear Hsp. destruct (length x =? p + S q) eqn:Hlen. 2:reflexivity. simpl. destruct (sumtrue (S p) x) eqn:Hp. 2:reflexivity. simpl. unfold throughout. simpl. rewrite Bool.andb_comm. destruct (forallb winb (proper_suffixes x)) eqn:Hw. 2:reflexivity. simpl. unfold winb. unfold sumtrue in Hp. repeat rewrite Nat.ltb_lt in *. repeat rewrite Nat.eqb_eq in *. simpl. rewrite countb_false. lia. + subst l. rewrite Heqn. clear. rewrite map_length. do 2 rewrite count_sumtrue. simpl (_ + _). replace (S q) with (p + S q - p) at 3 by lia. assert (L : p <= p + S q) by lia. revert L. generalize (p + S q); intros n L. assert (D : p = n \/ p < n) by lia. destruct D as [D | D]. * subst p. rewrite binomial_lt. rewrite binomial_diag. lia. lia. * rewrite binomial_complement. 2:lia. rewrite (binomial_complement (S n)). 2:lia. rewrite (binomial_S n (n - S p)). 2:lia. f_equal. lia. f_equal. lia. Qed.
imports: Arith ZArith String List Psatz Factorial