Coqの無限表現の有限部分集合を使った計算

Question

私は(Z, Z)からwhateverにマップの一種として扱う関数Z -> Z -> whateverを持っています。FFとタイプしましょう。

whateverは、nixまたはinj_whateverから構成可能な単純和です。

私はの形で、いくつかのデータを初期化し、このマップ：

Definition i (x y : Z) (f : FF) : FF := 
    fun x' y' => 
    if andb (x =? x') (y =? y') 
    then inj_whatever 
    else f x y. 

=?はコックのZArithから、Zのブール決定可能平等を表します。

ここでは、FFのうちの2つについて同等性を持たせたいと考えています。私はfunctional_extensionalityを呼び出しても構いません。私が今やりたいことは、Coqが2つの等価性を計算的に決定させることです。FF例えば

、我々はの線に沿って何かやるとします今、私たちはfooとfoo'を作るために、いくつかの任意の値を追加

Definition empty : FF := fun x y => nix.

を、それらが機能extensionalityの下に等価です：

Definition foo := i 0 0 (i 0 (-42) (i 56 1 empty)).
Definition foo' := i 0 (-42) (i 56 1 (i 0 0 empty)).

omctをfoo = foo'とCoqで決める。 Ltacレベルのもの？実際の終了計算？有限なものにドメイン制限が必要ですか？

ドメインの制限は、複雑なものです。 f : FF -> FFという方法でマップを操作します。fは、計算が定義されているZ x Zのサブセットを拡張できます。考えてみると、f : FF -> FFはありませんが、f : FF -> FF_1のようになります。ここで、FF_1は、小さな定数で拡張されたZ x Zのサブセットです。そのため、fをn回適用すると、ドメイン制限がFFに加えてn * constantのドメインに相当するFF_nになります。関数fはゆっくり（一定の係数で）ドメインFFを定義して拡張します。

Answer 1

私がこのコメントで述べたように、満足のいく答えを詳述するためにはより詳細な説明が必要です。最後の補題が実際にあなたが機能の平等を削減できるようにする必要があり

From mathcomp Require Import all_ssreflect all_algebra. 

Set Implicit Arguments. 
Unset Strict Implicit. 
Unset Printing Implicit Defensive. 

(* We need this in order for the computation to work. *) 
Section AllU. 
Variable n : nat. 

(* Bounded and unbounded fun *) 
Definition FFb := {ffun 'I_n -> nat}. 

Implicit Type (f : FFb). 

Lemma FFP1 f1 f2 : reflect (f1 = f2) [forall x : 'I_n, f1 x == f2 x]. 
Proof. exact/(equivP eqfunP)/ffunP. Qed. 

Lemma FFP2 f1 f2 : 
    [forall x : 'I_n, f1 x == f2 x] = all [fun x => f1 x == f2 x] (enum 'I_n). 
Proof. 
by apply/eqfunP/allP=> [eqf x he|eqf x]; apply/eqP/eqf; rewrite ?enumT. 
Qed. 

Definition f_inj (f : nat -> nat) : FFb := [ffun x => f (val x)]. 

Lemma FFP3 (f1 f2 : nat -> nat) : 
    all [fun x => f1 x == f2 x] (iota 0 n) -> f_inj f1 = f_inj f2. 
Proof. 
move/allP=> /= hb; apply/FFP1; rewrite FFP2; apply/allP=> x hx /=. 
by rewrite !ffunE; apply/hb; rewrite mem_iota ?ltn_ord. 
Qed. 

(* Exercise, derive bounded eq from f_inj f1 = f_inj f2 *) 

End AllU. 

：制限された機能上の平等と遊ぶ方法に関するステップの説明によってステップ---ためのもの例---以下mathcompを使用して範囲を参照してください。計算上、完全に実行可能なGallina関数。

Lemma FFP n (f1 f2 : nat -> nat) : 
    [forall x : 'I_n, f1 x == f2 x] = all [pred x | f1 x == f2 x] (iota 0 n). 
Proof. 
apply/eqfunP/allP=> eqf x; last by apply/eqP/eqf; rewrite mem_iota /=. 
by rewrite mem_iota; case/andP=> ? hx; have /= -> := eqf (Ordinal hx). 
Qed. 

しかし、それは範囲の制限にあなた（欠席）条件が指定されている方法によって異なります。あなたに

簡素上記のバージョン、およびおそらくより有用です。

編集後、マップの平等に関するより一般的なトピックについてのメモを追加する必要があります。A -> B以外のより具体的な種類のマップを定義してから、決定手順を作成することができます。

[バインディング検索]の操作をサポートしている限り、[stdlibのものを含めて]最も一般的なマップタイプが機能するため、非常に多くのバインドされた値のチェックと等価性を減らすことができます。

実際、Coqの標準ライブラリのマップは、すでにこのような計算平等関数を提供しています。

Answer 2

これは、同じケースの区別を何度も繰り返すことを避けようとしていない、残酷な解決策ですが、完全に自動化されています。

2つの整数が等しいかどうか（Z.eqbを使用して）検査し、その結果をomegaが処理できる命題に変換する方法から始めます。

Ltac inspect_eq y x := 
    let p := fresh "p" in 
    let q := fresh "q" in 
    let H := fresh "H" in 
    assert (p := proj1 (Z.eqb_eq x y)); 
    assert (q := proj1 (Z.eqb_neq x y)); 
    destruct (Z.eqb x y) eqn: H; 
    [apply (fun p => p eq_refl) in p; clear q| 
    apply (fun p => p eq_refl) in q; clear p]. 

我々はそれが見つけることができるiの最初の発生を発射する機能を書くことができます。これは、状況に矛盾する仮定を導入することができる。前回の一致がx = 0であるが、今度はinspect x 0と呼び出すと、2番目のブランチはx = 0とx <> 0の両方のコンテキストになります。それは自動的にomegaによって却下されます。

Ltac fire_i x y := match goal with 
    | [ |- context[i ?x' ?y' _ _] ] => 
    unfold i at 1; inspect_eq x x'; inspect_eq y y'; (omega || simpl) 
end. 

私たちは、その後、一緒にすべてを置くことができます（！確かに矛盾を持つすべてのブランチが自動的に却下されています）reflexivityによって検査し、締結する他に何もないまでfire_iを繰り返し、二回機能extensionalityを呼び出します。

Ltac eqFF := 
    let x := fresh "x" in 
    let y := fresh "y" in 
    intros; 
    apply functional_extensionality; intro x; 
    apply functional_extensionality; intro y; 
    repeat fire_i x y; reflexivity. 

我々は、それがどんな問題なくあなたの補題を排出していることがわかります。すべての輸入品との定義と

Lemma foo_eq : foo = foo'. 
Proof. 
unfold foo, foo'; eqFF. 
Qed. 

Here is a self-contained gistを。