conv の中で apply でターゲットを書き換える

[Seasawher]

@aconite-ac

Lean 勉強会の analysis3 の theorem «0.9999999 = 1» についてです．

下記のように，apply を用いてターゲットを書き換えようとしました．

theorem «0.9999999 = 1» : Real.ofCauchy (Quotient.mk CauSeq.equiv «0.9999999») = (1 : ℝ) := by
  calc _ = Real.ofCauchy (Quotient.mk CauSeq.equiv (CauSeq.const abs 1)) := ?_
       _ = (1 : ℝ) := Real.ofCauchy_one
  rw [«0.9999999»]
  congr 1
  apply Quotient.sound
  intro ε ε0
  suffices ∃ i, ∀ (j : ℕ), j ≥ i → (10 ^ j : ℚ)⁻¹ < ε by simpa [abs]
  -- ヒント: `pow_unbounded_of_one_lt`と`inv_lt_of_inv_lt`を使って、欲しい`i`を手に入れよう
  
  -- 示すべき式を書き換える
  conv =>
    congr
    intro i j hji
    tactic =>
      have h1: ε⁻¹ < 10 ^ j → (10 ^ j: ℚ)⁻¹ < ε := by
        apply inv_lt_of_inv_lt
        assumption
    
    tactic =>
      -- 下記の行がエラーになる
      apply h1
  sorry

エラーになり，うまくいきません．

tactic 'apply' failed, failed to unify
  (10 ^ j)⁻¹ < ε
with
  ((10 ^ j)⁻¹ < ε) = ?m.35205 i j hji

なぜうまくいかないのでしょうか？書き換え自体は，h1 としてより強く同値を示し，rw [←h1] を使用すればできました．

[haruhisa-enomoto]

convに慣れていないので想像ですが、convの中に入ると、「ゴールを示す」ではなくて「項を書き換える」ことが目的になるはずです。（⊢じゃなくて|になる）
なので| (10 ^ j)⁻¹ < εがあってもapplyは使えず、書き換えのrwしか通らないのだと思います。

[Seasawher]

@haruhisa-enomoto ありがとうございます。rw するには同値が必要ですが、数学的にはここで同値は必要ないはずなので、apply のようなことができてほしいです

他の書き方で実現できないか考えてみます

[haruhisa-enomoto]

convがその目的に合わない（convは項をそれと等しい項に書き換えることを目的とする）ので、convを使わない書き方を考えてみるとapplyが使えると思います。

[Seasawher]

conv を使わない場合，どうやったら量化を外せるでしょうか？

存在量化がありますが，具体的に値を与えることなく存在量化を外したいと思っています．（示すべきことを言い換えてから，具体的な値を与えたいので）

[haruhisa-enomoto]

例えばsufficesを使うとゴールを求めるものに変えることができると思います。

[aconite-ac]

convモード中にターゲットの部分項をapplyによって十分条件に書き換えられないのは、次のような理由によると思われます。

---

いかなる状況でも、ターゲットの部分項をapplyによって十分条件に書き換えることができるとします。

ここで、例えば、

p q : Prop
⊢ p → q

という本来証明不可能なゴールがあった場合、
have h : p ∧ q → p := fun hh : p ∧ q => hh.leftによってコンテキストにh: p ∧ q → pを追加した後、
上記のゴールをconvとapplyによって

p q : Prop
h : p ∧ q → p
⊢ p ∧ q → q

に書き換えられることになります。
このゴールは証明できるため、本来証明不可能なゴールが証明できてしまうという事態が起きてしまいます。
したがって、「いかなる状況でもターゲットの部分項をapplyによって十分条件に書き換えることができる」という機能はあってはならないと分かります。

もちろんターゲットが含意命題の場合、その後件を十分条件によって書き換えるのは論理的に許される書き換えです。
しかし、一般にターゲットの部分項をapplyによって十分条件に書き換えてよいかどうかを判断するためには、
その部分項の情報だけでは不十分で、
「それがターゲット全体の後件であるか」といったターゲット全体の情報が必要です。
部分項を十分条件に書き換える機能は、convモードのタクティクではなく元々ターゲット全体の情報を必要とするsuffices等の通常のタクティクが担うべきであり、実際Leanではそのように実装されているのだと思います。

結局、convモード中に同値命題や等号命題を用いて部分項をrwすることはできるものの、
部分項をapplyによって十分条件に書き換えることはできないのは、
前者の書き換えが「いかなる状況でも許される」一方で、後者の書き換えは「特定の状況下でしか許されない」という違いに起因すると思われます。

[Seasawher]

部分項を十分条件に書き換える機能は、convモードのタクティクではなく元々ターゲット全体の情報を必要とするsuffices等の通常のタクティクが担うべきであり、実際Leanではそのように実装されているのだと思います。

ありがとうございます。なるほど…！