Я хотел доказательство того, что if there is m which is less than 10 and there is n which is less than 15 then there exist z which is less than 25.Как использовать логическую операцию И между двумя наборами в agda?
thm : ((∃ λ m → (m < 10)) AND (∃ λ n → (n < 15))) -> (∃ λ z → (z < 25))
thm = ?
Как определить и здесь ?? Пожалуйста, помогите мне. И как это доказать?
and соответствует product в Агда. Here is соответствующая конструкция в стандартной библиотеке. В вашем случае вы можете использовать the non-dependent version_×_.
Теорема, которую вы пытаетесь доказать, кажется немного странной. В частности, ∃ λ z → z < 25 не имеет никаких предположений!
Давайте сделаем импорт в первую очередь.
open import Data.Nat.Base
open import Data.Product
Одно простое доказательство обобщения вашей теоремы (без предположений) работает следующим образом:
lem : ∃ λ z → z < 25
lem = zero , s≤s z≤n
В стандартной библиотеке, m < n определяется как suc m ≤ n. Таким образом, лемма эквивалентна ∃ λ z → suc z ≤ suc 24. Для z = zero это удерживается s≤s z≤n.
Вот несколько различных способов выражения своей исходной теоремы (фактическое доказательство всегда одинакова):
thm : (∃ λ m → m < 10) × (∃ λ n → n < 15) → ∃ λ z → z < 25
thm _ = lem
thm′ : (∃₂ λ m n → m < 10 × n < 15) → ∃ λ z → z < 25
thm′ _ = lem
thm″ : (∃ λ m → m < 10) → (∃ λ n → n < 15) → ∃ λ z → z < 25
thm″ _ _ = lem
Я бы предпочел последний вариант в большинстве случаев.
Обратите внимание, что глагол, который вы ищете, «доказывает». Слово «доказательство» обычно используется как существительное для описания того, что вы создаете, когда вы что-то доказываете. Это обычная ошибка. – dfeuer
моя ошибка .. я запомню. Благодарю . – ajayv