coq - 匿名関数内の式を単純化する簡単な方法は?

Question

次のようなことを証明する必要があるとします。

x: nat

(fun _ : nat => 0) = (fun y : nat => if beq_nat x y then 0 else 0)

は環境にないので、右辺を単純化してy上に破壊することはできないようです。beq_nat x y無名関数内の式を単純化する簡単な方法はありますか?

2 つの関数が同じように見えるように処理する以外に、すべての入力で同じ値を生成することを示すことで、2 つの関数が同じであると推測する方法はありますか?

EDIT：私は不可能なことを求めているかもしれないことを認識しています。これらの関数は同じではないため、引数に適用すると同じ値が生成されるだけです。Coqがこれをどのように解釈するかは正確にはわかりません。

score 1 · Accepted Answer

functional extensionalityこれは、 2 つの関数が拡張的に等しい (呼び出し元の観点からは同じように動作する) ことを証明したい、と呼ばれるもののケースだと思います。

Coq で直接証明することはできません (=は定義上の等式であるため、真ではありません)。ただし、必要に応じて、次のモジュールを要求できます。

これは、機能拡張性の公理を提供します。extensionality y.へのアクセスを可能にする戦術を呼び出すことができますy。

1 に答える 1