[Agda] Re: pattern match for LessThan'?

[Kenichi Asai]

Thanks.  Yes, ⊥-elim is something that I should have considered.
After some struggle, I came up with the following solution (attached):

inv′ : {m n : ℕ} → (m≤′n : m ≤′ n) → 
      (Σ[ m≡n ∈ m ≡ n ]
       m≤′n ≡ subst (λ n' → m ≤′ n') m≡n (≤′-refl {m})) ⊎
      (Σ[ n' ∈ ℕ ] Σ[ sucn'≡n ∈ suc n' ≡ n ] Σ[ m≤′n' ∈ m ≤′ n' ]
       m≤′n ≡ subst (λ n' → m ≤′ n') sucn'≡n (≤′-step m≤′n'))
inv′ ≤′-refl = inj₁ (refl , refl)
inv′ {n = suc n} (≤′-step m≤′n) = inj₂ (n , refl , m≤′n , refl)

which uses 'subst' to adjust types.  I expect I could then use ⊥-elim
to eliminate unnecessary cases.  Does this seem a good solution?  If
there are any better ways, please let me know.

Sincerely,

-- 
Kenichi Asai
-------------- next part --------------
module LessThan where

open import Data.Nat
open import Data.Sum
open import Data.Product
open import Relation.Binary.PropositionalEquality

-- definition of _≤′_ in the standard library
-- data _≤′_ (m : ℕ) : ℕ → Set where
  -- ≤′-refl :                         m ≤′ m
  -- ≤′-step : ∀ {n} (m≤′n : m ≤′ n) → m ≤′ suc n

inv′ : {m n : ℕ} → (m≤′n : m ≤′ n) → 
      (Σ[ m≡n ∈ m ≡ n ]
       m≤′n ≡ subst (λ n' → m ≤′ n') m≡n (≤′-refl {m})) ⊎
      (Σ[ n' ∈ ℕ ] Σ[ sucn'≡n ∈ suc n' ≡ n ] Σ[ m≤′n' ∈ m ≤′ n' ]
       m≤′n ≡ subst (λ n' → m ≤′ n') sucn'≡n (≤′-step m≤′n'))
inv′ ≤′-refl = inj₁ (refl , refl)
inv′ {n = suc n} (≤′-step m≤′n) = inj₂ (n , refl , m≤′n , refl)