Прочитал недавно в книге С. Клини "Введение в метаматематику" о теореме Евклида, которая говорит, что простых чисел существует бесконечное количество. Теорема эта доказывается так же и в интуиционистской логике. Это и послужило стимулом реализовать его на Agda.
Конечно же в интуиционистской логике бесконечность только потенциальна, поэтому теорема там звучит так: "Для каждого натурального числа существует большее простое". В терминах Agda это будет функция которая принимает аргумент — натуральное число и возвращает другое натуральное число, доказательство, что оно простое и другое доказательство, что оно больше первого.
Краткое описание
Алгоритм доказательства предельно прост. Сначала нужно для заданного числа n найти его факториал (на самом деле можно любое общее кратное, но факториал проще всего). Далее нужно заметить, что n! + 1 не делится на числа меньше или равно n, кроме единицы конечно. Поэтому, если найти любой простой делитель n! + 1, то он будет больше n.
Общее кратное
Ниже описана функция которая для ненулевого натурального n возвращает число m и функцию, которая для всех чисел x от единицы до входного числа n возвращает доказательство, что x делит m. Реализация конечно же рекурсивная.
common-multiple : ∀ n → 1 ≤ n → Σ[ m ∶ ℕ ] n ≤ m × (∀ k → 1 ≤ k → k ≤ n → k ∣ m) common-multiple zero () common-multiple (suc zero) (s≤s z≤n) = 1 , s≤s z≤n , f where f : ∀ k → 1 ≤ k → k ≤ 1 → k ∣ 1 f .1 (s≤s z≤n) (s≤s z≤n) = 1 , refl common-multiple (suc (suc n)) (s≤s z≤n) = step $ common-multiple (suc n) 1≤n₀ where n₀ = suc n 1≤n₀ = s≤s z≤n ∶ 1 ≤ n₀ n₁ = suc n₀ step : Σ[ m₀ ∶ ℕ ] n₀ ≤ m₀ × (∀ k → 1 ≤ k → k ≤ n₀ → k ∣ m₀) → Σ[ m₁ ∶ ℕ ] n₁ ≤ m₁ × (∀ k → 1 ≤ k → k ≤ n₁ → k ∣ m₁) step (m₀ , n₀≤m₀ , f₀) = (m₁ , n₁≤m₁ , f₁) where m₁ = m₀ * n₁ n₁≤m₁ : n₁ ≤ m₁ n₁≤m₁ = b≤a*b m₀ (≤-trans 1≤n₀ n₀≤m₀) n₁ f₁ : ∀ k → 1 ≤ k → k ≤ n₁ → k ∣ m₁ f₁ k 1≤k k≤n₁ with a<b⊎a≡b k≤n₁ ... | inj₁ (s≤s k≤n₀) = ∣-trans₁ k m₀ n₁ (f₀ k 1≤k k≤n₀) ... | inj₂ k≡n₁ = m₀ , ≡-trans (≡-cong (λ x → x * m₀) k≡n₁) (*-commut n₁ m₀)
Простой делитель. Вспомогательные функции
Сначала опишем функцию, которая будет для некоторого числа возвращать его делитель или доказательство, что оно простое. Для n! + 1 будем рекурсивно применять эту функцию, если результат — это доказательство, что вход — простое, значит нашли что искали, если же делитель, то применяем эту функцию к делителю.
Ниже вспомогательная функция для рекурсивного спуска:
divisor-or-prime-step : ∀ n m → 1 < m → (∀ k → suc m ≤ k → k < n → ¬ k ∣ n) → (∀ k → m ≤ k → k < n → ¬ k ∣ n) ⊎ m ∣ n divisor-or-prime-step n m 1<m f₁ with m∣n⊎¬m∣n n m $ ≤-trans (s≤s z≤n) 1<m ... | inj₁ m∣n = inj₂ m∣n ... | inj₂ ¬m∣n = inj₁ f₂ where f₂ : ∀ k → m ≤ k → k < n → ¬ k ∣ n f₂ k m≤k k<n with a<b⊎a≡b m≤k ... | inj₁ m<k = f₁ k m<k k<n ... | inj₂ m≡k = ≡-elim m≡k (λ x → ¬ x ∣ n) ¬m∣n
Ниже функция, которая возвращает делитель входного числа или доказательство, что оно — простое:
divisor-or-prime : ∀ n → 1 ≤ n → (Σ[ m ∶ ℕ ] 1 < m × m < n × m ∣ n) ⊎ prime n divisor-or-prime zero () divisor-or-prime (suc zero) _ = inj₂ p where p : prime 1 p .0 () (s≤s z≤n) divisor-or-prime (suc (suc zero)) _ = inj₂ p where p : prime 2 p .1 (s≤s ()) (s≤s (s≤s z≤n)) divisor-or-prime (suc (suc (suc n₀))) (s≤s z≤n) with m∣n⊎¬m∣n (3 + n₀) (2 + n₀) (s≤s z≤n) ... | inj₁ m∣n = inj₁ $ 2 + n₀ , s≤s(s≤s z≤n) , a≤a(3 + n₀) , m∣n ... | inj₂ ¬m∣n = loop (2 + n₀) (s≤s(s≤s z≤n)) (a≤a(3 + n₀)) f₀ where n = 3 + n₀ f₀ : (∀ k → suc (suc n₀) ≤ k → k < n → ¬ k ∣ n) f₀ zero () _ f₀ (suc zero) (s≤s ()) _ f₀ (suc (suc k₀)) m≤k (s≤s k≤m) = ≡-elim (a≤b×b≤a m≤k k≤m) (λ x → ¬ x ∣ n) ¬m∣n loop : ∀ m → 1 < m → m < n → (∀ k → m ≤ k → k < n → ¬ k ∣ n) → (Σ[ m ∶ ℕ ] 1 < m × m < n × m ∣ n) ⊎ prime n loop zero () _ _ loop (suc zero) (s≤s ()) _ _ loop (suc (suc zero)) _ _ f₁ = inj₂ f₁ loop (suc (suc (suc m₀))) 1<m m<n f₁ with divisor-or-prime-step n (2 + m₀) (a≤a+b 2 m₀) f₁ ... | inj₂ m''∣n = inj₁ (2 + m₀ , s≤s (s≤s z≤n) , ≤-trans (a≤b+a (3 + m₀) 1) m<n , m''∣n) ... | inj₁ f₂ = loop (suc (suc m₀)) (s≤s(s≤s z≤n)) (≤-trans (a≤b+a (3 + m₀) 1) m<n) f₂
Простой делитель. Конец
Использовать напрямую divisor-or-prime для рекурсивного спуска нельзя, поскольку Agda termination checker'у чтобы определить, что рекурсия остановится нужно чтобы она была структурная. Обойти это поможет дополнительный параметр g, для которого эта рекурсия будет структурной. Его с каждым шагом можно уменьшать на единицу и при этом утверждать, что если он был больше n то уменьшенный на единицу будет больше делителя n.
prime-divisor-hlp : ∀ n → 1 < n → ∀ g → n ≤ g → Σ[ m ∶ ℕ ] 1 < m × m ∣ n × prime m prime-divisor-hlp n 1<n zero n≤g = ⊥-elim $ ¬x≤y×x>y ( ≤-trans 1<n n≤g ∶ 2 ≤ 0) (s≤s z≤n ∶ 0 < 2) prime-divisor-hlp n 1<n (suc g₀) n≤g with divisor-or-prime n ( ≤-trans (s≤s z≤n) 1<n) ... | inj₂ pr-n = n , 1<n , a∣a n , pr-n ... | inj₁ (m , 1<m , m<n , m∣n) = step $ prime-divisor-hlp m 1<m g₀ $ ≤-pred $ ≤-trans m<n n≤g where step : Σ[ m₀ ∶ ℕ ] 1 < m₀ × m₀ ∣ m × prime m₀ → Σ[ m₀ ∶ ℕ ] 1 < m₀ × m₀ ∣ n × prime m₀ step (m₀ , 1<m₀ , m₀∣m , pr-m₀) = m₀ , 1<m₀ , ∣-trans₂ m₀ m n m₀∣m m∣n , pr-m₀
Ниже функция для поиска простого делителя уже без вспомогательных параметров:
prime-divisor : ∀ n → 1 < n → Σ[ m ∶ ℕ ] 1 < m × m ∣ n × prime m prime-divisor n 1<n = prime-divisor-hlp n 1<n n (a≤a _)
Теорема Евклида
Ищем общее кратное, далее прибавляем единицу, ищем простой делитель. Осталось доказать, что этот простой делитель больше входного числа. Для этого воспользуемся фактом, что x и x + 1 не имеют общих делителей. И в случае если искомый результат m окажется меньше входа, нам удастся доказать, что m делит n!, а как мы помним m — это делитель n! + 1. Противоречие.
Euclid : ∀ a → Σ[ b ∶ ℕ ] a < b × prime b Euclid zero = 1 , s≤s z≤n , p where p : prime 1 p .0 () (s≤s z≤n) Euclid (suc a₀) = pd , a<pd , pr-pd where a = suc a₀ 1≤a = s≤s z≤n com-mult-all : Σ[ m ∶ ℕ ] a ≤ m × (∀ k → 1 ≤ k → k ≤ a → k ∣ m) com-mult-all = common-multiple a 1≤a cm = proj₁ com-mult-all a≤cm = proj₁ $ proj₂ com-mult-all f-cm = proj₂ $ proj₂ com-mult-all prime-div-all : Σ[ m ∶ ℕ ] 1 < m × m ∣ suc cm × prime m prime-div-all = prime-divisor (suc cm) (s≤s $ ≤-trans 1≤a a≤cm) pd = proj₁ prime-div-all 1<pd = proj₁ $ proj₂ prime-div-all pd∣cm' = proj₁ $ proj₂ $ proj₂ prime-div-all pr-pd = proj₂ $ proj₂ $ proj₂ prime-div-all a<pd : a < pd a<pd with pd ≤? a ... | inj₁ pd≤a = ⊥-elim $ divisor-a,a' 1<pd (f-cm pd (≤-trans (s≤s z≤n) 1<pd) pd≤a) pd∣cm' ... | inj₂ pd>a = pd>a
Немає коментарів:
Дописати коментар