有限集合の濃度の存在を証明する - Qiita

2019/05/01 この文書のソースコードは以下にあります。 OCaml 4.07.1, Coq 8.9.0, MathComp 1.9.0 説明 へんなタイトルですが、MathComp を使った定理の証明の問題です。 有限集合の濃度、すなわち要素の個数は、適当な自然数に一意的に決まります。濃度を #| _ | で表すとすると、 ∃ i : nat, #| p | = i ですね。これ自体は自明なのですが、MathComp で証明しようとすると、取り付く島もないように見えます。 でも、すこし考えてみると、MathComp の場合、集合は有限型(finType)をドメインとするbooleanな関数で表されます。すなわち、T : finType とすると、 p : pred T なお、pred T は単に T -> bool の Notation (構文糖衣) です。 pが、常にtrueを返