<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"><<a href="mailto:mechvel@botik.ru" target="_blank">mechvel@botik.ru</a>></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>
><br>
><br>
> On Mon, Feb 29, 2016 at 9:31 PM, Sergei Meshveliani <<a href="mailto:mechvel@botik.ru">mechvel@botik.ru</a>><br>
> wrote:<br>
> On Mon, 2016-02-29 at 19:40 +0100, Ulf Norell wrote:<br>
> ><br>
> > On Mon, Feb 29, 2016 at 2:27 PM, Sergei Meshveliani<br>
> <<a href="mailto:mechvel@botik.ru">mechvel@botik.ru</a>><br>
> > wrote:<br>
> ><br>
> > 2. The given proof for two+0 is constructed only<br>
> from the<br>
> > signature of<br>
> > +0. Hence +0 can be placed under<br>
> `abstract' (for this<br>
> > example).<br>
> ><br>
> > Also I expect that the implementation part for +0<br>
> will not<br>
> > be used<br>
> > anywhere in type-checking any future client<br>
> function, the type<br>
> > checker<br>
> > will be satisfied with the signature of +0.<br>
> ><br>
> > Can you imagine the necessity of using the<br>
> implementation<br>
> > rules for 0+<br>
> > in type checking something?<br>
> ><br>
> ><br>
> > There are certainly cases where you need equality proofs<br>
> > to reduce.<br>
</div></div>> > []<br>
<span class=""><br>
<br>
> Here's a concrete example:<br>
><br>
> open import Data.Nat<br>
> open import Data.Vec<br>
> open import Relation.Binary.PropositionalEquality<br>
><br>
> abstract<br>
> +0 : ∀ n → n + 0 ≡ n<br>
> +0 zero = refl<br>
> +0 (suc n) = cong suc (+0 n)<br>
<br>
> module _ {a} {A : Set a} where<br>
<br>
> castVec : ∀ {m n} → m ≡ n → Vec A m → Vec A n<br>
> castVec refl xs = xs<br>
<br>
> ++[] : ∀ {n} (xs : Vec A n) → castVec (+0 n) (xs ++ []) ≡ xs<br>
> ++[] [] = ? -- castVec (+0 0) [] ≡ [] cannot be proven with refl<br>
> ++[] (x ∷ xs) = ? -- similar problems<br>
><br>
><br>
> Since +0 is abstract, castVec doesn't evaluate so you can't prove this<br>
> formulation of ++[].<br>
><br>
<br>
</span>And what proof is possible when `abstract' 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>