我现在是Idris的初学者,所以我想寻求帮助。 我有除法的定义:
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 =(S Z)或d =(S(S Z))的情况非常简单:
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 _)))
进行证明。我如何证明这些情况是不可能的?