- apply は backward apply〈deapply | reverse apply〉の意味。だいぶ困る。
- 複数のゴールは左〈上〉から順に攻撃する。ツリー辿りは深さ優先再帰かな。
- ゴールの固有名はないが、left, right のcaseラベルは付く。並びの順番でも参照できる。
- ツリーが構成されると、各ゴール〈ノード〉に付くラベルはツリーパスになる。ただし、ツリーの全貌は表示されない。時間方向にツリーが展開される。ツリーがビジュアルではないので認知負荷が大きい。
- ドットの使いみちが、モジュールパス、名前空間パス、そして、バックワード・リーズニング・ツリーパス。あと、箇条書き記法のブレット。
- バックワードリーズニングのツリーは、タブローツリーと同じで、タクティクはタブローコマンドと同じ。
#print 定理名で、格納形式〈パックド形式〉の証明項＝定理ボディが表示される。これは役立つ。[Ctrl]+[Shift]+[Enter]で InfoView の表示／非表示がトグルする。（知らんかった。）InfoViewが出てないときに便利。- exactの代わりにapplyでもよい。applyに「それで終わり」の意味を付け加えたのがexact。exactly apply で、その意味は exactly deapply。
- applyに推論規則〈定理〉だけでなく、(推論規則 証拠) の形が使える。これも意味はdeappyだからややこしい。
- ゴールのラベル（ゴール名）をタグとも呼ぶ。タグは推論規則（例： And.intro）の引数名から取られる。推論規則は定理であり、定理は証明に名前を付けたもので、定理ヘッドに仮引数リストがあり、仮引数リストに引数名が付けられている。
- タクティクのシーケンスだと、複数ゴールのどれにタクティクが適用されるかが非常に分かりににくい。ゴールのタグ〈ラベル〉を利用して、ツリー構造を反映したタクティクコーディングが出来る。
case タグ => タクティクコードと書く。 - caseの入れ子を使わないと、ツリー構造が平坦化されたコードになる。極めて分かりにくい。case構造は、タクティクコードの構造化構文として有用。
- リスト・ツリーが、推論規則の引数名でラベルされた、ラベル付き木になる。ラベルを使わないと、ラベル無し順序木となる。ツリーのノードが逆推論規則で、子ノードへのラベルが引数名。
- タグ＝ラベルを書くのが面倒なら、入れ子箇条書き記法が使える。箇条書きの各箇条の頭にはブレット。
- introは「仮説を導入する」と書いてあるが、全然ダメ！ intro の正体はカリー化の逆で、つまりは反カリー化操作。導入するのは、シークエントのコンテキスで使う証拠ラベル。シークエントのコンテキスを前提とも呼ぶので、前提に新たな証拠ラベルを導入する、とは言える。
- introは反カリー化だが、コンテキスがラベル付きを要求しているので、ラベルだけは人間が指定する必要がある。「ラベル必須」の影響は色々とある。依存パイ型の記述でもラベルが要求される。が、ラベルはアルファ変換可能。
- example, theorem, by は通常の関数定義にも使える。
theorem myIdFunc (α : Type) : α → α := by intro x; exact x
