[Agda] missed wildcard pattern

[Jesper Cockx]

Oops, I forgot about the constructor `gen` in my previous mail. My point
still stands, though.

If the problem of spelling out all the cases really gets out of hand, you
can define f using a view type instead:

data f-View : Expr → Expr → Set where
>   instance
>     f0y : {y : Expr}   → f-View :0 y
>     fx0 : {x : Expr}   → f-View x  :0
>     fxy : {x y : Expr} → f-View x  y
>
> f-view : (x y : Expr) → f-View x y
> f-view :0        y         = f0y
> f-view (gen x)   :0        = fx0
> f-view (gen x)   (gen y)   = fxy
> f-view (gen x)   (y₁ + y₂) = fxy
> f-view (x₁ + x₂) :0        = fx0
> f-view (x₁ + x₂) (gen y)   = fxy
> f-view (x₁ + x₂) (y₁ + y₂) = fxy
>
> f : (x y : Expr) → Expr
> f x y with f-view x y
> f .:0 y   | f0y = y
> f x   .:0 | fx0 = x
> f x   y   | fxy = x + y
>
> lemma :  ∀ {x y} → x ≢ :0 → y ≢ :0 → f x y ≡ x + y
> lemma {x}   {y}   p q with f-view x y
> lemma {.:0} {y}   p q | f0y = ⊥-elim (p refl)
> lemma {x}   {.:0} p q | fx0 = ⊥-elim (q refl)
> lemma {x}   {y  } p q | fxy = refl
>

This way you only have to spell out all the cases once (in the f-view
function). Full code in the attachment.

On Sat, May 27, 2017 at 12:36 PM, Jesper Cockx <Jesper at sikanda.be> wrote:

> 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/b5f011c1/attachment.html>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: ViewExample.agda
Type: application/octet-stream
Size: 1151 bytes
Desc: not available
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20170527/b5f011c1/attachment.obj>