[Agda] _<=_ and _<_

Sergei Meshveliani mechvel at botik.ru
Tue Sep 24 15:18:52 CEST 2013

People, I have a couple of questions about general relation between 
                                                            _≤_ and _<_ 
in the  lib-0.7 standard library.

1. What is the most general situation in  lib-0.7  under which these
usual properties can be proved:
                       x ≤ y  iff  x < y ⊎ x ≈ y               (I),
                       x < y  ->  ¬ y ≤ x                      (II)

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.

Well,  Data.Nat  has  decTotalOrder.  But it is silent about 

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
(B) Having _≈_ and _≤_,   _<_ needs to be defined immediately.

Because this is natural.

Let us follow (A):

  record IsPartialOrder {a ℓ₁ ℓ₂} {A : Set a}
                        (_≈_ : Rel A ℓ₁) (_<_ : Rel A ℓ₂) :
                        Set (a ⊔ ℓ₁ ⊔ ℓ₂) where
      isPreorder : IsPreorder _≈_ _<_   
                                   -- redefine IsPreorder respectively
      antisym    : Antisymmetric _≈_ _<_

    _≤_ : Rel A ℓ₂
    x ≤ y =  x < y ⊎ x ≈ y

Of course, the axioms need to be corrected slightly.
And  StrictPartialOrder  will not need to introduce  _<_  as something
independent on  _≤_.

I suspect that if the  Ordering library part  is reorganized this way,
then using orderings will become easier.

Am I missing something? What is your opinion?



More information about the Agda mailing list