proposition: Lemma collision_count l : collision l = false -> Forall (fun x1 : nat => count_occ Nat.eq_dec l x1 = 1) l.
proof: Proof. change (collision ([] ++ l) = false -> Forall (fun x1 : nat => count_occ Nat.eq_dec ([] ++ l) x1 = 1) l). generalize ([] : list nat). induction l; intros pre Hcol. constructor. constructor. - clear -Hcol. induction pre as [| b pre IHpre]. + simpl in *. destruct (Nat.eq_dec a a) as [ _ | ]; [ | tauto ]. f_equal. destruct (appears a l) eqn:Ha. discriminate. clear Hcol. induction l as [|b l IHl]. reflexivity. simpl. destruct (Nat.eq_dec b a). * subst. simpl in Ha. rewrite Nat.eqb_refl in Ha. discriminate. * apply IHl. simpl in Ha. destruct (a =? b); auto; discriminate. + simpl in *. destruct (appears b (pre ++ a :: l)) eqn:Eb. discriminate. rewrite IHpre; auto. destruct (Nat.eq_dec b a); auto. subst. cut (appears a (pre ++ a :: l) = true). congruence. clear. induction pre as [|b pre IHpre]. simpl. rewrite Nat.eqb_refl. reflexivity. simpl. destruct (a =? b); auto. - assert (E : pre ++ a :: l = (pre ++ a :: nil) ++ l). { rewrite <-app_assoc. reflexivity. } rewrite E. apply IHl. congruence. Qed.
imports: Arith ZArith List Lia