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

[wren ng thornton]

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
> lemma for  (Total <=)  of that   not (x <= y)  ==>  y <= x.
> I see in  Relation.Binary, Core:
>
>    record IsTotalOrder ...
>           isPartialOrder : IsPartialOrder _~~_ _<=_
>           total          : Total _<=_
>
> (here I replace some math symbols)
>
>    Total : forall {a l} {A : Set a} -> Rel A l -> Set _
>    Total _~_ = forall x y -> (x ~ y) \u+ (y ~ x)
>
> , where  \u+  denotes, I think, something close to union of types.
> How to operate with a data from  (P \u+ Q) ?
> what are the constructors?

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

-- 
Live well,
~wren