<div dir="ltr"><div><div><div><div>A way to improve how Agda handles these cases would be to do coverage checking before type checking and only type checking the resulting case tree. Since case trees don&#39;t have any default cases, this would have the effect that default cases aren&#39;t typechecked themselves, but only their expanded versions. However, there are currently (at least) two obstacles that make this approach impossible:<br><br></div>- The current representation of case trees used by Agda doesn&#39;t contain enough type information to be typechecked independently, since they are mainly used for faster evaluation. This could be solved by adding the required information.<br><br></div>- Agda currently accepts functions with clauses that depend on the reduction behavior of previous clauses in order to pass the typechecker. Here&#39;s an artificial example of such a function that&#39;s currently allowed:<br><br><blockquote style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex" class="gmail_quote">data Bool : Set where tt ff : Bool<br>data ⊥ : Set where<br>record ⊤ : Set where<br><br>T : Bool → Set<br>T tt = ⊤<br>T ff = ⊥<br><br>Foo : Bool → Set<br>foo : (x : Bool) → Foo x<br><br>Foo tt = Bool<br>Foo ff = T (foo tt)<br><br>foo tt = tt<br>foo ff = record{}<br></blockquote><br>This wouldn&#39;t be allowed if the coverage checker is run first. [However I&#39;m also not sure if functions like this have any theoretical justification, so maybe it would be better to prohibit them anyways?]<br></div><div><br></div>cheers,<br></div>Jesper<br></div><div class="gmail_extra"><br><div class="gmail_quote">On Thu, Nov 12, 2015 at 7:34 PM, Peter Selinger <span dir="ltr">&lt;<a href="mailto:selinger@mathstat.dal.ca" target="_blank">selinger@mathstat.dal.ca</a>&gt;</span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">Here is a different idea. The way I usually solve this problem is by<br>
defining the function and the lemma simultaneously.<br>
<br>
This is not entirely ideal from the point of view of readability, but<br>
it is usually reasonably elegant. It seems to be the only solution, in<br>
my experience, that avoids writing out a potentially large case<br>
distinction when a definition and a lemma follow the same non-trivial<br>
pattern matching.<br>
<br>
f-with-lemma : (τ : Ty) -&gt; ∃ λ(x : ℕ) -&gt; x ≡ 0<br>
f-with-lemma Bool = ( 0 , refl )<br>
f-with-lemma τ = ( 0 , refl )<br>
<br>
f : Ty -&gt; ℕ<br>
f τ = fst (f-with-lemma τ)<br>
<span class=""><br>
lemma : (τ : Ty) -&gt; f τ ≡ 0<br>
</span>lemma τ = snd (f-with-lemma τ)<br>
<span class="HOEnZb"><font color="#888888"><br>
-- Peter<br>
</font></span><div class="HOEnZb"><div class="h5"><br>
Marco Vassena wrote:<br>
&gt;<br>
&gt; Suppose I have defined a function by pattern match.<br>
&gt; In the function I am interested in one specific case, therefore I explicitly<br>
&gt; match that one, while all the others are implicitly covered:<br>
&gt;<br>
&gt; f : Ty -&gt; ℕ<br>
&gt; f Bool = 0<br>
&gt; f τ = 0<br>
&gt;<br>
&gt; Now I want to prove something about this function, however the<br>
&gt; proof cannot be as concise as the definition of f:<br>
&gt;<br>
&gt; lemma : (τ : Ty) -&gt; f τ ≡ 0<br>
&gt; lemma Bool = refl<br>
&gt; lemma τ = {! refl !}  -- f τ != zero<br>
&gt;<br>
&gt; I have to explicitly go through all the other cases, otherwise f τ won&#39;t reduce:<br>
&gt;<br>
&gt; lemma : (τ : Ty) -&gt; f τ ≡ 0<br>
&gt; lemma Bool = refl<br>
&gt; lemma Int = refl<br>
&gt; lemma (τ =&gt; τ₁) = refl<br>
&gt; ...<br>
&gt;<br>
&gt; As you can imagine this can be very repetitive and annoying if the proofs are more involved<br>
&gt; and there are many values that fall in the &quot;default&quot; case.<br>
&gt;<br>
&gt; Do you know if it is possible to abstract over this pattern when reasoning about<br>
&gt; functions defined by pattern matching with a default case?<br>
&gt;<br>
&gt; All the best,<br>
&gt; Marco<br>
</div></div><div class="HOEnZb"><div class="h5">_______________________________________________<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>
</div></div></blockquote></div><br></div>