Hi Thorsten

I'm not sure I understand what's going on here.

Thorsten Altenkirch wrote:
Indeed, in the setoid model we can construct a function

    f : A -> [B]
    lift f : [A -> B]

if the setoid A is "trivial", i.e. has the identity as its equivalence relation.

I can do it if A is decided. If you give me a : A, then I pick

 lift f = iI const (f a) Ii

or, in less idiomatic longhand

 lift f = do
   c <- return const
   b <- f a
   return (c b)

If you give me A -> 0, it's easy.

    f : A -> B/~
    lift f : (A -> B)/~'

Again, if you give me some a : A, I say

lift f = const (f a) -- const respects the equivalence because const b a ~' const b' a if b ~ b'

But hang on - what stops us from doing a Diaconescu? Excluded middle doesn't hold in the setoid model, even though we only get P \/ not P where A \/ B = [A + B]. But this would still require that we have P + not P in the underlying set. So what goes wrong?

We define the type of non-empty subsets of Bool as

NE = Sigma Q : Bool-> Prop.Sigma x:Bool.Q x

Note that NE is inhabited, eg by

 moo = (const 1; true; ()).

We define the equivalence relation of extensional equality of subsets

~ : NE -> NE -> Prop

(Q,_) ~ (R,_) = forall b:Bool.Q b <-> R b

Now we derive:

h : NE/~ -> [ NE ]

which is just the indentity on the underlying elements. The point is that obviously ~ implies the trivial equality of [..].

Now, if we were able to lift h we get

lift h : [ NE/~ -> NE]

 return (const moo) : [ NE/~ -> NE]

Obviously, NE/~ isn't a setoid with a trivial equality!

The Diaconescu argument shows that we can prove for any P:Prop

    H : NE/~ -> NE
    Dia H : P \/ not P = [P + not P]

 Dia (const moo) : P \/ not P

see below for a Epigram 2+n style proof of Dia.

Under the circumstances, I really hope you've cocked this up.

We can also see what goes wrong in general: The principle

    f : A -> B/~
    lift f : (A -> B)/~'

fails because given the setoid A = (A0,~A) the premise gives us an underlying function f0:A0 -> B (for simplicity we assume that B is trivial) s.t. a ~A b implies f0 a ~B f0 b, where to use the same function to construct an element of A -> B we need to show that a ~A b implies f0 a = f0 b, and there is no reason to believe this - unless ~A is the equality.

I just about swallow that. But if A0 is decided, you need to use the spec part (which you're eliding for simplicity) to force me to use f0 in the way you're suggesting.

For completeness: Dia itself can be constructed as in the COQ script: we use T,F : Bool -> Prop

    T b = (b=true) \/ P
    F b = (b=false) \/ P

by applying H to the equivalence classe <T>,<F> and projecting out the components we get

    t,f : Bool
    t = fst (H <T>)
    f = fst (H <F>)
    snd (H <T>) : t=true \/ P
    snd (H <F>) : f=false \/ P

Are you sure? I thought

 H had return type NE, giving
 (P; a; p) = fst (H <T>), (Q, b, q) := fst(H <F>) : Bool -> Prop
 where a,b : Bool, p : P a, q : Q b

but no connection necessary between T and P, F and Q.

Now, I know that my pathological functions are not the functions you're thinking of, but it does rather show that the real action, whatever it is, lies in the "spec" parts which you're throwing away.

More later


PS I blogged a bit about implementing OTT...

Reply via email to