하위 유형 Coq

Question

subtypes을 Coq에 연습하고 ssreflect을 사용하여 사물을 단순화하려고합니다. 하지만 하위 유형을 다시 작성할 때는 항상 문제가 발생합니다. 예 :

Require Import Omega. 
From mathcomp Require Import ssreflect ssrfun ssrbool ssrnat eqtype. 

(* a type A to build X *) 
Inductive A: Set := 
| mkA: nat -> A. 

Definition getNat_A (a: A) := 
match a with 
| mkA n => n 
end. 

Inductive X: Set := 
| r1 : A -> X. 

(* subtype of X that satisfying some property *) 
Definition Instantiated_X (x : X) : bool := 
    match x with 
    | r1 a => (getNat_A a) > 10 
end. 

Definition iX : Set := {x:X | (Instantiated_X x)}. 

(* rewrite constructor of X, stating the fact of elements of A, under certain condition creates element of iX *) 
Program Definition r1_rewrite : A -> option iX := 
fun a: A => 
match (Instantiated_X (r1 a)) with 
| true => Some (exist _ (r1 a) _) 
| false => None 
end. 

(* try to prove r1_rewrite is surjective *) 
Example r1_rewrite_surj: 
forall t : iX, exists (a : A), 
match (r1_rewrite a) with 
| None => True 
| Some e => eq t e 
end. 
Proof. 
    intros. 
    destruct t eqn: caseiX. 
    destruct x eqn: caseX. 
    exists a. 
    destruct (r1_rewrite a) eqn: r_res. 
    - destruct (10 < getNat_A a) eqn: guard. 
    destruct i0. 
    destruct x0. 
    unfold r1_rewrite in r_res. 
    simpl in r_res. 
    rewrite <- guard in r_res. (* <- stuck *) 
Abort. 

왜 거기에 붙어 있는지 이해할 수 없었습니다. 오류 메시지의 말 :

Error: Abstracting over the term "true" leads to a term: ... 
which is ill-typed. 

나는 COQ이 같은 리드하는 r_res에 true와 (10 < getNat_A a)의 모든 항목을 바꾸 것이라고 생각 :

Some (exist (fun x : X => Instantiated_X x) (r1 a) 
      (r1_rewrite_obligation_1 a Heq_anonymous) = 
Some (exist (fun x : X => Instantiated_X x) (r1 a0) i0) 

및 proof irrelevance 및 r1 injectivity에 의해, 내 증거가 갈 수 있습니다 을 통하여. 그래서, 나는이 경우에 r_res을 어떻게 마사지 할 수 있는지에 대한 포인터를 얻을 수 있을지 궁금해합니다. 그래서 재 작성을 용이하게합니다.

편집 : 증명서 시도와

Answer 1

문제 예를 더 간결하게 Eq 타입 클래스를 제거하고, 그 경우 당신은 당신이 다시 작성 방법에 대한 조심해야한다는 것입니다. 여기에 가능한 해결책이 있습니다.

Example r1_rewrite_surj: 
forall t : iX, exists (a : A), 
match (r1_rewrite a) with 
| None => True 
| Some e => eq t e 
end. 
Proof. 
move=> [[a] Pa]; exists a; rewrite /r1_rewrite. 
move: (erefl _); rewrite {1 3}Pa. 
by move=> e; rewrite (eq_irrelevance (r1_rewrite_obligation_1 _ _) Pa). 
Qed. 

여기에서 무슨 일이 일어나고 있는지 지켜 보는 것은 약간 까다 롭습니다. 첫 번째 줄에 후, 증거 상태는 다음과 같습니다

a : A 
    Pa : Instantiated_X (r1 a) 
    ============================ 
    match 
    (if Instantiated_X (r1 a) as b return b = Instantiated_X (r1 a) -> option iX 
    then 
     fun H : true = Instantiated_X (r1 a) => 
     Some (exist (fun x : X => Instantiated_X x) (r1 a) (r1_rewrite_obligation_1 a H)) 
    else fun _ : false = Instantiated_X (r1 a) => None) (erefl (Instantiated_X (r1 a))) 
    with 
    | Some e => exist (fun x : X => Instantiated_X x) (r1 a) Pa = e 
    | None => True 
    end 

우리가 아래의 발생의에서 Pa으로 재 작성하려고하면

, 우리는 유형의 오류가 발생합니다. 예를 들어 우리가 Instantiated_X (r1 a)의 첫 번째 항목을 대체하려고하면

1. , COQ은 우리가 if(erefl (Instantiated_X (r1 a))의 결과를 적용 할 수 없습니다.

2. 의 첫 번째, 두 번째 및 여섯 번째 (erefl에있는 것)를 true으로 바꾸면 위의 문제를 해결할 수 있습니다. 또한 r1_rewrite_obligation_1의 입력을 잘못 입력하면이 기능이 작동하지 않습니다.

   forall e : Instantiated_X (r1 a) = Instantiated_X (r1 a), 
       match 
       (if Instantiated_X (r1 a) as b return b = Instantiated_X (r1 a) -> option iX 
       then 
        fun H : true = Instantiated_X (r1 a) => 
        Some (exist (fun x : X => Instantiated_X x) (r1 a) (r1_rewrite_obligation_1 a H)) 
       else fun _ : false = Instantiated_X (r1 a) => None) e 
       with 
       | Some e0 => exist (fun x : X => Instantiated_X x) (r1 a) Pa = e0 
       | None => True 
       end 
   

   아마 쉽게 볼 수없는, 그러나이 시점에서 안전 :

이 솔루션은 다음과 같은 증거 상태로 선도 (전화 move: (erefl _)과) erefl을 통해 일반화하는 것입니다 Pa으로 다시 작성하여 Instantiated_X (r1 a)의 첫 번째 및 세 번째 항목을 대체하고 if을 줄일 수 있습니다. 우리는 부울 평등과 무관하다는 증거에 호소함으로써 결론을 내릴 수 있습니다.

물론 이런 식으로 타이핑하는 문제에 대한 추론은 악몽입니다. ejgallego가 지적했듯이이 경우 ssreflect의 하위 유형 지정 시스템을 재사용하는 것이 훨씬 쉽습니다. 예를 들어 :

(* Other definitions remain the same *) 
Definition r1_rewrite a : option iX := insub (r1 a). 

Example r1_rewrite_surj: 
forall t : iX, exists (a : A), 
match (r1_rewrite a) with 
| None => True 
| Some e => eq t e 
end. 
Proof. 
by move=> [[a] Pa]; exists a; rewrite /r1_rewrite insubT. 
Qed. 

insub 기능은 r1_rewrite의 일반 버전입니다.하위 유형을 정의하는 속성이 있는지 여부를 확인하고 일치하는 경우 해당 증명과 일치하는 쌍을 검사합니다. insubT 보조 정리 (lemma)는 속성이 보유 될 때 insub이 Some을 반환한다고 말합니다.