Clever Geek Handbook

Writing evidence in Agda

I want to write proofs of the statement "for all x there are y such that x <y and y are even". I tried 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 ie for 'suc a' agda cannot find a solution. I once tried to write 2 * suc a, record {}. But that doesn't work either. Any help would be appreciated.

+3


source to share


1 answer


What you really want is to do two things at once.

The problem with such definitions is what's called "logical blindness" - by encoding your sentences as logical, you lose whatever 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 a proof basis).

However, in your case, you can change the definition slightly thm0

to help Agda with normalization. even

does two steps suc

in each step of the recursion - you can thm0

do two steps.

We'll see:

thm0 : βˆ€ x β†’ βˆƒ Ξ» y β†’ Teven ((x ll y) ∧ (even y))
thm0 zero = suc (suc zero) , tt

Two new cases 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 that you existentially quantified) is suc (suc y')

for some other y'

, Agda can normalize even y

to even y'

(this is only after definition). The same goes for "less than" proof - once you know what x = suc (suc x')

and y = suc (suc y')

for some y'

( x'

which 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'

along with proof that even y'

and x' ll y'

is exactly what we want.

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


Then we just plug in y = suc (suc y')

and p

(as above, (x ll y) ∧ even y

boils down 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, if said, I would advise against that. Don't code your sentences as boolean and then use them at the level level via Teven

. This really only works for simple things and cannot be extended to more complex sentences. Try explicit test conditions instead:

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 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 means that either is n

even or its successor is even). In fact, it 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

Oddly enough, when I wrote this definition, I just matched with something-even (suc n)

and used C-a

(autocomplete) to fill in the right-hand sides! When you give enough hints, Agda can write the code without my help.

+3


source






More articles:


All Articles