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..
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..
Let's dissect
thm2
.The type of the expression
∃
is defined in Data.Product as an alias forΣ
where the first argument is left implicit. This means that∃
is taking an elementB
of typeA → Set
and returning the type of pairs containing ana
of typeA
and ab
of typeB a
.Now,
λ m → m < 10
is taking anm
inℕ
and returning the type of proofs thatm < 10
.So
∃ λ m → m < 10
is the type of pairs of anℕ
and a proof that it is less than10
.The expression itself
For the whole thing to typecheck, we need:
zero
to be aℕ
which it is.s≤s z≤n
to be a proof that0 < 10
._<_
is defined inData.Nat.Base
as an alias forλ m n → suc m ≤ n
. So proving that0 < 10
is the same as proving that1 ≤ 10
.Now,
_≤_
is an inductive type with two constructors:z≤n
saying that0
is less than or equal to all natural numberss≤s
saying that if one number is less than or equal to another, then theirsuc
s also are less than or equal.The proof
s≤s z≤n
is indeed a valid proof that1 ≤ 10
:z≤n
proves that0 ≤ 9
ands≤s
concludes that therefore1 ≤ 10
.