proposition: Lemma enumeratesE f s : enumerates f s <-> << RNG: forall i (LTi: lt_size i s), s (f i) >> /\ << INJ: forall i (LTi: lt_size i s) j (LTj: lt_size j s) (EQ: f i = f j), i = j >> /\ << SUR: forall a (IN: s a), exists i, lt_size i s /\ f i = a >>.
proof: Proof. unfold enumerates; split; ins; desf. { splits; ins; eauto. eapply SUR in IN; desc; exists i; split; ins. exists (map f (List.seq 0 (S i))); splits; ins; try rewrite length_map, length_seq; ins; desf. apply nodup_map; eauto using nodup_seq. rewrite in_map_iff in *; desf. } { assert (LTI: forall i, lt_size i s -> i < n). { ins; red in H; desc. replace n with (length (map f (List.seq 0 n))). 2: by rewrite length_map, length_seq. eapply Nat.lt_le_trans; eauto. ins; apply NoDup_incl_length; ins. red; ins; apply H0, SUR in H2; desf. by apply in_map, in_seq0_iff. } splits; ins; eauto. apply SUR in IN; desf; exists i; split; ins. exists (map f (List.seq 0 n)); splits; ins; try rewrite length_map, length_seq; ins; desf. apply nodup_map; eauto using nodup_seq. red; ins; rewrite in_seq0_iff in *; eauto. ins; rewrite in_map_iff in *; desf; rewrite in_seq0_iff in *; eauto. } destruct (classic (set_finite s)) as [[dom X]|INF]. { right; exists (length (undup (filterP s dom))). assert (LTI: forall i, lt_size i s -> i < length (undup (filterP s dom))). { ins; red in H; desc. eapply Nat.lt_le_trans; eauto. apply NoDup_incl_length; ins. red; ins; apply H0 in H2; desf. apply in_undup_iff, in_filterP_iff; eauto. } assert (LTI': forall i, i < length (undup (filterP s dom)) -> lt_size i s). { exists (undup (filterP s dom)); splits; ins. apply in_undup_iff, in_filterP_iff in H0; desf. } splits; ins; eauto; apply SUR in IN; desf; eauto. } { left; splits; ins; eauto using lt_size_infinite. eapply SUR in IN; desf; eauto. } Qed.
imports: Arith micromega.Lia Setoid IndefiniteDescription ClassicalChoice HahnBase HahnList HahnEquational HahnRewrite HahnRelationsBasic HahnSets HahnNatExtra HahnListBefore HahnWf HahnSorted HahnTotalExt