[Agda] _<=_ and _<_
Sergei Meshveliani
mechvel at botik.ru
Wed Sep 25 17:23:12 CEST 2013
On Tue, 2013-09-24 at 17:18 +0400, Sergei Meshveliani wrote:
> []
> 2. For Nat,
> it is natural to derive (I) and (II) from DecTotalOrder,
> as a specialization of the above generic laws.
>
> But DecTotalOrder says nothing about _<_.
> Then, we are forced to derive (I) and (II) from the union of
> DecTotalOrder and StrictTotalOrder.
> Right?
>
> Well, Data.Nat has decTotalOrder. But it is silent about
> Strict(Total)Order.
>
> What is the way out?
> The approach "prove (I) and (II) individually for Nat"
> will cause individual proofs for Integer, Nat × Nat, List Nat,
> and so on.
>
>
> 3. Consider the Order organization that follows literally the usual
> formula "less or equal".
>
> (A) Having _≈_ and _<_, _≤_ needs to be defined
> (implemented) immediately
> Or
> (B) Having _≈_ and _≤_, _<_ needs to be defined immediately.
>
> Because this is natural.
But I see now Relation.Binary.StrictToNonStrict
which defines x ≤ y = (x < y) ⊎ (x ≈ y)
I hope this will do of what I asked for.
If so, then I am sorry for the noise.
Regards,
------
Sergei
More information about the Agda
mailing list