Как доказать, что 2 является Prime в Идрисе? - PullRequest
Новая
       41

Как доказать, что 2 является Prime в Идрисе?

2 голосов
/ 28 марта 2020

Я новичок в Идрисе, поэтому хочу обратиться за помощью. У меня есть определение деления: 

data DividesNat : (a : Nat) -> (b : Nat) -> Type where
    Div : (k ** (k * x = y)) -> DividesNat y x

и определение простого числа, основанное на DividesNat: 

data Prime : (p : Nat) -> Type where
    ConsPrime : LTE 2 p ->
        ((d : Nat) -> DividesNat p d -> Either (d = 1) (d = p)) ->
        Prime p

Теперь я хочу доказать, что 2 простое: 

prf2IsPrime : Prime (S (S Z))
prf2IsPrime = ConsPrime (LTESucc (LTESucc LTEZero)) prf
    where
        prf : (d : Nat) -> DividesNat (S (S Z)) d ->
            Either (d = 1) (d = (S (S Z)))
        prf d x = ?prf_rhs

Случаи с d = (SZ) или d = (S (SZ)) довольно просты: 

prf : (d : Nat) -> DividesNat (S (S Z)) d ->
            Either (d = 1) (d = (S (S Z)))
        prf Z (Div (x ** pf)) = ?prf_rhs2_3
        prf (S Z) (Div (x ** pf)) = Left Refl
        prf (S (S Z)) (Div (x ** pf)) = Right Refl
        prf (S (S (S _))) (Div (x ** pf)) = ?rr_2

, но я не знаю, как доказать это для d = Z или d = (S (S (S _))). Как я могу показать, что эти случаи невозможны?

...