Skip to content

Instantly share code, notes, and snippets.

View mathink's full-sized avatar

m mathink

9 followers · 1 following
View GitHub Profile
@mathink
mathink / coq_omit_fun.md
Created April 3, 2020 00:05
Coq で map や filter の fun を省略したい。
title tags author slide
Coq で map や filter の fun を省略したい。
Coq
mathink
false

言いたいこと

  • 結果的に引数が一つの函数となる (fun x => f ... x ...) という項が 　`(f ... x ...) と書ける
  • そのためには　Generalizable Variables オプションを使う。
@mathink
mathink / coq_ring_ideal.md
Created April 3, 2020 00:04
Coq で環のイデアルを作ってみる
title tags author slide
Coq で環のイデアルを作ってみる
Coq
mathink
false

まとめ

  • Coq で環のイデアルを定義して、具体例を一個作ってみた。
  • 「Coq で環」 の続き。
@mathink
mathink / coq_ring.md
Created April 3, 2020 00:04
Coq で環
title tags author slide
Coq で環
Coq
mathink
false

まとめ

  • Coq で Setoid ベースの環を定義した。
  • Z が環だよって言った。
@mathink
mathink / coq_semiring.md
Created April 3, 2020 00:04
Coq で半環
title tags author slide
Coq で半環
Coq
mathink
false

何をした？

  • Coq で半環を定義した
  • 足し算とかけ算で半環になることを示した。
@mathink
mathink / coq_dep_typeclass_notation.md
Created April 3, 2020 00:02
依存型/\型クラス/\記法 -> (テスト失敗 <-> 型エラー)
title tags author slide
依存型/\型クラス/\記法 -> (テスト失敗 <-> 型エラー)
Coq
mathink
false

アドベントカレンダー

7日目の記事は fetburner さんの 単一化の証明 でした。

@mathink
mathink / coq_cat_background.md
Created April 3, 2020 00:02
Coq で圏論：背景と普遍性について
title tags author slide
Coq で圏論：背景と普遍性について
Coq-8.5 Coq
mathink
false

まとめ

  • そもそもどんな風に Coq で圏論やってるのかという話
  • 存在性と唯一性で構成される普遍性を「函数とその性質」という形に変換して記述した
  • 証明を割愛するという暴挙
@mathink
mathink / coq_cat_functor.md
Created April 3, 2020 00:01
Coq で圏論：函手とその等価性
title tags author slide
Coq で圏論：函手とその等価性
Coq Coq-8.5
mathink
false

まとめ

  • Coq 上で函手と圏の圏を定義した
  • 具体例もいくつか作ってみた
  • 函手の等価性が少し面倒だよ
@mathink
mathink / coq_cat_natrans.md
Created April 3, 2020 00:01
Coq で圏論：自然変換とデータ型
title tags author slide
Coq で圏論：自然変換とデータ型
Coq Coq-8.5
mathink
false

まとめ

  • Coq 上で自然変換を定義
  • 米田の補題を示してみた(証明そのものは省略)
  • list とか tree と自然変換の関連を見た
@mathink
mathink / coq_pattern_in_arguments.md
Created April 3, 2020 00:00
Coq: 引数にパターンが使えるようになったので試してみた
Error in user YAML: (<unknown>): mapping values are not allowed in this context at line 1 column 11
---
title: Coq: 引数にパターンが使えるようになったので試してみた
tags: Coq Coq-8.6
author: mathink
slide: false
---

まえおき

Coq の 8.6 が出た ので CHANGES を覗いてみたら

@mathink
mathink / coq_primitive_projection.md
Created April 2, 2020 23:59
Coq: Set Primitive Projections と injection タクティックのお話
Error in user YAML: (<unknown>): mapping values are not allowed in this context at line 1 column 11
---
title: Coq: Set Primitive Projections と injection タクティックのお話
tags: Coq Coq-8.5
author: mathink
slide: false
---

まとめ

  • Set Primitive Projections 時は Record と injection の相性が悪いよ
  • Unset Primitive Projections するか、 Inductive で定義してアクセサを別途定義する形にするといいかもね