[Agda] printed goal type

[Andreas Abel]

It seems like you need to use the inspect pattern on d, as you want a 
proof of d == 0 when matching d against 0.

On 18.01.2015 13:11, Sergei Meshveliani wrote:
> 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
>
>
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>


-- 
Andreas Abel  <><      Du bist der geliebte Mensch.

Department of Computer Science and Engineering
Chalmers and Gothenburg University, Sweden

andreas.abel at gu.se
http://www2.tcs.ifi.lmu.de/~abel/