TPPmark 2025
https://tpp2025.blogspot.com/2025/09/tppmark-2025.html

著者: 田中哲
証明ツール: Rocq 9.0.0 と mathcomp

| 問題
| n ≥1 を整数とする．同じサイズの立方体型ランプを隙間なく n^3 個並べて，
| 全体として n×n×n の大きな立方体を作る． すると，その外面には各面に n×n 個，
| 計 6n^2 個の小正方形（外側に見えているランプの外面）が現れる．
| 各ランプは on/off のいずれかの状態をもち，外面の小正方形のうち一つを押すと，
| その小正方形とちょうど反対側にある小正方形を結ぶ直線上(*1)の n 個のランプ
| だけが同時に反転（on↔off）する．
|
| 全ランプの on/off の状態が与えられたとき，
| 上記の操作の繰り返しのみですべてのランプを off にできるための必要十分条件を
| なるべく簡潔に記述し，その条件の正しさを証明せよ．
|
| (*1) 追記(2025/9/16):「その小正方形とちょうど反対側にある小正方形を結ぶ
| 直線上」は「その小正方形を垂直に貫通する直線上」の意です．

形式化の方針

以下のように、2段階に分けて形式化を行う。

1. 問題を一般化し、任意有限個のスイッチと任意有限個のランプが
   任意に接続されているという設定を形式化
2. 問題に示されている立方体の構造の形式化
2.1. 座標の各軸の型など、型の定義
2.2. 辺の長さ n が 1以上の場合の証明
2.3. 辺の長さ n が 0も含む場合の証明

# 任意接続の場合の形式化

まず、問題を一般化し、任意有限個のスイッチと任意有限個のランプが
任意に接続されているという状況を形式化する。

スイッチとランプはなんらかの有限型で指定されるとし、
ランプからスイッチ集合への関数で接続を表現する。

```
Variable switch : finType.
Variable lump : finType.

Variable switches_of_lump : lump -> {set switch}.
```

あるスイッチ操作列でランプが点灯するというのは、
あるランプに接続されているスイッチが操作されるたびに
点灯・消灯が反転するので、
接続されているスイッチを true、
接続されていないスイッチを false として、
addb (mathcomp で xor を表現する関数) で集約すればよい。

```
Definition status (sws : seq switch) (l : lump) : bool :=
  \big[addb/false]_(sw <- sws) (sw \in switches_of_lump l).
```

xor は associative かつ commutative なので、リストの順序に意味はない。
また、a xor a = false であることは、同じスイッチを 2回操作するとキャンセルされることを意味する。
従って、スイッチのリストはそのリストに奇数個含まれるスイッチの集合と
(結果のランプの状態において) 等価であることを示せる。

```
Definition odd_switches (sws : seq switch) : {set switch} :=
  [set:: [seq sw <- sws | odd (count_mem sw sws)]].

Lemma odd_switches_ok (sws : seq switch) (l : lump) :
  status (enum (odd_switches sws)) l = status sws l.
```

というわけで、スイッチのリストのかわりにスイッチ集合を扱うことにする。
そのために、スイッチ集合からランプ状態を得る関数 status_set を定義して、
それが status と相互変換可能であることを証明する。

```
Definition status_set (swset : {set switch}) (l : lump) : bool :=
  odd #|swset :&: switches_of_lump l|.

Lemma status_set_status (swset : {set switch}) (l : lump) :
  status_set swset l = status (enum swset) l.

Lemma status_status_set (sws : seq switch) (l : lump) :
  status sws l = status_set (odd_switches sws) l.
```

これにより、スイッチの個数を n として、スイッチの操作を、
任意長のリストという無限状態から、2^n という有限状態に限定できた。

つまり、2^n の場合をすべて確認すれば、
あるランプ状態を実現できるかどうか確認できる。

これにより、問題の必要十分条件
「上記の操作の繰り返しのみですべてのランプを off にできるための必要十分条件」
を有限時間で実行できる関数で記述できることがわかる。

# 問題に示されている立方体の構造の形式化

次に問題に示されている立方体の構造を形式化する。
型の定義、辺の長さが1以上の場合、辺の長さに制限がない場合の
それぞれをモジュールにする。

## 座標の各軸の型など、型の定義

型の定義を CubeT というモジュールにする。
後続するモジュールでは Import CubeT として使う。

