[Agda] Unification assumes injective postulates?

[Dominique Devriese]

Interesting, I also always assumed interpretation 2 for postulates,
even though it has never mattered for me.  Perhaps interpretation 2
can be modelled by making the postulate a section argument instead?

Dominique

2012/11/14 Andreas Abel <andreas.abel at ifi.lmu.de>:
> 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/
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda