記事中で紹介したスクリプトの全体はCordbergに置いてあります。 今回は型XからXへのbijection、すなわち、X上の自己同型のなす群を形式化します。 ポイントは自己同型の定義方法です。 Structure automorphism_base (X : Type) : Type := mk_automorphism { carrier :> X -&...

サンプルコードの全体はCodebergにて公開しています。 今回は$${n}$$を法とする剰余群を、証明支援システムRocqで形式化してみました。 今回の形式化の特徴を以下に要約します。 コア・ライブラリだけを利用し、Standard Library などの他のライブラリはインポートしない 同値関係は$${\mathbb Z}$$でなくnat上に構成する Nat.modulo...

本記事で紹介するコードの全体はCodebergをご参照ください。 当アカウントでは、なるべく簡単な題材を使って、証明支援システムRocqを使ってみる記事を紹介していますが、今回もその続きです。 今回は以下の記事で構成したSetoidと関数のなす圏を使います。 Setoidと関数のなす圏において、射fがepimorphismであるという条件と、全射である条件が同値であることを証明します。 ...

コードの全体はCodebergにて公開しています。 今回は証明支援システムRocqを使って、圏論の簡単な部分をフォーマライズする話です。 Setoidというのは同値関係を備えた型のことであり、集合という概念の形式化のひとつです。 なのでSetoidの作る圏というのは、集合のなす圏の形式化であると言えます。 本記事では、Setoidのなす圏を3種類、射の与え方を変えることによって構成します。...

YouTube video by 雪夜のともしび