型は辺の長さ n を受け取る形で定義する。
この型の定義のところを独立したセクションにして、
以下のように Variable で n を受け取る。

```
Variable n : nat.
```

座標は有限型 (ordinal 型) で表現する。
3次元のどの軸も 'I_n とする。
個々のランプは立方体内の座標で特定できるので、それらの直積とする。

```
Definition xType := 'I_n.
Definition yType := 'I_n.
Definition zType := 'I_n.

Definition lump : Type := xType * yType * zType.
```

小正方形がスイッチとなるが、
反対側の小正方形はスイッチとして同じ効果をもつので無視することにし、
6n^2 ではなく 3n^2 のスイッチがあると考える。
これを n^2 個の値を持つコンストラクタ 3個の型で表現する。

```
Inductive switch :=
| inxy : (xType * yType) -> switch
| inyz : (yType * zType) -> switch
| inzx : (zType * xType) -> switch.
```

## 辺の長さが 1以上の場合の証明

辺の長さが 1以上の場合を Cube1 というモジュールで形式化する。

```
Module Cube1.
Import CubeT.
```

ここでは、辺の長さ n が 1 以上の場合について証明する。
この証明にはランプ (0, 0, 0) など、座標 0 を利用するので、
辺の長さ 0 の場合には適用できない。

上の型定義のセクションは終わっているので、
xType は fun (n : nat) => 'I_n となっているため、xType を使うときには常に n を与えなければならない。
(yType, zType, lump, switch, inxy, inyz, inzx も同様である。)
しかし、ここでは辺の長さを n.+1 としてずっと一定なので、省略したい。

そのために以下のように Section でくくって、
xType, yType, zType, switch, inxy, inyz, inzx, lump に n.+1 を与えた形の notation を定義する。
ただし、match 式のパターンのところに inxy, inyz, inzx を書くときには n.+1 を与えてはいけないので、
そこはコンストラクタの CubeT.inxy, CubeT.inyz, CubeT.inzx という完全修飾名で参照する。
notation を使っているのは、セクション外に影響を漏らさないためである。
(セクション外に影響を漏らさないのは Let でも可能だが、コンテキストに常に表示されて邪魔だし、証明中に展開された型が出てくることがある。)
(試行錯誤の結果こうなったが、もっとよいやりかたがあれば教えてほしい。)

```
Section Cube1.

Variable n : nat.

Notation xType := (xType n.+1).
Notation yType := (yType n.+1).
Notation zType := (zType n.+1).
Notation lump := (lump n.+1).
Notation switch := (switch n.+1).
Notation inxy := (@inxy n.+1).
Notation inyz := (@inyz n.+1).
Notation inzx := (@inzx n.+1).
```

ランプの集合を lumps, スイッチの集合を swset とすると、
それらの接続を以下のように形式化できる。
あるランプは、そのランプから x方向、y方向、z方向それぞれに
線を伸ばしたところにあるスイッチ 3つに接続されているという意味である。
また、status と status_set は常に switches_of_lump を引数とするので、
省略して記述できるよう notation を定義する。

```
Variable switches_of_lump : lump -> {set switch}.
Hypothesis connection :
  forall (x : xType) (y : yType) (z : zType),
    switches_of_lump (x, y, z) = [set (inxy (x, y)); (inyz (y, z)); (inzx (z, x))].

Notation status := (status switches_of_lump).
Notation status_set := (status_set switches_of_lump).
```

ランプの状態を実現するスイッチの集合を (可能な場合に) 求める関数を記述する
ただし、ひとつのランプ状態に対応するスイッチ集合は複数あるので、
以下の条件のものを求める。

- inyz (y, 0) が off
- inzx (0, x) が off
- inzx (z, 0) が off

この条件により、inxy (x, y) がスイッチ集合に含まれていることは
ランプ (x, y, 0) が点灯していることと等しいなどとして、
スイッチに接触しているランプ (ランプ (x, y, 0), (x, 0, z), (0, y, z)) から
決定的にスイッチの状態を求めることができる。
そのスイッチ状態からすべてのランプの状態を求め、
与えられたランプ状態 (スイッチに接触していないランプも含む) に
一致したらそれが求めるスイッチ集合であり、
一致していなかったらそのランプ状態を実現するスイッチ集合は存在しないことを示す。

