逆描画

variables (P Q:Prop)

theorem sample (hp : P) (hq : Q) : P ∧ Q ∧ P :=
begin
  apply and.intro, -- 5
  assumption, -- 4
  apply and.intro, -- 3
  assumption, -- 2
  assumption -- 1
end

try it!

  ☆             ☆
 ---------- 1  ---------- 2
  P, Q → P      P, Q → Q          ☆
 ------------------------ 3   --------- 4
      P, Q → P∧Q              P, Q → P
      ----------------------------------- 5 swap
                P, Q → P∧(Q∧P)

順行タクティク証明記述

      ☆
 ------------------------------ 1 ↓assumption
  P Q: Pro, hp : P, hq : Q ⊢ P (★1)
 
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
      ☆
 ------------------------------ 2 ↓assumption
  P Q: Pro, hp : P, hq : Q ⊢ Q (★2)
  P Q: Pro, hp : P, hq : Q ⊢ P (★1)
 ------------------------------ 3 ↓apply and.intro
  P Q: Pro, hp : P, hq : Q ⊢ Q ∧ P (★3)

 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
      ☆
 ------------------------------ 4 ↓assumption
  P Q: Pro, hp : P, hq : Q ⊢ P (★4)
  P Q: Pro, hp : P, hq : Q ⊢ Q ∧ P (★3)
 --------------------------------------- 5 ↓aply and.intro
  P Q: Pro, hp : P, hq : Q ⊢ P ∧ Q ∧ P (★5)

逆行タクティク証明記述

  P Q: Pro, hp : P, hq : Q ⊢ P ∧ Q ∧ P  (★5)＜＝＝
 --------------------------------------- 5 ↑aply and.intro
  P Q: Pro, hp : P, hq : Q ⊢ P (★4)＜＝＝
  P Q: Pro, hp : P, hq : Q ⊢ Q ∧ P (★3)
 ------------------------------ 4 ↑assumption
  P Q: Pro, hp : P, hq : Q ⊢ Q ∧ P (★3)＜＝＝
 ------------------------------ 3 ↑apply and.intro
  P Q: Pro, hp : P, hq : Q ⊢ Q (★2)＜＝＝
  P Q: Pro, hp : P, hq : Q ⊢ P (★1)
 ------------------------------ 2 ↑assumption
  P Q: Pro, hp : P, hq : Q ⊢ P (★1)＜＝＝
 ------------------------------ 1 ↑assumption
      ☆(closed)

深さ優先再帰的順序によるツリートラバース〈ツリーウォーク〉によりシリアライゼーションが出来る。

      P, Q → P∧(Q∧P)
  ----------------------------- 5↑
   P, Q → P       P, Q → P∧Q
  --------- 4↑  --------------------- 3↑
    ☆          P, Q → Q     P, Q → P
              ---------- 2↑ ---------- 1↑
                  ☆             ☆