<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>f :0 y = y<br></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="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.<wbr>PropositionalEquality 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">Agda@lists.chalmers.se</a><br>
<a href="https://lists.chalmers.se/mailman/listinfo/agda" rel="noreferrer" target="_blank">https://lists.chalmers.se/<wbr>mailman/listinfo/agda</a><br>
</blockquote></div><br></div>