[Agda] Reasoning with Pattern Match with Default Cases

[Jesper Cockx]

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:

- 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.

- 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:

data Bool : Set where tt ff : Bool
> data ⊥ : Set where
> record ⊤ : Set where
>
> T : Bool → Set
> T tt = ⊤
> T ff = ⊥
>
> Foo : Bool → Set
> foo : (x : Bool) → Foo x
>
> Foo tt = Bool
> Foo ff = T (foo tt)
>
> foo tt = tt
> foo ff = record{}
>

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?]

cheers,
Jesper

On Thu, Nov 12, 2015 at 7:34 PM, Peter Selinger <selinger at mathstat.dal.ca>
wrote:

> 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
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20151112/cbc34647/attachment.html