at 構文

at 構文とは、タクティク tac に対してその書き換え対象を指定する構文のことです。rw タクティクや simp タクティクなど、「書き換え」を行う多くのタクティクがこの構文を受け入れるようになっています。

利用可能な構文

at h

ローカルコンテキストにある仮定 h : P に対して at h と書くことで h に対して書き換えを行うことができます。

section
  variable {a b : Nat}

  example (lem : a + 0 = a) (h : a + (a + 0) = a) : a + a = a := by
    -- ローカルコンテキストの `h` に対して書き換えを行う
    rw [lem] at h

    rw [h]

end

at h₁ h₂ ..

また、ローカルコンテキストにある複数の仮定 h₁, h₂, .. に対して書き換えを行うには空白区切りで at h₁ h₂ .. とします。

section
  variable (x m n : ℕ)

  example (left : (x : ℝ) < ↑m + ↑n) (right : ↑m + ↑n < (x : ℝ) + 1) : False := by
    -- `left`と`right`に対して書き換えを行う
    norm_cast at left right

    omega
end

at h ⊢

ローカルコンテキストにある仮定 h : P とゴールに対して同時に書き換えを行うには、at h ⊢ とします。

example (x : Nat) (h : x ≥ 1) : 2 * x ≥ 2 := by
  -- 自然数から有理数にキャストする
  qify at h ⊢

  have : (2 : ℚ) ≤ 2 * x := calc
    _ = 2 * 1 := by simp
    _ ≤ 2 * (x : ℚ) := by gcongr
  assumption

at *

ローカルコンテキストのすべての仮定とゴールに対して書き換えを行うには、at * とします。

section
  set_option linter.flexible false

  variable (P : Nat → Bool)

  example (h1 : P (if 0 = 0 then 1 else 2)) (h2 : P (0 * 1)) : P 0 ∧ P (1 + 0) := by
    simp at *

    exact ⟨h2, h1⟩
end

at 構文を受け入れるタクティクを作る

次に示すのは at 構文を受け入れるようなタクティクをマクロとして構成する例です。

/-- 自前で定義した狭義順序 -/
def Nat.mylt (m n : Nat) : Prop := (m + 1) ≤ n

/-- 単に `m < n` と書いたら上で定義した自前の順序が使われるようにする -/
instance : LT Nat where
  lt m n := m.mylt n

open Lean.Parser.Tactic in

/-- `(· < ·)`を定義に展開して中身を確認するための専用自作タクティク -/
syntax (name := dsimp_lt) "dsimp_lt" (location)? : tactic

macro_rules
  | `(tactic| dsimp_lt $[at $location]?) =>
    `(tactic| dsimp only [(· < ·), Nat.mylt] $[at $location]?)

example : 1 < 4 := by
  dsimp_lt
  guard_target =ₛ 1 + 1 ≤ 4

  decide

example (_h : 1 < 3) : True := by
  dsimp_lt at _h
  guard_hyp _h : 1 + 1 ≤ 3

  trivial