Skip to content

Instantly share code, notes, and snippets.

View yoshihiro503's full-sized avatar

YOSHIHIRO Imai yoshihiro503

99 followers · 51 following
View GitHub Profile
@yoshihiro503
yoshihiro503 / Coqdocでコロンやドット記号を含むid属性のHTMLを生成している件.md
Last active October 21, 2026 05:42
  • ツール html_validate では : や .を含む id属性を標準でエラーにしている．
  • HTML5の規格で禁止されているわけではないが CSSセレクタでの実用上の都合が悪いから
  • とはいえ，coqdocでも以下の点でドットやコロンをそのままidとして使っている

.（ドット）を含む例 — https://rocq-prover.org/doc/V9.1.0/stdlib/Stdlib.Arith.PeanoNat.html <... id="Nat.Decidable_eq_nat" ...> <... id="Nat.EvenT_Even" ...> <... id="Nat.Even_Odd_dec" ...> （モジュールNat内の補題名がそのままモジュール名.補題名の形でid化されています）

@yoshihiro503
yoshihiro503 / nat.zfp
Last active August 13, 2026 13:03
(**
ZFCert で自然数定義してみた
*)
(* フォン・ノイマン式の自然数の構成。
0 := 空集合、succ(n) := n ∪ {n} = n ∪ singleton(n)。 *)
(* 0 は空集合公理からそのまま得られる。 *)
Choose zero Hzero from empty_set.
@yoshihiro503
yoshihiro503 / 業績目録2026.md
Created December 11, 2025 09:59

著書

  • 型システム入門 −プログラミング言語と型の理論, オーム社 (2013/3/26)
  • 入門OCaml ~プログラミング基礎と実践理解, 毎日コミュニケーションズ (2007/5/22)

学術論文

  • システム群のBASE特性を保証するためのCoqを用いた検証 - 2013 Fundamental of Software Engineering.
  • 検証済みのコードによるCoqからScalaへのコード抽出 - 2014 The 31th Japan Society for Software Science and Technology Annual Conference

発表、講演

@yoshihiro503
yoshihiro503 / githubでforkの分岐点を探す.md
Created October 24, 2025 02:56

cometbft/cometbft から派生した 0xPolygon/cometbft リポジトリを見ているが、どのタイミングで分岐したか知りたい

分岐点のコミットを探す

git clone https://github.com/0xPolygon/cometbft.git cometbft-polygonfork
cd cometbft-polygonfork/
git remote add upstream https://github.com/cometbft/cometbft.git
git fetch upstream
@yoshihiro503
yoshihiro503 / Heimdall_checkpoint.go_fungraph.dot.md
Last active May 15, 2025 08:55

Alt text

#CUT
digraph G {
    aize ="4,4";
    subgraph cluster_public {
        label="Public";
        Start [shape=box];
        RegisterTasks [shape=box, layer=cluster_public];
        Stop [shape=box];
@yoshihiro503
yoshihiro503 / Coqのコードをopamに登録する方法.md
Last active April 11, 2025 07:56
@yoshihiro503
yoshihiro503 / CoqのModule内定義に関するglobがなんか変な件について.md
Created August 30, 2024 06:59

mathcomp analysisのtopology.vにおいて，

...
Module PropInFilter : PropInFilterSig.
  Definition t := prop_in_filter_proj.
  ...
End PropInFilter.
Notation prop_of := PropInFilter.t.
...
@yoshihiro503
yoshihiro503 / 長さ付きリストの証明_ssreflect.v
Created July 12, 2024 06:42
From mathcomp Require Import all_ssreflect.
Require Import JMeq.
Inductive sizseq (T:Type) : nat -> Type :=
| SizNil : sizseq T 0
| SizCons n : T -> sizseq T n -> sizseq T n.+1.
Lemma sizseq0nil_aux (T:Type) n : forall xs : sizseq T n, n = 0 -> JMeq xs (SizNil T).
Proof.
@yoshihiro503
yoshihiro503 / coqtokyo_EqClass_sort2.v
Last active April 30, 2024 11:47
From mathcomp Require Import all_ssreflect.
Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.
(* :> を複数持つと予期せぬことがおきることがあるぞ *)
Structure S : Type := MakeS {
sort2 :> Type;
sort :> Type;
@yoshihiro503
yoshihiro503 / mathcompbook_edivn.v
Created March 20, 2024 00:05
From mathcomp Require Import all_ssreflect.
Fixpoint evivn_rec pred_d m q :=
if m - pred_d is m'.+1 then edivn_rec pred_d m' q.+1 else (q, m).
Definition edivn m d := if d > 0 then edivn_rec d.-1 m 0 else (0, m).
Lemma edivn_recP1 q r m pred_d q0:
(q, r) = edivn_rec pred_d m q0 ->
r < pred_d.+1.