Skip to content

Instantly share code, notes, and snippets.

View msakai's full-sized avatar

Masahiro Sakai msakai

236 followers · 202 following
View GitHub Profile
@msakai
msakai / ZERO.v
Created May 4, 2011 09:40
Empty Category
Require Export Category.
Set Implicit Arguments.
Unset Strict Implicit.
Inductive Empty : Type := .
(* The category Zero *)
Definition Zero_ob : Type := Empty.
@msakai
msakai / ALG.v
Created May 4, 2011 09:42
Category of F-Algebras
Require Export Functor.
Set Implicit Arguments.
Unset Strict Implicit.
Section alg_def.
Variable (C : Category).
Variable (F : Functor C C).
@msakai
msakai / Allegory.v
Created May 6, 2011 03:52
Definition of Allegory
Require Export Category.
Set Implicit Arguments.
Unset Strict Implicit.
Section allegory.
Variable C : Category.
Variable Op_intersect : forall a b : Ob C, Map2 (Hom a b) (Hom a b) (Hom a b).
Variable Op_converse  : forall a b : Ob C, Map (Hom a b) (Hom b a).
@msakai
msakai / file_rwpms_wcnf_L3_V100_C600_H100_0.wcnf
Created July 10, 2011 23:25
LP file converted from wpms_random/wpmax3sat/hi/file_rwpms_wcnf_L3_V100_C600_H100_0.wcnf of MAX-SAT Evaluation 2011 Benchmark
c Weighted CNF
c from Selman's wff generator
p wcnf 100 600 3237
3237 2 5 30 0
3237 -68 -41 -22 0
3237 62 -58 9 0
3237 77 -70 42 0
3237 -94 -17 -26 0
3237 -72 84 2 0
3237 51 60 39 0
@msakai
msakai / DistributiveLattice.als
Created July 27, 2011 00:04
Alloy model that demonstrate every non-distributive lattice contains one of the two particular lattices as a subpseudolattice.
sig L {
join, meet : L -> one L
}
one sig top, bot in L {}
fact {
all x, y, z : L {
-- commutativity
x.join[y] = y.join[x]
x.meet[y] = y.meet[x]
@msakai
msakai / excel-sheets-to-csv.js
Created August 11, 2011 12:16
Excelの各シートをCSVファイルに書き出すWSH
var fso = new ActiveXObject("Scripting.FileSystemObject")
var file = fso.GetFile(WScript.Arguments.Item(0))
var dirname = file.ParentFolder.Path
var basename = file.Name
var name = basename.replace(/\.xlsx?$/i, "")
var Excel = {
xlCSV : 6
}
@msakai
msakai / InequationalNumberPlace.als
Created August 12, 2011 13:49
『不等号ナンプレ』(しんや+ドロップ)の表紙の問題をAlloyで解く
abstract sig Number {
data: Number -> one Number,
lt : set Number
}
one sig N1, N2, N3, N4, N5 extends Number {}
fact {
lt = ^(N1->N2 + N2->N3 + N3->N4 + N4->N5)
}
@msakai
msakai / LawvereFixedPointTheorem.v
Created August 13, 2011 16:31
Lawvere's fixed-point theorem formalized in Coq with ConCaT
(*
Lawvere's fixed point theorem.
References:
F. W. Lawvere and S. H. Schanuel, Conceptual Mathematics: A First Introduction to Categories.
Cambridge University Press, Nov. 1997.
*)
Require Export Category.
Require Export CCC.
@msakai
msakai / ALG2.v
Created August 16, 2011 17:35
If (μFG, in) is initial FG-algebra, then (GμFG, Gin) is initial GF-algebra.
(*
Let F: C→D and G: D→C be functors.
If (μFG, in) is initial FG-algebra, then (GμFG, Gin) is initial GF-algebra.
Based on https://gist.github.com/955007
*)
Require Export Functor.
Set Implicit Arguments.
Unset Strict Implicit.
@msakai
msakai / JMeq.agda
Created September 26, 2011 11:32
John Major's equality in Agda2
-- John Major's equality is definable in Agda2!
module JMeq where
data JMeq {A : Set} (a : A) : {B : Set} → B → Set where
refl : JMeq a a
JMeq-elim
: {A : Set} → (a a' : A) → (e : JMeq a a')
→ (P : (a' : A) → JMeq a a' → Set)
→ P a refl → P a' e