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 / gist:5893703
Created June 30, 2013 03:24
型クラスの引数に型クラス内部で別名を与えることで，異なる実体に共通の記法を提供するというやり方． 既にやっているライブラリとかもあると思いますが，メモ的な意味で投下．
Definition relation (A: Type) := A -> A -> Prop.
(* Definition: Equivalence relation *)
Reserved Notation "x == y" (at level 80, no associativity).
Class Equivalence {A: Type}(eq: relation A) :=
{
equiv_eq := eq
where "x == y" := (equiv_eq x y);
@mathink
mathink / monad_coercion.v
Created July 20, 2013 17:49
(* Monad with Coercion *)
Definition relation (A: Type) := A -> A -> Prop.
Hint Unfold relation.
Reserved Notation "x == y" (at level 85, no associativity).
Class Equivalence (A: Type) :=
{
equiv_eq: relation A where "x == y" := (equiv_eq x y);
equiv_refl:
@mathink
mathink / monad_coercion.v
Created July 21, 2013 06:28
(* Monad with Coercion *)
Require Import ssreflect.
Definition relation (A: Type) := A -> A -> Prop.
Hint Unfold relation.
Definition refl {A: Type}(R: relation A)
:= forall a, R a a.
Definition sym {A: Type}(R: relation A)
@mathink
mathink / MetaCategory_on_Coq
Created August 28, 2013 13:14
「圏論の基礎」に倣いまして，メタ圏の対象と射をそれぞれ Setoid にするという形で圏の定義を行いました． Coq で圏論をしっかりやるには，定義する際にも証明項を自分で作って云々，というパートが要るような雰囲気が漂っていた今日このごろですが，そうなりました．
Class Category :=
{ objects:> Setoid;
arrows:> Setoid;
domain: Map arrows objects;
codomain: Map arrows objects;
identity: Map objects arrows;
compose: forall (f g: arrows)(composable: codomain f == domain g), arrows;
@mathink
mathink / function_setoid
Created August 28, 2013 16:22
JMeq的なやつといろいろ使って，関数全体を Setoid に仕立てあげた．が，此処から先に進めない． おそらく，Setoid と言いつつキャリアが Type であることが超問題なのであろーう．
(* Cat_on_Coq の Setoid を使ってるよ *)
Inductive function_eq {X Y: Set}(f: X -> Y): forall (X' Y': Set)(g: X' -> Y'), Prop :=
| feq_def: forall f': X -> Y, (forall x: X, f x = f' x) -> function_eq f f'.
Lemma function_eq_refl:
forall (Xf Yf: Set)(f: Xf -> Yf),
function_eq f f.
Proof.
move => Xf Yf f.
@mathink
mathink / Typoid_Typoid.v
Created September 3, 2013 15:38
Typoid_Typoid は Universe inconsistency になる．のは，そりゃそうだろって感じなんですが，Typoid_is_Typoid が作れるのはいい感じだなぁ，などと思っている．
Class is_Typoid (carrier: Type): Type :=
{ equal: relation carrier;
prf_equiv :> Equivalence equal }.
Class Typoid: Type :=
{ typoid_carrier: Type;
is_typoid:> is_Typoid typoid_carrier }.
Coercion typoid_carrier: Typoid >-> Sortclass.
Definition eq_Typoid (S T: Typoid) :=
@mathink
mathink / binomial_prime_exp.v
Last active December 22, 2015 13:59
Ssreflect の練習． http://www.tcp-ip.or.jp/~n01/math/binomial.pdf を参考に補題作ってごりごりやってみた．大変だった... でも楽しい!
Require Import
Ssreflect.ssreflect Ssreflect.ssrbool Ssreflect.ssrfun
Ssreflect.ssrnat Ssreflect.prime Ssreflect.seq
Ssreflect.div Ssreflect.binomial Ssreflect.bigop.
Lemma coprime_plus a b:
coprime a (b+a) -> coprime b (b+a).
Proof.
by rewrite /coprime gcdnDl gcdnDr gcdnC.
Qed.
@mathink
mathink / hors.v
Last active December 22, 2015 17:19
HORS を Coq で扱うにはどうしたらいいんでしょーか．
(* HORS? *)
Set Implicit Arguments.
Require Import List.
CoInductive List (A: Set): Set :=
| Nil | Cons (head: A)(tail: List A).
Arguments Nil {A}.
Arguments Cons {A}(head)(tail).
@mathink
mathink / 1350.v
Created September 11, 2013 15:38
ユニバァァァス!!
Check (1: nat: Set: Type: Type: Type: Type: Type: Type: Type: Type: Type: Type: Type: Type: Type: Type: Type: Type: Type: Type: Type: Type: Type: Type: Type: Type: Type: Type: Type: Type: Type: Type: Type: Type: Type: Type: Type: Type: Type: Type: Type: Type: Type: Type: Type: Type: Type: Type: Type: Type: Type: Type: Type: Type: Type: Type: Type: Type: Type: Type: Type: Type: Type: Type: Type: Type: Type: Type: Type: Type: Type: Type: Type: Type: Type: Type: Type: Type: Type: Type: Type: Type: Type: Type: Type: Type: Type: Type: Type: Type: Type: Type: Type: Type: Type: Type: Type: Type: Type: Type: Type: Type: Type: Type: Type: Type: Type: Type: Type: Type: Type: Type: Type: Type: Type: Type: Type: Type: Type: Type: Type: Type: Type: Type: Type: Type: Type: Type: Type: Type: Type: Type: Type: Type: Type: Type: Type: Type: Type: Type: Type: Type: Type: Type: Type: Type: Type: Type: Type: Type: Type: Type: Type: Type: Type: Type: Type: Type: Type: Type: Type: Type: Type: Type: Type: Type: Type: Type: Type: Ty
@mathink
mathink / digraph.v
Created September 28, 2013 18:02
(* Directed finite graph *)
Require Import
Ssreflect.ssreflect Ssreflect.ssrbool
Ssreflect.ssrfun Ssreflect.eqtype
Ssreflect.ssrnat Ssreflect.seq
Ssreflect.path Ssreflect.fintype
Ssreflect.fingraph.