個人的おすすめアクションゲームリスト

気が向いたら画像付けたりします。

Rabi-Ribi

store.steampowered.com

平成一の神アクションゲーム。キャラが可愛い。ボスが多い。メトロイド系。やりこみ要素も多め。

Terraria

store.steampowered.com

王道。オンライン協力プレイ可。

Iconoclasts

store.steampowered.com

ボスが多め。ストーリーが面白い。謎解き寄り。

Joggernauts

store.steampowered.com

4人までローカル協力プレイ可。複数人でやると楽しい。

Touhou Luna Nights

store.steampowered.com

メトロイド系。難易度は低め。ボリュームもそんなに。でも全体的にクオリティが高い。

Cuphead

store.steampowered.com

2人でローカル協力プレイ可。ほぼボス戦のみ。

Celeste

store.steampowered.com

難しいけどセーブポイントが多いのでアクション苦手でも楽しめると思う。

ギミックが多くて面白い。

Evoland 2

store.steampowered.com

これは何ゲーだ?アクションRPG?横スクロールアクション?縦スクロールアクション?シューティング?パズル?ストラテジー?格ゲー?音ゲー?カードゲーム?全部です。

面白いけど、英語つらいとつらいです。

エリィのアクション

xtalsword.jp

謎解き要素強めの死にゲー。演出が面白い。steamだと日本語版がないことに注意。

Furi

store.steampowered.com

ボスのみ。反射神経ゲー。そこそこ難しい。

個人的おすすめパズルゲームリスト

PVだけで十分ってやつはコメント付けてません。

気が向いたら画像付けたりします。

Baba Is You

store.steampowered.com

平成一の神ゲー。気付きや驚きの連続でずっと面白い。ボリュームもある。

パズルゲームで1500円は高い方だけど、たとえ5000円だったとしても買って後悔しないと思う。

Ittle Dew

store.steampowered.com

パズルしかないゼルダって感じ。謎解き寄りのパズル。実績集めがかなり楽しい。一周目クリアまではチュートリアル

あと地味に重要なことだけど、日本語化が上手く出来ていてセリフが面白い。

これ面白くても Ittle Dew 2 はただのアクションなのでおすすめしません。

Pipe Push Paradise

store.steampowered.com

シンプルだけど奥深い。気付きや驚きがまあまああって良い。倉庫番が好きなら絶対楽しめる。

かむたこ

www.vector.co.jp

無料。古いゲームだけど面白いからやってみて。超むずいけど。

ゼリーのパズル

qrostar.skr.jp

無料。

ハナノパズル、ハナノパズル2

qrostar.skr.jp

qrostar.skr.jp

無料。

Recursed

store.steampowered.com

最序盤は簡単なんだけど途中から一気に難しくなって、頭壊れるギミックが現れる。

終盤はどのステージも重めで結構疲れるけど解けたときの達成感は大きい。

是非無料の DLC までプレイしてほしい。

Portal 2

store.steampowered.com

王道だよね。2人オンライン協力プレイ可。

ラビ×ラビ

www.silverstar.co.jp

PCじゃできないけど...

べくたーぷらいむ

n-linear.org

ぷよぷよとか好きなら

Human: Fall Flat

store.steampowered.com

8人までローカル・オンライン協力プレイ可。友達とやると楽しい。

Hiding Spot

store.steampowered.com

ボリューム少ないし操作難しいけどいくつか気付きがあって値段分は遊べる。

The Witness

store.steampowered.com

小さいパズルを大量に解くタイプ。ルールが与えられないので謎解き寄り。

A Good Snowman Is Hard To Build

store.steampowered.com

操作性はちょっと悪いかも。普通にパズルとしてまあまあだし、すごく大きな驚きがある。超むずいパズルはないけど。

Lara Croft Go

store.steampowered.com

簡単なステージがしばらく続いてつらいし操作性悪いけど終盤になると面白いのでパズルやりたいけどやるパズルがねえって人にはおすすめ。

