314maro’s gists

314maro / conat.hs

Created July 5, 2014 05:10

http://msakai.jp/d/?date=20100628 を参考にした前に挫折した覚えがあるがよくよく考えてみればfoldnとnatを対応させたのだからunfoldnとconatを対応させるだけだった

	{-# LANGUAGE RankNTypes, ExistentialQuantification #-}

	-- forall X, N -> (X + 1 -> X) -> X
	-- N -> (forall X, (X + 1 -> X) -> X)
	-- => forall X, (X + 1 -> X) -> X
	--
	-- forall X, (X -> X + 1) -> X -> N
	-- (exists X, (X -> X + 1) * X) -> N
	-- => exists X, (X -> X + 1) * X

314maro / README

Last active August 29, 2015 14:02

Conway's game of life

main' に初期状態を与えればいい

314maro / Output

Last active August 29, 2015 14:02

cellar automata

314maro / 9.v

Created June 16, 2014 15:53

繰り返しを使うっぽい

	Module Q41.

	Ltac split_all := try (split; split_all).

	Lemma bar :
	forall P Q R S : Prop,
	R -> Q -> P -> S -> (P /\ R) /\ (S /\ Q).
	Proof.
	intros P Q R S H0 H1 H2 H3.
	split_all.

314maro / 8.v

Created June 16, 2014 15:52

適当に同値関係定めればいけそうだけど面倒になりそう… うまくやる方法があるのかな

	Module Q36.
	Require Import ZArith.

	Section Principal_Ideal.
	Variable a : Z.

	Definition pi : Set := { x : Z \| ( a \| x )%Z }.

	Program Definition plus(a b : pi) : pi := (a + b)%Z.
	Next Obligation.

314maro / AVL.cpp

Last active August 29, 2015 14:02

できたかもしれない!

	#include <iostream>
	#include <stack>
	#include <utility>
	#include <exception>

	namespace Map {
	enum MapTag { Left, Right, Equal };

	template <typename K, typename T>
	struct Map {

314maro / AVL.hs

Last active August 29, 2015 14:02

AVL木によるMap

314maro / tableau.hs

Last active August 29, 2015 14:02

タブローの方法

	{-# LANGUAGE FlexibleContexts #-}

	import qualified Text.Parsec as P
	import Text.Parsec.String (Parser)
	import Data.List (intercalate)
	import Control.Applicative
	import Control.Monad
	import Control.Monad.Reader
	import Control.Monad.State
	import qualified Data.Map as M

314maro / 7.v

Created May 29, 2014 08:48

35がわからない

314maro / 6.v

Created May 28, 2014 15:03

C以外

	Module Q26.
	Require Import NArith.
	Goal (221 * 293 * 389 * 397 + 17 = 14 * 119 * 127 * 151 * 313)%nat.
	Proof.
	apply Nat2N.inj.
	rewrite Nat2N.inj_add.
	rewrite Nat2N.inj_mul. rewrite Nat2N.inj_mul. rewrite Nat2N.inj_mul.
	rewrite Nat2N.inj_mul. rewrite Nat2N.inj_mul.
	rewrite Nat2N.inj_mul. rewrite Nat2N.inj_mul.
	simpl. reflexivity.

maro 314maro