kik’s gists

kik / gist:717629

Created November 27, 2010 06:17

kik / A.v

Created May 8, 2011 15:37

GCJ 2011 Qual-A 全然だめぽ。下界のひとつを与えられたけど最小かどうか証明できてないバージョン

	Require Import ZArith.
	Require Import Zminmax.
	Require Import List.
	Open Scope Z_scope.

	Inductive Robo : Set := Blue \| Orange.
	Inductive Order : Set := order : Robo -> Z -> Order.

	Inductive Move : Set := Left \| Right \| Push \| Stay.
	Inductive Moves : Set := moves : Move -> Move -> Moves.

kik / A2.v

Created May 8, 2011 15:40

GCJ 2011 Qual-A やり直し。今度は正しいパスを得られてるけど、最小生の証明ができてない。まだ途中

	Require Import ZArith.
	Require Import List.
	Open Scope Z_scope.

	Inductive Robo : Set := Blue \| Orange.
	Inductive Order : Set := order : Robo -> Z -> Order.

	Inductive Move : Set := Left \| Right \| Stay.
	Inductive Moves : Set :=
	\| moves : Move -> Move -> Moves

kik / Q.v

Created May 13, 2011 19:20

CoqでLeibniz EqなQを書いてみる

	Require Import ZArith Znumtheory.

	Open Scope Z_scope.

	Section ZP.

	Record ZP := zp { quot : Z; denom : positive }.

	Definition ZP_eq (x y : ZP) :=
	quot x * (Zpos (denom y)) = quot y * (Zpos (denom x)).

kik / GCJ2011Qual-A.v

Created May 14, 2011 01:40

GCJ 2011 Qual-A さらにやり直し。今度こそ完璧な証明が書けたはずだ

	Require Import ZArith.
	Require Import List.
	Open Scope Z_scope.

	Set Implicit Arguments.
	Unset Strict Implicit.

	Inductive Robo : Set := Blue \| Orange.
	Inductive Order : Set := order : Robo -> Z -> Order.

kik / GCJ2011Qual-Assr.v

Created May 22, 2011 10:44

GCJ 2011 Qual-A をssreflectで書いてみた。なんかOpaqueなデータが多くて計算できないし抽出もできなさげになった。ssreflectの雰囲気を見る用

	Require Import ssreflect ssrfun ssrbool eqtype ssrnat div seq.
	Require Import choice fintype tuple finfun ssralg.
	Require Import ssrz smallord.
	Require Import ZArith.

	Set Implicit Arguments.
	Unset Strict Implicit.
	Import Prenex Implicits.

	Inductive Robo : Set := Blue \| Orange.

kik / gist:1019788

Created June 10, 2011 21:12

これか

	Definition foo (x : bool) (e : x = true) := tt.

	Definition bar (x : bool) : unit :=
	match x as y return x = y -> unit with
	\| true => fun e => foo x e
	\| false => fun _ => tt
	end (eq_refl x).

kik / gist:1046226

Created June 25, 2011 06:18

ST and runST interface in Coq (WIP)

	Class fmonad (M : (Type -> Type) -> Type) := {
	fmreturn : forall {A : Type -> Type} {B}, (B -> A B) -> M A;
	fmbind : forall {A B : Type -> Type} {C}, M A -> ((C -> A C) -> M B) -> M B
	}.

	Class ST (T : (Type -> Type) -> Type) := {
	monadOfST :> fmonad T;
	runST : forall {A}, T (fun _ => A) -> A
	}.

kik / gist:1047493

Created June 26, 2011 10:35

Coq and Monad

	(*
	* http://mattam.org/repos/coq/prelude/ を改造
	* Matthieu さんおれおれCoq使ってるから通らないところを頑張りつつ、SetoidをSetoidClassで定義してるのに置き換えてみた
	*)

	Require Import Program FunctionalExtensionality Morphisms Classes.Equivalence Setoid.

	Open Scope equiv_scope.
	Open Scope program_scope.
	Local Open Scope signature_scope.

kik / gist:1059873

Created July 2, 2011 08:56

F**king Debian. make command is completely broken

	kik@icfpc-debian:~/tmp$ file /usr/share/ocamlmakefile/OCamlMakefile
	/usr/share/ocamlmakefile/OCamlMakefile: ASCII English text
	kik@icfpc-debian:~/tmp$ cat Makefile
	include /usr/share/ocamlmakefile/OCamlMakefile
	kik@icfpc-debian:~/tmp$ make
	make[1]: Entering directory `/home/kik/tmp'
	make[1]: OCamlMakefile: No such file or directory
	make[1]: *** No rule to make target `OCamlMakefile'. Stop.
	make[1]: Leaving directory `/home/kik/tmp'
	make: *** [byte-code] Error 2

kik kik