Push Pull

store.steampowered.com

操作性悪いけどまあ悪くないゲーム。やるゲームがないなら。

vscoqでproof viewが出ない

vscoqは3年前から更新されていない

vscoqのバージョンを1.32くらいに下げると動くが、自動更新まわりの設定とか使い分けるのとかめんどい

よく見ると↓に移動したらしいので入れてみたら動いた

github.com

Requirements

  • node

Installation

git clone https://github.com/coq-community/vscoq.git
cd vscoq
npm i -g vsce
make vsix
code --install-extension client/vscoq-0.2.8.vsix

nまでの整数からm個ランダムに選ぶ

testlib.h を使ったgenerator用のライブラリです。

vector<long long> select(n, m)

\{0, 1, ..., n-1\} から m 要素をランダムに取り出します。戻り値はソートされています。

vector<long long> grouping(n, m, min_size=0)

n 個を m グループにランダムに分けます。戻り値はグループサイズの配列です。

計算量はどちらも O(mlogm) です。

配列 v から m 要素ランダムに取り出す関数だけ必要なら、これを使わずに shuffle して先頭 m 要素取り出す方法でも良いと思います。
n が小さいときもこれでいけます。

アルゴリズム

grouping は select を使っています。なので、select についてのみ解説します。

select(n, m) は  n \geq 2m、すなわち半分以下しか select しない場合は、ランダムに選んでまだ選ばれていなかったら追加し、そうでなければまだ選ばれていないものが選ばれるまで再抽選し続けることを m 回繰り返します。少なくとも半分はまだ選ばれていないので、1回あたり抽選回数の期待値は2回以下となり、平均して O(m) が達成されます。

 n > 2m の場合、選ばないものを select(n, n-m) によって選びます。

// select S ⊆ {0, 1, ..., n-1} and |S| = m
std::vector<long long> select(long long n, int m) {
  assert(m <= n);
  if (m * 50 <= n) {
    std::set<long long> used;
    std::vector<long long> res(m);
    for (int i = 0; i < m; ++i) {
      long long x;
      do {
        x = rnd.next(n);
      } while (used.count(x) > 0);
      res[i] = x;
      used.insert(x);
    }
    std::sort(std::begin(res), std::end(res));
    return res;
  }
  if (m * 2 <= n) {
    std::vector<bool> used(n, false);
    std::vector<long long> res(m);
    for (int i = 0; i < m; ++i) {
      long long x;
      do {
        x = rnd.next(n);
      } while (used[x]);
      res[i] = x;
      used[x] = true;
    }
    std::sort(std::begin(res), std::end(res));
    return res;
  }
  std::vector<long long> unselect = select(n, n-m);
  std::vector<long long> res;
  long long j = 0;
  for (int i = 0; i < n; ++i) {
    while (j < unselect.size() && unselect[j] < i) ++j;
    if (j < unselect.size() && unselect[j] == i) {
      continue;
    }
    res.push_back(i);
  }
  return res;
}

// select m elements from v
template<class T>
std::vector<T> select(const std::vector<T>& v, const long long m) {
  std::vector<long long> sel = select(v.size(), m);
  std::vector<T> res(m);
  for (int i = 0; i < m; ++i) {
    res[i] = v[sel[i]];
  }
  std::sort(std::begin(res), std::end(res));
  return res;
}

// res_1 + ... + res_gsz = n
// res_1, ..., res_gsz >= min_size
std::vector<long long> grouping(long long n, long long gsz, long long min_size=0) {
  assert(1 <= gsz && min_size * gsz <= n);
  n -= min_size * gsz;
  std::vector<long long> pos = select(n+gsz-1, gsz-1);
  pos.push_back(n+gsz-1);
  std::vector<long long> res(gsz);
  long long prv = -1;
  for (int i = 0; i < gsz; ++i) {
    res[i] = pos[i] - prv - 1 + min_size;
    prv = pos[i];
  }
  return res;
}