```
Definition xy_switches_for_lumpset (lumps : {set lump}) : {set xType * yType} :=
  [set (x, y) | x in xType, y in yType & (x, y, ord0) \in lumps].

Definition yz_switches_for_lumpset (lumps : {set lump}) : {set yType * zType} :=
  [set (y, z) | y in yType, z in zType &
   ((ord0, y, ord0) \in lumps) (+) ((ord0, y, z) \in lumps)].

Definition zx_switches_for_lumpset (lumps : {set lump}) : {set zType * xType} :=
  [set (z, x) | z in zType, x in xType &
    ((ord0, ord0, ord0) \in lumps) (+) ((ord0, ord0, z) \in lumps)
    (+) ((x, ord0, ord0) \in lumps) (+) ((x, ord0, z) \in lumps)].

(* 二項演算子 :|: は mathcomp が提供している和集合の演算子である *)
Definition all_switches_for_lumpset (lumps : {set lump}) : {set switch} :=
  [set inxy xy | xy in xy_switches_for_lumpset lumps] :|:
  [set inyz yz | yz in yz_switches_for_lumpset lumps] :|:
  [set inzx zx | zx in zx_switches_for_lumpset lumps].

(* 二項演算子 (+) は mathcomp が提供している bool の排他的論理和 addb である *)
Definition switches_for_lumpset1 (lumps : {set lump}) : option {set switch} :=
  if all (fun '(x, y, z) => ((x, y) \in xy_switches_for_lumpset lumps) (+)
                            ((y, z) \in yz_switches_for_lumpset lumps) (+)
                            ((z, x) \in zx_switches_for_lumpset lumps)
                            == ((x, y, z) \in lumps))
         (enum (setT : {set xType * yType * zType}))
  then
    Some (all_switches_for_lumpset lumps)
  else
    None.
```

その switches_for_lumpset1 がスイッチ集合を返すなら、
そのスイッチ集合で実現されるランプの状態を実現することを証明する。

```
Lemma switches_for_lumpset1_ok_1 :
  forall (lumps : {set lump}) (swset : {set switch}) (l : lump),
    switches_for_lumpset1 lumps = Some swset ->
    (status_set swset l) = (l \in lumps).
```

次に、なんらかのスイッチ集合で実現できるランプ状態に対して、
上記の switches_for_lumpset1 がスイッチ集合を返すことを証明する。

ただし「なんらかのスイッチ集合」と「switches_for_lumpset1 が返すスイッチ集合」は
異なる可能性があるので調整が必要になる。

ここで立方体の中の平面 (x-y 平面、y-z 平面、z-x 平面のいずれか) に注目して、
その平面についているスイッチをすべて操作すると、
ひとつのランプについてふたつのスイッチがあるので、ランプの状態は変化しない。
これを利用し、あるスイッチ集合が実現するランプ状態と同じランプ状態を実現して、かつ、
「inyz (y, 0) が off」「inzx (0, x) が off」「inzx (z, 0) が off」
という条件を満たすスイッチ集合を求めることができる。
これを tweak_switches として実装する。
そうすると、そうやって調整したスイッチ集合が
switches_for_lumpset1 が返すスイッチ集合と一致する。

```
Definition plane_xy_switches (z : zType) : {set switch} :=
  [set inyz (y, z) | y in yType] :|: [set inzx (z, x) | x in xType].

Definition plane_yz_switches (x : xType) : {set switch} :=
  [set inzx (z, x) | z in zType] :|: [set inxy (x, y) | y in yType].

Definition plane_zx_switches (y : yType) : {set switch} :=
  [set inxy (x, y) | x in xType] :|: [set inyz (y, z) | z in zType].

(* 二項演算子 :+: は自前で定義したもので、有限集合の排他的論理和である *)
Definition clear_switches_y0_in_yz (swset : {set switch}) : {set switch} :=
  swset :+: \bigcup_(y | (inyz (y, ord0) \in swset)) (plane_zx_switches y).

Definition clear_switches_0x_in_zx (swset : {set switch}) : {set switch} :=
  swset :+: \bigcup_(x | (inzx (ord0, x) \in swset)) (plane_yz_switches x).

Definition clear_switches_z0_in_zx (swset : {set switch}) : {set switch} :=
  swset :+: \bigcup_(z | (inzx (z, ord0) \in swset)) (plane_xy_switches z).

Definition tweak_switches (swset : {set switch}) : {set switch} :=
  let swset2 := clear_switches_y0_in_yz swset in
  let swset3 := clear_switches_0x_in_zx swset2 in
  let swset4 := clear_switches_z0_in_zx swset3 in
  swset4.

Lemma switches_for_lumpset1_ok_2 :
  forall (lumps : {set lump}) (swset : {set switch}),
    (forall (l : lump), (status_set swset l) = (l \in lumps)) ->
    switches_for_lumpset1 lumps = Some (tweak_switches swset).
```

