<div dir="ltr">The best you can do, in my experience, is not use default cases in functions you want to prove lots of properties about. That doesn&#39;t mean you should spell out all the cases, though. Instead you can define a view for the particular set of patterns you are interested in. In your case<div><br></div><div><div>data Ty : Set where</div><div>  int bool : Ty</div><div>  _=&gt;_ : Ty → Ty → Ty</div><div><br></div><div>data BoolView : Ty → Set where</div><div>  bool : BoolView bool</div><div>  other : ∀ {τ} → BoolView τ</div><div><br></div><div>boolView : ∀ τ → BoolView τ</div><div>boolView bool = bool</div><div>boolView τ = other</div><div><br></div><div>f : Ty → Nat</div><div>f τ  with boolView τ</div><div>f .bool | bool  = 0</div><div>f τ     | other = 0</div><div><br></div><div>lemma : (τ : Ty) -&gt; f τ ≡ 0</div><div>lemma τ  with boolView τ</div><div>lemma .bool | bool  = refl</div><div>lemma τ     | other = refl</div></div><div><br></div><div>/ Ulf</div></div><div class="gmail_extra"><br><div class="gmail_quote">On Thu, Nov 12, 2015 at 3:05 PM, Marco Vassena <span dir="ltr">&lt;<a href="mailto:vassena@chalmers.se" target="_blank">vassena@chalmers.se</a>&gt;</span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">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 -&gt; ℕ<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) -&gt; 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&#39;t reduce:<br>
<br>
lemma : (τ : Ty) -&gt; f τ ≡ 0<br>
lemma Bool = refl<br>
lemma Int = refl<br>
lemma (τ =&gt; τ₁) = 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 &quot;default&quot; 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>_______________________________________________<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>
<br></blockquote></div><br></div>