귀납적 Coq 정의에서 실존 적 한정사와 일반 한정사 사이의 관계

Question

문자열이 목록의 동의어 인 부분 문자열의 귀납적 한정자를 원한다고 가정합니다. 여기

Inductive substring {A : Set} (w : string A) : 
        (string A) -> Prop := 
    | SS_substr : forall x y z : string A, 
        x ++ y ++ z = w -> 
        substring w y. 

내가 예를 들어 다음과 같은 증명할 수 :

이

Theorem test : substring [3;4;1] [4]. 
Proof. 
    eapply SS_substr. 
    cbn. 
    instantiate (1:=[1]). 
    instantiate (1:=[3]). 
    reflexivity. 
Qed. 

그러나 증거는 사실에도 불구하고, 오히려 "보편적"이 아닌 "존재"입니다 유도 정의 상태 forall x y z 만 그들의 모양을 제한한다. 이것은 다소 비현실적입니다. 뭐라 구요?

또한 유도 정의를 exists x : string A, exists y : string A, exists z : string, x ++ y ++ z = w -> substring w y을 사용하여 만들 수 있습니까?

Answer 1

참고로 중요한 점은 exists은 Coq의 기본 제공 기능 (forall과 반대)이라는 점입니다. 실제로는 exists 자체가 표기이지만 뒤에는 ex이라는 유도 형이 있습니다. 표기법과 유도 형은 Coq standard library에 정의되어 있습니다. 여기 ex의 정의는 다음과 같습니다

그것은 하나의 생성자와 substring 유형과 같은 보편적 인 정량을 사용하여 정의됩니다, 그래서 당신의 susbtring 유형은 어떤 점에서 "존재"가 될 것으로 보인다 것은 놀라운 일이 아니다

Inductive ex (A:Type) (P:A -> Prop) : Prop := 
    ex_intro : forall x:A, P x -> ex (A:=A) P. 

.

물론 exists을 사용하여 유형을 정의 할 수 있으며 Inductive도 필요하지 않습니다.

Definition substring' {A : Set} (w y : string A) : Prop := 
    exists x z, x ++ y ++ z = w.