<div dir="ltr"><div><div><div>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).<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"><<a href="mailto:mechvel@botik.ru" target="_blank">mechvel@botik.ru</a>></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>