[Agda] Reasoning with Pattern Match with Default Cases

[Andreas Abel]

In principle, there is no reason why reduction of open terms should be 
restricted to the rules that suffice to compute values of closed terms. 
  However, in Martin-Löf Type Theory, this is the guiding principle.  I 
think it should be dropped.

Jesper has contributed to a paper that allows overlapping but coherent 
rewrite rules, which I think makes much sense.

Of course, all rewrite rules for open terms should be sound for a case 
tree semantics for closed terms.

Concretely, for Agda, there is work to do to replace the the case trees 
for open term evaluation by something more flexible, but still 
efficient, that allows to reduce the equations as the user wrote them 
and the added REWRITE rules.

There are efficient representation of rewrite rules that go beyond case 
splits, see e.g. Ronan Saillard's thesis (which refers to an older paper).

Cheers,
Andreas

On 12.11.2015 20:59, Jesper Cockx wrote:
> 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 <mailto: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 <mailto:Agda at lists.chalmers.se>
>     https://lists.chalmers.se/mailman/listinfo/agda
>
>
>
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>


-- 
Andreas Abel  <><      Du bist der geliebte Mensch.

Department of Computer Science and Engineering
Chalmers and Gothenburg University, Sweden

andreas.abel at gu.se
http://www2.tcs.ifi.lmu.de/~abel/