Coq의 제한된 유도 형 정의

Question

귀납적 인 정의에서 어떤 종류의 입력 생성자가 허용되는지 제한하고 싶습니다. 나는 다음과 같이 진수를 정의 말하고 싶은 말 :

Inductive bin : Type := 
    | O : bin 
    | D : bin -> bin 
    | S : bin -> bin. 

생각이 여기 D가 마지막에 0을 추가하여 0이 아닌 숫자를 두 배로 S가 마지막 숫자로 0으로 숫자를 취하고 변이다 마지막 숫자를 하나에 입력하십시오.

S 0 
D (S 0) 
D (D (S 0)) 

다음은되지 않을 것 동안 : 이것은 다음 법적 숫자는 것을 의미 깨끗한 방법으로 유도 정의에 이러한 제한을 적용 할 수있는 방법이

S (S 0) 
D 0 

있습니까?

Answer 1

bin이 술어와 합법적이라는 것을 정의한 다음 해당 술어를 따르는 서브 세트 bin에 이름을 지정할 수 있습니다. 그런 다음 Definition 및 Fixpoint 대신 Program Definition 및 Program Fixpoint을 사용하여 함수를 작성합니다. 재귀 함수의 경우 함수가 더 이상 구조적으로 재귀 적이 아니므로 함수의 인수가 크기가 감소 함을 증명하는 척도가 필요합니다.

Require Import Coq.Program.Program. 

Fixpoint Legal (b1 : bin) : Prop := 
    match b1 with 
    | O  => True 
    | D O  => False 
    | D b2 => Legal b2 
    | S (S _) => False 
    | S b2 => Legal b2 
    end. 

Definition lbin : Type := {b1 : bin | Legal b1}. 

Fixpoint to_un (b1 : bin) : nat := 
    match b1 with 
    | O => 0 
    | D b2 => to_un b2 + to_un b2 
    | S b2 => Coq.Init.Datatypes.S (to_un b2) 
    end. 

Program Definition zer (b1 : lbin) := O. 

Program Fixpoint succ (b1 : lbin) {measure (to_un b1)} : lbin := 

그러나 this 간단 유형 접근 방식은 아마 더 쉬울 것입니다.

Answer 2

유도 성 재귀 정의를 사용하여 수행 할 수 있지만 불행히도 Coq는이를 지원하지 않습니다. 객체 지향 프로그래밍 관점에서

는 O, D 및 S는 bin의 서브 타입이며, 자신의 생성자 유형은 논리적 술어에 의존하지 않고 다음 정의하지만, COQ는 기본적으로 두 객체 지향 프로그래밍을 지원하지 않습니다.

그러나 Coq에는 typeclasses가 있습니다. 그래서 내가 할 수있는 일은 bin을 typeclass로 만들고 각각의 생성자를 각각 유도 유형으로 만들고 각 인스턴스는 bin typeclass의 인스턴스를 갖습니다. 나는 typeclass의 방법 (들)이 어떤 것인지 확신하지 못한다.