Исках да докажа, че 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.
thm : ((∃ λ m → (m < 10)) AND (∃ λ n → (n < 15))) -> (∃ λ z → (z < 25))
thm = ?
Как да дефинирам И тук?? Моля, помогни ми. И как да го докажа??
Теоремата, която се опитвате да докажете, изглежда малко странна. По-специално, ∃ λ 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
В повечето случаи бих предпочел последната версия.
and съответства на product в Agda. Ето съответната конструкция в стандартната библиотека. Във вашия случай може да искате да използвате независимата версия _×_.
