[Agda] printed goal type

[Sergei Meshveliani]

Please,
how to fix the attached program?
(about 100 lines).

It ends with 

  e | yes k≡k'  with d
  e | yes k≡k' | suc _ =  PE.refl
  e | yes k≡k' | 0     =  ⊥-elim $ <→≢ d>0 $ PE.sym d≡0
                          where
                          ...
                          d>0 : d > 0
                          d>0 = m<n→n∸m>0 m<m'

                          d≡0 : d ≡ 0
                          d≡0 = ?

The only remaining point is as follows.
In the last branch of  "0",  d ≡ 0  needs, of course, to have a proof.
But I fail to provide such.

I tried     inspect PE.inspect (_≟_ k) k'  ... 
and failed.

Then, I try to write an explicit goal  e'  for  (yes k≡k'),  in a hope
that it will be easier to simplify a proof of  e'.  I set "?" for e' and
copy the type expression given by interactive Agda:  

  e | yes k≡k' = e'                                                    
    where     
    postulate                                                          
     e' :                                                
       map (λ r → proj₁ r) 
         ( (λ { (no ¬p) → (ps , m<mty-p'ps) ∷ minus (k' , m') k≡k'
              ; (yes p) → case m<mty-p'ps ∸ m' of   
                             (λ { Data.Nat.zero → k≡k' ;
                                  (suc n) → (ps , suc n) ∷ k≡k' }
                             )                         
                               k' m' ps m<mty-p'ps k≡k' p  
              }  
           ) k m k' m' ps (yes k≡k')   
         )                                              
       ≡ k' ∷ map (λ r → proj₁ r) ps 

And Agda reports of many _unsolved metas_ in this (strangest)
expression.
I wonder of how to help this.
Also it is full of strangest names. For example,  m<mty-p'ps  means in
the program  (m' : Nat) < mty k (p' ∷ ps),

and the suggested expression contains  "case m<mty-p'ps ∸ m' "  
-- it looks like subtracting m' from something of an inappropriate type.
Another question: the `case' subexpression has  \lambda,  and there go  
"k' m' ps m<mty-p'ps k≡k' p"  after this closed \lambda. Where k' is
instantiated to?

How to handle these things, please?

Thanks,

------
Sergei

-------------- next part --------------
module With where

open import Function using (_$_; _∘_; case_of_) 
open import Relation.Nullary using (yes; no; Dec; ¬_)
open import Relation.Binary  using 
                             (module DecTotalOrder; module StrictTotalOrder)
open import Relation.Binary.PropositionalEquality as PE using (_≡_; _≢_)
open import Data.Empty   using (⊥-elim)
open import Data.Product using (_×_; _,_; _,′_; proj₁; proj₂) 
open import Data.Nat     using (ℕ; suc; _≟_; _<_; _>_; _≤_; _≥_; _∸_; s≤s; 
                                                                      z≤n)
open import Data.Nat.Properties using (strictTotalOrder)
open import Data.List    using (List; []; _∷_; map)




------------------------------------------------------------------------------
open StrictTotalOrder strictTotalOrder using (compare; <-resp-≈)
                               renaming (irrefl to <-irrefl; trans to <-trans)

<→≢ : ∀ {m n} → m < n → m ≢ n
<→≢ {_} {n} m<n m=n =  <-irrefl PE.refl n<n  where
                                             resp = proj₂ <-resp-≈
                                             n<n  = resp m=n m<n

m<n→n∸m>0 : ∀ {m n} → m < n → n ∸ m > 0
m<n→n∸m>0 (s≤s z≤n)     = s≤s z≤n          
m<n→n∸m>0 (s≤s (s≤s h)) = m<n→n∸m>0 (s≤s h)


Pair  = ℕ × ℕ
Pairs = List Pair 

keys : Pairs → List ℕ 
keys = map proj₁

mty : ℕ → Pairs → ℕ             
mty k []              = 0 
mty k ((k' , m) ∷ ps) = case k ≟ k' of \ { (yes _) → m
                                         ; _       → mty k ps }

minus : Pair → Pairs → Pairs
minus _       []               =  []
minus (k , m) ((k' , m') ∷ ps) =  
                case k ≟ k'
                of \ 
                { (no _)  → (k' , m') ∷ minus (k , m) ps
                ; (yes _) → case m' ∸ m of \ { 0       → ps
                                             ; (suc n) → (k' , suc n) ∷ ps }
                }

------------------------------------------------------------------------------
minus-preserves-keys-if : ∀ k m ps → let ks' = keys $ minus (k , m) ps
                                     in
                                     m < mty k ps → ks' ≡ keys ps

minus-preserves-keys-if _ _ []               _          =  PE.refl 
minus-preserves-keys-if k m ((k' , m') ∷ ps) m<mty-p'ps =  e
  where
  p'            = (k' , m') 
  ks            = keys ps
  tail-res      = minus (k , m) ps 
  res-keys      = keys $ minus (k , m) (p' ∷ ps) 
  tail-res-keys = keys tail-res 
  d             = m' ∸ m
 
  e : res-keys ≡ k' ∷ ks
  e  with k ≟ k'

  e | no k≢k' =  case-k≉
        where
        mty-p'ps≡mty-ps : mty k (p' ∷ ps) ≡ mty k ps
        mty-p'ps≡mty-ps with k ≟ k'
        ... | no _     = PE.refl
        ... | yes k≡k' = ⊥-elim $ k≢k' k≡k'

        m<mty-ps : m < mty k ps
        m<mty-ps = PE.subst (_<_ m) mty-p'ps≡mty-ps m<mty-p'ps

        case-k≉ :  k' ∷ tail-res-keys ≡ k' ∷ ks
        case-k≉ =  PE.cong (_∷_ k') $ minus-preserves-keys-if k m ps m<mty-ps


  e | yes k≡k'  with d
  e | yes k≡k' | suc _ =  PE.refl                                             
  e | yes k≡k' | 0     =  ⊥-elim $ <→≢ d>0 $ PE.sym d≡0                       
                          where                                              
                          mty-p'ps≡m' : mty k (p' ∷ ps) ≡ m'                 
                          mty-p'ps≡m'  with k ≟ k'                           
                          ... | yes _   = PE.refl                             
                          ... | no k≢k' = ⊥-elim $ k≢k' k≡k'
                                                                               
                          m<m' : m < m'     
                          m<m' = PE.subst (_<_ m) mty-p'ps≡m' m<mty-p'ps     
                                                                          
                          d>0 : d > 0                                       
                          d>0 = m<n→n∸m>0 m<m'                             
                                                             
                          postulate d≡0 : d ≡ 0 
                          -- d≡0 = PE.refl

{-
  e | yes k≡k' =  e' 
    where
    postulate 
     e' : 
       map (λ r → proj₁ r)
         ( (λ { (no ¬p) → (ps , m<mty-p'ps) ∷ minus (k' , m') k≡k'
              ; (yes p) → case m<mty-p'ps ∸ m' of
                             (λ { Data.Nat.zero → k≡k' ; 
                                  (suc n) → (ps , suc n) ∷ k≡k' }
                             ) 
                               k' m' ps m<mty-p'ps k≡k' p
              }
           ) k m k' m' ps (yes k≡k')
         )
       ≡ k' ∷ map (λ r → proj₁ r) ps
-}