[Agda] Unification assumes injective postulates?

[Andreas Abel]

On 14.11.2012 15:40, Dan Licata wrote:
> On Nov14, Andreas Abel wrote:
>> 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).
>
> I'd like to understand what's going on here better.  I think it would be
> bad for postulates to be *propositionally* injective, because then
> e.g. the following logical-framework-style definition would be wrong:
>
>    postulate
>      bool : Set
>      true : bool
>      false : bool
>      if : {X : Set} -> bool -> X -> X -> X
>      beta1 : forall {X} {e1 e2 : X} -> Id (if true e1 e2) e1
>      beta2 : forall {X} {e1 e2 : X} -> Id (if false e1 e2) e2
>
>    if-inj : forall {X} {e e'} {e1 e2 : X} ->
>             Id (if e e1 e2) (if e' e1 e2) -> Id e e'
>    if-inj p = ?
>
>    -- get a contradiction from showing that
>    -- if true true true = if false true true
>    wrong : Id true false
>    wrong = if-inj {bool} {true} {false} {true} {true}
>    	  (IdM.trans beta1 (IdM.sym beta2))
>
> But Agda doesn't let me prove if-inj (I'm a few versions back, so let me
> know if this changed).

No, if-inj cannot be proved still.

> On the other hand, the intuition that
>
>    if two neutral terms with the same head are definitionally equal,
>    then they have the same spine
>
> makes sense to me.  Is this the property that justifies the move you're
> making above?
>
> On the other other hand, I can imagine situations where that fails,
> because e.g. you have eta for coproducts definitionally.
>
> So, what is it about definitional equality that justifies that move from
> foo x == foo y to x == y, and how does Agda know not to apply the same
> reasoning to propositional equality?

The unifier called during pattern-checking behaves different than the 
constraint solver called during equality-checking.  The unifier is based 
on extensional equality (run-time equality of closed things) while the 
constraint solver is based on intensional equality (compile-time 
definitional equality of open things).

This is a bit subtle, I keep mixing this up myself...

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