Idris - 소수 유형 정의

Question

나는 이드리스를 배우기 때문에 개인 연습으로 모든 소수로 구성된 Primes 유형을 구현하고 싶습니다.

유형 및 속성에서 시작하여 새로운 유형을 정의하는 idris에 속성이있는 시작 유형의 모든 요소를 ​​선택하는 방법이 있습니까? 제 경우에는 Primes을 Nat의 집합으로 정의하는 방법이 있습니까? n <= p and n|p => n=1 or n=p?

이것이 가능하지 않은 경우, 일종의 체를 사용하여 유도 식으로 구성하는 소수를 정의해야합니까?

Answer 1

나는 이드리스에서 다음과 같이 보이는, copumpkin's Agda definition of Prime을 좋아한다 :

data Divides : Nat -> Nat -> Type where 
    MkDivides : (q : Nat) -> 
       n = q * S m -> 
       Divides (S m) n 

data Prime : Nat -> Type where 
    MkPrime : GT p 1 -> 
      ((d : Nat) -> Divides d p -> Either (d = 1) (d = p)) 
      -> Prime p 

읽기로 "p가 D로 나누어 경우, 다음 d를 1 P해야"- 소수성에 대한 일반적인 정의.

숫자에 대한 손으로 이것을 증명하는 것은 매우 지루한 될 수 있습니다

p2' : (d : Nat) -> Divides d 2 -> Either (d = 1) (d = 2) 
p2' Z (MkDivides _ _) impossible 
p2' (S Z) (MkDivides Z Refl) impossible 
p2' (S Z) (MkDivides (S Z) Refl) impossible 
p2' (S Z) (MkDivides (S (S Z)) Refl) = Left Refl 
p2' (S Z) (MkDivides (S (S (S _))) Refl) impossible 
p2' (S (S Z)) (MkDivides Z Refl) impossible 
p2' (S (S Z)) (MkDivides (S Z) Refl) = Right Refl 
p2' (S (S Z)) (MkDivides (S (S _)) Refl) impossible 
p2' (S (S (S _))) (MkDivides Z Refl) impossible 
p2' (S (S (S _))) (MkDivides (S _) Refl) impossible 

p2 : Prime 2 
p2 = MkPrime (LTESucc (LTESucc LTEZero)) p2' 

그것은 이것에 대한 의사 결정 절차를 쓰기도 매우 복잡합니다. 그게 큰 운동이 될거야! 나머지 정의는 유용 할 것입니다.

https://gist.github.com/copumpkin/1286093