[Agda] Total: x !<= y ==> y <= x
Serge D. Mechveliani
mechvel at botik.ru
Thu Oct 11 19:06:49 CEST 2012
On Thu, Oct 11, 2012 at 07:18:49PM +0400, Serge D. Mechveliani wrote:
> 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 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.
>
> [..]
> 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?
I am sorry for disturbance!
I have fixed the pattern syntax usage, and now find quite a simple
expression:
with total ord x y
... | inj_2 y<=x = y<=x
... | inj_1 x<=y with neg x<=y
... | ()
I do not know, may be it worths adding this !<=thenFlip to
Relation.Binary of Standard library.
Regards,
Sergei
More information about the Agda
mailing list