y-taka-23’s gists

y-taka-23 / coq_kleisli.v

Last active December 10, 2015 01:28

Kleisli Construction of Monads (Equivalency of Category Theory Style and Haskell Style)

	(******************************************************)
	(** //// Kliesli Construction of Monads //// *)
	(******************************************************)

	Require Import Logic.FunctionalExtensionality.


	(////////////////////////////////////////////////////)
	(** Preliminaries *)
	(////////////////////////////////////////////////////)

y-taka-23 / coq_mlattice.v

Created December 22, 2012 17:10

An Example of Modular Lattices (The Lattice of Normal Subgroups of a Group)

	(******************************************************)
	(** //// Modular Lattices //// *)
	(******************************************************)

	Section ModularLattice.

	Require Import Relation_Definitions Setoid Morphisms.


	(////////////////////////////////////////////////////)

y-taka-23 / coq_filter.v

Last active May 21, 2018 03:26

Validation of the filter Function (via "Software Foundations" http://www.cis.upenn.edu/~bcpierce/sf/Logic.html)

	(******************************************************)
	(** //// Validation of the "filter" Function //// *)
	(******************************************************)

	Require Import List Bool Lt.

	Section Filter.


	(////////////////////////////////////////////////////)

y-taka-23 / coq_topology.v

Created January 6, 2013 12:24

A Proof of the Elementary Property of Connected Spaces

y-taka-23 / coq_qsort.v

Last active December 11, 2015 01:49

Validation of the Quick Sort

	(******************************************************)
	(** //// Validation of the Quick Sort //// *)
	(******************************************************)

	Section QuickSort.

	Require Import Arith List.
	Require Import Recdef.
	Require Import Sorting.Sorted Sorting.Permutation.

y-taka-23 / coq_quine.v

Last active November 15, 2019 20:44

Quine (Self-Reproducing Program) on Coq

y-taka-23 / coq_stackcomp.v

Created July 27, 2013 07:34

Validation of the Compiler for the Stack Machine (via "Software Foundations" http://www.cis.upenn.edu/~bcpierce/sf/Imp.html.html)

	(*******************************************************)
	(** //// Validation of the Stack Machine Compiler //// *)
	(*******************************************************)

	Require Import List.

	(* Definition : Identifiers *)
	Inductive id : Type :=
	\| Id : nat -> id.

y-taka-23 / alloy_vender.als

Last active July 27, 2018 12:53

Alloy による自動販売機のモデリング

	// ************************************
	// ジュースの自動販売機のモデル
	// ************************************

	open util/ordering[Time]

	// 時刻パラメータ
	sig Time {}

	// 簡略化のため、コインの額面とジュースの種類はそれぞれ 1 種類とする

y-taka-23 / coq_perceptron.v

Created September 17, 2013 11:43

Proof of Novikoff's Perceptron Convergence Theorem (Unfinished)

y-taka-23 / alloy_decimal.als

Created October 9, 2013 16:12

Alloy による十進位取り記数法のモデリング

Cheshire Cat y-taka-23