[Agda] `with' question

[Sergei Meshveliani]

On Fri, 2016-02-05 at 16:29 -0800, Martin Stone Davis wrote:
> You didn't include the definition of h, so it's hard to check for
> sure, 

Sorry, please, insert  h  there as 

h : Null ps → f ps ≡ 1
h null-ps with  ps | null-ps
... | []    | _  = PE.refl
... | _ ∷ _ | ()



> but my guess is that you need a dot-pattern on the yes line of g',
> because ps is inferred as [].
> 
> g' : Dec (f ps ≡ 1)
> g'
>    with ps | null? ps
> ... | ._ | yes null-ps =  yes (h null-ps)

"Failed to infer the value of dotted pattern
 when checking that the pattern ._ has type List ℕ
".

and  ps  is postulated as  ": List ℕ".
-- ?

Regards,

------
Sergei




> On Fri, Feb 5, 2016 at 12:34 PM, Sergei Meshveliani <mechvel at botik.ru>
> wrote:
>         Please, what is wrong in the below program?
>         
>         -----------------------------------------------------------
>         module Useful where
>         open import Relation.Nullary using (Dec; yes; no)
>         open import Relation.Binary.PropositionalEquality as PE using
>         (_≡_; _≢_)
>         open import Data.Nat   using (ℕ)
>         open import Data.List  using (List; []; _∷_)
>         
>         --------------------------------------------------------
>         module _ {α} {A : Set α}
>             where
>             data Null : List A → Set α  where  isNull : Null []
>         
>             null? :  (xs : List A) → Dec (Null xs)
>             null? []      = yes isNull
>             null? (_ ∷ _) = no λ()
>         
>         --------------------------------------------------------
>         f : List ℕ  → ℕ
>         f []      =  1
>         f (_ ∷ _) =  0
>         
>         postulate  ps : List ℕ
>         
>         g : Dec (f ps ≡ 1)
>         g with null? ps
>         ... | yes null-ps =  yes (h null-ps)
>         ... | no _        =  no neq
>                              where
>                              postulate neq : f ps ≢ 1
>         
>         g' : Dec (f ps ≡ 1)
>         g'
>            with ps | null? ps
>         ... | _ | yes null-ps =  yes (h null-ps)
>         ... | _ | no _        =  no neq
>                                  where
>                                  postulate neq : f ps ≢ 1
>         --------------------------------------------------------------------
>         
>         g  is type-checked,
>         and for  g'  it reports that  null-ps  has not the needed
>         type.
>         
>         (The Agda language is difficult in its proof composition part.
>         I do not understand basics of Agda after 3 year practicing
>         with it).
>         
>         In this example, the part  "ps |"  is dummy.
>         But in the real example I need to use both  ps  and  null? ps,
>         like this:
>         
>           ... | []           | null-ps =  foo null-ps
>           ... | (_ , 0) :: _ | _       =  \bot-elim ... 0>0
>           ...
>         
>         g'  is a simplification for this real example.
>         
>         Thank you in advance for explanation,
>         
>         ------
>         Sergei
>         
>         
>         
>         
>         _______________________________________________
>         Agda mailing list
>         Agda at lists.chalmers.se
>         https://lists.chalmers.se/mailman/listinfo/agda
> 
>