実際に等式推論演算子はどのように使用されていますか？

Question

Agda Standard Libraryは、紙に書いたことと同様の方法で証明書を書くことができる演算子や、Haskellコミュニティでどのように教えられているかを書き出す演算子をエクスポートします。あなたはwith抽象化、rewriteまたはヘルパー補助を使用して目標を洗練することによって、「慣習的な」Agdaプルーフを幾分体系的なやり方で書くことができますが、等価推論プリミティブを使った証明がどのようになるかは本当にわかりません"

つまり、これらの校正が完了し、タイプチェックがhereとthereの場合の例を見つけることができますが、これらの実例は、システムが段階的にどのように開発されたかを示していません。ステップ（おそらくホールドリブン方式）で行われる。

実際にどのように行われますか？人々の「リファクタ」にはすでに存在する証明がありますか？あなたは最初のゴールの左手と右手から始め、中央に穴を開けて「両脇からろうそくを燃やそう」としますか？

Agda documentationには、等価推論プリミティブが範囲内にある場合、「Autoはこれらの構文を使用して等価推論を行います」と記載されています。どういう意味ですか？

誰かが正しい方向に私を指すことができれば、また、これらの種類の証拠をどのように開発するかの例を投稿してもらうことができます。穴などを入れてください。ありがとう！

Answer 1

アイデンティティの等価推論の定義をここで見ると、より役に立つと思います。Equational Reasoning要点は、推移性連鎖を適用して、読みやすいほどの証拠ではなく、コード内の実際の式をユーザーが見ることができるようにするのは単なる良い方法だということです。

私は、任意のセトイドのための等式推論を使用して証明を構築する方法はこれです。自然数の例を用いて

open import Relation.Binary.PropositionalEquality 
open ≡-Reasoning 

data ℕ : Set where 
    zero : ℕ 
    succ : ℕ → ℕ 

_+_ : ℕ → ℕ → ℕ 
m + zero = m 
m + succ n = succ (m + n) 

例として、可換性を取ってみましょう。 これは私が目標から始める方法です。

comm+ : ∀ m n → m + n ≡ n + m 
comm+ m zero  = {!!} 
comm+ m (succ n) = 
    begin 
    succ (m + n) 
    ≡⟨ {!!} ⟩ 
    succ n + m 
    ∎ 

ここで、私はオリジナルの表現と目標を見ています。私の目標は括弧の間にあります。 私は、プルーフオブジェクトをそのままにしておきたい表現にのみ取り組み、 を追加してください。

comm+ : ∀ m n → m + n ≡ n + m 
comm+ m zero  = {!!} 
comm+ m (succ n) = 
    begin 
    succ (m + n) 
    ≡⟨ {!!} ⟩ 
    succ (n + m) 
    ≡⟨ {!!}⟩ 
    succ n + m 
    ∎ 

私に証拠があると思えば、私は自分のステップを正当化する証明オブジェクトを扱います。

オート・タクティクに関しては、私の意見では気にしないでください。それはしばらくの間働いていない。