[Agda] Unification assumes injective postulates?
Dan Licata
drl at cs.cmu.edu
Wed Nov 14 15:40:21 CET 2012
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).
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?
Thanks!
-Dan
More information about the Agda
mailing list