在Coq中表達可數無窮大的慣用方法是什麼？

Question

假設我想斷言存在數量可以無限的不同的x : X。我的第一個猜測是遵循可數無窮的定義從字面上看，例如：

Definition aleph_null (X : Type) := 
exists (R : nat -> X -> Prop), 
(forall (n : nat), exists (x : X), R n x) 
/\ (forall (x : X), exists (n : nat), R n x) 
/\ (forall (n : nat) (x y : X), R n x -> R n y -> x = y) 
/\ (forall (n m : nat) (x : X), R n x -> R m x -> n = m). 

但似乎有點笨拙，在實際樣張使用，不使用庫。 我想我可以通過使用現有的雙向性定義使其更短，但我可以找到的所有定義都是關於函數，而不是二元關係。

有沒有更好的，習慣用法來表達Coq中的可數無窮大？

Answer 1

最好的選擇很大程度上取決於你想要的特定應用。我會說使用函數可能是大多數情況下最簡單的選擇。既然你提到了圖書館的支持，ssreflect圖書館對這種推理提供了很好的支持;您可以定義，例如

Inductive count_inf (X : Type) : Type := CountInf { 
    count : X -> nat; 
    _ : bijective count 
}. 

ssreflect其實有它自己的countable types定義，但它包括了有限與無限類型，因此它不會給你想你想的開箱。