[Agda] trustMe and make my coercion go

[Andreas Abel]

Hi Benja, my answer is at the very end...

On Sep 15, 2010, at 11:56 PM, Benja Fallenstein wrote:
> On Wed, Sep 15, 2010 at 11:00 PM, Andreas Abel <andreas.abel at ifi.lmu.de 
> > wrote:
>> I have looked a bit at the theory of primTrustMe.  Actually it is a  
>> special
>> case of eta-expansion for Leibniz-Equality.
>
> Right, because the type checker checks the definitional equality
> before reducing primTrustMe to refl, so you can't put refl into types
> that don't contain it already -- e.g., in (\(q : Top == Bottom) ->
> coerce (compute-dammit! q) unit), the coercion would not go, because
> the primTrustMe would not reduce to refl. I guess that makes the
> effect on the metatheory much less drastic...
>
>> I have a (fairly theoretical) paper on this on my homepage, it was  
>> presented
>> at the NBE'09 workshop.
>
> Thanks, I'll have to try whether I can follow it :-)
>
>> On Sep 15, 2010, at 9:56 PM, Benja Fallenstein wrote:
>>> Now I'm wondering what effect introducing compute-dammit!
>>
>> Maybe you mean primTrustMe?  compute-dammit! is just a definition  
>> so it does
>> not change the metatheory.
>>
>>> would have
>>> on the metatheory
>
> No, I mean what the effect would be of introducing a constant with the
> behavior of compute-dammit!, which could be implemented in Agda by the
> definition I gave (i.e., through a module that exposes
> compute-dammit!, but not primTrustMe).
>
> Actually, with this context I'm not really sure what you mean by,
>
>> Consistency holds rather directly, since each closed term of type a  
>> == a is refl anyway.
>
> After all, if you introduce primTrustMe itself, true == false is  
> inhabited, so:
>
> resp : {X : Set} → (F : X → Set)
>     → {x y : X} → x == y → F x ==₁ F y
> resp f refl = refl₁
>
> bad : ⊥
> bad = coerce (resp (\b → if b then ⊤ else ⊥) (primTrustMe {Bool}
> {true} {false})) unit
>
> Could you elaborate a little there? :-)

In my remarks about consistency and normalization I had eta-equality  
for Leibniz equality in mind (where primTrustMe is not needed).  In  
this context, you would have postulates instead of primTrustMe, so  
having

   p : true == false
   p = primTrustMe

is the same as

   postulate p : true == false

Consistency of course holds only if you can replace each postulate by  
a closed term.

Cheers,
Andreas


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/