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.
P.S.
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
Conor
PS I blogged a bit about implementing OTT...
