Skip to content

Instantly share code, notes, and snippets.

View gyu-don's full-sized avatar

Takumi Kato gyu-don

View GitHub Profile
@gyu-don
gyu-don / concat_is_monad.v
Last active February 22, 2020 11:26
リストのリストをリストにするやつがモナドであることを示しました。
Require Import List.
Import ListNotations.
Theorem concat_assoc(X: Type):
forall tttx: list (list (list X)), (concat (concat tttx)) = (concat (map (@concat X) tttx)).
Proof.
intros.
induction tttx.
simpl. reflexivity.
simpl. rewrite <- IHtttx. apply concat_app.
from blueqat import Circuit, pauli, vqe
from blueqat.pauli import qubo_bit as q
from math import pi
import numpy as np
def an(index):
return 0.5 * pauli.X[index] + 0.5j * pauli.Y[index]
def cr(index):
return 0.5 * pauli.X[index] - 0.5j * pauli.Y[index]
@gyu-don
gyu-don / chap3.v
Created September 30, 2019 03:43
Coq/SSReflect/MathComp Chapter 3
(* 3.1 *)
Inductive 紅白玉 :=
| 赤玉
| 白玉.
(* 3.2 *)
Print list.
(*
Inductive list (A : Type) : Type :=
nil : list A
@gyu-don
gyu-don / はじめてのblueqat.ipynb
Last active December 28, 2018 02:08
はじめてのBlueqat.ipynb
Loading
Sorry, something went wrong. Reload?
Sorry, we cannot display this file.
Sorry, this file is invalid so it cannot be displayed.
@gyu-don
gyu-don / blueqat_optuna_minimizer.py
Created December 3, 2018 11:46
Blueqat VQE minimizer using PFN's Optuna library
import optuna
def get_optuna_minimizer(n_trials, study=None):
if study is None:
study = optuna.create_study()
def minimizer(objective, n_params):
def optuna_objective(trial):
params = [trial.suggest_uniform(f'params[{i}]', 0.0, 1.0) for i in range(n_params)]
return objective(params)
study.optimize(optuna_objective, n_trials=n_trials)
@gyu-don
gyu-don / wildqat_4x4sudoku.ipynb
Created November 4, 2018 04:16
wildqatで4x4数独
Loading
Sorry, something went wrong. Reload?
Sorry, we cannot display this file.
Sorry, this file is invalid so it cannot be displayed.
@gyu-don
gyu-don / Dockerfile
Last active September 17, 2018 13:32
sqaod Dockerfile
FROM nvidia/cuda:9.2-runtime-ubuntu16.04
RUN apt update && \
apt install -y --no-install-recommends apt-transport-https curl python-pip python-setuptools ipython && \
. /etc/lsb-release && \
(echo "deb [arch=amd64] https://shinmorino.github.io/sqaod/ubuntu ${DISTRIB_CODENAME} multiverse" | tee /etc/apt/sources.list.d/sqaod.list) && \
(curl -s -L https://shinmorino.github.io/sqaod/gpgkey | apt-key add -) && \
apt update && apt install -y libsqaodc libsqaodc-dev libsqaodc-cuda-9-2 && pip install sqaod
CMD ipython
@gyu-don
gyu-don / c.fish
Created September 7, 2018 03:27
fish_functions
function c
if test (count $argv) -eq 0
cd
else if test (count $argv) -gt 1
echo "Too many arguments" >&2
else if test -d $argv[1]
cd $argv[1]
else if test ! -e $argv[1]
echo "Not exists" >&2
else if test (head -26 $argv[1] | wc -l) -lt 26
@gyu-don
gyu-don / reduce.cu
Created September 12, 2017 20:12
CUDA reduction
// This software contains source code provided by NVIDIA Corporation.
// http://docs.nvidia.com/cuda/eula/index.html#nvidia-cuda-samples-end-user-license-agreement
#include <cuda_runtime.h>
__global__ void reduce0(int *g_idata, int *g_odata, unsigned int n)
{
// shared memoryは、うまく使えば速度が速い。(ここでは、うまく使ってない。後で直す)
// 同じブロック内のスレッド間で共有される。
extern __shared__ int sdata[];
@gyu-don
gyu-don / bingo.cu
Created September 2, 2017 07:39
CUDAの練習。100万人ビンゴ大会
#include <stdio.h>
#include <inttypes.h>
#include <stdlib.h>
#include <cuda_runtime.h>
#include <curand_kernel.h>
__constant__ uint8_t seq[75];
__device__ void make_card(uint8_t *card)
{