rflの解説について

[iehality]

現在の記述 https://lean-ja.github.io/tactic-cheetsheet/rfl.html ではrflは項のdefinitional equalityを証明するもののように書かれていますが, ドキュメント https://leanprover-community.github.io/mathlib4_docs//Mathlib/Tactic/Relation/Rfl.html によるとこれは refl attributeのついた定理を用いて関係の反射性を示すといったほうが正確ではないかと思います。例えば以下のように順序の反射性を証明することが可能です.

example (n : ℕ) : n ≤ n := by rfl

[Seasawher]

ありがとうございます

たしかに @[refl] で登録されたレンマを使用するという情報があった方がいいですね．

また現状で「定義そのまま」になっている一言説明も，「反射性を示す」など反射性という言葉を使った方がよさそうですね．

修正方針に問題ありませんので，よろしければPR を出していただきたいです。

[iehality]

私自身も勘違いしていたのですが, Mathlib.Tactic.Relation.Rflを含むMathlibのファイルをimportした場合rflはLean.MVarId.rflを参照しますが, そうでないときはLean.MVarId.reflを参照するようです(前者は@[refl]が証明された一般の関係の反射性を証明できますが, 後者は_ = _の等価性のみ証明します).

ringなどMathlib限定のtacticも多く解説されているので, ここではMathlibだけの用法だけでも良い気がしますが, 後者についても触れておくべきでしょうか?

[Seasawher]

全然知りませんでした．ありがとうございます．

ringなどMathlib限定のtacticも多く解説されているので, ここではMathlibだけの用法だけでも良い気がしますが, 後者についても触れておくべきでしょうか?

確かに Mathlib 依存のタクティクも紹介していますが，Mathlib 等のライブラリに依存するタクティクはそれを明示するというルールで今まで運用してきました．したがって，rfl の Mathlib 依存挙動だけを紹介すると，今度は「Mathlib を import しなくても rfl が使える...?」という混乱を招きそうです．

かといって Mathlib 依存の挙動を無視すると「Mathlib のDocumentの記述と違う！」という混乱を招きます．

両方に触れるしかないと思います．

rfl の挙動が変わることを示す MWE を提供していただけると助かります．

[iehality]

参照される関数が不適切だったため前の返信を修正しました.

rflの挙動については, Mathlibをimportした場合例えば以下の証明は両方可能です.

import Mathlib.Data.Nat.Basic

example (n : Nat) : n = n := by rfl

example (n : Nat) : n ≤ n := by rfl

一方importを外すと下の証明にエラーが発生します.

example (n : Nat) : n = n := by rfl

example (n : Nat) : n ≤ n := by rfl -- error
/-
tactic 'rfl' failed, equality expected
  Nat.le n n

n: Nat
⊢ n ≤ n
-/

[Seasawher]

ありがとうございます．Mathlib 側の rfl の方が真に強く，Mathlib なしの rfl で示せることは Mathlib ありでも示せるという認識で相違ないでしょうか？（つまり，import 文を追加することによりコンパイルが通らなくなる現象は起きない）

もしそうであれば，いまある Examples/Rfl.lean に上記の例と import 文を追記して，markdown 側に Mathlib を import することにより示せる命題が増えることに言及する文章を追加するとよさそうです．

ext タクティクも「タクティク使用に必要なライブラリ」と「タクティクで示せる命題を増やすのに必要なライブラリ」が異なっているので，ext の記述に似せて修正するといいかと思いました．

[Seasawher]

ところで相談なのですが，下記のコードは通らないようです．参照先のタクティクの違いというより，@[refl] がついているレンマのうち必要なものがインポートされているかどうかで，通るかどうかが変わってきているのではないでしょうか…？

import Mathlib.Tactic.Relation.Rfl

example (n : Nat) : n ≤ n := by rfl

[iehality]

Mathlib 側の rfl の方が真に強く，Mathlib なしの rfl で示せることは Mathlib ありでも示せるという認識で相違ないでしょうか？（つまり，import 文を追加することによりコンパイルが通らなくなる現象は起きない）

そのように理解しています.

ところで相談なのですが，下記のコードは通らないようです．参照先のタクティクの違いというより，@[refl] がついているレンマのうち必要なものがインポートされているかどうかで，通るかどうかが変わってきているのではないでしょうか…？

extなどと同様に, @[refl]のついた補題がimportに含まれていることは必要だと思います. しかし_ = _でない関係の反射性を示すにはMathlib.Tactic.Relation.Rflが（本質的に）必要だろうと思います.

以下の例は@[refl]の証明も含んだコードですが, importがないと通りません（そもそもrefl attributeがMathlibで定義されているので, 6行目にエラーが発生します）.

import Mathlib.Tactic.Relation.Rfl

inductive MyEq {α : Type u} : α → α → Prop
  | refl (a : α) : MyEq a a

attribute [refl] MyEq.refl

example (n : ℕ) : MyEq n n := by rfl

[Seasawher]

ありがとうございます．そろそろ PR を作ってみます．