[Agda] Total: x !<= y ==> y <= x

[Serge D. Mechveliani]

On Wed, Oct 10, 2012 at 10:20:08AM -0700, wren ng thornton wrote:
> On 10/10/12 11:59 AM, Serge D. Mechveliani wrote:> People,
> > I have a beginner question on usage of DecTotalOrder of Standard
> > library.
> >
> > I have  ord : DecTotalOrder,
> >          _<=_  extracted from this  ord,
> >          ``with  x <=? y''   produced    no x-!<=-y
> >          (I think,   x-!<=-y :  \neg x <= y )
> >
> > (here I replace \<= with <= ).
> >
> > And from this   x-!<=-y,  I need to construct  y<=x : y <= x.
> > Because I think that this a constructive reifation for a classical
[..]

> I'm not sure of the particular names of things in Agda, but \u+ is the
> disjoint union operator (aka Either in Haskell).
> 
> So, the way you'd use it is:
> (1) this is a decidable total order, so let's analyze: total x y
> (2) Case x <= y: absurd, because we have a proof of \neg x <= y
> (3) Case y <= x: hey, I can just return this proof


I am sorry for my stupidity,
but I fail to force Agda to reject  Case x <= y
(when having   neg : \neg (x <= y))
!

Thanks to people,
now as I see the definition of  \u+  in  Data.Sum,  I try to derive  
y <= x  from  \neg (x <= y)  under  ord : DecTotalOrder ...

The corresponding lemma coded in Agda is 

  !<=thenFlip : {c l1 l2 : Level} -> (ord : DecTotalOrder c l1 l2) ->
                let leq = _<=_ ord
                in  (x y : Carrier ord) -> \neg (leq x y) -> leq y x

  !<=thenFlip ord x y neg =   ??

(I replace the math symbols in an evident way).

Please,  what is the simplest code for it?

First, I tried 
                    with  total ord x y
              ... | inj_2 y<=x = y<=x 

And I fail to force it to skip the pattern of  (inj_1 _)
(tried also setting () in various places).
Somehow the  neg  map to  \bottom  needs to be used for this ...
Or do I need to add 
                    inj_1 _ = p  where p = postulate p : leq y x
?
The second attempt is via mapping it to  Empty \u+ (leq y x) :

   f v 
   where
   leq = _<=_ ord

   v : Empty \u+ (leq y x)
   v = Sum.map neg id $ total ord x y

   f : Empty \u+ (leq y x) -> leq y x
   f (inj_2 u) = u
   f ()             ??

Here  Empty  is the empty type -- denoted by a math symbol  \bottom.

Sum.map  applies  neg   and obtains a member of a disjoint sum  
                                             v : Empty \u+ (leq y x)
(is \u+ a disjoint sum?).

Further, it is clear to us that for any set T we can define a map 
                                                 f : Empty \u+ T -> T
If any such  f  is defined for  T = (y <= x),  then  f v  is the goal.
But I fail to define such  f  in Agda !
Agda asks for the value for a pattern   f (inj_1 _) -- despite that
(inj-1 u)  has  u  being a member of Empty.
And I fail to force it to skip this pattern, and fail with setting ()
in various places.
Do I need to add   f (inj_1 _) = p  where p = postulate p : leq y x
?
What a constructive philosophy has Agda for a map
                                              f : \bottom \u+ T -> T
?
Thank you in advance for explanation,

------
Sergei