title | tags | author | slide |
---|---|---|---|
Coq で圏論:随伴、モナド、Kleisli triple |
Coq Coq-8.5 |
mathink |
false |
- Coq 上で随伴とモナドを定義
- Kleisli triple(Haskell でいう Monad)も定義
- 随伴から、モナドを通じて Kleisli triple を構成してみた
(** 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 .!"). |
(* 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) |
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. |
Set Implicit Arguments. | |
Unset Strict Implicit. | |
Unset Printing Implicit Defensive. | |
Set Reversible Pattern Implicit. | |
Generalizable All Variables. | |
Set Primitive Projections. | |
Set Universe Polymorphism. |
Set Implicit Arguments. | |
Unset Strict Implicit. | |
Require Import Setoids.Setoid Morphisms. | |
Generalizable All Variables. | |
Class Setoid := | |
{ | |
carrier: Type; | |
equal: carrier -> carrier -> Prop; |
Set Implicit Arguments. | |
Unset Strict Implicit. | |
Generalizable All Variables. | |
Require Export Basics Tactics Coq.Setoids.Setoid Morphisms. | |
Structure Setoid := | |
{ | |
carrier:> Type; |
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) := |
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 := | |
{ |