[Agda] _<_ of agda-prelude

[Sergei Meshveliani]

On Fri, 2017-06-23 at 05:35 +0200, Jannis Limperg wrote:
> > Can anybody, please, show a proof for equivalence of standard _<_ and
> > the one of agda-prelude?
> 
> Below is one proof; there are probably more elegant ones. It uses some
> standard lemmas which I only redefine because I was too lazy to look up
> their names.
> 
> In the future, it would be nice if you could provide a complete template
> for your problem so that I don't have to muck around with the imports.


Jannis,
thank you very much.

Bringing several library items there makes it the following code:

----------------------------------------------------------------------
open import Relation.Binary using (DecTotalOrder)
open import Relation.Binary.PropositionalEquality as PE using (_≡_)
open import Data.Nat using (suc; _+_ ; _<_ ; _≤_; z≤n; s≤s)
open import Data.Nat.Properties using (≤-decTotalOrder; ≤-step; n≤m+n)
open import Data.Nat.Properties.Simple using (+-comm)

open import Prelude.Nat using (diff)
open import Prelude     using () renaming (_<_ to _<o_)

open DecTotalOrder ≤-decTotalOrder using () renaming (refl to ≤refl)

<o⇒< : ∀ {n m} → n <o m → n < m
<o⇒< {n} {0}     (diff k ())
<o⇒< {n} {suc m} (diff k PE.refl) =  s≤s (n≤m+n k n)

+-id-right : ∀ n → n ≡ n + 0
+-id-right n =  PE.sym (+-comm n 0)

+-suc : ∀ n m → n + suc m ≡ suc (n + m)
+-suc 0 m = PE.refl
+-suc (suc n) m = PE.cong suc (+-suc n m)

≤⇒≤o : ∀ {n m} → n ≤ m → n <o suc m
≤⇒≤o {0} {m} z≤n =  diff m (+-id-right _)
≤⇒≤o {suc n} {suc m} (s≤s n≤m)  with ≤⇒≤o n≤m
... |
      diff k eq = diff k (PE.cong suc 
                          (PE.trans eq (PE.sym (+-suc k n))))

<⇒<o : ∀ {n m} → n < m → n <o m
<⇒<o {n} {suc m} (s≤s n≤m) = ≤⇒≤o n≤m
----------------------------------------------------------------------


Thanks,

------
Sergei




> ----------------------------------------------------------------------
> open import Data.Nat
>   using (ℕ ; zero ; suc ; _+_ ; _<_ ; _≤_ ; z≤n ; s≤s)
> open import Prelude.Ord using () renaming (_<_ to _<o_)
> open import Prelude.Nat using (diff)
> open import Relation.Binary.PropositionalEquality
>   using (_≡_ ; refl ; cong ; sym ; trans)
> 
> 
> ≤-refl : ∀ {n} → n ≤ n
> ≤-refl {zero} = z≤n
> ≤-refl {suc n} = s≤s ≤-refl
> 
> 
> ≤-step : ∀ {n m} → n ≤ m → n ≤ suc m
> ≤-step z≤n = z≤n
> ≤-step (s≤s m≤n) = s≤s (≤-step m≤n)
> 
> 
> ≤-+ : ∀ n m → n ≤ m + n
> ≤-+ n zero = ≤-refl
> ≤-+ n (suc m) = ≤-step (≤-+ n m)
> 
> 
> <o⇒< : ∀ {n m} → n <o m → n < m
> <o⇒< {n} {zero} (diff k ())
> <o⇒< {n} {suc m} (diff k refl) = s≤s (≤-+ n k)
> 
> 
> +-id-right : ∀ n → n ≡ n + 0
> +-id-right zero = refl
> +-id-right (suc n) = cong suc (+-id-right n)
> 
> 
> +-suc : ∀ n m → n + suc m ≡ suc (n + m)
> +-suc zero m = refl
> +-suc (suc n) m = cong suc (+-suc n m)
> 
> 
> ≤⇒≤o : ∀ {n m} → n ≤ m → n <o suc m
> ≤⇒≤o {zero} {m} z≤n = diff m (+-id-right _)
> ≤⇒≤o {suc n} {suc m} (s≤s n≤m) with ≤⇒≤o n≤m
> ... | diff k eq = diff k (cong suc (trans eq (sym (+-suc k n))))
> 
> 
> <⇒<o : ∀ {n m} → n < m → n <o m
> <⇒<o {n} {suc m} (s≤s n≤m) = ≤⇒≤o n≤m