CODEWITHSUNDEEP
proofidris
yanos
yanos

Reputation: 23

How to prove that 2 is Prime in Idris?

I'm a beginner in Idris now, so I want to ask for help. I have definition of division:

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

and definition of prime number, based on DividesNat:

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

Now I want to prove that 2 is prime:

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

Cases with d = (S Z) or d = (S (S Z)) are pretty simple:

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

but I have no idea how to prove it for d = Z or d = (S (S (S _))). How can I show that these cases are impossible?

Upvotes: 2

Views: 111

Answers (1)

Cactus
Cactus

Reputation: 27626

Finally I found the solution:

prf2IsPrime : Prime (S (S Z))
prf2IsPrime = ConsPrime (LTESucc (LTESucc LTEZero)) prf
    where
        prfGT32 : (S (S (S a))) `GT` (S (S Z))
        prfGT32 = LTESucc (LTESucc (LTESucc LTEZero))

        prf : (d : Nat) -> DividesNat (S (S Z)) d -> Either (d = 1) (d = (S (S Z)))
        prf Z (Div (x ** pf)) = absurd (zeroIsNotDiv (x ** pf))
        prf (S Z) (Div (x ** pf)) = Left Refl
        prf (S (S Z)) (Div (x ** pf)) = Right Refl
        prf (S (S (S _))) (Div (k ** pf)) =
            absurd (gtIsNotDiv prfGT32 (k ** pf))

Upvotes: 0

Related Questions