proposition: Lemma length_no_collision_picks k l : collision l = false -> Zlength (filter (no collision) (picks k l)) = partial_fact k (Zlength l).
proof: Proof. rewrite Zlength_correct. revert l; induction k; intros l Hcol. reflexivity. simpl. set (l1 := l) at 1 3. assert (Huniq : Forall (fun x1 => count_occ Nat.eq_dec l x1 = 1) l1). { apply collision_count; auto. } clearbody l1. induction l1 as [| a l1 IHl1]. reflexivity. simpl. rewrite map_app, filter_app, app_length. rewrite Zlength_cons, Z.mul_succ_l, Nat2Z.inj_add. rewrite Z.add_comm. f_equal. - rewrite IHl1. auto. inversion Huniq; auto. - clear IHl1. rewrite map_map. simpl. pose (l' := filter (no (Nat.eqb a)) l). assert (El' : Zlength l' = (Zlength l - 1)%Z). { apply Forall_inv in Huniq. cut (Zlength l' + 1 = Zlength l)%Z. { intros <-. lia. } unfold l'. do 2 rewrite Zlength_correct. change 1%Z with (Z.of_nat 1). rewrite <-Nat2Z.inj_add. f_equal. rewrite <-Huniq. clear IHk k Hcol l' Huniq. induction l as [| b l IHl]. reflexivity. simpl. rewrite <-IHl. unfold no. destruct (Nat.eq_dec b a). - subst. rewrite Nat.eqb_refl. simpl. lia. - replace (a =? b) with false; simpl. reflexivity. symmetry. apply Nat.eqb_neq. auto. } assert (Hl' : collision l' = false). { unfold l'. generalize (no (Nat.eqb a)); intros f. clear -Hcol. apply collision_filter; auto. } rewrite <-El'. rewrite <-IHk; auto. f_equal. transitivity (length (map (fun x => a :: x) (filter (no collision) (picks k l')))). 2: rewrite map_length; reflexivity. f_equal. unfold l'. apply Forall_inv in Huniq. clear IHk El' l' Hl' l1. rewrite picks_remove. induction (picks k l) as [| l' ll' IHll']. reflexivity. simpl. unfold no at 1 5. simpl. destruct (appears a l'). simpl; congruence. simpl. unfold no at 3. destruct (collision l'); simpl; congruence. Qed.
imports: Arith ZArith List Lia