Re: [Agda] "xs ≡ [] → " question

[Jesper Cockx]

1) As 'ps' is a postulate and not a variable, it cannot be instantiated to
[]. So in order to prove this, it's better to make the statement more
general first (by replacing ps by xs as you do in the lemma).

2) Yes:

  g : ps ≡ [] → f ps ≡ 1
  g e = PE.subst (λ xs → f xs ≡ 1) (PE.sym e) PE.refl

Best regards,
Jesper


On Thu, Feb 4, 2016 at 6:46 PM, Sergei Meshveliani <mechvel at botik.ru> wrote:

> Please,
> what is the most natural way to prove  g  below?
>
> ------------------------------------------------------
> open import Data.Nat  using (ℕ)
> open import Data.List using (List; []; _∷_)
> open import Relation.Binary.PropositionalEquality as PE using (_≡_)
>
> f : List ℕ  → ℕ
> f []      =  1
> f (_ ∷ _) =  0
>
> postulate  ps : List ℕ
>
> g : ps ≡ [] → f ps ≡ 1
> g PE.refl =  PE.refl    -- is not type-checked
> --------------------------------------------------------
>
>
> I find the proof that uses
>
>   lemma : ∀ {xs} → xs ≡ [] → f xs ≡ 1
>   lemma PE.refl = PE.refl
>
> But
> 1) why the same implementation rule does not work for  g ?
> 2) is there possible a simpler proof than by introducing  lemma ?
>
> Thanks,
>
> ------
> Sergei
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20160204/de65b98f/attachment.html