[Agda] `with' question

[Andreas Abel]

If you replace _ by a variable w you can see what is going on

   g' : Dec (f ps ≡ 1)
   g' with ps | null? ps
   ... | w | yes null-ps =  yes {!!}
   ... | w | no _        =  no {!!}

ps has been abstracted to w, as you requested, so your first goal is

   f w == 1

and h is not useful to solve it, as h is only applicable to the fixed 
list ps, not an arbitrary list w.

I guess your original problem has to do with the fact that you would 
Agda to know that ps and w are equal.  This can be achieved by using the

   inspect pattern

defined in Relation.Binary.Propositional equality.

On 06.02.2016 10:26, Sergei Meshveliani wrote:
> 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
>>
>>
>
>
> _______________________________________________
> 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/