trans
trans
は、推移律を利用して示すべきことを分割するタクティクです。
推移的な関係 ∼
に対してゴールが a ∼ c
であるとき、trans b
により2つのサブゴール a ∼ b
と b ∼ c
が生成されます。calc
を使っても同じことができますが、calc
を使うまでもないときに便利かもしれません。
import Batteries.Tactic.Trans
example {n m : Nat} (h1 : n ≤ 1) (h2 : 1 ≤ m) : n ≤ m := by
-- 1 を仲介して示す
trans 1
· show n ≤ 1
assumption
· show 1 ≤ m
assumption