[Agda] Reasoning with Pattern Match with Default Cases

[Peter Selinger]

Here is a different idea. The way I usually solve this problem is by
defining the function and the lemma simultaneously.

This is not entirely ideal from the point of view of readability, but
it is usually reasonably elegant. It seems to be the only solution, in
my experience, that avoids writing out a potentially large case
distinction when a definition and a lemma follow the same non-trivial
pattern matching.

f-with-lemma : (τ : Ty) -> ∃ λ(x : ℕ) -> x ≡ 0
f-with-lemma Bool = ( 0 , refl )
f-with-lemma τ = ( 0 , refl )

f : Ty -> ℕ
f τ = fst (f-with-lemma τ)

lemma : (τ : Ty) -> f τ ≡ 0
lemma τ = snd (f-with-lemma τ)

-- Peter

Marco Vassena wrote:
> 
> Suppose I have defined a function by pattern match.
> In the function I am interested in one specific case, therefore I explicitly
> match that one, while all the others are implicitly covered:
> 
> f : Ty -> ℕ
> f Bool = 0
> f τ = 0
> 
> Now I want to prove something about this function, however the
> proof cannot be as concise as the definition of f:
> 
> lemma : (τ : Ty) -> f τ ≡ 0
> lemma Bool = refl
> lemma τ = {! refl !}  -- f τ != zero
> 
> I have to explicitly go through all the other cases, otherwise f τ won't reduce:
> 
> lemma : (τ : Ty) -> f τ ≡ 0
> lemma Bool = refl
> lemma Int = refl
> lemma (τ => τ₁) = refl
> ...
> 
> As you can imagine this can be very repetitive and annoying if the proofs are more involved
> and there are many values that fall in the "default" case.
> 
> Do you know if it is possible to abstract over this pattern when reasoning about
> functions defined by pattern matching with a default case?
> 
> All the best,
> Marco