Writing Proofs in Agda

Question

I want to write proofs of the statement "for all x there exist a y such that x < y and y is even ". I tried in this way...

-- ll means less function i.e ' < '

_ll_ : ℕ → ℕ → Bool
0 ll 0 = false
0 ll _ = true
a ll 0 = false
(suc a) ll (suc b) = a ll b 

even : ℕ → Bool
even 0 = true
even 1 = false
even (suc (suc n)) = even n

Teven : Bool → Set
Teven true = ⊤
Teven false = ⊥


thm0 : (x : ℕ) →  Σ[ y ∈ ℕ ]  (Teven ( and (x ll y) (even y))) 
thm0 0 = suc (suc zero) , record {}
thm0 (suc a) = ?

for the last line i.e for 'suc a' agda is not able to find solution. I once tried by writing 2 * suc a , record {}. But this is also not working. Any help will be appreciated.

Answer 1

What you actually want is to do two steps at once.

The problem with this kind of definitions is something that is called "boolean blindness" - by encoding your propositions as booleans, you lose any kind of useful information they contain. The effect is that you have to rely on normalization to (hopefully) do its thing, you cannot help Agda in any other way (say by pattern matching on proof terms).

However, in your case, you can change the definition of thm0 slightly to help Agda with normalization. even makes two suc steps in every recursion step - you can make thm0 do two steps as well.

Let's take a look:

thm0 : ∀ x → ∃ λ y → Teven ((x ll y) ∧ (even y))
thm0 zero = suc (suc zero) , tt

Two new cases are for suc zero (also known as 1):

thm0 (suc zero) = suc (suc zero) , tt

And for suc (suc x'):

thm0 (suc (suc x') = ?

Now, if we knew that y (the one you existentially quantified over) is suc (suc y') for some other y', Agda could normalize even y to even y' (this is just following the definition). Same deal with the "less-than" proof - once you know that x = suc (suc x') and y = suc (suc y') for some y' (x' we already know), you can reduce x ll y to x' ll y'.

So the choice for y is simple... but how do we get y' (and the proof, of course)? We can use induction (recursion) and apply thm0 to x'! Remember that given x', thm0 returns some y' together with a proof that even y' and x' ll y' - this is precisely what we need.

thm0 (suc (suc a)) with thm0 a
... | y' , p = ?

Then we simply plug in y = suc (suc y') and p (as stated above, (x ll y) ∧ even y reduces to (x' ll y') ∧ even y', which is p).

Final code:

thm0 : ∀ x → ∃ λ y → Teven ((x ll y) ∧ (even y))
thm0 zero = suc (suc zero) , tt
thm0 (suc zero) = suc (suc zero) , tt
thm0 (suc (suc x')) with thm0 x'
... | y' , p = suc (suc y') , p

---

However, that being said, I'd advice against this. Do not encode your propositions as booleans and then use them at the type level via Teven. This really only works for simple things and cannot be extended to more complicated propositions. Instead, try explicit proof terms:

data _less-than_ : ℕ → ℕ → Set where
  suc : ∀ {x y} → x less-than y → x less-than suc y
  ref : ∀ {x}                   → x less-than suc x

data Even : ℕ → Set where
  zero    :                  Even 0
  suc-suc : ∀ {x} → Even x → Even (2 + x)

thm0 can be then written using a simple lemma:

something-even : ∀ n → Even n ⊎ Even (suc n)
something-even zero = inj₁ zero
something-even (suc n) with something-even n
... | inj₁ x = inj₂ (suc-suc x)
... | inj₂ y = inj₁ y

(this states that either n is even or its successor is even). In fact, thm0 can be implemented without using recursion!

thm0 : ∀ x → ∃ λ y → Even y × x less-than y
thm0 n with something-even n
... | inj₁ x = suc (suc n) , suc-suc x , suc ref
... | inj₂ y = suc n , y , ref

Funnily enough, when I wrote this definition, I just pattern matched on something-even (suc n) and used C-a (autocomplete) to fill in the right sides! When given enough hints, Agda can write the code without my help.