with_reducible の使用例

[Seasawher]

macro_rules でタクティクを定義しようとして失敗する例

Zulip: https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/.60apply.20Nat.2Ele_trans.60.20succeed.20for.20.60a.20.3C.20c.60.20unexpectedly

以下の例は with_reducible がないと失敗する

syntax "my_trans" term : tactic

macro_rules
  | `(tactic| my_trans $e) => `(tactic| with_reducible apply Nat.lt_trans (m := $e))

macro_rules
  | `(tactic| my_trans $e) => `(tactic| with_reducible apply Nat.le_trans (m := $e))

variable (a b c : Nat)

example (h0 : a < b) (h1 : b < c) : a < c := by
  my_trans b <;> assumption

example (h0 : a ≤ b) (h1 : b ≤ c) : a ≤ c := by
  my_trans b <;> assumption

[Seasawher]

#help コマンドの出力

---

with_reducible tacs executes tacs using the reducible transparency setting. In this setting only definitions tagged as [reducible] are unfolded.

[Seasawher]

transparency という用語の翻訳が問題。トランスパレンシと訳すのはさすがに読みづらそう。

Metapro book には下記のように書かれている：

see https://leanprover-community.github.io/lean4-metaprogramming-book/main/04_metam.html?highlight=transparency#transparency

An ugly but important detail of Lean 4 metaprogramming is that any given expression does not have a single normal form. Rather, it has a normal form up to a given transparency.

A transparency is a value of Lean.Meta.TransparencyMode, an enumeration with four values: reducible, instances, default and all. Any MetaM computation has access to an ambient TransparencyMode which can be obtained with Lean.Meta.getTransparency.

The current transparency determines which constants get unfolded during normalisation, e.g. by reduce. (To unfold a constant means to replace it with its definition.) The four settings unfold progressively more constants:

[Seasawher]

age