<div dir="ltr"><br><div class="gmail_extra"><br><div class="gmail_quote">On Mon, Feb 29, 2016 at 9:31 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"><span class="">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 <<a href="mailto:mechvel@botik.ru">mechvel@botik.ru</a>><br>
> wrote:<br>
><br>
> 2. The given proof for two+0 is constructed only from the<br>
> signature of<br>
> +0. Hence +0 can be placed under `abstract' (for this<br>
> example).<br>
><br>
> Also I expect that the implementation part for +0 will not<br>
> be used<br>
> anywhere in type-checking any future client function, the type<br>
> checker<br>
> will be satisfied with the signature of +0.<br>
><br>
> Can you imagine the necessity of using the implementation<br>
> rules for 0+<br>
> in type checking something?<br>
><br>
><br>
> There are certainly cases where you need equality proofs to reduce. In<br>
> this case you might be writing a function on vectors and needing to<br>
> product a Vec A n from a Vec A (n + 0). That's easy to do given +0,<br>
> but if it is abstract your function won't evaluate (at compile time,<br>
> at run-time there's no problem).<br>
<br>
<br>
</span>Please, what precisely is the example?<br>
Is it to program, say<br>
<br>
f : Vec Bool (2 + 0) → Vec Bool 2<br>
and<br>
bi-f : Bijective f<br>
?<br>
I thought that (Vec A m) and (Vec A n) are considered as different<br>
domains, but it it possible to program a provable bijection<br></blockquote><div><br></div><div>Here's a concrete example:</div><div><br></div><div>open import Data.Nat</div><div>open import Data.Vec</div><div>open import Relation.Binary.PropositionalEquality</div><div><br></div><div>abstract</div><div> +0 : ∀ n → n + 0 ≡ n</div><div> +0 zero = refl</div><div> +0 (suc n) = cong suc (+0 n)</div><div><br></div><div>module _ {a} {A : Set a} where</div><div><br></div><div> castVec : ∀ {m n} → m ≡ n → Vec A m → Vec A n</div><div> castVec refl xs = xs</div><div><br></div><div> ++[] : ∀ {n} (xs : Vec A n) → castVec (+0 n) (xs ++ []) ≡ xs</div><div> ++[] [] = ? -- castVec (+0 0) [] ≡ [] cannot be proven with refl</div><div> ++[] (x ∷ xs) = ? -- similar problems</div><div><br></div><div>Since +0 is abstract, castVec doesn't evaluate so you can't prove this formulation</div><div>of ++[].</div><div><br></div><div>/ Ulf </div></div><br></div></div>