switches_for_lumpset1_ok_1 と switches_for_lumpset1_ok_2 をあわせて
命題の等価性の形で証明する。

なお、switches_for_lumpset1 lumps は option {set switch} 型であって命題ではないが、
isSome という coercion が隠れていて、それが Some になるという命題になっている。

```
Lemma switches_for_lumpset1_ok' :
  forall (lumps : {set lump}),
    switches_for_lumpset1 lumps <->
    (exists (swset : {set switch}), forall (l : lump),
      (status_set swset l) = (l \in lumps)).
```

問題はスイッチ操作列について述べているので、スイッチ集合じゃなくてスイッチ操作のリストとの等価性も証明する

```
Lemma switches_for_lumpset1_ok (lumps : {set lump}) :
  switches_for_lumpset1 lumps <->
  (exists (sws : seq switch), forall (l : lump),
    (status sws l) = (l \in lumps)).
```

つまり、
switches_for_lumpset1 が Some を返すか None を返すかで
あるランプ状態を実現可能なスイッチ操作列が存在するかどうかを判定できる。

あるランプ状態を実現可能であることは、(それを実現するスイッチ操作をもう一回行えば)
そのランプ状態から全部 off にできるということなので、
問題に示された条件
「上記の操作の繰り返しのみですべてのランプを off にできるための必要十分条件」
を決定的な関数で記述できたことがわかる。

```
End Cube1.
End Cube1.
```

## 辺の長さが 0 も含む場合の証明

辺の長さが 0 の場合はランプもスイッチもないので、スイッチ集合は空集合とするしかない。
辺の長さが 0 でない場合は上の結果を使う。
これらをあわて、ランプ集合からスイッチ集合を求める決定的な関数を実装できる。
ただし、これらの場合分けでは convoy pattern を使って型をあわせる必要がある。

ここでは辺の長さは固定ではないので、Variable n : nat とはせず、明示的に記述する。

```
Section Cube.

Variable switches_of_lump : forall (n : nat), lump n -> {set switch n}.

Variable connection :
  forall (n : nat) (x : xType n) (y : yType n) (z : zType n),
    switches_of_lump (x, y, z) = [set (inxy (x, y)); (inyz (y, z)); (inzx (z, x))].

Definition switches_for_lumpset (n : nat) (lumps : {set lump n}) : option {set switch n} :=
  match n as n' return n = n' -> option {set switch n} with
  | 0 => fun (H : n = 0) => Some set0
  | m.+1 => fun (H : n = m.+1) =>
      rew <- [fun i => option {set switch i}] H in
        (@Cube1.switches_for_lumpset1 m
          (rew [fun i => ({set lump i})%type] H in lumps))
  end erefl.
```

このランプ状態からスイッチ集合を求める関数について、
以下のように正しいことを証明できる。

```
Lemma switches_for_lumpset_ok (n : nat) (lumps : {set lump n}) :
  switches_for_lumpset lumps <->
  (exists (sws : seq (switch n)), forall (l : lump n),
    (status (@switches_of_lump n) sws l) = (l \in lumps)).
```

ただ、この命題には上の (convoy pattern を使った) switches_for_lumpset が入っていて、
簡潔かというとどうかなぁ。

# 興味深かった点

