How this is working in agda?

Question

I want to prove that there exist a natural number which is less than 10. I write the code in this way..

thm2 : (∃ λ m → (m < 10))
thm2 = zero , s≤s z≤n

I am not able to understand how this is working. Please explain..

Answer 1

Let's dissect thm2.

The type of the expression

∃ λ m → m < 10

∃ is defined in Data.Product as an alias for Σ where the first argument is left implicit. This means that ∃ is taking an element B of type A → Set and returning the type of pairs containing an a of type A and a b of type B a.

Now, λ m → m < 10 is taking an m in ℕ and returning the type of proofs that m < 10.

So ∃ λ m → m < 10 is the type of pairs of an ℕ and a proof that it is less than 10.

The expression itself

zero , s≤s z≤n

For the whole thing to typecheck, we need:

zero to be a ℕ which it is.

s≤s z≤n to be a proof that 0 < 10. _<_ is defined in Data.Nat.Base as an alias for λ m n → suc m ≤ n. So proving that 0 < 10 is the same as proving that 1 ≤ 10.

Now, _≤_ is an inductive type with two constructors:

• a base case z≤n saying that 0 is less than or equal to all natural numbers
• a step case s≤s saying that if one number is less than or equal to another, then their sucs also are less than or equal.

The proof s≤s z≤n is indeed a valid proof that 1 ≤ 10: z≤n proves that 0 ≤ 9 and s≤s concludes that therefore 1 ≤ 10.