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. 

=?이 COQ의 ZArith에서 Z에 부울 decidable 평등을 나타냅니다.

이제 FF 두 개에 평등을 갖고 싶습니다. functional_extensionality을 불러도 괜찮습니다. 내가 지금하고 싶은 것은 Coq가 두 개의 균등성을 계산으로 결정하도록하는 것이다.

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

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

이제 우리는 foo 및 foo', 사람들은 기능 extensionality에서 동일을 만들기 위해 어떤 임의의 값을 추가 :

예를 들어

, 우리는의 라인을 따라 뭔가를 생각 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으로 끝나며 이는 도메인 제한 인 FF에 n * constant을 도메인에 해당하는 것과 같습니다. 따라서 함수 f은 천천히 (상수 인자에 의해) FF가 정의 된 도메인을 확장합니다.

Answer 1

필자는 코멘트에서 만족스러운 대답을 자세히 설명하기 위해 더 자세한 내용이 필요하다고 말했기 때문에. 제한 기능에 대한 평등 재생하는 방법에 대한 단계를 설명 ---에 의해 단계를위한 아래의 예를 --- 참조하는 mathcomp를 사용하여 범위 :

는

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. 

마지막 보조 정리는 실제로 당신이에 기능의 평등을 줄일 수 있도록해야 전산, 완벽하게 실행 가능한 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

좋아, 이것은 대소 문자 구별을 여러 번 반복하지 않아도되지만 완전히 자동화 된 다소 잔인한 솔루션입니다.

두 정수가 같은지 (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이라고 부르는 경우 두 번째 분기는 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 모든 수입과 정의와 함께.