Proof in Agda and how to evaluate list based function in C-c C-n

Question

I am new in Agda

BTW, how could i evaluate a list related function like reverse by C-c C-n ?

I mean how could i type the list like reverse [1,2,3] as in Haskell but it not work in agda.

Many thanks

Answer 1

"For any" is universal quantification, which translates into dependent function types. As an example, let's take the following theorem: For any natural number n greater than zero, there exists a natural number m, such that S(m) = n.

open import Data.Nat
open import Data.Product
open import Relation.Binary.PropositionalEquality

theorem : (n : ℕ) → 0 < n → Σ[ m ∈ ℕ ] (suc m ≡ n)
theorem zero    ()
theorem (suc n) _  = n , refl

We can rewrite your theorem using the same pattern:

theorem : {A B : Set} (f : A → B) {m n : ℕ} →
  A has-size m → B has-size n → n < m →
  Σ[ a ∈ A ] Σ[ a′ ∈ A ] (a ≢ a′ → f a ≡ f a′)

This is a bit more involved: for any sets A and B, any function f from A to B and any natural numbers m and n such that A has m and B has n elements and m is greater than n, there exist elements a and a′ in A such that even if a is different from a′, f a is equal to f a′. Note that I cut the b element; it's still the same theorem but a bit easier to write down.

_has-size_ remains to be defined. I suggest defining A has-size m to be the statement that A is isomorphic to Fin m (Fin can be found in Data.Fin). If your assumptions are that A is isomorphic to Fin m and B to Fin n, you can do the proof on numbers (which is far easier) and then transform those numbers back to elements of A or B.

---

As for your second question:

C-c C-n reverse (1 ∷ 2 ∷ 3 ∷ [])

gives back

3 ∷ 2 ∷ 1 ∷ []

You might have tried to write the list as [1, 2, 3] as you would in Haskell, but this shortcut is not present in Agda. With clever use of operators, you could probably make it sort of work, though it would certainly require more whitespace (such as [ 1 , 2 , 3 ]), but I don't think it's worth the effort.