<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't have any default cases, this would have the effect that default cases aren'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'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's an artificial example of such a function that'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't be allowed if the coverage checker is run first. [However I'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"><<a href="mailto:selinger@mathstat.dal.ca" target="_blank">selinger@mathstat.dal.ca</a>></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) -> ∃ λ(x : ℕ) -> x ≡ 0<br>
f-with-lemma Bool = ( 0 , refl )<br>
f-with-lemma τ = ( 0 , refl )<br>
<br>
f : Ty -> ℕ<br>
f τ = fst (f-with-lemma τ)<br>
<span class=""><br>
lemma : (τ : Ty) -> 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>
><br>
> Suppose I have defined a function by pattern match.<br>
> In the function I am interested in one specific case, therefore I explicitly<br>
> match that one, while all the others are implicitly covered:<br>
><br>
> f : Ty -> ℕ<br>
> f Bool = 0<br>
> f τ = 0<br>
><br>
> Now I want to prove something about this function, however the<br>
> proof cannot be as concise as the definition of f:<br>
><br>
> lemma : (τ : Ty) -> f τ ≡ 0<br>
> lemma Bool = refl<br>
> lemma τ = {! refl !} -- f τ != zero<br>
><br>
> I have to explicitly go through all the other cases, otherwise f τ won't reduce:<br>
><br>
> lemma : (τ : Ty) -> f τ ≡ 0<br>
> lemma Bool = refl<br>
> lemma Int = refl<br>
> lemma (τ => τ₁) = refl<br>
> ...<br>
><br>
> As you can imagine this can be very repetitive and annoying if the proofs are more involved<br>
> and there are many values that fall in the "default" case.<br>
><br>
> Do you know if it is possible to abstract over this pattern when reasoning about<br>
> functions defined by pattern matching with a default case?<br>
><br>
> All the best,<br>
> 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>