[Agda] hidden proofs
Sergei Meshveliani
mechvel at botik.ru
Tue Jul 30 19:33:50 CEST 2013
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
More information about the Agda
mailing list