mathink’s gists

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 / 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 / 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 / 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 / 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 / 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 / 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 / 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 / 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 / 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.

m mathink