- switches_for_lumpset1_ok_2 の途中で以下の証明をする必要があった。

  (inxy (x, y) \in swset) (+) (inyz (y, ord0) \in swset)
  (+) (inzx (ord0, x) \in swset)
  (+) ((inxy (ord0, y) \in swset)
       (+) (inyz (y, ord0) \in swset)
       (+) (inzx (ord0, ord0) \in swset)
       (+) ((inxy (ord0, y) \in swset)
            (+) (inyz (y, z) \in swset)
            (+) (inzx (z, ord0) \in swset)))
  (+) ((inxy (ord0, ord0) \in swset)
       (+) (inyz (ord0, ord0) \in swset)
       (+) (inzx (ord0, ord0) \in swset)
       (+) ((inxy (ord0, ord0) \in swset)
            (+) (inyz (ord0, z) \in swset)
            (+) (inzx (z, ord0) \in swset))
       (+) ((inxy (x, ord0) \in swset)
            (+) (inyz (ord0, ord0) \in swset)
            (+) (inzx (ord0, x) \in swset))
       (+) ((inxy (x, ord0) \in swset)
            (+) (inyz (ord0, z) \in swset)
            (+) (inzx (z, x) \in swset))) =
  (inxy (x, y) \in swset) (+) (inyz (y, z) \in swset)
  (+) (inzx (z, x) \in swset)

  これは同じ項を xor しているのを消すと両辺に同じ項が残るので証明できる。
  しかし、具体的に証明するには手間がかかるので、いろいろなやりかたを試した

  - 計算による証明
  - 項変形による証明
  - ring
  - ssrAC

  SSReflect でよくやる計算による証明を使うと、以下のように証明できる。

  by case: (inxy (ord0, ord0) \in swset);
     case: (inxy (ord0, y) \in swset);
     case: (inxy (x, ord0) \in swset);
     case: (inxy (x, y) \in swset);
     case: (inyz (ord0, ord0) \in swset);
     case: (inyz (ord0, z) \in swset);
     case: (inyz (y, ord0) \in swset);
     case: (inyz (y, z) \in swset);
     case: (inzx (ord0, ord0) \in swset);
     case: (inzx (ord0, x) \in swset);
     case: (inzx (z, ord0) \in swset);
     case: (inzx (z, x) \in swset).

  しかし、この場合分けをして計算するのは 70秒くらいかかって遅すぎる。
  SSReflect は計算による証明が便利といっても、
  2^12 = 4096 とおりの場合分けはちょっとつらいようだ。
  (でも、最初に brute force な場合分けで証明可能なことを確認できたのは、
  後の作業中に証明できないという疑いを持たなくて済んだのでよかった。)

  そこで以下のように項の変形で証明しなおした。
  まず addbA でフラットな構造にする。
  addbAC で指定した項をなるべく左に動かして同じ項が並ぶようにして addbK で除去する、
  というのを繰り返す。

  rewrite !addbA.
  rewrite -!(addbAC _ (inyz (y, ord0) \in swset)) addbK.
  rewrite -!(addbAC _ (inzx (ord0, x) \in swset)) addbK.
  rewrite -!(addbAC _ (inxy (ord0, y) \in swset)) addbK.
  rewrite -!(addbAC _ (inxy (x, ord0) \in swset)) addbK.
  rewrite -!(addbAC _ (inzx (ord0, ord0) \in swset)) addbK.
  rewrite -!(addbAC _ (inzx (z, ord0) \in swset)) addbK.
  rewrite -!(addbAC _ (inxy (ord0, ord0) \in swset)) addbK.
  rewrite -!(addbAC _ (inyz (ord0, ord0) \in swset)) addbK.
  rewrite addbK.
  by [].

  しかしこれも面倒くさいので、簡単にできる方法を探したところ、
  Rocq 標準の ring (環を対象とする自動証明 tactic) が
  bool_ring という排他的論理和 (xorb) と論理積 (andb) の環を
  扱えるように最初から用意されていて、これが利用できることがわかった。

  move: (inxy (ord0, ord0) \in swset)
        (inxy (ord0, y) \in swset)
        (inxy (x, ord0) \in swset)
        (inxy (x, y) \in swset)
        (inyz (ord0, ord0) \in swset)
        (inyz (ord0, z) \in swset)
        (inyz (y, ord0) \in swset)
        (inyz (y, z) \in swset)
        (inzx (ord0, ord0) \in swset)
        (inzx (ord0, x) \in swset)
        (inzx (z, ord0) \in swset)
        (inzx (z, x) \in swset)
    => b1 b2 b3 b4 b5 b6 b7 b8 b9 b10 b11 b12.
  (* ゴールは以下となる
    b4 (+) b7 (+) b10 (+) (b2 (+) b7 (+) b9 (+) (b2 (+) b8 (+) b11))
    (+) (b1 (+) b5 (+) b9 (+) (b1 (+) b6 (+) b11) (+) (b3 (+) b5 (+) b10)
         (+) (b3 (+) b6 (+) b12)) =
    b4 (+) b8 (+) b12
  *)
  by rewrite -!xorb_addb /=; ring.

  ただし、ring を使うには内部の複雑な式を変数にする必要があったので、
  あまり行数は短くならない。
  あと、SSReflect の addb を vanilla Coq の xorb にする補題も必要になる。

  また、そもそも ring はおおげさで、
  環になっていないものは扱えないので使える場面も限られる。
  今回は xor だったので使えたが、たとえば or には使えない。

  そこでさらに探したところ、SSReflect 標準で ssrAC というライブラリがあって、これを使うと、
  以下のように証明できることがわかった。

  by rewrite !addbA addb.[ACl 1*8*21*2*5*3*18*4*7*6*12*9*15*10*13*11*17*14*20*16*19] !addbK.

  これは左辺の順序を書き換えるのだが、
  最初の 1*8*21 で右辺と同じ並びを指定し、残りは同じ項が続くようにしている。
  そして、同じ項の並びを addbK で消すと、両辺が同じになって証明できる。

  これで証明を 1行に短縮できたが、
  1*8*21*2*5*3*18*4*7*6*12*9*15*10*13*11*17*14*20*16*19 を指定するのは面倒なので、
  単に associative, commutative な演算子のネストを
  (同じ項が連続するような) 一定の順序に並び替える tactic が欲しいと思った。

  あと、それはそれとして、ssrAC のドキュメントは拡充したほうがいいと思う。

