<div dir="ltr"><div><div>Oops, I forgot about the constructor `gen` in my previous mail. My point still stands, though.<br><br></div>If the problem of spelling out all the cases really gets out of hand, you can define f using a view type instead:<br><br><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex"><span style="font-family:monospace,monospace">data f-View : Expr → Expr → Set where<br>  instance<br>    f0y : {y : Expr}   → f-View :0 y<br>    fx0 : {x : Expr}   → f-View x  :0<br>    fxy : {x y : Expr} → f-View x  y<br><br>f-view : (x y : Expr) → f-View x y<br>f-view :0        y         = f0y<br>f-view (gen x)   :0        = fx0<br>f-view (gen x)   (gen y)   = fxy<br>f-view (gen x)   (y₁ + y₂) = fxy<br>f-view (x₁ + x₂) :0        = fx0<br>f-view (x₁ + x₂) (gen y)   = fxy<br>f-view (x₁ + x₂) (y₁ + y₂) = fxy<br><br>f : (x y : Expr) → Expr<br>f x y with f-view x y<br>f .:0 y   | f0y = y<br>f x   .:0 | fx0 = x<br>f x   y   | fxy = x + y<br><br>lemma :  ∀ {x y} → x ≢ :0 → y ≢ :0 → f x y ≡ x + y<br>lemma {x}   {y}   p q with f-view x y<br>lemma {.:0} {y}   p q | f0y = ⊥-elim (p refl)<br>lemma {x}   {.:0} p q | fx0 = ⊥-elim (q refl)<br>lemma {x}   {y  } p q | fxy = refl</span><br></blockquote><br></div>This way you only have to spell out all the cases once (in the f-view function). Full code in the attachment.<br></div><div class="gmail_extra"><br><div class="gmail_quote">On Sat, May 27, 2017 at 12:36 PM, Jesper Cockx <span dir="ltr"><<a href="mailto:Jesper@sikanda.be" target="_blank">Jesper@sikanda.be</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div dir="ltr"><div><div><div><div><div><div><div><div>Hi Sergei,<br><br></div>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:<br><br></div>f x y -> case x of<br></div><div>  | :0 -> y<br></div><div>  | (x1 + x2) -> case y of<br>    | :0 -> (x1 + x2)<br></div><div>    | (y1 + y2) -> (x1 + x2) + (y1 + y2)<br></div><div><br></div>(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:<br><br></div><span class="">f :0 y = y<br></span></div>f (x1 + x2) :0 = x1 + x2<br></div>f (x1 + x2) (y1 + y2) = (x1 + x2) + (y1 + y2)<br><br></div>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)).<br><br></div>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.<br></div><div class="HOEnZb"><div class="h5"><div class="gmail_extra"><br><div class="gmail_quote">On Sat, May 27, 2017 at 11:51 AM, Sergei Meshveliani <span dir="ltr"><<a href="mailto:mechvel@botik.ru" target="_blank">mechvel@botik.ru</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">Dear Agda developers,<br>
I have the following question about the Agda language.<br>
Consider the program<br>
<br>
------------------------------<wbr>------------------------------<wbr>------------<br>
open import Relation.Binary  using (Decidable)<br>
open import Relation.Binary.PropositionalE<wbr>quality as PE using (_≡_; _≢_)<br>
open import Data.Empty using (⊥-elim)<br>
open import Data.Nat   using (ℕ)<br>
<br>
data Expr : Set where :0   : Expr<br>
                      gen  : ℕ → Expr<br>
                      _+_  : Expr → Expr → Expr<br>
                   -- _*_  : Expr → Expr → Expr    -- reserve<br>
<br>
f : Expr → Expr → Expr<br>
f :0 y  = y<br>
f x  :0 = x<br>
f x  y  = x + y<br>
<br>
lemma :  ∀ {x y} → x ≢ :0 → y ≢ :0 → f x y ≡ x + y<br>
<br>
lemma {:0}    {_}     e≢0 _    =  ⊥-elim (e≢0 PE.refl)<br>
lemma {_}     {:0}    _   e'≢0 =  ⊥-elim (e'≢0 PE.refl)<br>
lemma {_}     {_}     _   _    =  PE.refl                 -- I<br>
<br>
{- II<br>
lemma {gen _} {gen _} _   _    =  PE.refl<br>
lemma {gen _} {_ + _} _   _    =  PE.refl<br>
lemma {_ + _} {gen _} _   _    =  PE.refl<br>
lemma {_ + _} {_ + _} _   _    =  PE.refl<br>
-}<br>
------------------------------<wbr>------------------------------<wbr>---------------<br>
<br>
Agda  reports  refl  in (I) as not sufficient. Why?<br>
<br>
Each wildcard in (I) intends to denote any  x : Expr  which top<br>
constructor is not  :0.<br>
And all these cases (II) can be filled automatically by the type checker<br>
in place of (I).<br>
Am I missing something?<br>
May be there is some keyword that switches such an automatic filling?<br>
<br>
It may well happen that  Expr  has more binary constructors, for<br>
example,  _*_ and  div.<br>
Then the patterns for `lemma' will probably fill more that three pages<br>
of text.<br>
<br>
What is the way out?<br>
<br>
Thanks,<br>
<br>
------<br>
Sergei<br>
<br>
______________________________<wbr>_________________<br>
Agda mailing list<br>
<a href="mailto:Agda@lists.chalmers.se" target="_blank">Agda@lists.chalmers.se</a><br>
<a href="https://lists.chalmers.se/mailman/listinfo/agda" rel="noreferrer" target="_blank">https://lists.chalmers.se/mail<wbr>man/listinfo/agda</a><br>
</blockquote></div><br></div>
</div></div></blockquote></div><br></div>