Leanのシーケント形式とタクティク

Leanのシーケントは、ゴール＝リクエストとして出てくるが、その形式は

• コンテキスト ⊢ ターゲット

コンテキストは型宣言のカンマ区切り列、ターゲットは型式〈かたしき〉。その意味はリクエストだから、

• コンテキスト ⊢? _:ターゲット

例：

• p q : Prop, hp : p, hq : q ⊢ p ∧ q ∧ p

p q : Prop は、p : Prop, q : Prop の省略記法。コンテキストのなかで、型データの型宣言（単数または複数）をセットアップ〈setup{s}?〉、証明データ〈証明オブジェクト〉の型宣言を仮説〈hypothesis, hypotheses(複数)〉と呼ぶ。

Leanのタクティクは逆行〈backward〉でしか使えないが、概念的には順行〈forward〉タクティク（'↓'を付ける）もある。

     p q : Prop, hp : p, hq : q ⊢! p 
     p q : Prop, hp : p, hq : q ⊢! q ∧ p
   ------------------------------------------- ↓apply and.intro
     p q : Prop, hp : p, hq : q ⊢! p ∧ q ∧ p

このapplyは、復圏（または多圏）における復結合で、復射のリストに単一の復射を結合する。用語法は apply より compose が相応しいが歴史的にしょうがない。クローン＝デカルト復圏（または多クローン＝デカルト多圏）の計算が背後にある。

逆行タクティクには'↑'を付ける。

     p q : Prop, hp : p, hq : q ⊢? p ∧ q ∧ p
   ------------------------------------------- ↑apply and.intro
     p q : Prop, hp : p, hq : q ⊢? p 
     p q : Prop, hp : p, hq : q ⊢? q ∧ p

同様に、

                  ☆(empty)
   ----------------------------------- ↓exact hp
     p q : Prop, hp : p, hq : q ⊢! p

同様に、

     p q : Prop, hp : p, hq : q ⊢? p
   ----------------------------------- ↑exact hp
                  ☆(closed)

「declarative style VS procedural style」＝「forward term style VS backward tactic style」になっている。実際は、次の四区分。

	term	tactic
backward	backward term style	backward tactic style
forward	forward term style	forward tactic style

forward tactic style がないので、シーケント計算との連絡が悪い。forward term style が自然演繹証明のテキストシリアライゼーションだと考えることができる。

backward tactic style は、シーケント計算のリーズニング図の逆方向でのテキストシリアライゼーション。逆方向である点が難しくしている。