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

Serge D. Mechveliani mechvel at botik.ru
Thu Oct 11 17:18:49 CEST 2012

```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
```