[Agda] hidden proofs

[Sergei Meshveliani]

People,
I have doubts about constructive computation in Agda.

First, I defined a decidable subset via a function  
                                          member? : A -> Bool,  

with  member? x ≡ true  expressing that  x  belongs to this subset.

One professor (who knows Agda and Coq) has told me that I need to avoid
this Bool, because it leads to implicit proofs, and this is against
constructive mathematics,
that I need to define a decidable subset in a different way,
that I need first to find and read various wise papers about
intuitionism.

And it is difficult for me to believe that one can avoid things similar
to Bool in this situation. 

1. Suppose that I try to avoid Bool. For example, let us define the
subset Even  in  ℕ :

  mutual
  data Even : ℕ → Set
       where
       even0    : Even 0
       even-suc : {n : ℕ} → Odd n → Even (suc n)  

  data Odd : ℕ → Set where
                     odd-suc : {n : ℕ} → Even n → Odd (suc n) 

Then, how to define  even? : ℕ → Dec $ Even n
?
In particular, how to prove  ¬ Even (suc 0)
?

In computer algebra almost nothing interesting can be computed for a
domain which equality is not decidable. Equality in a quotient (residue)
domain R/I needs to be decidable, hence  member? x I  needs to be
decidable.
For example, what is the degree of a polynomial  (a - b)*x^2 + x
in x ?
If  a - b = 0  then it is  1,  otherwise  2.  And  a and b often are in
a quotient domain of something.
On practice, most these things need to be decidable. 


2. Another attempt to avoid Bool with having a decidable  Even:

  rem2 : ℕ → ℕ
  rem2 0             = 0
  rem2 (suc 0)       = suc 0
  rem2 (suc (suc n)) = rem2 n

  Even : ℕ → Set
  Even n =  rem2 n ≡ 0

Here we can program   even? : ℕ → Dec $ Even n.
And statements like
                      Even (suc $ suc $ suc $ suc 0)
have explicit proofs.
And these proofs are:

    refl  +  (normalization by the definition of  rem2).      

And its  normalization  part is built-in, hidden, is not an Agda data.
The same result we have with using Bool.

I suspect that if one needs to express a decidable subset, like Even,
one cannot avoid using Bool, or something which brings hidden
normalization proofs (and still the effect is like of Bool).

Is this so?

And this breaks the approach of constructive (intuitionistic)
mathematics  -- if I ever understand of what is this.

The matter is that the normalization part of a proof may be very
non-trivial, essential. For example, there may be arbitrary difficult to
predict of whether some  f(x)  normalizes to  0  or to  1.  

3. Suppose that there is a function `normalize' 

which returns the full normalization trace (which equation is currently
applied, and under which substitution, and to which subterm ...).
Suppose that it is somehow implemented in Agda, with representing all
the data by meta-coding, reflection
(because here a program is a data for `normalize').
Then, this will provide explicit proofs for decidable subsets, and
such. 

What people would advise?

Thanks,

------
Sergei