[Agda] Unification assumes injective postulates?

[Andreas Abel]

The basic question here is how we should understand

   postulate foo : Nat -> Nat

I see two basic interpretations here:

1. foo is a fixed, arbitrary unknown function.
2. foo is a fixed, specific unknown function.

Interpretation 1, which seems to be the one taken by Agda, allows to 
reduce foo x == foo y to x == y, since there are non-constant functions. 
  A postulate behaves like a module parameter or a function parameter 
(free variable).

Interpretation 2 is what you seem to expect.  You get this behavior when 
you write

   foo : Nat -> Nat
   foo = ?

Then, Agda only complains about unsolved constraints.

One solution for your issue could be that you replace your postulates by 
holes.  However, that might litter your Agda session with distracting 
goals.  Another take would be to have a second form of postulate, an 
"existential postulate" opposed to the current "universal postulate".

Cheers,
Andreas

On 14.11.12 10:37 AM, Nils Anders Danielsson wrote:
> On 2012-11-14 00:46, Jan Malakhovski wrote:
>> postulate foo : ℕ → ℕ
>>
>> bar : foo zero ≡ foo (succ zero) → foo zero ≡ foo (succ zero)
>> bar refl = {!!}
>> ~~~~
>>
>> fails with:
>> ~~~~
>> zero != succ zero of type ℕ
>> when checking that the pattern refl has type
>> foo zero ≡ foo (succ zero)
>> ~~~~
>
> The only way Agda can succeed here is if zero and succ zero are
> definitionally equal.
>
> For some discussion about whether postulates should be injective or not,
> see the following bug report:
>
>    http://code.google.com/p/agda/issues/detail?id=170
>

-- 
Andreas Abel  <><      Du bist der geliebte Mensch.

Theoretical Computer Science, University of Munich
Oettingenstr. 67, D-80538 Munich, GERMANY

andreas.abel at ifi.lmu.de
http://www2.tcs.ifi.lmu.de/~abel/