累積帰納法の一般化

TopProver で行われたCoqコンテストに参加して、モチベが上がったため、coqのライブラリを整備することに。
とりあえず便利なので累積帰納法を整備した。
自然数に関する累積帰納法だけだと不便なことがあるので、より一般化し、任意の型 X の f による nat への写像に関する累積帰納法を扱えるようにした。

これによって

  • l : list X の 長さ に関する帰納法
  • l : list nat の 合計 に関する帰納法
  • l : list nat の 長さ + 合計 に関する帰納法 (これ便利)
  • (n, m) : nat * natn + m に関する帰納法

などが簡単にでき、超便利。

(*
  Lib for induction

 累積帰納法(cov_induction)
  usage:
    apply (cov_induction (fun n => ...)).

 一般化累積帰納法(mapped_cov_induction)
  example:
    apply (cov_induction (fun l => length l) (fun l => ...)).
*)

Require Import Le Omega.

Theorem cov_induction: forall P: nat -> Prop, (forall n: nat, ((forall (m: nat), m < n -> P m) -> P n)) -> (forall n: nat, P n).
Proof.
  assert(Lem: forall P: nat -> Prop, (forall n: nat, ((forall (m: nat), m < n -> P m) -> P n)) -> (forall n m: nat, n < m -> P n)). {
    intros P IH n m. generalize dependent n.
    induction m.
    - intros n H. inversion H.
    - intros n H. inversion H.
    -- apply IH. apply IHm.
    -- apply IHm. apply H1.
  }
  - intros P H1 n.
    apply Lem with (m := S n).
  -- apply H1.
  -- apply le_n_S. apply le_refl.
Qed.

Theorem mapped_cov_induction:
  forall {X} (f: X -> nat) (P: X -> Prop), (forall x: X, (forall y: X, f y < f x -> P y) -> P x) -> forall z, P z.
Proof.
  intros X f P.
  generalize (cov_induction (fun n => forall (x: X), n = f x -> P x)); intro Ind.
  intros Asm1 z. apply Ind with (n := f z).
  - intros n IH x H.
    apply Asm1.
    intros y H4.
    apply IH with (m := f y); omega.
  - reflexivity.
Qed.

(* endlib: induction *)

opam install z3 が "clang: error: unsupported option '-fopenmp'" で落ちる

解決策

ocamlc, ocamlopt の -cc オプションで clang の代わりに gcc を指定させる.
バッドノウハウだが, ocamlc, ocamlopt, ocamlfind を wrap する.

前提

  • gcc にパスが通っている
  • ocmalfind がinstallされている

コマンドを理解してから使ってください

ocamlcのwrap用sh
cc=`which gcc`

dir="$(dirname $(which ocamlc))"

if [ ! -e $dir/ocamlc_ -a -e $dir/ocamlc ]; then
  mv "$dir/ocamlc" "$dir/ocamlc_"
fi

if [ -e $dir/ocamlc_ ]; then
  echo "#\!/bin/sh
\`dirname \$0\`/ocamlc_ \"\$@\" -cc \"$cc\"
" > "$dir/ocamlc"
  chmod 755 "$dir/ocamlc"
fi
ocamlfindのwrap用sh
cc=`which gcc`

dir="$(dirname $(which ocamlfind))"

if [ ! -e $dir/ocamlfind_ -a -e $dir/ocamlfind ]; then
  mv "$dir/ocamlfind" "$dir/ocamlfind_"
fi

if [ -e $dir/ocamlfind_ ]; then
  echo "#\!/bin/sh

if [ \"\$1\" = \"ocamlc\" ] || [ \"$1\" = \"ocamlopt\" ]; then
  \`dirname \$0\`/ocamlfind_ \"\$@\" -cc \"$cc\"
else
  \`dirname \$0\`/ocamlfind_ \"\$@\"
fi" > "$dir/ocamlfind"
  chmod 755 $dir/ocamlfind
fi