[Agda] Unification assumes injective postulates?

Andreas Abel andreas.abel at ifi.lmu.de
Wed Nov 14 11:03:54 CET 2012

```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:
>
>

--
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/
```