---
# System prepended metadata

title: バニラCoqユーザーのためのSsreflectチートシート
tags: [coqtokyo]

---

# バニラCoqユーザーのためのSsreflectチートシート

全く同じ働きをするものへの対応ではないけど、こういうことをやりたいというときに参考になるかも。

### 基本

| 状況 | Coq | Ssreflect |
| -------- | -------- | -------- |
| tacのあと自明なのでターミネーターにしたい|　now tac. | by tac. |
| tacのあと自明なsubgoalを刈りたい | tac; try easy. | tac => //. |
| tacのあとsimplしたい | tac; simpl. | tac => /=. |

### 命題論理

| 状況 | Coq | Ssreflect |
| -------- | -------- | -------- |
| 一つのapply で2つの補題を適用したい | apply H1, H2. | apply/H1/H2. |
|cutしたい|cut (...).| suff H: (...).|
|assertしたい | assert (...). | have H: (...). |

### 帰納法

| 状況 | Coq | Ssreflect |
| -------- | -------- | -------- |
| xs: list X で帰納法を回したいとき| induction xs.     | elim: xs. | 
| x_indを使って帰納法したいとき | induction 1 using x_ind | elim/x_ind. |

### 等式とか

| 状況 | Coq | Ssreflect |
| -------- | -------- | -------- |
| 定義に従って展開 | unfold foo. | rewrite /foo. |
| H: 42=x を使ってxを42にrewriteしたい | rewrite <- H | rewrite -H. |
| H: S a = S b から a = b を得たい | injection H.     | case: H.     | 
| 複数の補題を使ってrewrite | rewrite H1,H2. | rewrite/H1/H2. |
| 同じrewriteを何回も | do 3 rewrite H. | rewrite 3!H. |
| 2番目の出現を書き換える | rewrite H at 2. | rewrite {2}H. |
| cutrewrite | cutrewrite (x = y). | rewrite (_ : x = y). |
| replace | |rewrite [(_ * 1 + 0)addn0.]


### 帰納的述語を扱う


| 状況 | Coq | Ssreflect |
| -------- | -------- | -------- |
| odd 0 -> ... みたいなとき | inversion 1. | move H: exp => v He. case: He H|

## 場合分け

| 状況 | Coq例 | Ssreflect |
| -------- | -------- | -------- |
| 複数の値を一度に場合分したい| case a, b. | case: a b => [...] [...] |
| case_eq | case_eq (exp). | `case H: (exp) => [explicitname\|].`|
| boolのときのcase_eq | case_eq (a <= b). | case: (boolP (a <= b)). |

## reflect関連

| 状況 | Coq例 | Ssreflect |
| -------- | -------- | -------- |
| 帰結が `hoge x` のときに `Hoge x` にしたい  |  | `apply /hogeP.` |
| 前提に `h: hoge x` があるとき | | `move:h => /andP.`

ここで
```coq
hogeP : forall x, reflect (Hoge x) (hoge x)
```
とする。

* https://coq.inria.fr/refman/proof-engine/ssreflect-proof-language.html#interpreting-goals

## タクティック以外のやつ

### Search
Searchコマンドの振る舞いは現在バニラCoqとおなじになっている。

### Check eta
補題の型を見るためにCheckしたときに、 `right_distributive` みたいに一段くるまった形で表示されてしまうことがある

```coq=
Coq < Check mulnBr.
mulnBr
     : right_distributive muln subn
```
こういうときに `[eta ...]`という記法と組み合わせてCheckするのが便利です。
```coq=
Coq < Check [eta mulnBr].
[eta mulnBr]
     : forall x y z : nat, x * (y - z) = x * y - x * z

```
## 謝辞

この知見は coqtokyo 勉強会で得られた情報などをもとに作成しています。

- coqtokyo
- 開催日時: 隔週火曜日 19:00 - 21:00
- 場所: オンラインミーティング
- 参加URL: https://readcoqart.connpass.com/