- 辺の長さとして 0 も許すことにこだわった結果、以下のように証明を構造化するに至った

  Module CubeT.
  Section CubeT.
  Variable n : nat.
  ... n に依存したいろいろな型定義 ...
  End CubeT.
  End CubeT.

  Module Cube1. (* 辺の長さが 1 以上の場合の証明 *)
  Import CubeT.
  Section Cube1.
  Variable n : nat.
  (* CubeT の n を n.+1 に固定して使う *)
  ...
  End Cube1.
  End Cube1.

  Module Cube. (* 辺の長さが 0 以上の場合の証明 *)
  Import CubeT.
  Section Cube.
  (* ここでは n は固定せずに使う *)
  End Cube.
  End Cube.

  ここで、Cube1 で「CubeT の n を n.+1 に固定して使う」というのには
  以下のように Notation を使うのがよいようだ。

  Notation xType := (xType n.+1).
  ...
  Notation inxy := (@inxy n.+1).
  ...

  しかし、CubeT の定義すべてについて記述する必要がある。
  また、この inxy は switch 型のコンストラクタで、
  match のパターンに使う場合は CubeT.inxy と記述する必要がある。
  (match のパターンにおいてコンストラクタのパラメータは _ にしないといけない)

  以前のセクションの変数を固定するもっと簡単な方法が欲しいと思った。
  (とりあえずパターンには適用されない notation が欲しいが、見当たらない。)

- 帰納型 switch は、最初は sum 型で
  Definition switch : Type := (xType * yType) + (yType * zType) + (zType * xType).
  と定義して使っていたが、最終的には独自の帰納型に変更した。
  inl (inl (x, y)) などと書くのはわかりにくいので、
  inxy (x, y) という関数を定義したのだが、
  意図せず展開されてしまうことがあるので
  Arguments inxy : simpl never.
  として抑制したが、それでも展開した形がでてくることは残り、
  また、場合分けで [[x y]|[y z]|[z x]] でなく [[[x y]|[y z]]|[z x]] と
  書かなければならないのは sum 型ではどうしようもない。
  ということで結局、自前の帰納型にしたが、
  これを mathcomp の finType にする方法を調べるのに手間取った。

- 証明を整理するのに、いくつか定理ではなく、Ltac が必要になったところがあった

  in_clear_switches_y0_in_yz, in_clear_switches_0x_in_zx, in_clear_switches_z0_in_zx の
  共通部分をまとめるために Ltac を使ったが、SSReflect の => で作った変数を
  参照するとエラーになるので intros を使う必要があった。

# 謝辞

議論していただいた coqtokyo 勉強会のかたに感謝する。