Skip to content

Instantly share code, notes, and snippets.

View y-taka-23's full-sized avatar

Cheshire Cat y-taka-23

83 followers · 31 following
View GitHub Profile
@y-taka-23
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
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
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
y-taka-23 / coq_topology.v
Created January 6, 2013 12:24
A Proof of the Elementary Property of Connected Spaces
(******************************************************)
(** //// Topology Spaces //// *)
(******************************************************)
Section Topology.
(*////////////////////////////////////////////////////*)
(** Axioms *)
(*////////////////////////////////////////////////////*)
@y-taka-23
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
y-taka-23 / coq_quine.v
Last active November 15, 2019 20:44
Quine (Self-Reproducing Program) on Coq
Require Import Ascii String.
Open Scope string_scope.
Definition Q : string := "
Eval compute in ""
Require Import Ascii String.
Open Scope string_scope.
Definition Q : string := "" ++ """" ++ Q ++ """" ++ ""."" ++ Q.".
Eval compute in "
Require Import Ascii String.
Open Scope string_scope.
@y-taka-23
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
y-taka-23 / alloy_vender.als
Last active July 27, 2018 12:53
Alloy による自動販売機のモデリング
// ************************************
// ジュースの自動販売機のモデル
// ************************************
open util/ordering[Time]
// 時刻パラメータ
sig Time {}
// 簡略化のため、コインの額面とジュースの種類はそれぞれ 1 種類とする
@y-taka-23
y-taka-23 / coq_perceptron.v
Created September 17, 2013 11:43
Proof of Novikoff's Perceptron Convergence Theorem (Unfinished)
Section Perceptron.
Require Import QArith List.
Inductive Q_vector : nat -> Set :=
| vnil : Q_vector O
| vcons : forall n : nat,
Q -> Q_vector n -> Q_vector (S n).
Implicit Arguments vcons [n].
Notation "x ; v" := (vcons x v)
@y-taka-23
y-taka-23 / alloy_decimal.als
Created October 9, 2013 16:12
Alloy による十進位取り記数法のモデリング
// ************************************
// 十進法による符号なし整数演算のモデル
// ************************************
open util/ordering[Position]
// ------------------------------------
// 位取り記数法のモデリング
// ------------------------------------