Coq의 증명 인수

Question

Coq에서 약하게 지정된 유형의 함수를 정의하려고합니다. 특히, 재귀 적 생성자 집합에 의해 유도 적으로 정의되는 유형이 있고, 인수의 일부만 사용하여 생성 된 경우에만 정의되는 함수를 정의하려고합니다.

Inductive Example : Set := 
    | Example_cons0 : nat -> Example 
    | Example_cons1 : Example -> Example 
    . 

지금, 난 단지 땅 케이스에 적용되는 기능을 가지고 :

더 구체적를하기 위해, 나는 다음과 같은 유형의 정의를 가지고있다. (다음 정의는 분명히 작동하지 않습니다,하지만 내 의도를 제안하기위한 것입니다.)

Definition example (x:Example) : nat := 
    match x with 
    | Example_cons0 n => n 
    end. 

를 이상적으로, 나는 일반적인 유형 생성자의 일부를 사용하여 내 인수, X는, 구축 된 것을 전달하고 싶습니다 ,이 경우 Example_cons0. 나는이 사실을 언급하고 술어의 증거를 논증으로 전달하는 술어를 정의함으로써 이것을 할 수 있다고 생각했다. 예를 들어 :

Definition example_pred (x:Example) : Prop := 
    match x with 
    | Example_cons0 _ => True 
    | _ => False 
    end. 

그리고 뭔가 같은

Definition example2 (x:Example) : example_pred x -> nat := 
    (use proof to define example2?) 

불행하게도, 나는이 중 하나를 수행 가겠어요 방법을 잘 모르겠어요 (로빈 그린에 의해 주어진 권고에 따라). 필자는 약한 유형의 제한된 함수를 정의하는 올바른 방법이라고 확신하지 못합니다.

모든 안내, 제안 또는 제안 사항을 강력하게 환영합니다. - 리

업데이트 : 세부 사항에 대한 자신의 의견을 참조

Definition example (x:Example) : example_pred x -> nat := 
    match x with 
    | Example_cons0 n => fun _ => n 
    | _    => fun proof => match proof with end 
    end. 

:

jozefg에 의한 권고에 따라이 예제 함수는 다음과 같이 정의 할 수 있습니다. 이 함수는 다음 구문을 사용하여 평가할 수 있습니다. 증명 용어가 Coq에 표시되는 방법을 보여줍니다.

Coq < Eval compute in Example.example (Example.Example_cons0 0) (I : Example.example_pred (Example.Example_cons0 0)). 
    = 0 
    : nat 

Answer 1

내가

우리가 도움이 기능을

Definition bar f := 
    match f with 
    | Bar _ => True 
    | Baz => False 
    end. 

그리고 정의

Inductive Foo := 
| Bar : nat -> Foo 
| Baz. 

이제 간단한 데이터 유형을 고려 간단한 예로서 이것을 써서 방법은 마지막으로 당신이 원하는 것을 쓰기 :

Definition example f := 
    match f return bar f -> nat with 
    | Bar n => fun _ => n 
    | Baz => fun p => match p with end 
    end. 

이 유형은 forall f : Foo, bar f -> nat입니다. 이것은 example에 Bar이 제공되지 않은 경우 사용자가 false (불가능)의 증명을 제공해야한다는 것을 확인함으로써 작동합니다. 그렇지 않으면 어떻게 COQ 알고 가정된다,

이

이

example (Bar n) I 

처럼 호출 할 수 있습니다 그러나 문제는 수동으로 일부 용어는 Bar로 구성되어 증명해야 할 수도있다?

Answer 2

예, 올바른 행에 있습니다. 원한다면 :

Definition example2 (x:Example) (example_pred x) : nat := 

어떻게 진행할 것인가는 당신이 증명하고 싶은 것에 달려 있습니다.

당신은 카레 - 하워드 대응하여, 전술을 증명하여 정의를 확인하는 것이 도움이 될 : 나는 sig 및 sigT 유형이 자주 사용되는 것을 지적하고 싶습니다, 또한

Definition example2 (x:Example) (example_pred x) : nat. 
Proof. 
    some proof 
Defined. 

을 "weakly-specified types"와 술어를 결합하여 제약합니다.여기