<div dir="ltr"><div><div><div>1) As &#39;ps&#39; is a postulate and not a variable, it cannot be instantiated to []. So in order to prove this, it&#39;s better to make the statement more general first (by replacing ps by xs as you do in the lemma).<br><br></div>2) Yes:<br><br>  g : ps ≡ [] → f ps ≡ 1<br>  g e = PE.subst (λ xs → f xs ≡ 1) (PE.sym e) PE.refl<br><br></div>Best regards,<br></div>Jesper<br><div><div><br></div></div></div><div class="gmail_extra"><br><div class="gmail_quote">On Thu, Feb 4, 2016 at 6:46 PM, Sergei Meshveliani <span dir="ltr">&lt;<a href="mailto:mechvel@botik.ru" target="_blank">mechvel@botik.ru</a>&gt;</span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">Please,<br>
what is the most natural way to prove  g  below?<br>
<br>
------------------------------------------------------<br>
open import Data.Nat  using (ℕ)<br>
open import Data.List using (List; []; _∷_)<br>
open import Relation.Binary.PropositionalEquality as PE using (_≡_)<br>
<br>
f : List ℕ  → ℕ<br>
f []      =  1<br>
f (_ ∷ _) =  0<br>
<br>
postulate  ps : List ℕ<br>
<br>
g : ps ≡ [] → f ps ≡ 1<br>
g PE.refl =  PE.refl    -- is not type-checked<br>
--------------------------------------------------------<br>
<br>
<br>
I find the proof that uses<br>
<br>
  lemma : ∀ {xs} → xs ≡ [] → f xs ≡ 1<br>
  lemma PE.refl = PE.refl<br>
<br>
But<br>
1) why the same implementation rule does not work for  g ?<br>
2) is there possible a simpler proof than by introducing  lemma ?<br>
<br>
Thanks,<br>
<br>
------<br>
Sergei<br>
<br>
_______________________________________________<br>
Agda mailing list<br>
<a href="mailto:Agda@lists.chalmers.se">Agda@lists.chalmers.se</a><br>
<a href="https://lists.chalmers.se/mailman/listinfo/agda" rel="noreferrer" target="_blank">https://lists.chalmers.se/mailman/listinfo/agda</a><br>
</blockquote></div><br></div>