Coq機能の拡張性

Question

私は、本体を書き直したい機能を持つ目標を持っていますが、 いくつかの関数引数が書き換えの途中にあります。 アイデンティティ関数を使って状況を再現しました。

機能がDefinedであれば、それは動作しますが、機能 はパラメータであり、私が書き換えする方法を述べる公理を持っているとき、私は書き換えることができ ありませんよ。

機能的な拡張性を前提として動作させることができます。 機能的な拡張性を前提としないで何とか書き直すことは可能ですか？

Axiom functional_extensionality: forall {A B} (f g:A->B) , (forall x, f x = g x) -> f = g. 

Variables A B : Type. 
Variable f : A -> B. 

Definition Id (x : B) := x.   (* here my function is Defined *) 

Goal (fun x => Id (f x)) = f.  (* I'd like to rewrite inside the fun *) 

Proof. auto. Qed.     (* This works (eta reduction). *) 

Variable Id' : B -> B.    (* Here I don't have the function definition *) 
Axiom ID  : forall x, Id' x = x. (* only proof that it does the same thing *) 
Goal (fun x => Id' (f x)) = f. 
Proof. 
    rewrite ID.      (* this doesnt work *) 
    eauto using functional_extensionality, ID. (* but this works *) 

Answer 1

残念ながら、機能的な拡張性を前提としないとこれを証明することはできません。 Coqは、fun x => Id' (f x)) = fun x => f xが「定義的に」保持することを要求する。

「定義的に」ここでは何を意味していますか？簡潔に言えば、両方の用語が同じ普通形を持たなければならないことを意味します。構文的にはです。 Coqでは、すべての項がベータ還元によって（主に）誘導される正規形を持つことを思い出してください。

しかし、われわれはId' x = xを「判断する」ことしか知りません。したがって、Coqは上記の両方の用語が「定義的に」等しくならないように、Id' x ~> xを実行することはできません。

これは確かにCoqの理論の限界です。私は理解しているので、タイプチェックは決定可能なままです。

この証明を完成するもう1つのアプローチは、この方程式を満たす唯一の関数がfun x => x（パラメトリック）であることを導出することです。これにより、証明書を完成させるための仮説Hid: ID' = (fun x => x)が得られます。残念ながらHidはCoqの内部では証明できません。