<div dir="ltr"><br><div class="gmail_extra"><br><div class="gmail_quote">On Thu, Mar 3, 2016 at 1:12 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:0px 0px 0px 0.8ex;border-left-width:1px;border-left-color:rgb(204,204,204);border-left-style:solid;padding-left:1ex"><div class=""><div class="h5">On Wed, 2016-03-02 at 16:14 +0100, Ulf Norell wrote:<br>
&gt;<br>
&gt;<br>
&gt; On Mon, Feb 29, 2016 at 9:31 PM, Sergei Meshveliani &lt;<a href="mailto:mechvel@botik.ru">mechvel@botik.ru</a>&gt;<br>
&gt; wrote:<br>
&gt;         On Mon, 2016-02-29 at 19:40 +0100, Ulf Norell wrote:<br>
&gt;         &gt;<br>
&gt;         &gt; On Mon, Feb 29, 2016 at 2:27 PM, Sergei Meshveliani<br>
&gt;         &lt;<a href="mailto:mechvel@botik.ru">mechvel@botik.ru</a>&gt;<br>
&gt;         &gt; wrote:<br>
&gt;         &gt;<br>
&gt;         &gt;         2. The given proof for  two+0  is constructed only<br>
&gt;         from the<br>
&gt;         &gt;         signature of<br>
&gt;         &gt;            +0.  Hence  +0  can be placed under<br>
&gt;         `abstract&#39; (for this<br>
&gt;         &gt;         example).<br>
&gt;         &gt;<br>
&gt;         &gt;         Also I expect that the implementation part for  +0<br>
&gt;         will not<br>
&gt;         &gt;         be used<br>
&gt;         &gt;         anywhere in type-checking any future client<br>
&gt;         function, the type<br>
&gt;         &gt;         checker<br>
&gt;         &gt;         will be satisfied with the signature of  +0.<br>
&gt;         &gt;<br>
&gt;         &gt;         Can you imagine the necessity of using the<br>
&gt;         implementation<br>
&gt;         &gt;         rules for 0+<br>
&gt;         &gt;         in type checking something?<br>
&gt;         &gt;<br>
&gt;         &gt;<br>
&gt;         &gt; There are certainly cases where you need equality proofs<br>
&gt;         &gt; to reduce.<br>
</div></div>&gt;         &gt; []<br>
<span class=""><br>
<br>
&gt; Here&#39;s a concrete example:<br>
&gt;<br>
&gt; open import Data.Nat<br>
&gt; open import Data.Vec<br>
&gt; open import Relation.Binary.PropositionalEquality<br>
&gt;<br>
&gt; abstract<br>
&gt;   +0 : ∀ n → n + 0 ≡ n<br>
&gt;   +0 zero    = refl<br>
&gt;   +0 (suc n) = cong suc (+0 n)<br>
<br>
&gt; module _ {a} {A : Set a} where<br>
<br>
&gt;   castVec : ∀ {m n} → m ≡ n → Vec A m → Vec A n<br>
&gt;   castVec refl xs = xs<br>
<br>
&gt;   ++[] : ∀ {n} (xs : Vec A n) → castVec (+0 n) (xs ++ []) ≡ xs<br>
&gt;   ++[] [] = ?  -- castVec (+0 0) [] ≡ []  cannot be proven with refl<br>
&gt;   ++[] (x ∷ xs) = ?  -- similar problems<br>
&gt;<br>
&gt;<br>
&gt; Since +0 is abstract, castVec doesn&#39;t evaluate so you can&#39;t prove this<br>
&gt; formulation of ++[].<br>
&gt;<br>
<br>
</span>And what proof is possible when `abstract&#39; is removed?<br>
I do not find such, so far:<br>
<span class=""><br>
  ++[] : ∀ {n} (xs : Vec A n) → castVec (+0 n) (xs ++ []) ≡ xs<br>
</span>  ++[] {_}     []       = refl<br>
  ++[] {suc n} (x ∷ xs) = goal<br>
            where<br>
            eq : castVec (+0 n) (xs ++ []) ≡ xs<br>
            eq = ++[] xs<br>
<br>
            goal :  castVec (cong suc (+0 n)) ((x ∷ xs) ++ []) ≡  x ∷ xs<br>
<br>
            goal = ?   -- refl             ?<br>
                       -- cong (_∷_ x) eq  ?<br></blockquote><div><br></div><div>How about</div><div><br></div><div><div>  castVec-∷ : ∀ {m n} (eq : m ≡ n) x (xs : Vec A m) →</div><div>                 castVec (cong suc eq) (x ∷ xs) ≡ x ∷ castVec eq xs</div><div>  castVec-∷ refl _ _ = refl</div><div><br></div><div>  ++[] : ∀ {n} (xs : Vec A n) → castVec (+0 n) (xs ++ []) ≡ xs</div><div>  ++[] [] = refl</div><div>  ++[] (_∷_ {n} x xs) rewrite castVec-∷ (+0 n) x (xs ++ []) = cong (x ∷_) (++[] xs)</div></div><div><br></div><div>/ Ulf</div></div></div></div>