雪夜のともしび

【Rocq】ユークリッドの互除法｜雪夜のともしび 当アカウントでは、なるべく簡単な題材を使って、証明支援システムRocqによるプログラミングを紹介しています。 今回は、コア・ライブラリCorelib.Init.Natに登録されているユークリッドの互除法の関数gcdについて、基本的な挙動を証明していきます。 Rocq Core Library Rocq Core Library rocq-prover.org ※紹介し...

Rocqでユークリッドの互除法に関する命題の証明を書いてみました。

note.com/snowy_lanter...

24.01.2026 05:19 — 👍 0    🔁 0    💬 0    📌 0

【Rocq】自然数の整除関係｜雪夜のともしび ※紹介しているスクリプトの全体はCodebergに置きました。Coq Version 8.19.2 で動作確認してます。 当アカウントでは、証明支援システムRocqについて、なるべく簡単な題材を用いて形式化を紹介しています。 今回は、自然数natの間の整除関係を定義し、それが順序関係を公理を満たすことを証明してみます。 まず、整除関係は以下のように形式化することにします。 Definiti...

note.com/snowy_lanter...

21.01.2026 11:01 — 👍 0    🔁 0    💬 0    📌 0

【Rocq】整数を構成する｜雪夜のともしび ※紹介しているスクリプトの全体はCodebergに置いてあります。 当アカウントでは、証明支援システムRocqによる形式化を、なるべく簡単な題材を用いて紹介しています。 今回は、整数全体の集合 $$ \{\dots, -3, -2, -1, 0, 1, 2,3,\dots\} $$ を構成して、 加法の結合則 加法の交換則 分配法則 乗法の交換則 乗法の結合則...

note.com/snowy_lanter...

20.01.2026 10:34 — 👍 0    🔁 0    💬 0    📌 0

不動点コンビネータと無名再帰 - 芳賀 雅樹 のページ 不動点コンビネータと実践的な示唆について紹介します．

書いた
silasol.la/posts/2026-0...

16.01.2026 01:46 — 👍 7    🔁 3    💬 0    📌 1

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

note.com/snowy_lanter...

17.01.2026 03:47 — 👍 0    🔁 0    💬 0    📌 0

Your proof assistant is strict.
Your type system is expressive.
Your coffee mug should be too ☕

FP & ITP mugs (OCaml, Haskell, Lean, Rocq, Isabelle, Agda):
store.typetheoryfora...

15.01.2026 18:10 — 👍 9    🔁 3    💬 0    📌 0

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

ブログを更新しました。
note.com/snowy_lanter...

15.01.2026 11:15 — 👍 0    🔁 0    💬 0    📌 0

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

noteに記事を投稿しました。Setoidと関数のなす圏において、epimorphismと全射が同値になることの証明です。証明支援システムRocqでの形式化を書いてみました。

note.com/snowy_lanter...

13.01.2026 06:39 — 👍 0    🔁 0    💬 0    📌 0

↓数学で学ぶBlenderの基本

13.01.2026 05:05 — 👍 0    🔁 0    💬 0    📌 0

GeoNodeとかシェーダーとか触ってると改めて数学の大切さを実感するよね…
Blenderを活用した数学の基礎解説本が発売中📚️

Blenderで学ぶ数学のきほん
～そろそろ覚えたいベクトル・行列～
3dnchu.com/archives/ble...

著者：中島 一崇 氏

07.01.2026 03:50 — 👍 6    🔁 1    💬 0    📌 0

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

noteを更新しました。Setoidを対象とする圏を3種類構成する話です。
note.com/snowy_lanter...

12.01.2026 12:36 — 👍 0    🔁 0    💬 0    📌 0

動画を更新しました。
youtu.be/xcxyvHMFbB8?...

11.01.2026 05:49 — 👍 1    🔁 0    💬 0    📌 0