Skip to content

Instantly share code, notes, and snippets.

View mathink's full-sized avatar

m mathink

11 followers · 1 following
View GitHub Profile
@mathink
mathink / coq_cat_adj_monad_kt.md
Created April 2, 2020 23:57
Coq で圏論：随伴、モナド、Kleisli triple
title Coq で圏論：随伴、モナド、Kleisli triple
tags Coq Coq-8.5
author mathink
slide false

まとめ

  • Coq 上で随伴とモナドを定義
  • Kleisli triple(Haskell でいう Monad)も定義
  • 随伴から、モナドを通じて Kleisli triple を構成してみた
@mathink
mathink / coq_nat_to_string_easy.md
Last active April 3, 2020 00:08
Coq: nat を string で十進表記する
Error in user YAML: (<unknown>): mapping values are not allowed in this context at line 1 column 11
---
title: Coq: nat を string で十進表記する
tags: Coq
author: mathink
slide: false
---

まとめ

  • n: nat を十進表記の文字列に変換してみた
  • Functional Scheme 使えば大した手間はかからない。
@mathink
mathink / string_nat_with_proof.v
Created December 7, 2018 14:44
文字列と自然数の相互変換(証明付き)。
(** numeral string <-> nat *)
Require Import Arith List Omega Ascii String.
Require Import Recdef Wf_nat Program.Wf Program.Tactics.
Require Import ProofIrrelevance.
Set Implicit Arguments.
Unset Strict Implicit.
(** * 0. Utilities *)
Notation "x .!" := (proj1_sig x) (at level 2, left associativity, format "x .!").
@mathink
mathink / show_with_proof.v
Last active December 21, 2016 14:06
nat を string で十進表記する(ハードモード)
(* safe translator from nat to string *)
Require Import Arith List Omega Ascii String Recdef Wf_nat Program.Wf Program.Tactics.
Generalizable All Variables.
Fixpoint div10 (n: nat): nat * nat :=
match n with
| S (S (S (S (S (S (S (S (S (S n'))))))))) =>
let (q, r) := div10 n' in (S q, r)
@mathink
mathink / print_nat.v
Last active December 15, 2016 12:48
Coq の nat を十進表記で string に変換
Require Import Arith Ascii String Recdef Wf_nat.
Fixpoint div10 (n: nat): nat * nat :=
match n with
| S (S (S (S (S (S (S (S (S (S n'))))))))) =>
let (q, r) := div10 n' in (S q, r)
| digit => (0, digit)
end.
Eval compute in div10 8.
@mathink
mathink / cat_on_coq_201612.v
Last active December 7, 2016 13:07
Coq で圏論 2016 年 12 月 ver.
Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.
Set Reversible Pattern Implicit.
Generalizable All Variables.
Set Primitive Projections.
Set Universe Polymorphism.
@mathink
mathink / mpl_state.v
Created May 19, 2016 15:22
predicate lifting 使ってモナディックな計算についてホーア論理的な形式で命題記述できるようにする仕組みを Maybe モナドと State モナドに具体化したやつ。
Set Implicit Arguments.
Unset Strict Implicit.
Require Import Setoids.Setoid Morphisms.
Generalizable All Variables.
Class Setoid :=
{
carrier: Type;
equal: carrier -> carrier -> Prop;
@mathink
mathink / Polynomial.v
Created April 28, 2016 12:40
Set Implicit Arguments.
Unset Strict Implicit.
Generalizable All Variables.
Require Export Basics Tactics Coq.Setoids.Setoid Morphisms.
Structure Setoid :=
{
carrier:> Type;
@mathink
mathink / adv_cal_2015_1205_answer.v
Created December 11, 2015 14:27
https://gist.github.com/mathink/b4d071232b35dfd814a1 の証明付きバージョン
Set Implicit Arguments.
Unset Strict Implicit.
Require Import Arith.
Notation "g \o f" := (fun x => g (f x)) (at level 50, left associativity).
Notation Id X := (fun x: X => x).
Notation Endo X := (X -> X).
Definition ext_eq {X Y: Type}(f g: X -> Y) :=
@mathink
mathink / check_with_type_error.v
Created December 8, 2015 09:34
Set Implicit Arguments.
Unset Strict Implicit.
Definition True_or_Eq (P: Prop)(dec: {P}+{~P}): Prop := if dec then True else 0 = 0.
Definition I_or_0eq0 (P: Prop)(dec: {P}+{~P}): True_or_Eq dec :=
if dec as dec' return True_or_Eq dec' then I else eq_refl 0.
Definition onlyTrue (H: True): True := H.
Class dec_Type :=
{