How to use Logical AND operation between two sets in agda?

Question

I wanted to proof that 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 = ?

How to define AND here?? Please help me. And how to proof this??

Answer 1

and corresponds to product in Agda. Here is the corresponding construct in the standard library. In your case, you may want to use the non-dependent version _×_.

Answer 2

The theorem you're trying to prove seems a little strange. In particular, ∃ λ z → z < 25 holds without any assumptions!

Let's do the imports first.

open import Data.Nat.Base
open import Data.Product

One simple proof of a generalisation of your theorem (without the assumptions) works as follows:

lem : ∃ λ z → z < 25
lem = zero , s≤s z≤n

In the standard library, m < n is defined as suc m ≤ n. The lemma is thus equivalent to ∃ λ z → suc z ≤ suc 24. For z = zero this holds by s≤s z≤n.

Here are a few different ways of expressing your original theorem (the actual proof is always the same):

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

I would prefer the last version in most circumstances.