[Agda] missed wildcard pattern

[Jesper Cockx]

Hi Sergei,

The reason why your first proof `lemma` doesn't work is because the
definition of `f` isn't what it looks like. When Agda checks the definition
of `f`, it translates the definition to a case tree, which looks something
like this:

f x y -> case x of
  | :0 -> y
  | (x1 + x2) -> case y of
    | :0 -> (x1 + x2)
    | (y1 + y2) -> (x1 + x2) + (y1 + y2)

(this is not valid Agda syntax, but an attempt at writing down the internal
representation of f). So your definition of `f` is to Agda equivalent to
the following one:

f :0 y = y
f (x1 + x2) :0 = x1 + x2
f (x1 + x2) (y1 + y2) = (x1 + x2) + (y1 + y2)

Consequently, when you want to prove something about `f`, you have to spell
out the same three cases (lemma :0 y, lemma (x1 + x2) :0, and lemma (x1 +
x2) (y1 + y2)).

Because this is so confusing to most people, I added the --exact-split
option to Agda. If you enable this option, Agda will warn you when it has
to expand a clause of a definition in the translation to a case tree (such
as the second and third clause of your definition of f). I know this is far
from perfect, but at least Agda can warn you when a situation like this
occurs.

On Sat, May 27, 2017 at 11:51 AM, Sergei Meshveliani <mechvel at botik.ru>
wrote:

> Dear Agda developers,
> I have the following question about the Agda language.
> Consider the program
>
> ------------------------------------------------------------------------
> open import Relation.Binary  using (Decidable)
> open import Relation.Binary.PropositionalEquality as PE using (_≡_; _≢_)
> open import Data.Empty using (⊥-elim)
> open import Data.Nat   using (ℕ)
>
> data Expr : Set where :0   : Expr
>                       gen  : ℕ → Expr
>                       _+_  : Expr → Expr → Expr
>                    -- _*_  : Expr → Expr → Expr    -- reserve
>
> f : Expr → Expr → Expr
> f :0 y  = y
> f x  :0 = x
> f x  y  = x + y
>
> lemma :  ∀ {x y} → x ≢ :0 → y ≢ :0 → f x y ≡ x + y
>
> lemma {:0}    {_}     e≢0 _    =  ⊥-elim (e≢0 PE.refl)
> lemma {_}     {:0}    _   e'≢0 =  ⊥-elim (e'≢0 PE.refl)
> lemma {_}     {_}     _   _    =  PE.refl                 -- I
>
> {- II
> lemma {gen _} {gen _} _   _    =  PE.refl
> lemma {gen _} {_ + _} _   _    =  PE.refl
> lemma {_ + _} {gen _} _   _    =  PE.refl
> lemma {_ + _} {_ + _} _   _    =  PE.refl
> -}
> ------------------------------------------------------------
> ---------------
>
> Agda  reports  refl  in (I) as not sufficient. Why?
>
> Each wildcard in (I) intends to denote any  x : Expr  which top
> constructor is not  :0.
> And all these cases (II) can be filled automatically by the type checker
> in place of (I).
> Am I missing something?
> May be there is some keyword that switches such an automatic filling?
>
> It may well happen that  Expr  has more binary constructors, for
> example,  _*_ and  div.
> Then the patterns for `lemma' will probably fill more that three pages
> of text.
>
> What is the way out?
>
> Thanks,
>
> ------
> Sergei
>
> _______________________________________________
> 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/20170527/3e5be256/attachment.html>