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

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.